about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/ArrayExprOptimizer.h69
-rw-r--r--include/klee/ArrayExprRewriter.h47
-rw-r--r--include/klee/AssignmentGenerator.h59
-rw-r--r--include/klee/util/ArrayExprVisitor.h143
4 files changed, 0 insertions, 318 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h
deleted file mode 100644
index aafe1d27..00000000
--- a/include/klee/ArrayExprOptimizer.h
+++ /dev/null
@@ -1,69 +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_EXPROPTIMIZER_H
-#define KLEE_EXPROPTIMIZER_H
-
-#include <cstdint>
-#include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <utility>
-#include <vector>
-
-#include "Expr.h"
-#include "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;
-};
-}
-
-#endif
diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h
deleted file mode 100644
index 2b6c78b4..00000000
--- a/include/klee/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 LIB_EXPRREWRITER_H_
-#define LIB_EXPRREWRITER_H_
-
-#include <iterator>
-#include <map>
-#include <vector>
-
-#include "Expr.h"
-#include "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);
-};
-}
-
-#endif /* LIB_EXPRREWRITER_H_ */
diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h
deleted file mode 100644
index 404c8632..00000000
--- a/include/klee/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 <vector>
-
-#include "Expr.h"
-#include "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);
-};
-}
-
-#endif
diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h
deleted file mode 100644
index d8c64c2d..00000000
--- a/include/klee/util/ArrayExprVisitor.h
+++ /dev/null
@@ -1,143 +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/util/ExprVisitor.h"
-#include "klee/ExprBuilder.h"
-#include "klee/CommandLine.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; }
-};
-}
-
-#endif
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 10:09:26 +0000