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/ArrayExprOptimizer.cpp | 33 ++++++++++++++++-----------------
 1 file changed, 16 insertions(+), 17 deletions(-)

(limited to 'lib/Expr/ArrayExprOptimizer.cpp')

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));
         }
       }
-- 
cgit v1.2.3