 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
61.6% |
69 / 112 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
73.2% |
82 / 112 |
| |
|
Line Coverage: |
82.2% |
97 / 118 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Solver.h"
4 :
5 : #include "klee/Constraints.h"
6 : #include "klee/Expr.h"
7 : // FIXME: This should not be here.
8 : #include "klee/Memory.h"
9 : #include "klee/SolverImpl.h"
10 : #include "klee/TimerStatIncrementer.h"
11 : #include "klee/util/Assignment.h"
12 : #include "klee/util/ExprUtil.h"
13 : #include "klee/util/ExprVisitor.h"
14 : #include "klee/Internal/ADT/MapOfSets.h"
15 :
16 : #include "SolverStats.h"
17 :
18 : #include "llvm/Support/CommandLine.h"
19 :
20 : using namespace klee;
21 : using namespace llvm;
22 :
23 : namespace {
24 : cl::opt<bool>
25 104: DebugCexCacheCheckBinding("debug-cex-cache-check-binding");
26 :
27 : cl::opt<bool>
28 104: CexCacheTryAll("cex-cache-try-all",
29 : cl::desc("try substituting all counterexamples before asking STP"),
30 104: cl::init(false));
31 :
32 : cl::opt<bool>
33 208: CexCacheExperimental("cex-cache-exp", cl::init(false));
34 :
35 : }
36 :
37 : ///
38 :
39 : typedef std::set< ref<Expr> > KeyType;
40 :
41 : struct AssignmentLessThan {
42 8597: bool operator()(const Assignment *a, const Assignment *b) {
43 17194: return a->bindings < b->bindings;
44 : }
45 : };
46 :
47 :
48 : class CexCachingSolver : public SolverImpl {
49 : typedef std::set<Assignment*, AssignmentLessThan> assignmentsTable_ty;
50 :
51 : Solver *solver;
52 :
53 : MapOfSets<ref<Expr>, Assignment*> cache;
54 : // memo table
55 : assignmentsTable_ty assignmentsTable;
56 :
57 : bool searchForAssignment(KeyType &key,
58 : Assignment *&result);
59 :
60 : bool lookupAssignment(const Query& query, Assignment *&result);
61 :
62 : bool getAssignment(const Query& query, Assignment *&result);
63 :
64 : public:
65 312: CexCachingSolver(Solver *_solver) : solver(_solver) {}
66 : ~CexCachingSolver();
67 :
68 : bool computeTruth(const Query&, bool &isValid);
69 : bool computeValidity(const Query&, Solver::Validity &result);
70 : bool computeValue(const Query&, ref<Expr> &result);
71 : bool computeInitialValues(const Query&,
72 : const std::vector<const MemoryObject*> &objects,
73 : std::vector< std::vector<unsigned char> > &values,
74 : bool &hasSolution);
75 : };
76 :
77 : #if 0
78 : static llvm::OStream &operator<<(llvm::OStream &os, const KeyType &a) {
79 : os << "{";
80 : foreach(it, a.begin(), a.end()) {
81 : if (it!=a.begin())
82 : os << ", ";
83 : os << *it;
84 : }
85 : os << "}";
86 : return os;
87 : }
88 :
89 : static llvm::OStream &operator<<(llvm::OStream &os, const Assignment &a) {
90 : os << "{";
91 : foreach(it, a.bindings.begin(), a.bindings.end()) {
92 : if (it!=a.bindings.begin())
93 : os << ", ";
94 : const MemoryObject *mo = it->first;
95 : os << "MO" << mo->id << " : ";
96 : os << "[";
97 : foreach(valIt, it->second.begin(), it->second.end()) {
98 : if (valIt!=it->second.begin())
99 : os << ",";
100 : os << (unsigned) *valIt;
101 : }
102 : os << "]";
103 : }
104 : os << "}";
105 : return os;
106 : }
107 : #endif
108 :
109 : ///
110 :
111 : struct NullAssignment {
112 96: bool operator()(Assignment *a) const { return !a; }
113 : };
114 :
115 : struct NonNullAssignment {
116 441: bool operator()(Assignment *a) const { return a!=0; }
117 : };
118 :
119 : struct NullOrSatisfyingAssignment {
120 : KeyType &key;
121 :
122 3401: NullOrSatisfyingAssignment(KeyType &_key) : key(_key) {}
123 :
124 : bool operator()(Assignment *a) const {
5833: branch 0 taken
41: branch 1 taken
491: branch 3 taken
5342: branch 4 taken
125 17540: return !a || a->satisfies(key.begin(), key.end());
126 : }
127 : };
128 :
129 4138: bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
130 8276: Assignment * const *lookup = cache.lookup(key);
532: branch 0 taken
3606: branch 1 taken
131 4138: if (lookup) {
132 532: result = *lookup;
133 532: return true;
134 : }
135 :
56: branch 0 taken
3550: branch 1 taken
136 3606: if (CexCacheTryAll) {
137 112: Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
44: branch 0 taken
12: branch 1 taken
138 100: if (!lookup) lookup = cache.findSubset(key, NullAssignment());
12: branch 0 taken
44: branch 1 taken
139 56: if (lookup) {
140 12: result = *lookup;
141 12: return true;
142 : }
373: branch 0 taken
30: branch 1 taken
143 447: for (assignmentsTable_ty::iterator it = assignmentsTable.begin(),
144 44: ie = assignmentsTable.end(); it != ie; ++it) {
145 373: Assignment *a = *it;
14: branch 1 taken
359: branch 2 taken
146 373: if (a->satisfies(key.begin(), key.end())) {
147 14: result = a;
148 14: return true;
149 : }
150 : }
151 : } else {
152 : // XXX which order? one is sure to be better
153 7100: Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
3401: branch 0 taken
149: branch 1 taken
154 10352: if (!lookup) lookup = cache.findSubset(key, NullOrSatisfyingAssignment(key));
681: branch 0 taken
2869: branch 1 taken
155 3550: if (lookup) {
156 681: result = *lookup;
157 681: return true;
158 : }
159 : }
160 :
161 2899: return false;
162 : }
163 :
164 : bool CexCachingSolver::lookupAssignment(const Query &query,
165 0: Assignment *&result) {
166 0: KeyType key(query.constraints.begin(), query.constraints.end());
167 0: ref<Expr> neg = Expr::createNot(query.expr);
0: branch 1 not taken
0: branch 2 not taken
168 0: if (neg.isConstant()) {
0: branch 0 not taken
0: branch 1 not taken
169 0: if (!neg.getConstantValue()) {
170 0: result = (Assignment*) 0;
171 0: return true;
172 : }
173 : } else {
174 : key.insert(neg);
175 : }
176 :
177 0: return searchForAssignment(key, result);
178 : }
179 :
180 4138: bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
181 12414: KeyType key(query.constraints.begin(), query.constraints.end());
182 8276: ref<Expr> neg = Expr::createNot(query.expr);
1447: branch 1 taken
2691: branch 2 taken
183 4138: if (neg.isConstant()) {
0: branch 0 not taken
1447: branch 1 taken
184 1447: if (!neg.getConstantValue()) {
185 0: result = (Assignment*) 0;
186 0: return true;
187 : }
188 : } else {
189 : key.insert(neg);
190 : }
191 :
2899: branch 1 taken
1239: branch 2 taken
192 4138: if (!searchForAssignment(key, result)) {
193 : // need to solve
194 :
195 : std::vector<const MemoryObject*> objects;
196 2899: findSymbolicObjects(key.begin(), key.end(), objects);
197 :
198 : std::vector< std::vector<unsigned char> > values;
199 : bool hasSolution;
0: branch 1 not taken
2899: branch 2 taken
200 2899: if (!solver->impl->computeInitialValues(query, objects, values,
201 : hasSolution))
202 0: return false;
203 :
204 : Assignment *binding;
1324: branch 0 taken
1575: branch 1 taken
205 2899: if (hasSolution) {
206 2648: binding = new Assignment(objects, values);
207 :
208 : // memoization
209 : std::pair<assignmentsTable_ty::iterator, bool>
210 1324: res = assignmentsTable.insert(binding);
137: branch 0 taken
1187: branch 1 taken
211 1324: if (!res.second) {
137: branch 0 taken
0: branch 1 not taken
212 274: delete binding;
213 137: binding = *res.first;
214 : }
215 :
0: branch 0 not taken
1324: branch 1 taken
216 1324: if (DebugCexCacheCheckBinding)
0: branch 1 not taken
0: branch 2 not taken
217 0: assert(binding->satisfies(key.begin(), key.end()));
218 : } else {
219 1575: binding = (Assignment*) 0;
220 : }
221 :
222 2899: result = binding;
223 2899: cache.insert(key, binding);
224 : }
225 :
226 4138: return true;
227 : }
228 :
229 : ///
230 :
231 104: CexCachingSolver::~CexCachingSolver() {
232 104: cache.clear();
104: branch 0 taken
0: branch 1 not taken
104: branch 4 taken
104: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
233 104: delete solver;
1187: branch 0 taken
104: branch 1 taken
104: branch 2 taken
104: branch 3 taken
104: branch 4 taken
104: branch 5 taken
234 1395: for (assignmentsTable_ty::iterator it = assignmentsTable.begin(),
235 104: ie = assignmentsTable.end(); it != ie; ++it)
1187: branch 0 taken
0: branch 1 not taken
1187: branch 3 taken
1187: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
236 2374: delete *it;
104: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
237 312: }
238 :
239 : bool CexCachingSolver::computeValidity(const Query& query,
240 647: Solver::Validity &result) {
241 : TimerStatIncrementer t(stats::cexCacheTime);
242 : Assignment *a;
0: branch 2 not taken
647: branch 3 taken
243 1294: if (!getAssignment(query.withFalse(), a))
244 0: return false;
0: branch 0 not taken
647: branch 1 taken
245 647: assert(a && "computeValidity() must have assignment");
246 1294: ref<Expr> q = a->evaluate(query.expr);
0: branch 1 not taken
647: branch 2 taken
247 647: assert(q.isConstant() && "assignment evaluation did not result in constant");
248 :
382: branch 0 taken
265: branch 1 taken
249 647: if (q.getConstantValue()) {
0: branch 1 not taken
382: branch 2 taken
250 382: if (!getAssignment(query, a))
251 0: return false;
41: branch 0 taken
341: branch 1 taken
252 382: result = !a ? Solver::True : Solver::Unknown;
253 : } else {
0: branch 2 not taken
265: branch 3 taken
254 530: if (!getAssignment(query.negateExpr(), a))
255 0: return false;
88: branch 0 taken
177: branch 1 taken
256 265: result = !a ? Solver::False : Solver::Unknown;
257 : }
258 :
259 647: return true;
260 : }
261 :
262 : bool CexCachingSolver::computeTruth(const Query& query,
263 2044: bool &isValid) {
264 : TimerStatIncrementer t(stats::cexCacheTime);
265 :
266 : // There is a small amount of redundancy here. We only need to know
267 : // truth and do not really need to compute an assignment. This means
268 : // that we could check the cache to see if we already know that
269 : // state ^ query has no assignment. In that case, by the validity of
270 : // state, we know that state ^ !query must have an assignment, and
271 : // so query cannot be true (valid). This does get hits, but doesn't
272 : // really seem to be worth the overhead.
273 :
0: branch 0 not taken
2044: branch 1 taken
274 2044: if (CexCacheExperimental) {
275 : Assignment *a;
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 9 not taken
276 0: if (lookupAssignment(query.negateExpr(), a) && !a)
277 0: return false;
278 : }
279 :
280 : Assignment *a;
0: branch 1 not taken
2044: branch 2 taken
281 2044: if (!getAssignment(query, a))
282 0: return false;
283 :
284 2044: isValid = !a;
285 :
286 2044: return true;
287 : }
288 :
289 : bool CexCachingSolver::computeValue(const Query& query,
290 166: ref<Expr> &result) {
291 : TimerStatIncrementer t(stats::cexCacheTime);
292 :
293 : Assignment *a;
0: branch 2 not taken
166: branch 3 taken
294 332: if (!getAssignment(query.withFalse(), a))
295 0: return false;
0: branch 0 not taken
166: branch 1 taken
296 166: assert(a && "computeValue() must have assignment");
297 498: result = a->evaluate(query.expr);
298 : assert(result.isConstant() &&
0: branch 1 not taken
166: branch 2 taken
299 166: "assignment evaluation did not result in constant");
300 166: return true;
301 : }
302 :
303 : bool
304 : CexCachingSolver::computeInitialValues(const Query& query,
305 : const std::vector<const MemoryObject*>
306 : &objects,
307 : std::vector< std::vector<unsigned char> >
308 : &values,
309 634: bool &hasSolution) {
310 : TimerStatIncrementer t(stats::cexCacheTime);
311 : Assignment *a;
0: branch 1 not taken
634: branch 2 taken
312 634: if (!getAssignment(query, a))
313 0: return false;
314 634: hasSolution = !!a;
315 :
0: branch 0 not taken
634: branch 1 taken
316 634: if (!a)
317 0: return true;
318 :
319 : // FIXME: We should use smarter assignment for result so we don't
320 : // need redundant copy.
321 634: values = std::vector< std::vector<unsigned char> >(objects.size());
845: branch 0 taken
634: branch 1 taken
322 2958: for (unsigned i=0; i < objects.size(); ++i) {
323 845: const MemoryObject *os = objects[i];
324 845: Assignment::bindings_ty::iterator it = a->bindings.find(os);
325 :
241: branch 0 taken
604: branch 1 taken
326 1690: if (it == a->bindings.end()) {
327 482: values[i] = std::vector<unsigned char>(os->size, 0);
328 : } else {
329 1208: values[i] = it->second;
330 : }
331 : }
332 :
333 634: return true;
334 : }
335 :
336 : ///
337 :
338 104: Solver *klee::createCexCachingSolver(Solver *_solver) {
339 312: return new Solver(new CexCachingSolver(_solver));
104: branch 0 taken
0: branch 1 not taken
104: branch 2 taken
0: branch 3 not taken
340 312: }
Generated: 2009-05-17 22:47 by zcov