diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-10-20 20:50:29 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-30 17:30:11 +0000 |
commit | 251b28e464921a9507f56f1d1138ff8df146888f (patch) | |
tree | 64c0a7cecac444c547e48813bdc4c4df2dbc952a /lib | |
parent | cbf10dbdd7345434e0ec74526ec3ca3d0391797a (diff) | |
download | klee-251b28e464921a9507f56f1d1138ff8df146888f.tar.gz |
Concretize arguments to external function calls using seeds, if available. Added a test case.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e4fba39b..ebbcfaea 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3966,19 +3966,24 @@ 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> ce; - bool success = - solver->getValue(state.constraints, *ai, ce, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void) success; - ce->toMemory(&args[wordIndex]); + ref<ConstantExpr> cvalue; + ref<Expr> value = nullptr; + if (auto found = seedMap.find(&state); found != seedMap.end()) + value = getValueFromSeeds(found->second, *ai); + /* If no seed evaluation results in a constant, call the solver */ + if (!value || !(cvalue = dyn_cast<ConstantExpr>(value))) { + [[maybe_unused]] bool success = solver->getValue( + state.constraints, *ai, cvalue, state.queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); + } + cvalue->toMemory(&args[wordIndex]); ObjectPair op; // Checking to see if the argument is a pointer to something - if (ce->getWidth() == Context::get().getPointerWidth() && - state.addressSpace.resolveOne(ce, op)) { + if (cvalue->getWidth() == Context::get().getPointerWidth() && + state.addressSpace.resolveOne(cvalue, op)) { op.second->flushToConcreteStore(solver.get(), state); } - wordIndex += (ce->getWidth()+63)/64; + wordIndex += (cvalue->getWidth() + 63) / 64; } else { ref<Expr> arg = toUnique(state, *ai); if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) { |