diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2019-11-07 14:27:07 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-12-12 17:50:24 +0000 |
commit | d8deadd787d0f857d701b73aeaa3e0753efd9405 (patch) | |
tree | 4c28ae2980194460f6694b807fc8ede72aff57f9 /lib/Expr | |
parent | ebd3eb0ec11b053ddf5eee44c1217436948279d9 (diff) | |
download | klee-d8deadd787d0f857d701b73aeaa3e0753efd9405.tar.gz |
[optimize-array] Fix update list read order
ArrayExprOptimizer read the UpdateList in the wrong order, which meant that it used least recent update instead of the most recent one. This patch fixes this as well as adds a test to illustrate the issue.
Diffstat (limited to 'lib/Expr')
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 1a48adfe..e43530ec 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -280,8 +280,17 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( // assume that the UpdateNodes contain ConstantExpr indexes and values assert(read->updates.root->isConstantArray() && "Expected concrete array, found symbolic array"); + + // We need to read updates from lest recent to most recent, therefore + // reverse the list + std::vector<const UpdateNode *> us; + us.reserve(read->updates.getSize()); + for (const UpdateNode *un = read->updates.head; un; un = un->next) + us.push_back(un); + auto arrayConstValues = read->updates.root->constantValues; - for (const UpdateNode *un = read->updates.head; un; un = un->next) { + for (auto it = us.rbegin(); it != us.rend(); it++) { + const UpdateNode *un = *it; auto ce = dyn_cast<ConstantExpr>(un->index); assert(ce && "Not a constant expression"); uint64_t index = ce->getAPValue().getZExtValue(); @@ -356,7 +365,16 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( arrayConstValues.push_back(ConstantExpr::create(0, Expr::Int8)); } } - for (const UpdateNode *un = read->updates.head; un; un = un->next) { + + // We need to read updates from lest recent to most recent, therefore + // reverse the list + std::vector<const UpdateNode *> us; + us.reserve(read->updates.getSize()); + for (const UpdateNode *un = read->updates.head; un; un = un->next) + us.push_back(un); + + for (auto it = us.rbegin(); it != us.rend(); it++) { + const UpdateNode *un = *it; auto ce = dyn_cast<ConstantExpr>(un->index); assert(ce && "Not a constant expression"); uint64_t index = ce->getAPValue().getLimitedValue(); |