Fixed fail with preferCex, removed relation from first argument

7 files changed, 101 insertions, 34 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 47a3b3c6..2f585f96 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -103,6 +103,7 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     symPathOS(state.symPathOS),
     coveredLines(state.coveredLines),
     symbolics(state.symbolics),
+    cexPreferences(state.cexPreferences),
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
     steppedInstructions(state.steppedInstructions),
@@ -358,3 +359,7 @@ void ExecutionState::addConstraint(ref<Expr> e) {
   ConstraintManager c(constraints);
   c.addConstraint(e);
 }
+
+void ExecutionState::addCexPreference(const ref<Expr> &cond) {
+  cexPreferences = cexPreferences.insert(cond);
+}
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index f91790d5..8f5e57e8 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -13,6 +13,7 @@
 #include "AddressSpace.h"
 #include "MergeHandler.h"
 
+#include "klee/ADT/ImmutableSet.h"
 #include "klee/ADT/TreeStream.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
@@ -207,6 +208,10 @@ public:
   // FIXME: Move to a shared list structure (not critical).
   std::vector<std::pair<ref<const MemoryObject>, const Array *>> symbolics;
 
+  /// @brief A set of boolean expressions
+  /// the user has requested be true of a counterexample.
+  ImmutableSet<ref<Expr>> cexPreferences;
+
   /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
 
@@ -259,6 +264,7 @@ public:
   void addSymbolic(const MemoryObject *mo, const Array *array);
 
   void addConstraint(ref<Expr> e);
+  void addCexPreference(const ref<Expr> &cond);
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dcb078df..3d6ea4ae 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -4560,27 +4560,19 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   // 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 auto &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(extendedConstraints, Expr::createIsZero(*pi),
-                             mustBeTrue, state.queryMetaData);
-      // 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)
-        cm.addConstraint(*pi);
-    }
-    if (pi!=pie) break;
+  for (auto& pi: state.cexPreferences) {
+    bool mustBeTrue;
+    // Attempt to bound byte to constraints held in cexPreferences
+    bool success =
+      solver->mustBeTrue(extendedConstraints, Expr::createIsZero(pi),
+        mustBeTrue, state.queryMetaData);
+    // If it isn't possible to add the condition without making the entire list
+    // UNSAT, then just continue to the next condition
+    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)
+      cm.addConstraint(pi);
   }
 
   std::vector< std::vector<unsigned char> > values;
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index e88d5f55..d5189df5 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -64,12 +64,6 @@ public:
   /// should be either the allocating instruction or the global object
   /// it was allocated for (or whatever else makes sense).
   const llvm::Value *allocSite;
-  
-  /// A list of boolean expressions the user has requested be true of
-  /// a counterexample. Mutable since we play a little fast and loose
-  /// with allowing it to be added to during execution (although
-  /// should sensibly be only at creation time).
-  mutable std::vector< ref<Expr> > cexPreferences;
 
   // DO NOT IMPLEMENT
   MemoryObject(const MemoryObject &b);
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 27ca385c..94c4dc3c 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -549,13 +549,7 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
   if (cond->getWidth() != Expr::Bool)
     cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond->getWidth()));
 
-  Executor::ExactResolutionList rl;
-  executor.resolveExact(state, arguments[0], rl, "prefex_cex");
-  
-  assert(rl.size() == 1 &&
-         "prefer_cex target must resolve to precisely one object");
-
-  rl[0].first.first->cexPreferences.push_back(cond);
+  state.addCexPreference(cond);
 }
 
 void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state,
diff --git a/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c b/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c
new file mode 100644
index 00000000..09d60e79
--- /dev/null
+++ b/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c
@@ -0,0 +1,25 @@
+// RUN: %clang %s -S -emit-llvm -g -c -o %t.ll
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.ll
+// KLEE just must not fail
+#include "klee/klee.h"
+
+int main() {
+  char i;
+  char *p;
+  char *q;
+  klee_make_symbolic(&i, sizeof(i), "i");
+  klee_make_symbolic(&p, sizeof(p), "p");
+
+  if (i) {}
+
+  q = malloc(sizeof (char));
+  klee_assume(p == q);
+  klee_make_symbolic(p, sizeof (char), "p[0]");
+
+  char condition = (*p);
+  if (*p) condition = 1;
+  klee_prefer_cex(&i, condition);
+  if (i+5) {}
+  return 0;
+}
diff --git a/test/Replay/libkleeruntest/replay_cex_incorrect_result.c b/test/Replay/libkleeruntest/replay_cex_incorrect_result.c
new file mode 100644
index 00000000..46fab72e
--- /dev/null
+++ b/test/Replay/libkleeruntest/replay_cex_incorrect_result.c
@@ -0,0 +1,51 @@
+// RUN: %clang %s -S -emit-llvm -g -c -o %t.ll
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --search=dfs --output-dir=%t.klee-out %t.ll
+
+// This should produce four test cases.
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: test -f %t.klee-out/test000002.ktest
+// RUN: test -f %t.klee-out/test000003.ktest
+// RUN: test -f %t.klee-out/test000004.ktest
+// RUN: test ! -f %t.klee-out/test000005.ktest
+
+// Now try to replay with libkleeRuntest
+// RUN: %cc -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner
+
+// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_1 %s
+// RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_2 %s
+// RUN: env KTEST_FILE=%t.klee-out/test000003.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_3 %s
+// RUN: env KTEST_FILE=%t.klee-out/test000004.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_4 %s
+
+#include <klee/klee.h>
+#include <stdio.h>
+
+void f0(void) {}
+void f1(void) {}
+void f2(void) {}
+void f3(void) {}
+
+int main() {
+  int x = klee_range(0, 256, "x");
+
+  if (x == 17) {
+    f0();
+    // CHECK_4: x=17
+  } else if (x == 32) {
+    f1();
+    // CHECK_3: x=32
+  } else if (x == 99) {
+    f2();
+    // CHECK_2: x=99
+  } else {
+    klee_prefer_cex(&x, x == 0);
+    f3();
+    // CHECK_1: x=0
+  }
+
+#ifdef PRINT_VALUE
+  printf("x=%d\n", x);
+#endif
+
+  return 0;
+}