Merge pull request #243 from ccadar/master

Option --readable-posix-inputs used to turn on/off POSIX-related CEX preferences

8 files changed, 72 insertions, 54 deletions

diff --git a/include/klee/klee.h b/include/klee/klee.h
index 032e5243..d0980395 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -110,6 +110,7 @@ extern "C" {
   void klee_warning(const char *message);
   void klee_warning_once(const char *message);
   void klee_prefer_cex(void *object, uintptr_t condition);
+  void klee_posix_prefer_cex(void *object, uintptr_t condition);
   void klee_mark_global(void *object);
 
   /* Return a possible constant value for the input expression. This
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1b2bc15b..49e526f5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -140,12 +140,6 @@ namespace {
 		   cl::desc("Dump test cases for all active states on exit (default=on)"));
  
   cl::opt<bool>
-  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",
                 cl::init(false),
 		cl::desc("Randomly swap the true and false states on a fork (default=off)"));
@@ -3484,34 +3478,33 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   solver->setTimeout(coreSolverTimeout);
 
   ExecutionState tmp(state);
-  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;
-    }
+
+  // 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;
   }
 
   std::vector< std::vector<unsigned char> > values;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index f06ae4f5..52abff5f 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -22,6 +22,8 @@
 #include "Executor.h"
 #include "MemoryManager.h"
 
+#include "klee/CommandLine.h"
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Module.h"
 #else
@@ -34,6 +36,15 @@
 using namespace llvm;
 using namespace klee;
 
+namespace {
+  cl::opt<bool>
+  ReadablePosix("readable-posix-inputs",
+            cl::init(false),
+            cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. "
+                     "Note: option is expensive when creating lots of tests (default=false)"));
+}
+
+
 /// \todo Almost all of the demands in this file should be replaced
 /// with terminateState calls.
 
@@ -81,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_mark_global", handleMarkGlobal, false),
   add("klee_merge", handleMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
+  add("klee_posix_prefer_cex", handlePosixPreferCex, false),
   add("klee_print_expr", handlePrintExpr, false),
   add("klee_print_range", handlePrintRange, false),
   add("klee_set_forking", handleSetForking, false),
@@ -222,7 +234,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
   ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
   if (!state.addressSpace.resolveOne(address, op))
     assert(0 && "XXX out of bounds / multiple resolution unhandled");
-  bool res;
+  bool res __attribute__ ((unused));
   assert(executor.solver->mustBeTrue(state, 
                                      EqExpr::create(address, 
                                                     op.first->getBaseExpr()),
@@ -376,7 +388,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
     e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth()));
   
   bool res;
-  bool success = executor.solver->mustBeFalse(state, e, res);
+  bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res);
   assert(success && "FIXME: Unhandled solver failure");
   if (res) {
     executor.terminateStateOnError(state, 
@@ -416,6 +428,13 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
   rl[0].first.first->cexPreferences.push_back(cond);
 }
 
+void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state,
+                                             KInstruction *target,
+                                             std::vector<ref<Expr> > &arguments) {
+  if (ReadablePosix)
+    return handlePreferCex(state, target, arguments);
+}
+
 void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
                                   KInstruction *target,
                                   std::vector<ref<Expr> > &arguments) {
@@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<ConstantExpr> value;
-    bool success = executor.solver->getValue(state, arguments[1], value);
+    bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value);
     assert(success && "FIXME: Unhandled solver failure");
     bool res;
     success = executor.solver->mustBeTrue(state, 
@@ -679,7 +698,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
 
     // FIXME: Type coercion should be done consistently somewhere.
     bool res;
-    bool success =
+    bool success __attribute__ ((unused)) =
       executor.solver->mustBeTrue(*s, 
                                   EqExpr::create(ZExtExpr::create(arguments[1],
                                                                   Context::get().getPointerWidth()),
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index d52b8fc5..2dfdde43 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -120,6 +120,7 @@ namespace klee {
     HANDLER(handleNew);
     HANDLER(handleNewArray);
     HANDLER(handlePreferCex);
+    HANDLER(handlePosixPreferCex);
     HANDLER(handlePrintExpr);
     HANDLER(handlePrintRange);
     HANDLER(handleRange);
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index d976b0b4..8b69fd04 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -74,20 +74,20 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
      reasonable. */
   klee_assume((s->st_blksize & ~0xFFFF) == 0);
 
-  klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777)));
-  klee_prefer_cex(s, s->st_dev == defaults->st_dev);
-  klee_prefer_cex(s, s->st_rdev == defaults->st_rdev);
-  klee_prefer_cex(s, (s->st_mode&0700) == 0600);
-  klee_prefer_cex(s, (s->st_mode&0070) == 0020);
-  klee_prefer_cex(s, (s->st_mode&0007) == 0002);
-  klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG);
-  klee_prefer_cex(s, s->st_nlink == 1);
-  klee_prefer_cex(s, s->st_uid == defaults->st_uid);
-  klee_prefer_cex(s, s->st_gid == defaults->st_gid);
-  klee_prefer_cex(s, s->st_blksize == 4096);
-  klee_prefer_cex(s, s->st_atime == defaults->st_atime);
-  klee_prefer_cex(s, s->st_mtime == defaults->st_mtime);
-  klee_prefer_cex(s, s->st_ctime == defaults->st_ctime);
+  klee_posix_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777)));
+  klee_posix_prefer_cex(s, s->st_dev == defaults->st_dev);
+  klee_posix_prefer_cex(s, s->st_rdev == defaults->st_rdev);
+  klee_posix_prefer_cex(s, (s->st_mode&0700) == 0600);
+  klee_posix_prefer_cex(s, (s->st_mode&0070) == 0020);
+  klee_posix_prefer_cex(s, (s->st_mode&0007) == 0002);
+  klee_posix_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG);
+  klee_posix_prefer_cex(s, s->st_nlink == 1);
+  klee_posix_prefer_cex(s, s->st_uid == defaults->st_uid);
+  klee_posix_prefer_cex(s, s->st_gid == defaults->st_gid);
+  klee_posix_prefer_cex(s, s->st_blksize == 4096);
+  klee_posix_prefer_cex(s, s->st_atime == defaults->st_atime);
+  klee_posix_prefer_cex(s, s->st_mtime == defaults->st_mtime);
+  klee_posix_prefer_cex(s, s->st_ctime == defaults->st_ctime);
 
   s->st_size = dfile->size;
   s->st_blocks = 8;
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 2a6b6f68..cbcf31f4 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -67,7 +67,7 @@ static char *__get_sym_str(int numChars, char *name) {
   klee_make_symbolic(s, numChars+1, name);
 
   for (i=0; i<numChars; i++)
-    klee_prefer_cex(s, __isprint(s[i]));
+    klee_posix_prefer_cex(s, __isprint(s[i]));
   
   s[numChars] = '\0';
   return s;
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index cf67e647..180e03cf 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 --prefer-cex %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
 // RUN: ktest-tool %t.klee-out/test000001.ktest | FileCheck %s
 
 #include <assert.h>
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 73e2783e..6b4fb8f4 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -418,6 +418,10 @@ void klee_prefer_cex(void *buffer, uintptr_t condition) {
   ;
 }
 
+void klee_posix_prefer_cex(void *buffer, uintptr_t condition) {
+  ;
+}
+
 void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
   /* XXX remove model version code once new tests gen'd */
   if (obj_index >= input->numObjects) {