about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-10-20 20:50:29 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-30 17:30:11 +0000
commit251b28e464921a9507f56f1d1138ff8df146888f (patch)
tree64c0a7cecac444c547e48813bdc4c4df2dbc952a /lib
parentcbf10dbdd7345434e0ec74526ec3ca3d0391797a (diff)
downloadklee-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.cpp23
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)) {