From 3f2f8aa30b35bb87fa7b7aa914233437b5d68cb2 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <tk1713@ic.ac.uk>
Date: Tue, 5 Nov 2019 09:53:03 +0000
Subject: [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.
---
 lib/Expr/ArrayExprVisitor.h | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'lib/Expr/ArrayExprVisitor.h')

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) {}
 };
 
-- 
cgit 1.4.1