diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 22 | ||||
| -rw-r--r-- | test/Feature/PreferCex.c | 2 |
2 files changed, 20 insertions, 4 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 45876659..1b2bc15b 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -140,8 +140,10 @@ namespace { cl::desc("Dump test cases for all active states on exit (default=on)")); cl::opt<bool> - NoPreferCex("no-prefer-cex", - cl::init(false)); + PreferCex("prefer-cex", + cl::init(false), + cl::desc("Prefer creation of tests with human readable bytes. Can also pair with klee_prefer_cex api " + "to customize range. Note: option is expensive when creating lots of tests (default=false)")); cl::opt<bool> RandomizeFork("randomize-fork", @@ -3482,16 +3484,30 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); - if (!NoPreferCex) { + if (PreferCex) { + // When the PreferCex is enabled, go through each byte in every test case and + // attempt to restrict it to the constraints contained in cexPreferences. + // (Note: usually this means trying to make it an ASCII character (0-127) + // and therefore human readable. It is also possible to customize the preferred + // constraints. See test/Features/PreferCex.c for an example) While this + // process can be very expensive, it can also make understanding individual + // test cases much easier. for (unsigned i = 0; i != state.symbolics.size(); ++i) { const MemoryObject *mo = state.symbolics[i].first; std::vector< ref<Expr> >::const_iterator pi = mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); for (; pi != pie; ++pi) { bool mustBeTrue; + // Attempt to bound byte to constraints held in cexPreferences bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), mustBeTrue); + // If it isn't possible to constrain this particular byte in the desired + // way (normally this would mean that the byte can't be constrained to + // be between 0 and 127 without making the entire constraint list UNSAT) + // then just continue on to the next byte. if (!success) break; + // If the particular constraint operated on in this iteration through + // the loop isn't implied then add it to the list of constraints. if (!mustBeTrue) tmp.addConstraint(*pi); } if (pi!=pie) break; diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c index 180e03cf..cf67e647 100644 --- a/test/Feature/PreferCex.c +++ b/test/Feature/PreferCex.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --prefer-cex %t1.bc // RUN: ktest-tool %t.klee-out/test000001.ktest | FileCheck %s #include <assert.h> |