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/Expr/Expr.cpp | |
| 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/Expr/Expr.cpp')
| -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); } | 
