From 33417e4b63377e2825811096aaca026847cf2e26 Mon Sep 17 00:00:00 2001
From: Eric Rizzi <eric.rizzi@gmail.com>
Date: Mon, 11 May 2015 10:34:05 -0400
Subject: Make use of prefer-cex optional rather than default

Previously, default Klee would go through every byte in a test case
and attempt to bound it to be between 0 and 127, making it human
readable.  While this may be useful when attempting to understand Klee,
it also means that the time required to create large test suites was
greatly increased.  By making this behavior default off, unsuspecting
users won't incur these additional costs.
---
 lib/Core/Executor.cpp    | 22 +++++++++++++++++++---
 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>
-- 
cgit 1.4.1