1 //===-- ArrayExprOptimizer.h ----------------------------------------------===// 2 // 3 // The KLEE Symbolic Virtual Machine 4 // 5 // This file is distributed under the University of Illinois Open Source 6 // License. See LICENSE.TXT for details. 7 // 8 //===----------------------------------------------------------------------===// 9 10 #ifndef KLEE_ARRAYEXPROPTIMIZER_H 11 #define KLEE_ARRAYEXPROPTIMIZER_H 12 13 #include <cstdint> 14 #include <map> 15 #include <unordered_map> 16 #include <unordered_set> 17 #include <utility> 18 #include <vector> 19 20 #include "klee/ADT/Ref.h" 21 #include "klee/Expr/Expr.h" 22 #include "klee/Expr/ExprHashMap.h" 23 24 namespace klee { 25 26 enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE }; 27 28 using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>; 29 using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>; 30 31 class ExprOptimizer { 32 private: 33 ExprHashMap<ref<Expr>> cacheExprOptimized; 34 ExprHashSet cacheExprUnapplicable; 35 ExprHashMap<ref<Expr>> cacheReadExprOptimized; 36 37 public: 38 /// Returns the optimised version of e. 39 /// @param e expression to optimise 40 /// @param valueOnly XXX document 41 /// @return optimised expression 42 ref<Expr> optimizeExpr(const ref<Expr> &e, bool valueOnly); 43 44 private: 45 bool computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, 46 mapIndexOptimizedExpr_ty &idx_valIdx) const; 47 48 ref<Expr> getSelectOptExpr( 49 const ref<Expr> &e, std::vector<const ReadExpr *> &reads, 50 std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &readInfo, 51 bool isSymbolic); 52 53 ref<Expr> buildConstantSelectExpr(const ref<Expr> &index, 54 std::vector<uint64_t> &arrayValues, 55 Expr::Width width, 56 unsigned elementsInArray) const; 57 58 ref<Expr> 59 buildMixedSelectExpr(const ReadExpr *re, 60 std::vector<std::pair<uint64_t, bool>> &arrayValues, 61 Expr::Width width, unsigned elementsInArray) const; 62 }; 63 } // namespace klee 64 65 #endif /* KLEE_ARRAYEXPROPTIMIZER_H */ 66