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
|
#include "klee/ArrayExprOptimizer.h"
#include "klee/ArrayExprRewriter.h"
#include "klee/util/BitArray.h"
#include <iostream>
using namespace klee;
namespace klee {
llvm::cl::opt<ArrayOptimizationType> OptimizeArray(
"optimize-array",
llvm::cl::values(
clEnumValN(INDEX, "index", "Index-based transformation"),
clEnumValEnd),
llvm::cl::init(NONE),
llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic "
"arrays. (default=off)"));
};
void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
bool valueOnly) {
unsigned hash = e->hash();
if (cacheExprUnapplicable.find(hash) != cacheExprUnapplicable.end()) {
return;
}
// Find cached expressions
auto cached = cacheExprOptimized.find(hash);
if (cached != cacheExprOptimized.end()) {
result = cached->second;
return;
}
// ----------------------- INDEX-BASED OPTIMIZATION -------------------------
if (!valueOnly && OptimizeArray == INDEX) {
array2idx_ty arrays;
ConstantArrayExprVisitor aev(arrays);
aev.visit(e);
if (arrays.size() == 0 || aev.isIncompatible()) {
// We do not optimize expressions other than those with concrete
// arrays with a symbolic index
// If we cannot optimize the expression, we return a failure only
// when we are not combining the optimizations
if (OptimizeArray == INDEX) {
cacheExprUnapplicable.insert(hash);
return;
}
} else {
mapIndexOptimizedExpr_ty idx_valIdx;
// Compute those indexes s.t. orig_expr =equisat= (k==i|k==j|..)
if (computeIndexes(arrays, e, idx_valIdx)) {
if (idx_valIdx.size() > 0) {
// Create new expression on indexes
result = ExprRewriter::createOptExpr(e, arrays, idx_valIdx);
} else {
klee_warning("OPT_I: infeasible branch!");
result = ConstantExpr::create(0, Expr::Bool);
}
// Add new expression to cache
if (result.get()) {
klee_warning("OPT_I: successful");
cacheExprOptimized[hash] = result;
} else {
klee_warning("OPT_I: unsuccessful");
}
} else {
klee_warning("OPT_I: unsuccessful");
cacheExprUnapplicable.insert(hash);
}
}
}
}
bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
mapIndexOptimizedExpr_ty &idx_valIdx) const {
bool success = false;
// For each constant array found
for (auto &element : arrays) {
const Array *arr = element.first;
assert(arr->isConstantArray() && "Array is not concrete");
assert(element.second.size() == 1 && "Multiple indexes on the same array");
IndexTransformationExprVisitor idxt_v(arr);
idxt_v.visit(e);
assert((idxt_v.getWidth() % arr->range == 0) && "Read is not aligned");
Expr::Width width = idxt_v.getWidth() / arr->range;
if (idxt_v.getMul().get()) {
// If we have a MulExpr in the index, we can optimize our search by
// skipping all those indexes that are not multiple of such value.
// In fact, they will be rejected by the MulExpr interpreter since it
// will not find any integer solution
Expr &e = *idxt_v.getMul();
ConstantExpr &ce = static_cast<ConstantExpr &>(e);
uint64_t mulVal = (*ce.getAPValue().getRawData());
// So far we try to limit this optimization, but we may try some more
// aggressive conditions (i.e. mulVal > width)
if (width == 1 && mulVal > 1)
width = mulVal;
}
// For each concrete value 'i' stored in the array
for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) {
Assignment *a = new Assignment();
v_arr_ty objects;
std::vector<std::vector<unsigned char> > values;
// For each symbolic index Expr(k) found
for (auto &index_it : element.second) {
ref<Expr> idx = index_it;
ref<Expr> val = ConstantExpr::alloc(aIdx, arr->getDomain());
// We create a partial assignment on 'k' s.t. Expr(k)==i
bool assignmentSuccess =
AssignmentGenerator::generatePartialAssignment(idx, val, a);
success |= assignmentSuccess;
// If the assignment satisfies both the expression 'e' and the PC
ref<Expr> evaluation = a->evaluate(e);
if (assignmentSuccess && evaluation->isTrue()) {
if (idx_valIdx.find(idx) == idx_valIdx.end()) {
idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr> >()));
}
idx_valIdx[idx]
.push_back(ConstantExpr::alloc(aIdx, arr->getDomain()));
}
}
delete a;
}
}
return success;
}
|
