Added support for KLEE index-based array optimization

4 files changed, 262 insertions, 0 deletions

diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h
new file mode 100644
index 00000000..c5eac212
--- /dev/null
+++ b/include/klee/ArrayExprOptimizer.h
@@ -0,0 +1,70 @@
+#ifndef KLEE_EXPROPTIMIZER_H
+#define KLEE_EXPROPTIMIZER_H
+
+#include <cassert>
+#include <iterator>
+#include <map>
+#include <string>
+#include <utility>
+#include <vector>
+
+#include "Expr.h"
+#include "ExprBuilder.h"
+#include "Constraints.h"
+#include "Internal/Support/ErrorHandling.h"
+#include "util/ArrayExprVisitor.h"
+#include "util/Assignment.h"
+#include "util/Ref.h"
+#include "klee/AssignmentGenerator.h"
+#include "klee/ExecutionState.h"
+
+#include "llvm/Support/TimeValue.h"
+#include "klee/Internal/System/Time.h"
+
+#include <ciso646>
+
+#ifdef _LIBCPP_VERSION
+#include <unordered_map>
+#include <unordered_set>
+#define unordered_map std::unordered_map
+#define unordered_set std::unordered_set
+#else
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+#define unordered_map std::tr1::unordered_map
+#define unordered_set std::tr1::unordered_set
+#endif
+
+namespace klee {
+
+enum ArrayOptimizationType {
+  NONE,
+  INDEX
+};
+
+extern llvm::cl::opt<ArrayOptimizationType> OptimizeArray;
+
+class Expr;
+template <class T> class ref;
+typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty;
+typedef std::vector<const Array *> v_arr_ty;
+typedef std::map<ref<Expr>, std::vector<ref<Expr> > > mapIndexOptimizedExpr_ty;
+
+class ExprOptimizer {
+private:
+  unordered_map<unsigned, ref<Expr> > cacheExprOptimized;
+  unordered_set<unsigned> cacheExprUnapplicable;
+
+public:
+  void optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
+                    bool valueOnly = false);
+
+private:
+  bool computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
+                      std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx)
+      const;
+
+};
+}
+
+#endif
diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h
new file mode 100644
index 00000000..dafcfef6
--- /dev/null
+++ b/include/klee/ArrayExprRewriter.h
@@ -0,0 +1,43 @@
+#ifndef LIB_EXPRREWRITER_H_
+#define LIB_EXPRREWRITER_H_
+
+#include "klee/Expr.h"
+#include "klee/CommandLine.h"
+#include "klee/Constraints.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/util/ArrayExprVisitor.h"
+#include "klee/util/Assignment.h"
+#include "klee/util/Ref.h"
+#include "klee/AssignmentGenerator.h"
+
+namespace klee {
+
+typedef std::vector<const Array *> v_arr_ty;
+typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty;
+typedef std::map<ref<Expr>, std::vector<ref<Expr> > > mapIndexOptimizedExpr_ty;
+
+class ExprRewriter {
+public:
+  static ref<Expr> createOptExpr(
+      const ref<Expr> &e, const array2idx_ty &arrays,
+      const std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx);
+
+private:
+  static ref<Expr>
+  rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
+          const std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx);
+
+  static ref<Expr>
+  concatenateOrExpr(const std::vector<ref<Expr> >::const_iterator begin,
+                    const std::vector<ref<Expr> >::const_iterator end);
+
+  static ref<Expr> createEqExpr(const ref<Expr> &index,
+                                const ref<Expr> &valIndex);
+
+  static ref<Expr> createRangeExpr(const ref<Expr> &index,
+                                   const ref<Expr> &valStart,
+                                   const ref<Expr> &valEnd);
+};
+}
+
+#endif /* LIB_EXPRREWRITER_H_ */
diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h
new file mode 100644
index 00000000..835651b8
--- /dev/null
+++ b/include/klee/AssignmentGenerator.h
@@ -0,0 +1,58 @@
+#ifndef KLEE_ASSIGNMENTGENERATOR_H
+#define KLEE_ASSIGNMENTGENERATOR_H
+
+#include <cassert>
+#include <iterator>
+#include <map>
+#include <string>
+#include <utility>
+#include <vector>
+
+#include "Expr.h"
+#include "Constraints.h"
+#include "Internal/Support/ErrorHandling.h"
+#include "util/ArrayExprVisitor.h"
+#include "util/Assignment.h"
+#include "util/Ref.h"
+
+#include "llvm/Support/TimeValue.h"
+#include "klee/Internal/System/Time.h"
+
+namespace klee {
+
+class Expr;
+template <class T> class ref;
+
+class AssignmentGenerator {
+public:
+  static bool generatePartialAssignment(const ref<Expr> &e, ref<Expr> &val,
+                                        Assignment *&a);
+
+private:
+  static bool helperGenerateAssignment(const ref<Expr> &e, ref<Expr> &val,
+                                       Assignment *&a, Expr::Width width,
+                                       bool sign);
+
+  static bool isReadExprAtOffset(ref<Expr> e, const ReadExpr *base,
+                                 ref<Expr> offset);
+  static ReadExpr *hasOrderedReads(ref<Expr> e);
+
+  static ref<Expr> createSubExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createAddExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createMulExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createDivExpr(const ref<Expr> &l, ref<Expr> &r, bool sign);
+  static ref<Expr> createDivRem(const ref<Expr> &l, ref<Expr> &r, bool sign);
+  static ref<Expr> createShlExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createLShrExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createAndExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createExtractExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createExtendExpr(const ref<Expr> &l, ref<Expr> &r);
+
+  static std::vector<unsigned char> getByteValue(ref<Expr> &val);
+  static std::vector<unsigned char>
+  getIndexedValue(const std::vector<unsigned char> &c_val, ConstantExpr &index,
+                  const unsigned int size);
+};
+}
+
+#endif
diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h
new file mode 100644
index 00000000..42eead84
--- /dev/null
+++ b/include/klee/util/ArrayExprVisitor.h
@@ -0,0 +1,91 @@
+#ifndef KLEE_ARRAYEXPRVISITOR_H_
+#define KLEE_ARRAYEXPRVISITOR_H_
+
+#include "klee/util/ExprVisitor.h"
+#include "klee/ExprBuilder.h"
+#include "klee/CommandLine.h"
+
+#include <ciso646>
+#ifdef _LIBCPP_VERSION
+#include <unordered_map>
+#include <unordered_set>
+#define unordered_map std::unordered_map
+#define unordered_set std::unordered_set
+#else
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+#define unordered_map std::tr1::unordered_map
+#define unordered_set std::tr1::unordered_set
+#endif
+
+namespace klee {
+
+//------------------------------ HELPER FUNCTIONS ---------------------------//
+class ArrayExprHelper {
+private:
+  static bool isReadExprAtOffset(ref<Expr> e, const ReadExpr *base,
+                                 ref<Expr> offset);
+
+public:
+  static ReadExpr *hasOrderedReads(const ConcatExpr &ce);
+};
+
+//--------------------------- INDEX-BASED OPTIMIZATION-----------------------//
+class ConstantArrayExprVisitor : public ExprVisitor {
+private:
+  typedef std::map<const Array *, std::vector<ref<Expr> > > bindings_ty;
+  bindings_ty &arrays;
+  // Avoids adding the same index twice
+  unordered_set<unsigned> addedIndexes;
+  bool incompatible;
+
+protected:
+  Action visitConcat(const ConcatExpr &);
+  Action visitRead(const ReadExpr &);
+
+public:
+  ConstantArrayExprVisitor(bindings_ty &_arrays)
+      : arrays(_arrays), incompatible(false) {}
+  inline bool isIncompatible() { return incompatible; }
+};
+
+class IndexCompatibilityExprVisitor : public ExprVisitor {
+private:
+  bool compatible;
+  bool inner;
+
+protected:
+  Action visitRead(const ReadExpr &);
+  Action visitURem(const URemExpr &);
+  Action visitSRem(const SRemExpr &);
+  Action visitOr(const OrExpr &);
+
+public:
+  IndexCompatibilityExprVisitor() : compatible(true), inner(false) {}
+
+  inline bool isCompatible() { return compatible; }
+  inline bool hasInnerReads() { return inner; }
+};
+
+class IndexTransformationExprVisitor : public ExprVisitor {
+private:
+  const Array *array;
+  Expr::Width width;
+  ref<Expr> mul;
+
+protected:
+  Action visitConcat(const ConcatExpr &);
+  Action visitMul(const MulExpr &);
+
+public:
+  IndexTransformationExprVisitor(const Array *_array)
+      : array(_array), width(Expr::InvalidWidth) {}
+
+  inline Expr::Width getWidth() {
+    return width == Expr::InvalidWidth ? Expr::Int8 : width;
+  }
+  inline ref<Expr> getMul() { return mul; }
+};
+}
+
+#endif