aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp33
-rw-r--r--lib/Expr/ArrayExprOptimizer.h9
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp10
-rw-r--r--lib/Expr/ArrayExprVisitor.h14
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) {}
};
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-16 03:25:21 +0000