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
130
131
132
133
134
135
136
137
138
139
140
141
142
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/ExprBuilder.h"
#include "klee/SolverCmdLine.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:
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<unsigned, Expr::Width>> &readInfo;
bool symbolic;
bool incompatible;
Action inspectRead(unsigned 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<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 &) override;
Action visitRead(const ReadExpr &re) override;
public:
explicit ArrayValueOptReplaceVisitor(
std::map<unsigned, ref<Expr>> &_optimized, bool recursive = true)
: ExprVisitor(recursive), optimized(_optimized) {}
};
class IndexCleanerVisitor : public ExprVisitor {
private:
bool mul{true};
ref<Expr> index;
protected:
Action visitMul(const MulExpr &) override;
Action visitRead(const ReadExpr &) override;
public:
IndexCleanerVisitor() : ExprVisitor(true) {}
inline ref<Expr> getIndex() { return index; }
};
} // namespace klee
#endif
|
