aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-11-30 20:35:55 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-30 17:30:11 +0000
commitcb5e898561f9b8769d8838bc1bdca17a6f4f5d20 (patch)
tree751d654540fc79495c0e90b53d48391b0a574220 /lib
parent42662b71a53d2e72481bc46994f44e47c7528a34 (diff)
downloadklee-cb5e898561f9b8769d8838bc1bdca17a6f4f5d20.tar.gz
Modify getValueFromSeeds() to include more functionality and simplify its callers
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp30
-rw-r--r--lib/Core/Executor.h3
2 files changed, 13 insertions, 20 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 73f994ce..49df9790 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1321,11 +1321,8 @@ Executor::toConstant(ExecutionState &state,
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
return CE;
- ref<Expr> value;
- if (auto found = seedMap.find(&state); found != seedMap.end())
- value = getValueFromSeeds(found->second, e);
/* If no seed evaluation results in a constant, call the solver */
- ref<ConstantExpr> cvalue = llvm::dyn_cast_or_null<ConstantExpr>(value);
+ ref<ConstantExpr> cvalue = getValueFromSeeds(state, e);
if (!cvalue) {
[[maybe_unused]] bool success =
solver->getValue(state.constraints, e, cvalue, state.queryMetaData);
@@ -1348,9 +1345,13 @@ Executor::toConstant(ExecutionState &state,
return cvalue;
}
-ref<klee::Expr>
-Executor::getValueFromSeeds(std::vector<SeedInfo> &seeds, ref<Expr> e) {
- assert(!seeds.empty());
+ref<klee::ConstantExpr> Executor::getValueFromSeeds(ExecutionState &state,
+ ref<Expr> e) {
+ auto found = seedMap.find(&state);
+ if (found == seedMap.end())
+ return nullptr;
+
+ auto seeds = found->second;
for (auto const &seed : seeds) {
auto value = seed.assignment.evaluate(e);
if (isa<ConstantExpr>(value))
@@ -3958,12 +3959,9 @@ void Executor::callExternalFunction(ExecutionState &state,
ae = arguments.end(); ai!=ae; ++ai) {
if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness
*ai = optimizer.optimizeExpr(*ai, true);
- ref<ConstantExpr> cvalue;
- ref<Expr> value = nullptr;
- if (auto found = seedMap.find(&state); found != seedMap.end())
- value = getValueFromSeeds(found->second, *ai);
+ ref<ConstantExpr> cvalue = getValueFromSeeds(state, *ai);
/* If no seed evaluation results in a constant, call the solver */
- if (!value || !(cvalue = dyn_cast<ConstantExpr>(value))) {
+ if (!cvalue) {
[[maybe_unused]] bool success = solver->getValue(
state.constraints, *ai, cvalue, state.queryMetaData);
assert(success && "FIXME: Unhandled solver failure");
@@ -4196,13 +4194,9 @@ void Executor::executeAlloc(ExecutionState &state,
size = optimizer.optimizeExpr(size, true);
- ref<ConstantExpr> example;
// Check if in seed mode, then try to replicate size from a seed
- ref<Expr> value = nullptr;
- if (auto found = seedMap.find(&state); found != seedMap.end())
- value = getValueFromSeeds(found->second, size);
- /* If no seed evaluation results in a constant, call the solver */
- if (!value || !(example = dyn_cast<ConstantExpr>(value))) {
+ ref<ConstantExpr> example = getValueFromSeeds(state, size);
+ if (!example) {
bool success = solver->getValue(state.constraints, size, example,
state.queryMetaData);
assert(success && "FIXME: Unhandled solver failure");
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index bf773fa5..d19758d4 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -400,8 +400,7 @@ private:
/// first one that results in a constant, if such a seed exist. Otherwise,
/// return the non-constant evaluation of the expression under one of the
/// seeds.
- ref<klee::Expr> getValueFromSeeds(std::vector<SeedInfo> &seeds,
- ref<Expr> e);
+ ref<klee::ConstantExpr> getValueFromSeeds(ExecutionState &state, ref<Expr> e);
/// Bind a constant value for e to the given target. NOTE: This
/// function may fork state if the state has multiple seeds.