This commit fixes the concretization of arguments following an external call with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf.

4 files changed, 17 insertions, 9 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 45209617..c869f49d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -184,9 +184,10 @@ cl::opt<bool>
 /*** External call policy options ***/
 
 enum class ExternalCallPolicy {
-  None,     // No external calls allowed
-  Concrete, // Only external calls with concrete arguments allowed
-  All,      // All external calls allowed
+  None,       // No external calls allowed
+  Concrete,   // Only external calls with concrete arguments allowed
+  All,        // All external calls allowed, symbolic arguments concretized
+  OverApprox, // All external calls allowed, symbolic inputs are not constrained by the call
 };
 
 cl::opt<ExternalCallPolicy> ExternalCalls(
@@ -203,7 +204,11 @@ cl::opt<ExternalCallPolicy> ExternalCalls(
                    "allowed (default)"),
         clEnumValN(ExternalCallPolicy::All, "all",
                    "All external function calls are allowed.  This concretizes "
-                   "any symbolic arguments in calls to external functions.")),
+                   "any symbolic arguments in calls to external functions."),
+        clEnumValN(ExternalCallPolicy::OverApprox, "over-approx",
+                   "All external function calls are allowed.  This concretizes "
+                   "any symbolic arguments in calls to external functions but"
+                   "the concretization is ignored after the call (see docs).")),
     cl::init(ExternalCallPolicy::Concrete),
     cl::cat(ExtCallsCat));
 
@@ -4013,7 +4018,8 @@ void Executor::callExternalFunction(ExecutionState &state,
   unsigned wordIndex = 2;
   for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), 
        ae = arguments.end(); ai!=ae; ++ai) {
-    if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness
+    if (ExternalCalls == ExternalCallPolicy::All ||
+        ExternalCalls == ExternalCallPolicy::OverApprox) {
       *ai = optimizer.optimizeExpr(*ai, true);
       ref<ConstantExpr> cvalue = getValueFromSeeds(state, *ai);
       /* If no seed evaluation results in a constant, call the solver */
@@ -4022,7 +4028,11 @@ void Executor::callExternalFunction(ExecutionState &state,
             state.constraints, *ai, cvalue, state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");
       }
+
       cvalue->toMemory(&args[wordIndex]);
+      if (ExternalCalls == ExternalCallPolicy::All)
+        addConstraint(state, EqExpr::create(cvalue, *ai));
+
       ObjectPair op;
       // Checking to see if the argument is a pointer to something
       if (cvalue->getWidth() == Context::get().getPointerWidth() &&
diff --git a/test/Feature/ExtCall.c b/test/Feature/ExtCall.c
index 5d9c0684..e38f92d9 100644
--- a/test/Feature/ExtCall.c
+++ b/test/Feature/ExtCall.c
@@ -1,4 +1,3 @@
-// XFAIL: *
 // This test checks that symbolic arguments to a function call are correctly concretized
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
 
diff --git a/test/Feature/ExtCallOverapprox.c b/test/Feature/ExtCallOverapprox.c
index 83f73163..9f69b3dd 100644
--- a/test/Feature/ExtCallOverapprox.c
+++ b/test/Feature/ExtCallOverapprox.c
@@ -2,7 +2,7 @@
 
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --external-calls=all %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --external-calls=over-approx %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/SeedConcretizeExternalCall.c b/test/Feature/SeedConcretizeExternalCall.c
index afc7fb6a..18984170 100644
--- a/test/Feature/SeedConcretizeExternalCall.c
+++ b/test/Feature/SeedConcretizeExternalCall.c
@@ -24,6 +24,5 @@ int main() {
   klee_make_symbolic(&x, sizeof(x), "x");
   assert(abs(x) == 12345678);
 
-  // CHECK-STATS: 0
-  // No queries, but this will change once https://github.com/klee/klee/pull/1520 is merged
+  // CHECK-STATS: 1
 }