diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2019-11-05 09:53:03 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-12-12 17:50:24 +0000 |
commit | 3f2f8aa30b35bb87fa7b7aa914233437b5d68cb2 (patch) | |
tree | 1c15b6f34f723151279abb32ab906fac3c0a7889 /lib | |
parent | eedc49570c3ed3111b2a2a11a7861ac90ab650f8 (diff) | |
download | klee-3f2f8aa30b35bb87fa7b7aa914233437b5d68cb2.tar.gz |
[optimize-array] Fix hash collisions
The caching maps in ArrayExpr are broken, they only consider hashes and don't check for structural equality. This can lead to hash collisions and invalid Expr replacement. This is especially potetent for UpdateLists, who only put the array name in the hash, so there can be a lot of colisions.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 33 | ||||
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.h | 9 | ||||
-rw-r--r-- | lib/Expr/ArrayExprVisitor.cpp | 10 | ||||
-rw-r--r-- | lib/Expr/ArrayExprVisitor.h | 14 |
4 files changed, 33 insertions, 33 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index e43530ec..8ba0b40d 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -110,12 +110,11 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { if (OptimizeArray == NONE) return e; - unsigned hash = e->hash(); - if (cacheExprUnapplicable.find(hash) != cacheExprUnapplicable.end()) + if (cacheExprUnapplicable.count(e) > 0) return e; // Find cached expressions - auto cached = cacheExprOptimized.find(hash); + auto cached = cacheExprOptimized.find(e); if (cached != cacheExprOptimized.end()) return cached->second; @@ -132,7 +131,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { // If we cannot optimize the expression, we return a failure only // when we are not combining the optimizations if (OptimizeArray == INDEX) { - cacheExprUnapplicable.insert(hash); + cacheExprUnapplicable.insert(e); return e; } } else { @@ -150,13 +149,13 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { // Add new expression to cache if (result.get()) { klee_warning("OPT_I: successful"); - cacheExprOptimized[hash] = result; + cacheExprOptimized[e] = result; } else { klee_warning("OPT_I: unsuccessful"); } } else { klee_warning("OPT_I: unsuccessful"); - cacheExprUnapplicable.insert(hash); + cacheExprUnapplicable.insert(e); } } } @@ -164,13 +163,13 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { if (OptimizeArray == VALUE || (OptimizeArray == ALL && (!result.get() || valueOnly))) { std::vector<const ReadExpr *> reads; - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> readInfo; + std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> readInfo; ArrayReadExprVisitor are(reads, readInfo); are.visit(e); std::reverse(reads.begin(), reads.end()); if (reads.empty() || are.isIncompatible()) { - cacheExprUnapplicable.insert(hash); + cacheExprUnapplicable.insert(e); return e; } @@ -179,10 +178,10 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { if (selectOpt.get()) { klee_warning("OPT_V: successful"); result = selectOpt; - cacheExprOptimized[hash] = result; + cacheExprOptimized[e] = result; } else { klee_warning("OPT_V: unsuccessful"); - cacheExprUnapplicable.insert(hash); + cacheExprUnapplicable.insert(e); } } if (result.isNull()) @@ -253,17 +252,17 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, ref<Expr> ExprOptimizer::getSelectOptExpr( const ref<Expr> &e, std::vector<const ReadExpr *> &reads, - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo, + std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &readInfo, bool isSymbolic) { ref<Expr> notFound; ref<Expr> toReturn; // Array is concrete if (!isSymbolic) { - std::map<unsigned, ref<Expr>> optimized; + ExprHashMap<ref<Expr>> optimized; for (auto &read : reads) { auto info = readInfo[read]; - auto cached = cacheReadExprOptimized.find(read->hash()); + auto cached = cacheReadExprOptimized.find(const_cast<ReadExpr *>(read)); if (cached != cacheReadExprOptimized.end()) { optimized.insert(std::make_pair(info.first, (*cached).second)); continue; @@ -324,7 +323,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( ref<Expr> opt = buildConstantSelectExpr(index, arrayValues, width, elementsInArray); if (opt.get()) { - cacheReadExprOptimized[read->hash()] = opt; + cacheReadExprOptimized[const_cast<ReadExpr *>(read)] = opt; optimized.insert(std::make_pair(info.first, opt)); } } @@ -337,10 +336,10 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( // OR // array is symbolic && updatelist contains at least one concrete value else { - std::map<unsigned, ref<Expr>> optimized; + ExprHashMap<ref<Expr>> optimized; for (auto &read : reads) { auto info = readInfo[read]; - auto cached = cacheReadExprOptimized.find(read->hash()); + auto cached = cacheReadExprOptimized.find(const_cast<ReadExpr *>(read)); if (cached != cacheReadExprOptimized.end()) { optimized.insert(std::make_pair(info.first, (*cached).second)); continue; @@ -422,7 +421,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( ref<Expr> opt = buildMixedSelectExpr(read, arrayValues, width, elementsInArray); if (opt.get()) { - cacheReadExprOptimized[read->hash()] = opt; + cacheReadExprOptimized[const_cast<ReadExpr *>(read)] = opt; optimized.insert(std::make_pair(info.first, opt)); } } diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h index ca90931d..8fc040e5 100644 --- a/lib/Expr/ArrayExprOptimizer.h +++ b/lib/Expr/ArrayExprOptimizer.h @@ -18,6 +18,7 @@ #include <vector> #include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" #include "klee/util/Ref.h" namespace klee { @@ -29,9 +30,9 @@ using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>; class ExprOptimizer { private: - std::unordered_map<unsigned, ref<Expr>> cacheExprOptimized; - std::unordered_set<unsigned> cacheExprUnapplicable; - std::unordered_map<unsigned, ref<Expr>> cacheReadExprOptimized; + ExprHashMap<ref<Expr>> cacheExprOptimized; + ExprHashSet cacheExprUnapplicable; + ExprHashMap<ref<Expr>> cacheReadExprOptimized; public: /// Returns the optimised version of e. @@ -46,7 +47,7 @@ private: ref<Expr> getSelectOptExpr( const ref<Expr> &e, std::vector<const ReadExpr *> &reads, - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo, + std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &readInfo, bool isSymbolic); ref<Expr> buildConstantSelectExpr(const ref<Expr> &index, diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index e4ea9a1c..75604104 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -183,16 +183,16 @@ ExprVisitor::Action IndexTransformationExprVisitor::visitMul(const MulExpr &e) { ExprVisitor::Action ArrayReadExprVisitor::visitConcat(const ConcatExpr &ce) { ReadExpr *base = ArrayExprHelper::hasOrderedReads(ce); if (base) { - return inspectRead(ce.hash(), ce.getWidth(), *base); + return inspectRead(const_cast<ConcatExpr *>(&ce), ce.getWidth(), *base); } return Action::doChildren(); } ExprVisitor::Action ArrayReadExprVisitor::visitRead(const ReadExpr &re) { - return inspectRead(re.hash(), re.getWidth(), re); + return inspectRead(const_cast<ReadExpr *>(&re), re.getWidth(), re); } // This method is a mess because I want to avoid looping over the UpdateList // values twice -ExprVisitor::Action ArrayReadExprVisitor::inspectRead(unsigned hash, +ExprVisitor::Action ArrayReadExprVisitor::inspectRead(ref<Expr> hash, Expr::Width width, const ReadExpr &re) { // pre(*): index is symbolic @@ -243,14 +243,14 @@ ExprVisitor::Action ArrayReadExprVisitor::inspectRead(unsigned hash, ExprVisitor::Action ArrayValueOptReplaceVisitor::visitConcat(const ConcatExpr &ce) { - auto found = optimized.find(ce.hash()); + auto found = optimized.find(const_cast<ConcatExpr *>(&ce)); if (found != optimized.end()) { return Action::changeTo((*found).second.get()); } return Action::doChildren(); } ExprVisitor::Action ArrayValueOptReplaceVisitor::visitRead(const ReadExpr &re) { - auto found = optimized.find(re.hash()); + auto found = optimized.find(const_cast<ReadExpr *>(&re)); if (found != optimized.end()) { return Action::changeTo((*found).second.get()); } diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h index c5a4691e..37f14cd1 100644 --- a/lib/Expr/ArrayExprVisitor.h +++ b/lib/Expr/ArrayExprVisitor.h @@ -11,6 +11,7 @@ #define KLEE_ARRAYEXPRVISITOR_H #include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprVisitor.h" #include "klee/Solver/SolverCmdLine.h" @@ -90,11 +91,11 @@ public: class ArrayReadExprVisitor : public ExprVisitor { private: std::vector<const ReadExpr *> &reads; - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo; + std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &readInfo; bool symbolic; bool incompatible; - Action inspectRead(unsigned hash, Expr::Width width, const ReadExpr &); + Action inspectRead(ref<Expr> hash, Expr::Width width, const ReadExpr &); protected: Action visitConcat(const ConcatExpr &) override; @@ -103,7 +104,7 @@ protected: public: ArrayReadExprVisitor( std::vector<const ReadExpr *> &_reads, - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &_readInfo) + std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &_readInfo) : ExprVisitor(true), reads(_reads), readInfo(_readInfo), symbolic(false), incompatible(false) {} inline bool isIncompatible() { return incompatible; } @@ -112,16 +113,15 @@ public: class ArrayValueOptReplaceVisitor : public ExprVisitor { private: - std::unordered_set<unsigned> visited; - std::map<unsigned, ref<Expr>> optimized; + ExprHashMap<ref<Expr>> optimized; protected: Action visitConcat(const ConcatExpr &) override; Action visitRead(const ReadExpr &re) override; public: - explicit ArrayValueOptReplaceVisitor( - std::map<unsigned, ref<Expr>> &_optimized, bool recursive = true) + explicit ArrayValueOptReplaceVisitor(ExprHashMap<ref<Expr>> &_optimized, + bool recursive = true) : ExprVisitor(recursive), optimized(_optimized) {} }; |