about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Expr.h2
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp45
-rw-r--r--lib/Expr/Expr.cpp41
3 files changed, 43 insertions, 45 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 8eccdf11..212053b4 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -579,8 +579,6 @@ public:
   }
   
   static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
-  static ref<Expr> extendRead(const UpdateList &updates, ref<Expr> i,
-                              Expr::Width w);
   
   Width getWidth() const { assert(updates.root); return updates.root->getRange(); }
   Kind getKind() const { return Read; }
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 94bf2487..475b8b5c 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -54,6 +54,47 @@ llvm::cl::opt<double> ArrayValueSymbRatio(
     llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"));
 };
 
+ref<Expr> extendRead(const UpdateList &ul, const ref<Expr> index,
+                     Expr::Width w) {
+  switch (w) {
+  default:
+    assert(0 && "invalid width");
+  case Expr::Int8:
+    return ReadExpr::alloc(ul, index);
+  case Expr::Int16:
+    return ConcatExpr::create(
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
+        ReadExpr::alloc(ul, index));
+  case Expr::Int32:
+    return ConcatExpr::create4(
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
+        ReadExpr::alloc(ul, index));
+  case Expr::Int64:
+    return ConcatExpr::create8(
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
+        ReadExpr::alloc(ul, index));
+  }
+}
+
 ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
   // Nothing to optimise for constant expressions
   if (isa<ConstantExpr>(e))
@@ -574,7 +615,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
       ref<Expr> firstIndex = MulExpr::create(
           ConstantExpr::create(holes[0], re->index->getWidth()),
           ConstantExpr::create(width / 8, re->index->getWidth()));
-      result = ReadExpr::extendRead(re->updates, firstIndex, width);
+      result = extendRead(re->updates, firstIndex, width);
       for (size_t i = 1; i < holes.size(); i++) {
         ref<Expr> temp_idx = MulExpr::create(
             ConstantExpr::create(holes[i], re->index->getWidth()),
@@ -582,7 +623,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
         ref<Expr> cond = EqExpr::create(
             re->index, ConstantExpr::create(holes[i], re->index->getWidth()));
         ref<Expr> temp = SelectExpr::create(
-            cond, ReadExpr::extendRead(re->updates, temp_idx, width), result);
+            cond, extendRead(re->updates, temp_idx, width), result);
         result = temp;
       }
     }
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 9e524f62..a5c7f652 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -81,47 +81,6 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
   }
 }
 
-ref<Expr> ReadExpr::extendRead(const UpdateList &ul, const ref<Expr> index,
-                               Expr::Width w) {
-  switch (w) {
-  default:
-    assert(0 && "invalid width");
-  case Expr::Int8:
-    return ReadExpr::alloc(ul, index);
-  case Expr::Int16:
-    return ConcatExpr::create(
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
-        ReadExpr::alloc(ul, index));
-  case Expr::Int32:
-    return ConcatExpr::create4(
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
-        ReadExpr::alloc(ul, index));
-  case Expr::Int64:
-    return ConcatExpr::create8(
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
-        ReadExpr::alloc(
-            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
-        ReadExpr::alloc(ul, index));
-  }
-}
-
 int Expr::compare(const Expr &b) const {
   static ExprEquivSet equivs;
   int r = compare(b, equivs);