 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
74.5% |
41 / 55 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
92.7% |
51 / 55 |
| |
|
Line Coverage: |
88.0% |
81 / 92 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 : //===- CachingSolver.cpp - Caching expression solver ----------------------===//
3 :
4 : #include "klee/Solver.h"
5 :
6 : #include "klee/Constraints.h"
7 : #include "klee/Expr.h"
8 : #include "klee/IncompleteSolver.h"
9 : #include "klee/SolverImpl.h"
10 :
11 : #include "SolverStats.h"
12 :
13 : #include <tr1/unordered_map>
14 :
15 : using namespace klee;
16 :
17 : class CachingSolver : public SolverImpl {
18 : private:
19 : ref<Expr> canonicalizeQuery(ref<Expr> originalQuery,
20 : bool &negationUsed);
21 :
22 : void cacheInsert(const Query& query,
23 : IncompleteSolver::PartialValidity result);
24 :
25 : bool cacheLookup(const Query& query,
26 : IncompleteSolver::PartialValidity &result);
27 :
28 32738: struct CacheEntry {
29 : CacheEntry(const ConstraintManager &c, ref<Expr> q)
30 5655: : constraints(c), query(q) {}
31 :
32 10714: CacheEntry(const CacheEntry &ce)
33 21428: : constraints(ce.constraints), query(ce.query) {}
34 :
35 : ConstraintManager constraints;
36 : ref<Expr> query;
37 :
38 : bool operator==(const CacheEntry &b) const {
1344: branch 0 taken
2822: branch 1 taken
373: branch 4 taken
971: branch 5 taken
39 9676: return constraints==b.constraints && *query.get()==*b.query.get();
40 : }
41 : };
42 :
43 : struct CacheEntryHash {
44 8977: unsigned operator()(const CacheEntry &ce) const {
45 17954: unsigned result = ce.query.hash();
46 :
27541: branch 0 taken
8977: branch 1 taken
47 90990: for (ConstraintManager::constraint_iterator it = ce.constraints.begin();
48 : it != ce.constraints.end(); ++it)
49 27541: result ^= it->hash();
50 :
51 8977: return result;
52 : }
53 : };
54 :
55 : typedef std::tr1::unordered_map<CacheEntry,
56 : IncompleteSolver::PartialValidity,
57 : CacheEntryHash> cache_map;
58 :
59 : Solver *solver;
60 : cache_map cache;
61 :
62 : public:
63 312: CachingSolver(Solver *s) : solver(s) {}
104: branch 1 taken
0: branch 2 not taken
104: branch 7 taken
0: branch 8 not taken
0: branch 11 not taken
0: branch 12 not taken
0: branch 17 not taken
0: branch 18 not taken
64 104: ~CachingSolver() { cache.clear(); delete solver; }
65 :
66 : bool computeValidity(const Query&, Solver::Validity &result);
67 : bool computeTruth(const Query&, bool &isValid);
68 166: bool computeValue(const Query& query, ref<Expr> &result) {
69 166: return solver->impl->computeValue(query, result);
70 : }
71 : bool computeInitialValues(const Query& query,
72 : const std::vector<const MemoryObject*> &objects,
73 : std::vector< std::vector<unsigned char> > &values,
74 634: bool &hasSolution) {
75 : return solver->impl->computeInitialValues(query, objects, values,
76 634: hasSolution);
77 : }
78 : };
79 :
80 : /** @returns the canonical version of the given query. The reference
81 : negationUsed is set to true if the original query was negated in
82 : the canonicalization process. */
83 : ref<Expr> CachingSolver::canonicalizeQuery(ref<Expr> originalQuery,
84 5655: bool &negationUsed) {
85 5655: ref<Expr> negatedQuery = Expr::createNot(originalQuery);
86 :
87 : // select the "smaller" query to the be canonical representation
2951: branch 1 taken
2704: branch 2 taken
88 5655: if (originalQuery.compare(negatedQuery) < 0) {
89 2951: negationUsed = false;
90 2951: return originalQuery;
91 : } else {
92 2704: negationUsed = true;
93 2704: return negatedQuery;
94 5655: }
95 : }
96 :
97 : /** @returns true on a cache hit, false of a cache miss. Reference
98 : value result only valid on a cache hit. */
99 : bool CachingSolver::cacheLookup(const Query& query,
100 2964: IncompleteSolver::PartialValidity &result) {
101 : bool negationUsed;
102 5928: ref<Expr> canonicalQuery = canonicalizeQuery(query.expr, negationUsed);
103 :
104 5928: CacheEntry ce(query.constraints, canonicalQuery);
105 2964: cache_map::iterator it = cache.find(ce);
106 :
323: branch 0 taken
2641: branch 1 taken
107 5928: if (it != cache.end()) {
108 : result = (negationUsed ?
109 : IncompleteSolver::negatePartialValidity(it->second) :
229: branch 0 taken
94: branch 1 taken
110 646: it->second);
111 323: return true;
112 : }
113 :
114 2641: return false;
115 : }
116 :
117 : /// Inserts the given query, result pair into the cache.
118 : void CachingSolver::cacheInsert(const Query& query,
119 2691: IncompleteSolver::PartialValidity result) {
120 : bool negationUsed;
121 5382: ref<Expr> canonicalQuery = canonicalizeQuery(query.expr, negationUsed);
122 :
123 5382: CacheEntry ce(query.constraints, canonicalQuery);
124 : IncompleteSolver::PartialValidity cachedResult =
1258: branch 0 taken
1433: branch 1 taken
125 2691: (negationUsed ? IncompleteSolver::negatePartialValidity(result) : result);
126 :
127 10764: cache.insert(std::make_pair(ce, cachedResult));
128 2691: }
129 :
130 : bool CachingSolver::computeValidity(const Query& query,
131 736: Solver::Validity &result) {
132 : IncompleteSolver::PartialValidity cachedResult;
133 736: bool tmp, cacheHit = cacheLookup(query, cachedResult);
134 :
89: branch 0 taken
647: branch 1 taken
135 736: if (cacheHit) {
136 : ++stats::queryCacheHits;
137 :
20: branch 0 taken
20: branch 1 taken
43: branch 2 taken
1: branch 3 taken
5: branch 4 taken
0: branch 5 not taken
138 89: switch(cachedResult) {
139 : case IncompleteSolver::MustBeTrue:
140 20: result = Solver::True;
141 20: return true;
142 : case IncompleteSolver::MustBeFalse:
143 20: result = Solver::False;
144 20: return true;
145 : case IncompleteSolver::TrueOrFalse:
146 43: result = Solver::Unknown;
147 43: return true;
148 : case IncompleteSolver::MayBeTrue: {
0: branch 1 not taken
1: branch 2 taken
149 1: if (!solver->impl->computeTruth(query, tmp))
150 0: return false;
1: branch 0 taken
0: branch 1 not taken
151 1: if (tmp) {
152 1: cacheInsert(query, IncompleteSolver::MustBeTrue);
153 1: result = Solver::True;
154 1: return true;
155 : } else {
156 0: cacheInsert(query, IncompleteSolver::TrueOrFalse);
157 0: result = Solver::Unknown;
158 0: return true;
159 : }
160 : }
161 : case IncompleteSolver::MayBeFalse: {
0: branch 1 not taken
5: branch 2 taken
162 15: if (!solver->impl->computeTruth(query.negateExpr(), tmp))
163 0: return false;
0: branch 0 not taken
5: branch 1 taken
164 5: if (tmp) {
165 0: cacheInsert(query, IncompleteSolver::MustBeFalse);
166 0: result = Solver::False;
167 0: return true;
168 : } else {
169 5: cacheInsert(query, IncompleteSolver::TrueOrFalse);
170 5: result = Solver::Unknown;
171 5: return true;
172 : }
173 : }
174 0: default: assert(0 && "unreachable");
175 : }
176 : }
177 :
178 : ++stats::queryCacheMisses;
179 :
0: branch 1 not taken
647: branch 2 taken
180 647: if (!solver->impl->computeValidity(query, result))
181 0: return false;
182 :
41: branch 0 taken
88: branch 1 taken
518: branch 2 taken
183 647: switch (result) {
184 : case Solver::True:
185 41: cachedResult = IncompleteSolver::MustBeTrue; break;
186 : case Solver::False:
187 88: cachedResult = IncompleteSolver::MustBeFalse; break;
188 : default:
189 518: cachedResult = IncompleteSolver::TrueOrFalse; break;
190 : }
191 :
192 647: cacheInsert(query, cachedResult);
193 647: return true;
194 : }
195 :
196 : bool CachingSolver::computeTruth(const Query& query,
197 2228: bool &isValid) {
198 : IncompleteSolver::PartialValidity cachedResult;
199 2228: bool cacheHit = cacheLookup(query, cachedResult);
200 :
201 : // a cached result of MayBeTrue forces us to check whether
202 : // a False assignment exists.
234: branch 0 taken
1994: branch 1 taken
190: branch 2 taken
44: branch 3 taken
203 2228: if (cacheHit && cachedResult != IncompleteSolver::MayBeTrue) {
204 : ++stats::queryCacheHits;
205 190: isValid = (cachedResult == IncompleteSolver::MustBeTrue);
206 190: return true;
207 : }
208 :
209 : ++stats::queryCacheMisses;
210 :
211 : // cache miss: query solver
0: branch 1 not taken
2038: branch 2 taken
212 2038: if (!solver->impl->computeTruth(query, isValid))
213 0: return false;
214 :
1544: branch 0 taken
494: branch 1 taken
215 2038: if (isValid) {
216 1544: cachedResult = IncompleteSolver::MustBeTrue;
34: branch 0 taken
460: branch 1 taken
217 494: } else if (cacheHit) {
218 : // We know a true assignment exists, and query isn't valid, so
219 : // must be TrueOrFalse.
0: branch 0 not taken
34: branch 1 taken
220 34: assert(cachedResult == IncompleteSolver::MayBeTrue);
221 34: cachedResult = IncompleteSolver::TrueOrFalse;
222 : } else {
223 460: cachedResult = IncompleteSolver::MayBeFalse;
224 : }
225 :
226 2038: cacheInsert(query, cachedResult);
227 2038: return true;
228 : }
229 :
230 : ///
231 :
232 104: Solver *klee::createCachingSolver(Solver *_solver) {
233 312: return new Solver(new CachingSolver(_solver));
234 : }
Generated: 2009-05-17 22:47 by zcov