Move header files from lib/Expr to include/klee/Expr to eliminate includes using "../"

4 files changed, 300 insertions, 0 deletions

diff --git a/include/klee/Expr/ArrayExprOptimizer.h b/include/klee/Expr/ArrayExprOptimizer.h
new file mode 100644
index 00000000..8fc040e5
--- /dev/null
+++ b/include/klee/Expr/ArrayExprOptimizer.h
@@ -0,0 +1,65 @@
+//===-- ArrayExprOptimizer.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_ARRAYEXPROPTIMIZER_H
+#define KLEE_ARRAYEXPROPTIMIZER_H
+
+#include <cstdint>
+#include <map>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/util/Ref.h"
+
+namespace klee {
+
+enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE };
+
+using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>;
+using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>;
+
+class ExprOptimizer {
+private:
+  ExprHashMap<ref<Expr>> cacheExprOptimized;
+  ExprHashSet cacheExprUnapplicable;
+  ExprHashMap<ref<Expr>> cacheReadExprOptimized;
+
+public:
+  /// Returns the optimised version of e.
+  /// @param e expression to optimise
+  /// @param valueOnly XXX document
+  /// @return optimised expression
+  ref<Expr> optimizeExpr(const ref<Expr> &e, bool valueOnly);
+
+private:
+  bool computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
+                      mapIndexOptimizedExpr_ty &idx_valIdx) const;
+
+  ref<Expr> getSelectOptExpr(
+      const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
+      std::map<const ReadExpr *, std::pair<ref<Expr>, 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;
+};
+} // namespace klee
+
+#endif /* KLEE_ARRAYEXPROPTIMIZER_H */
diff --git a/include/klee/Expr/ArrayExprRewriter.h b/include/klee/Expr/ArrayExprRewriter.h
new file mode 100644
index 00000000..098cb0a6
--- /dev/null
+++ b/include/klee/Expr/ArrayExprRewriter.h
@@ -0,0 +1,47 @@
+//===-- ArrayExprRewriter.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_ARRAYEXPRREWRITER_H
+#define KLEE_ARRAYEXPRREWRITER_H
+
+#include <iterator>
+#include <map>
+#include <vector>
+
+#include "klee/Expr/Expr.h"
+#include "klee/util/Ref.h"
+
+namespace klee {
+
+using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>;
+using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>;
+
+class ExprRewriter {
+public:
+  static ref<Expr> createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays,
+                                 const mapIndexOptimizedExpr_ty &idx_valIdx);
+
+private:
+  static ref<Expr> rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
+                           const mapIndexOptimizedExpr_ty &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);
+};
+} // namespace klee
+
+#endif /* KLEE_ARRAYEXPRREWRITER_H */
diff --git a/include/klee/Expr/ArrayExprVisitor.h b/include/klee/Expr/ArrayExprVisitor.h
new file mode 100644
index 00000000..28f485d9
--- /dev/null
+++ b/include/klee/Expr/ArrayExprVisitor.h
@@ -0,0 +1,129 @@
+//===-- 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/Expr/ExprBuilder.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprVisitor.h"
+#include "klee/Solver/SolverCmdLine.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:
+  using bindings_ty = std::map<const Array *, std::vector<ref<Expr>>>;
+  bindings_ty &arrays;
+  // Avoids adding the same index twice
+  std::unordered_set<unsigned> addedIndexes;
+  bool incompatible;
+
+protected:
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitRead(const ReadExpr &) override;
+
+public:
+  explicit ConstantArrayExprVisitor(bindings_ty &_arrays)
+      : arrays(_arrays), incompatible(false) {}
+  inline bool isIncompatible() { return incompatible; }
+};
+
+class IndexCompatibilityExprVisitor : public ExprVisitor {
+private:
+  bool compatible{true};
+  bool inner{false};
+
+protected:
+  Action visitRead(const ReadExpr &) override;
+  Action visitURem(const URemExpr &) override;
+  Action visitSRem(const SRemExpr &) override;
+  Action visitOr(const OrExpr &) override;
+
+public:
+  IndexCompatibilityExprVisitor() = default;
+
+  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 &) override;
+  Action visitMul(const MulExpr &) override;
+
+public:
+  explicit 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<ref<Expr>, Expr::Width>> &readInfo;
+  bool symbolic;
+  bool incompatible;
+
+  Action inspectRead(ref<Expr> hash, Expr::Width width, const ReadExpr &);
+
+protected:
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitRead(const ReadExpr &) override;
+
+public:
+  ArrayReadExprVisitor(
+      std::vector<const ReadExpr *> &_reads,
+      std::map<const ReadExpr *, std::pair<ref<Expr>, 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:
+  ExprHashMap<ref<Expr>> optimized;
+
+protected:
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitRead(const ReadExpr &re) override;
+
+public:
+  explicit ArrayValueOptReplaceVisitor(ExprHashMap<ref<Expr>> &_optimized,
+                                       bool recursive = true)
+      : ExprVisitor(recursive), optimized(_optimized) {}
+};
+} // namespace klee
+
+#endif /* KLEE_ARRAYEXPRVISITOR_H */
diff --git a/include/klee/Expr/AssignmentGenerator.h b/include/klee/Expr/AssignmentGenerator.h
new file mode 100644
index 00000000..173b863e
--- /dev/null
+++ b/include/klee/Expr/AssignmentGenerator.h
@@ -0,0 +1,59 @@
+//===-- AssignmentGenerator.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_ASSIGNMENTGENERATOR_H
+#define KLEE_ASSIGNMENTGENERATOR_H
+
+#include "klee/Expr/Expr.h"
+#include "klee/util/Ref.h"
+
+#include <vector>
+
+namespace klee {
+class Assignment;
+} /* namespace klee */
+
+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);
+};
+} // namespace klee
+
+#endif /* KLEE_ASSIGNMENTGENERATOR_H */