From 95a9886b32c1b0086b60f828f3f2c139dd863211 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Fri, 24 Jun 2022 15:27:25 +0100 Subject: Implement getArrayForUpdate iteratively --- lib/Solver/MetaSMTBuilder.h | 39 +++++++++++++++++++++++++-------------- lib/Solver/STPBuilder.cpp | 38 +++++++++++++++++++++++--------------- lib/Solver/Z3Builder.cpp | 34 ++++++++++++++++++++++------------ 3 files changed, 70 insertions(+), 41 deletions(-) diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 376ffe25..7a3d7837 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -20,6 +20,7 @@ #ifdef ENABLE_METASMT +#include "llvm/ADT/iterator_range.h" #include "llvm/Support/CommandLine.h" #include @@ -172,22 +173,32 @@ template typename SolverContext::result_type MetaSMTBuilder::getArrayForUpdate(const Array *root, const UpdateNode *un) { - + // Iterate over the update nodes, until we find a cached version of the node, + // or no more update nodes remain + typename SolverContext::result_type un_expr; + std::vector update_nodes; + for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr); + un = un->next.get()) { + update_nodes.push_back(un); + } if (!un) { - return (getInitialArray(root)); - } else { - typename SolverContext::result_type un_expr; - bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); - - if (!hashed) { - un_expr = evaluate(_solver, - metaSMT::logic::Array::store( - getArrayForUpdate(root, un->next.get()), - construct(un->index, 0), construct(un->value, 0))); - _arr_hash.hashUpdateNodeExpr(un, un_expr); - } - return (un_expr); + un_expr = getInitialArray(root); + } + // `un_expr` now holds an expression for the array - either from cache or by + // virtue of being the initial array expression + + // Create and cache solver expressions based on the update nodes starting from + // the oldest + for (const auto &un : + llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) { + un_expr = evaluate( + _solver, metaSMT::logic::Array::store(un_expr, construct(un->index, 0), + construct(un->value, 0))); + + _arr_hash.hashUpdateNodeExpr(un, un_expr); } + + return un_expr; } template diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 13a42513..9a38183d 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -18,6 +18,7 @@ #include "ConstantDivision.h" #include "llvm/ADT/StringExtras.h" +#include "llvm/ADT/iterator_range.h" #include "llvm/Support/CommandLine.h" #include @@ -465,26 +466,33 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { return vc_readExpr(vc, getInitialArray(root), bvConst32(32, index)); } -::VCExpr STPBuilder::getArrayForUpdate(const Array *root, +::VCExpr STPBuilder::getArrayForUpdate(const Array *root, const UpdateNode *un) { + // Iterate over the update nodes, until we find a cached version of the node, + // or no more update nodes remain + ::VCExpr un_expr; + std::vector update_nodes; + for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr); + un = un->next.get()) { + update_nodes.push_back(un); + } if (!un) { - return getInitialArray(root); + un_expr = getInitialArray(root); } - else { - // FIXME: This really needs to be non-recursive. - ::VCExpr un_expr; - bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); - - if (!hashed) { - un_expr = - vc_writeExpr(vc, getArrayForUpdate(root, un->next.get()), - construct(un->index, 0), construct(un->value, 0)); + // `un_expr` now holds an expression for the array - either from cache or by + // virtue of being the initial array expression - _arr_hash.hashUpdateNodeExpr(un, un_expr); - } - - return un_expr; + // Create and cache solver expressions based on the update nodes starting from + // the oldest + for (const auto &un : + llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) { + un_expr = vc_writeExpr(vc, un_expr, construct(un->index, 0), + construct(un->value, 0)); + + _arr_hash.hashUpdateNodeExpr(un, un_expr); } + + return un_expr; } /** if *width_out!=1 then result is a bitvector, diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 950bd879..e1937158 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -17,6 +17,7 @@ #include "klee/Support/ErrorHandling.h" #include "llvm/ADT/StringExtras.h" +#include "llvm/ADT/iterator_range.h" #include "llvm/Support/CommandLine.h" using namespace klee; @@ -427,22 +428,31 @@ Z3ASTHandle Z3Builder::getInitialRead(const Array *root, unsigned index) { Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root, const UpdateNode *un) { + // Iterate over the update nodes, until we find a cached version of the node, + // or no more update nodes remain + Z3ASTHandle un_expr; + std::vector update_nodes; + for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr); + un = un->next.get()) { + update_nodes.push_back(un); + } if (!un) { - return (getInitialArray(root)); - } else { - // FIXME: This really needs to be non-recursive. - Z3ASTHandle un_expr; - bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); - - if (!hashed) { - un_expr = writeExpr(getArrayForUpdate(root, un->next.get()), - construct(un->index, 0), construct(un->value, 0)); + un_expr = getInitialArray(root); + } + // `un_expr` now holds an expression for the array - either from cache or by + // virtue of being the initial array expression - _arr_hash.hashUpdateNodeExpr(un, un_expr); - } + // Create and cache solver expressions based on the update nodes starting from + // the oldest + for (const auto &un : + llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) { + un_expr = + writeExpr(un_expr, construct(un->index, 0), construct(un->value, 0)); - return (un_expr); + _arr_hash.hashUpdateNodeExpr(un, un_expr); } + + return un_expr; } /** if *width_out!=1 then result is a bitvector, -- cgit 1.4.1