Move optimization specific headers away from the project include directory

Don't pollute the project include directory with optimization specific
headers.

1 files changed, 143 insertions, 0 deletions

diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h
new file mode 100644
index 00000000..c1eb7f58
--- /dev/null
+++ b/lib/Expr/ArrayExprVisitor.h
@@ -0,0 +1,143 @@
+//===-- ArrayExprVisitor.h ------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_ARRAYEXPRVISITOR_H_
+#define KLEE_ARRAYEXPRVISITOR_H_
+
+#include "klee/CommandLine.h"
+#include "klee/ExprBuilder.h"
+#include "klee/util/ExprVisitor.h"
+
+#include <unordered_map>
+#include <unordered_set>
+
+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
+  std::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; }
+};
+
+//------------------------- 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:
+  std::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; }
+};
+} // namespace klee
+
+#endif