Merge pull request #241 from holycrap872/NoPreferCex

Make creation of human readable test cases optional rather than default

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>