diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 20 | ||||
| -rw-r--r-- | test/Feature/ExtCall.c | 1 | ||||
| -rw-r--r-- | test/Feature/ExtCallOverapprox.c | 2 | ||||
| -rw-r--r-- | test/Feature/SeedConcretizeExternalCall.c | 3 |
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 } |