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

10 files changed, 18 insertions, 317 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index a3e84486..74965625 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -9,9 +9,9 @@
 
 #include "Executor.h"
 
-#include "../Expr/ArrayExprOptimizer.h"
 #include "Context.h"
 #include "CoreStats.h"
+#include "ExecutionState.h"
 #include "ExternalDispatcher.h"
 #include "ImpliedValue.h"
 #include "Memory.h"
@@ -26,7 +26,8 @@
 
 #include "klee/Common.h"
 #include "klee/Config/Version.h"
-#include "klee/ExecutionState.h"
+#include "klee/Core/Interpreter.h"
+#include "klee/Expr/ArrayExprOptimizer.h"
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprPPrinter.h"
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 374dd30b..cd6b173a 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -17,6 +17,7 @@
 
 #include "klee/ExecutionState.h"
 #include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/ArrayExprOptimizer.h"
 #include "klee/Module/Cell.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -26,8 +27,6 @@
 #include "llvm/ADT/Twine.h"
 #include "llvm/Support/raw_ostream.h"
 
-#include "../Expr/ArrayExprOptimizer.h"
-
 #include <map>
 #include <memory>
 #include <set>
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index c3be0690..6e10461f 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -7,16 +7,16 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "ArrayExprOptimizer.h"
-#include "ArrayExprRewriter.h"
-#include "ArrayExprVisitor.h"
-#include "AssignmentGenerator.h"
+#include "klee/Expr/ArrayExprOptimizer.h"
 
 #include "klee/Config/Version.h"
+#include "klee/Expr/ArrayExprRewriter.h"
+#include "klee/Expr/ArrayExprVisitor.h"
 #include "klee/Expr/Assignment.h"
+#include "klee/Expr/AssignmentGenerator.h"
 #include "klee/Expr/ExprBuilder.h"
-#include "klee/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
+#include "klee/Support/ErrorHandling.h"
 #include "klee/util/BitArray.h"
 
 #include <llvm/ADT/APInt.h>
diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h
deleted file mode 100644
index 8fc040e5..00000000
--- a/lib/Expr/ArrayExprOptimizer.h
+++ /dev/null
@@ -1,65 +0,0 @@
-//===-- 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/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp
index 8306e20a..32851679 100644
--- a/lib/Expr/ArrayExprRewriter.cpp
+++ b/lib/Expr/ArrayExprRewriter.cpp
@@ -7,18 +7,19 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "ArrayExprRewriter.h"
+#include "klee/Expr/ArrayExprRewriter.h"
+
+#include "klee/Expr/ArrayExprVisitor.h"
+#include "klee/util/BitArray.h"
 
-#include <cassert>
-#include <cstdint>
 #include <llvm/ADT/APInt.h>
 #include <llvm/Support/Casting.h>
+
+#include <cassert>
+#include <cstdint>
 #include <set>
 #include <utility>
 
-#include "ArrayExprVisitor.h"
-#include "klee/util/BitArray.h"
-
 using namespace klee;
 
 ref<Expr>
diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h
deleted file mode 100644
index 098cb0a6..00000000
--- a/lib/Expr/ArrayExprRewriter.h
+++ /dev/null
@@ -1,47 +0,0 @@
-//===-- 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/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index dd82c4d6..d3119754 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "ArrayExprVisitor.h"
+#include "klee/Expr/ArrayExprVisitor.h"
 
 #include "klee/Support/ErrorHandling.h"
 
diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h
deleted file mode 100644
index 28f485d9..00000000
--- a/lib/Expr/ArrayExprVisitor.h
+++ /dev/null
@@ -1,129 +0,0 @@
-//===-- 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/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp
index 0301b702..e7d2eb61 100644
--- a/lib/Expr/AssignmentGenerator.cpp
+++ b/lib/Expr/AssignmentGenerator.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "AssignmentGenerator.h"
+#include "klee/Expr/AssignmentGenerator.h"
 
 #include "klee/Expr/Assignment.h"
 #include "klee/Support/ErrorHandling.h"
diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h
deleted file mode 100644
index 173b863e..00000000
--- a/lib/Expr/AssignmentGenerator.h
+++ /dev/null
@@ -1,59 +0,0 @@
-//===-- 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 */