about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-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-pink 1.4.1 (git 2.36.1) at 2024-09-21 07:26:41 +0000