about summary refs log tree commit diff homepage
path: root/lib/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp8
-rw-r--r--lib/Expr/ArrayExprOptimizer.h64
-rw-r--r--lib/Expr/ArrayExprRewriter.cpp4
-rw-r--r--lib/Expr/ArrayExprRewriter.h47
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp2
-rw-r--r--lib/Expr/ArrayExprVisitor.h143
-rw-r--r--lib/Expr/AssignmentGenerator.cpp2
-rw-r--r--lib/Expr/AssignmentGenerator.h59
8 files changed, 321 insertions, 8 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index dc0b2002..63a9fb96 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/ArrayExprOptimizer.h"
+#include "ArrayExprOptimizer.h"
 
 #include <algorithm>
 #include <cassert>
@@ -17,12 +17,12 @@
 #include <set>
 #include <stddef.h>
 
-#include "klee/ArrayExprRewriter.h"
-#include "klee/AssignmentGenerator.h"
+#include "ArrayExprRewriter.h"
+#include "ArrayExprVisitor.h"
+#include "AssignmentGenerator.h"
 #include "klee/Config/Version.h"
 #include "klee/ExprBuilder.h"
 #include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/util/ArrayExprVisitor.h"
 #include "klee/util/Assignment.h"
 #include "klee/util/BitArray.h"
 
diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h
new file mode 100644
index 00000000..7d895a48
--- /dev/null
+++ b/lib/Expr/ArrayExprOptimizer.h
@@ -0,0 +1,64 @@
+//===-- 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_EXPROPTIMIZER_H
+#define KLEE_EXPROPTIMIZER_H
+
+#include <cstdint>
+#include <map>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+#include "klee/Expr.h"
+#include "klee/util/Ref.h"
+
+namespace klee {
+
+enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE };
+
+typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
+typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
+
+class ExprOptimizer {
+private:
+  std::unordered_map<unsigned, ref<Expr>> cacheExprOptimized;
+  std::unordered_set<unsigned> cacheExprUnapplicable;
+  std::unordered_map<unsigned, 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<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;
+};
+} // namespace klee
+
+#endif
diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp
index 26aef1ff..507ea753 100644
--- a/lib/Expr/ArrayExprRewriter.cpp
+++ b/lib/Expr/ArrayExprRewriter.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/ArrayExprRewriter.h"
+#include "ArrayExprRewriter.h"
 
 #include <cassert>
 #include <cstdint>
@@ -16,7 +16,7 @@
 #include <set>
 #include <utility>
 
-#include "klee/util/ArrayExprVisitor.h"
+#include "ArrayExprVisitor.h"
 #include "klee/util/BitArray.h"
 
 using namespace klee;
diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h
new file mode 100644
index 00000000..310ae8dd
--- /dev/null
+++ b/lib/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 LIB_EXPRREWRITER_H_
+#define LIB_EXPRREWRITER_H_
+
+#include <iterator>
+#include <map>
+#include <vector>
+
+#include "klee/Expr.h"
+#include "klee/util/Ref.h"
+
+namespace klee {
+
+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 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 /* LIB_EXPRREWRITER_H_ */
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index dae4c451..407c4c64 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/util/ArrayExprVisitor.h"
+#include "ArrayExprVisitor.h"
 
 #include "klee/Internal/Support/ErrorHandling.h"
 
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
diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp
index a906f796..87b75820 100644
--- a/lib/Expr/AssignmentGenerator.cpp
+++ b/lib/Expr/AssignmentGenerator.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "../../include/klee/AssignmentGenerator.h"
+#include "AssignmentGenerator.h"
 
 #include <cassert>
 #include <cstdint>
diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h
new file mode 100644
index 00000000..fea1168a
--- /dev/null
+++ b/lib/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 <vector>
+
+#include "klee/Expr.h"
+#include "klee/util/Ref.h"
+
+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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-10 21:53:12 +0000