Added support for KLEE value-based array optimization

3 files changed, 77 insertions, 1 deletions

diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h
index c5eac212..982136fb 100644
--- a/include/klee/ArrayExprOptimizer.h
+++ b/include/klee/ArrayExprOptimizer.h
@@ -39,11 +39,17 @@ namespace klee {
 
 enum ArrayOptimizationType {
   NONE,
-  INDEX
+  ALL,
+  INDEX,
+  VALUE
 };
 
 extern llvm::cl::opt<ArrayOptimizationType> OptimizeArray;
 
+extern llvm::cl::opt<double> ArrayValueRatio;
+
+extern llvm::cl::opt<double> ArrayValueSymbRatio;
+
 class Expr;
 template <class T> class ref;
 typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty;
@@ -54,6 +60,7 @@ class ExprOptimizer {
 private:
   unordered_map<unsigned, ref<Expr> > cacheExprOptimized;
   unordered_set<unsigned> cacheExprUnapplicable;
+  unordered_map<unsigned, ref<Expr> > cacheReadExprOptimized;
 
 public:
   void optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
@@ -64,6 +71,20 @@ private:
                       std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx)
       const;
 
+  ref<Expr> getSelectOptExpr(
+      const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
+      std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo,
+      bool isSymbolic);
+
+  ref<Expr> buildConstantSelectExpr(const ref<Expr> &index,
+                                   std::vector<uint64_t> &arrayValues,
+                                   Expr::Width width, unsigned elementsInArray) const;
+
+  ref<Expr>
+  buildMixedSelectExpr(const ReadExpr *re,
+                     std::vector<std::pair<uint64_t, bool> > &arrayValues,
+                     Expr::Width width, unsigned elementsInArray) const;
+
 };
 }
 
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 212053b4..8eccdf11 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -579,6 +579,8 @@ 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/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h
index 42eead84..70495989 100644
--- a/include/klee/util/ArrayExprVisitor.h
+++ b/include/klee/util/ArrayExprVisitor.h
@@ -86,6 +86,59 @@ public:
   }
   inline ref<Expr> getMul() { return mul; }
 };
+
+//------------------------- VALUE-BASED OPTIMIZATION-------------------------//
+class ArrayReadExprVisitor : public ExprVisitor {
+private:
+  std::vector<const ReadExpr *> &reads;
+  std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo;
+  bool symbolic;
+  bool incompatible;
+
+  Action inspectRead(unsigned hash, Expr::Width width, const ReadExpr &);
+
+protected:
+  Action visitConcat(const ConcatExpr &);
+  Action visitRead(const ReadExpr &);
+
+public:
+  ArrayReadExprVisitor(
+      std::vector<const ReadExpr *> &_reads,
+      std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &_readInfo)
+      : ExprVisitor(true), reads(_reads), readInfo(_readInfo), symbolic(false),
+        incompatible(false) {}
+  inline bool isIncompatible() { return incompatible; }
+  inline bool containsSymbolic() { return symbolic; }
+};
+
+class ArrayValueOptReplaceVisitor : public ExprVisitor {
+private:
+  unordered_set<unsigned> visited;
+  std::map<unsigned, ref<Expr> > optimized;
+
+protected:
+  Action visitConcat(const ConcatExpr &);
+  Action visitRead(const ReadExpr &re);
+
+public:
+  ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr> > &_optimized,
+                              bool recursive = true)
+      : ExprVisitor(recursive), optimized(_optimized) {}
+};
+
+class IndexCleanerVisitor : public ExprVisitor {
+private:
+  bool mul;
+  ref<Expr> index;
+
+protected:
+  Action visitMul(const MulExpr &);
+  Action visitRead(const ReadExpr &);
+
+public:
+  IndexCleanerVisitor() : ExprVisitor(true), mul(true) {}
+  inline ref<Expr> getIndex() { return index; }
+};
 }
 
 #endif