diff options
Diffstat (limited to 'lib/Expr/ArrayExprOptimizer.h')
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.h | 65 |
1 files changed, 0 insertions, 65 deletions
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 */ |