Add Read consistency test case, spelling

2 files changed, 42 insertions, 3 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 54f68f21..060595d6 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -533,9 +533,9 @@ unsigned Array::computeHash() {
 ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
   // rollback update nodes if possible
 
-  // Iterate throught the update list from the most recent to the
-  // least reasent to find a potential written value for a concrete index;
-  // stop, if an update with symbolic has been found as we don't know which
+  // Iterate through the update list from the most recent to the
+  // least recent to find a potential written value for a concrete index;
+  // stop if an update with symbolic has been found as we don't know which
   // array element has been updated
   const UpdateNode *un = ul.head;
   bool updateListHasSymbolicWrites = false;
diff --git a/test/Expr/ReadExprConsistency.c b/test/Expr/ReadExprConsistency.c
new file mode 100644
index 00000000..f71483ba
--- /dev/null
+++ b/test/Expr/ReadExprConsistency.c
@@ -0,0 +1,39 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t.bc 2>%t.log
+// RUN: cat %t.log | FileCheck %s
+
+#include <assert.h>
+
+/*
+This tests checks ensures that only relevant updates are present when doing
+concrete reads. If they are not, there can be situations where ReadExpr are
+in inconcistent state and depend on ordering of other operations.
+
+See
+https://github.com/klee/klee/issues/921
+https://github.com/klee/klee/pull/1061
+*/
+
+void klee_print_expr(const char*, char);
+int main() {
+	char  arr[3];
+  char symbolic;
+  klee_make_symbolic(&symbolic, sizeof(symbolic), "symbolic");
+  klee_assume(symbolic >= 0 & symbolic < 3); 
+  klee_make_symbolic(arr, sizeof(arr), "arr");
+  
+  
+  char a = arr[2];  // (ReadExpr 2 arr)
+  //CHECK: arr[2]:(Read w8 2 arr)
+  klee_print_expr("arr[2]", arr[2]);
+  arr[1] = 0;
+  char b = arr[symbolic];  // (ReadExpr symbolic [1=0]@arr)
+  //CHECK: arr[2]:(Read w8 2 arr)
+  //CHECK-NOT: arr[2]:(Read w8 2 [1=0]@arr)
+  klee_print_expr("arr[2]", arr[2]);
+  
+  if(a == b) printf("Equal!\n");
+  else printf("Not Equal!\n");
+  return 0;
+}