Concretize arguments to external function calls using seeds, if available. Added a test case.

2 files changed, 39 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)) {
diff --git a/test/Feature/SeedConcretizeExternalCall.c b/test/Feature/SeedConcretizeExternalCall.c
new file mode 100644
index 00000000..7eb69698
--- /dev/null
+++ b/test/Feature/SeedConcretizeExternalCall.c
@@ -0,0 +1,25 @@
+// RUN: %clang -emit-llvm -c -g %s -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --entry-point=TestGen %t.bc
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: not test -f %t.klee-out/test000002.ktest
+
+// RUN: rm -rf %t.klee-out-2
+// RUN: %klee --external-calls=all --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc
+
+#include "klee/klee.h"
+
+#include <assert.h>
+#include <stdlib.h>
+
+void TestGen() {
+  int x;
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_assume(x == 12345678);
+}
+
+int main() {
+  int x;
+  klee_make_symbolic(&x, sizeof(x), "x");
+  assert(abs(x) == 12345678);
+}