aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/MetaSMTBuilder.h39
-rw-r--r--lib/Solver/STPBuilder.cpp38
-rw-r--r--lib/Solver/Z3Builder.cpp34
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 <metaSMT/frontend/Logic.hpp>
@@ -172,22 +173,32 @@ template <typename SolverContext>
typename SolverContext::result_type
MetaSMTBuilder<SolverContext>::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<const UpdateNode *> 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 <typename SolverContext>
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 <cstdio>
@@ -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<const UpdateNode *> 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<const UpdateNode *> 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,
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-26 11:23:34 +0000