diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-11-30 20:35:55 +0000 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-30 17:30:11 +0000 |
commit | cb5e898561f9b8769d8838bc1bdca17a6f4f5d20 (patch) | |
tree | 751d654540fc79495c0e90b53d48391b0a574220 /lib | |
parent | 42662b71a53d2e72481bc46994f44e47c7528a34 (diff) | |
download | klee-cb5e898561f9b8769d8838bc1bdca17a6f4f5d20.tar.gz |
Modify getValueFromSeeds() to include more functionality and simplify its callers
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 30 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 |
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. |