1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
//===-- 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 */
|
