about summary refs log tree commit diff homepage
path: root/lib/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp17
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp16
-rw-r--r--lib/Expr/ArrayExprVisitor.h14
3 files changed, 5 insertions, 42 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index b55974d0..60f2ca6e 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -313,12 +313,9 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
         arrayValues.push_back(val);
       }
 
-      ref<Expr> index = read->index;
-      IndexCleanerVisitor ice;
-      ice.visit(index);
-      if (ice.getIndex().get()) {
-        index = ice.getIndex();
-      }
+      ref<Expr> index = UDivExpr::create(
+          read->index,
+          ConstantExpr::create(bytesPerElement, read->index->getWidth()));
 
       ref<Expr> opt =
           buildConstantSelectExpr(index, arrayValues, width, elementsInArray);
@@ -650,12 +647,8 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
       }
     }
 
-    ref<Expr> new_index = re->index;
-    IndexCleanerVisitor ice;
-    ice.visit(new_index);
-    if (ice.getIndex().get()) {
-      new_index = ice.getIndex();
-    }
+    ref<Expr> new_index = UDivExpr::create(
+        re->index, ConstantExpr::create(width / 8, re->index->getWidth()));
 
     int new_index_width = new_index->getWidth();
     // Iterate through all the ranges
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index 75604104..cada7867 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -256,19 +256,3 @@ ExprVisitor::Action ArrayValueOptReplaceVisitor::visitRead(const ReadExpr &re) {
   }
   return Action::doChildren();
 }
-
-ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) {
-  if (mul) {
-    if (!isa<ConstantExpr>(e.getKid(0)))
-      index = e.getKid(0);
-    else if (!isa<ConstantExpr>(e.getKid(1)))
-      index = e.getKid(1);
-    mul = false;
-  }
-  return Action::doChildren();
-}
-
-ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &) {
-  mul = false;
-  return Action::doChildren();
-}
diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h
index 37f14cd1..28f485d9 100644
--- a/lib/Expr/ArrayExprVisitor.h
+++ b/lib/Expr/ArrayExprVisitor.h
@@ -124,20 +124,6 @@ public:
                                        bool recursive = true)
       : ExprVisitor(recursive), optimized(_optimized) {}
 };
-
-class IndexCleanerVisitor : public ExprVisitor {
-private:
-  bool mul{true};
-  ref<Expr> index;
-
-protected:
-  Action visitMul(const MulExpr &) override;
-  Action visitRead(const ReadExpr &) override;
-
-public:
-  IndexCleanerVisitor() : ExprVisitor(true) {}
-  inline ref<Expr> getIndex() { return index; }
-};
 } // namespace klee
 
 #endif /* KLEE_ARRAYEXPRVISITOR_H */