diff options
| -rw-r--r-- | lib/Expr/Expr.cpp | 13 | ||||
| -rw-r--r-- | test/Feature/RewriteEqualities.c | 4 |
2 files changed, 16 insertions, 1 deletions
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 15f52184..ac50dda2 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -529,6 +529,7 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) { // a smart UpdateList so it is not worth rescanning. const UpdateNode *un = ul.head; + bool updateListHasSymbolicWrites = false; for (; un; un=un->next) { ref<Expr> cond = EqExpr::create(index, un->index); @@ -536,10 +537,22 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) { if (CE->isTrue()) return un->value; } else { + updateListHasSymbolicWrites = true; break; } } + if (ul.root->isConstantArray() && !updateListHasSymbolicWrites) { + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(index)) { + assert(CE->getWidth() <= 64 && "Index too large"); + uint64_t concreteIndex = CE->getZExtValue(); + uint64_t size = ul.root->size; + if (concreteIndex < size) { + return ul.root->constantValues[concreteIndex]; + } + } + } + return ReadExpr::alloc(ul, index); } diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c index 6bf199f7..b3cc0ef7 100644 --- a/test/Feature/RewriteEqualities.c +++ b/test/Feature/RewriteEqualities.c @@ -5,7 +5,7 @@ // RUN: grep "N0)" %t.klee-out/test000003.kquery // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities %t.bc -// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.kquery +// RUN: FileCheck -input-file=%t.klee-out/test000003.kquery %s #include <stdio.h> #include <klee/klee.h> @@ -19,6 +19,8 @@ int run(unsigned char * x, unsigned char * y) { if(y[x[2]] < 11){ if(x[2] == 8){ + // CHECK: (query [(Eq 8 (Read w8 2 x))] + // CHECK-NEXT: false) return 2; } else{ return 3; |