diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-20 18:38:36 +0000 |
---|---|---|
committer | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-02-14 13:10:05 +0000 |
commit | daf4eef5c3b99cdbc894f6bee40b4d047c5e6553 (patch) | |
tree | 6336f7aa46c84a3b19f4c0e982101d444aa00adc /lib | |
parent | 19b7bdd916c484b52ce1237401b15a346575b4cf (diff) | |
download | klee-daf4eef5c3b99cdbc894f6bee40b4d047c5e6553.tar.gz |
ReadExpr::create() was missing an opportunity to constant fold when handling constant arrays.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Expr/Expr.cpp | 13 |
1 files changed, 13 insertions, 0 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); } |