 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
72.9% |
51 / 70 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
80.0% |
56 / 70 |
| |
|
Line Coverage: |
83.2% |
84 / 101 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Solver.h"
4 :
5 : #include "klee/Expr.h"
6 : #include "klee/Constraints.h"
7 : // FIXME: This should not be here.
8 : #include "klee/Memory.h"
9 : #include "klee/SolverImpl.h"
10 :
11 : #include "klee/util/ExprUtil.h"
12 :
13 : #include "llvm/Support/Streams.h"
14 :
15 : #include "klee/Internal/FIXME/sugar.h"
16 :
17 : #include <map>
18 : #include <vector>
19 :
20 : using namespace klee;
21 : using namespace llvm;
22 :
23 : template<class T>
24 329042: class DenseSet {
25 : std::set<T> s;
26 :
27 : public:
28 20615: DenseSet() {}
29 :
30 : void add(T x) {
31 50331: s.insert(x);
32 : }
33 : void add(T start, T end) {
34 : for (; start<end; start++)
35 : s.insert(start);
36 : }
37 :
38 : // returns true iff set is changed by addition
39 : bool add(const DenseSet &b) {
40 11005: bool modified = false;
27154: branch 0 taken
11005: branch 1 taken
41 60169: foreach(it, b.s.begin(), b.s.end()) {
27152: branch 0 taken
2: branch 1 taken
2: branch 2 taken
27150: branch 3 taken
4: branch 4 taken
27150: branch 5 taken
42 81458: if (modified || !s.count(*it)) {
43 4: modified = true;
44 4: s.insert(*it);
45 : }
46 : }
47 11005: return modified;
48 : }
49 :
50 : bool intersects(const DenseSet &b) {
19554: branch 0 taken
4659: branch 1 taken
51 55529: foreach(it, s.begin(), s.end())
10999: branch 0 taken
8555: branch 1 taken
52 39108: if (b.s.count(*it))
53 10999: return true;
54 4659: return false;
55 : }
56 :
57 : void print(std::ostream &os) const {
58 : bool first = true;
59 : os << "{";
60 : foreach(it, s.begin(), s.end()) {
61 : if (first) {
62 : first = false;
63 : } else {
64 : os << ",";
65 : }
66 : os << *it;
67 : }
68 : os << "}";
69 : }
70 : };
71 :
72 : template<class T>
73 : inline std::ostream &operator<<(std::ostream &os, const DenseSet<T> &dis) {
74 : dis.print(os);
75 : return os;
76 : }
77 :
78 243657: class IndependentElementSet {
79 : std::map<const MemoryObject*, DenseSet<unsigned> > elements;
80 : std::set<const MemoryObject*> wholeObjects;
81 :
82 : public:
83 : IndependentElementSet() {}
84 39316: IndependentElementSet(ref<Expr> e) {
85 : std::vector< ref<ReadExpr> > reads;
86 19658: findReads(e, /* visitUpdates= */ true, reads);
58531: branch 0 taken
19658: branch 1 taken
87 97847: foreach(it, reads.begin(), reads.end()) {
88 58531: ReadExpr *re = it->get();
50335: branch 0 taken
8196: branch 1 taken
89 58531: if (re->updates.isRooted) {
90 50335: const MemoryObject *mo = re->updates.root;
50332: branch 1 taken
3: branch 2 taken
91 50335: if (!wholeObjects.count(mo)) {
50331: branch 0 taken
1: branch 1 taken
92 100664: if (re->index.isConstant()) {
93 100662: DenseSet<unsigned> &dis = elements[mo];
94 100662: dis.add((unsigned) re->index.getConstantValue());
95 : } else {
96 1: let(it2, elements.find(mo));
0: branch 0 not taken
1: branch 1 taken
97 2: if (it2!=elements.end())
98 0: elements.erase(it2);
99 1: wholeObjects.insert(mo);
100 : }
101 : }
102 : }
103 : }
104 19658: }
105 61561: IndependentElementSet(const IndependentElementSet &ies) :
106 : elements(ies.elements),
107 184683: wholeObjects(ies.wholeObjects) {}
108 :
109 : IndependentElementSet &operator=(const IndependentElementSet &ies) {
110 0: elements = ies.elements;
111 0: wholeObjects = ies.wholeObjects;
112 0: return *this;
113 : }
114 :
115 : void print(std::ostream &os) const {
116 : os << "{";
117 : bool first = true;
118 : foreach(it, wholeObjects.begin(), wholeObjects.end()) {
119 : const MemoryObject *mo = *it;
120 :
121 : if (first) {
122 : first = false;
123 : } else {
124 : os << ", ";
125 : }
126 :
127 : os << "MO" << mo->id;
128 : }
129 : foreach(it, elements.begin(), elements.end()) {
130 : const MemoryObject *mo = it->first;
131 : const DenseSet<unsigned> &dis = it->second;
132 :
133 : if (first) {
134 : first = false;
135 : } else {
136 : os << ", ";
137 : }
138 :
139 : os << "MO" << mo->id << " : " << dis;
140 : }
141 : os << "}";
142 : }
143 :
144 : // more efficient when this is the smaller set
145 : bool intersects(const IndependentElementSet &b) {
0: branch 0 not taken
16533: branch 1 taken
146 49599: foreach(it, wholeObjects.begin(), wholeObjects.end()) {
147 0: const MemoryObject *mo = *it;
0: branch 1 not taken
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
148 0: if (b.wholeObjects.count(mo) || b.elements.find(mo)!=b.elements.end())
149 0: return true;
150 : }
16535: branch 0 taken
5534: branch 1 taken
151 55135: foreach(it, elements.begin(), elements.end()) {
152 16535: const MemoryObject *mo = it->first;
0: branch 1 not taken
16535: branch 2 taken
153 16535: if (b.wholeObjects.count(mo))
154 0: return true;
155 16535: let(it2, b.elements.find(mo));
15658: branch 0 taken
877: branch 1 taken
156 33070: if (it2!=b.elements.end()) {
10999: branch 0 taken
4659: branch 1 taken
157 46974: if (it->second.intersects(it2->second))
158 10999: return true;
159 : }
160 : }
161 5534: return false;
162 : }
163 :
164 : // returns true iff set is changed by addition
165 : bool add(const IndependentElementSet &b) {
166 10999: bool modified = false;
0: branch 0 not taken
10999: branch 1 taken
167 32997: foreach(it, b.wholeObjects.begin(), b.wholeObjects.end()) {
168 0: const MemoryObject *mo = *it;
169 0: let(it2, elements.find(mo));
0: branch 0 not taken
0: branch 1 not taken
170 0: if (it2!=elements.end()) {
171 0: modified = true;
172 0: elements.erase(it2);
173 0: wholeObjects.insert(mo);
174 : } else {
0: branch 1 not taken
0: branch 2 not taken
175 0: if (!wholeObjects.count(mo)) {
176 0: modified = true;
177 0: wholeObjects.insert(mo);
178 : }
179 : }
180 : }
11007: branch 0 taken
10999: branch 1 taken
181 44004: foreach(it, b.elements.begin(), b.elements.end()) {
182 11007: const MemoryObject *mo = it->first;
11007: branch 1 taken
0: branch 2 not taken
183 11007: if (!wholeObjects.count(mo)) {
184 11007: let(it2, elements.find(mo));
2: branch 0 taken
11005: branch 1 taken
185 22014: if (it2==elements.end()) {
186 2: modified = true;
187 2: elements.insert(*it);
188 : } else {
2: branch 0 taken
11003: branch 1 taken
189 33015: if (it2->second.add(it->second))
190 2: modified = true;
191 : }
192 : }
193 : }
194 10999: return modified;
195 : }
196 : };
197 :
198 : inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) {
199 : ies.print(os);
200 : return os;
201 : }
202 :
203 : static
204 : IndependentElementSet getIndependentConstraints(const Query& query,
205 3130: std::vector< ref<Expr> > &result) {
206 6260: IndependentElementSet eltsClosure(query.expr);
207 : std::vector< std::pair<ref<Expr>, IndependentElementSet> > worklist;
208 :
16528: branch 0 taken
3130: branch 1 taken
209 25918: foreach(it, query.constraints.begin(), query.constraints.end())
210 33056: worklist.push_back(std::make_pair(*it, IndependentElementSet(*it)));
211 :
212 : // XXX This should be more efficient (in terms of low level copy stuff).
213 3130: bool done = false;
2: branch 0 taken
3130: branch 1 taken
214 3132: do {
215 3132: done = true;
216 : std::vector< std::pair<ref<Expr>, IndependentElementSet> > newWorklist;
16533: branch 0 taken
3132: branch 1 taken
217 22797: foreach(it, worklist.begin(), worklist.end()) {
10999: branch 0 taken
5534: branch 1 taken
218 49599: if (it->second.intersects(eltsClosure)) {
4: branch 0 taken
10995: branch 1 taken
219 21998: if (eltsClosure.add(it->second))
220 4: done = false;
221 10999: result.push_back(it->first);
222 : } else {
223 5534: newWorklist.push_back(*it);
224 : }
225 : }
226 3132: worklist.swap(newWorklist);
227 : } while (!done);
228 :
229 : if (0) {
230 : std::set< ref<Expr> > reqset(result.begin(), result.end());
231 : llvm::cerr << "--\n";
232 : llvm::cerr << "Q: " << query.expr << "\n";
233 : llvm::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n";
234 : int i = 0;
235 : foreach(it, query.constraints.begin(), query.constraints.end()) {
236 : llvm::cerr << "C" << i++ << ": " << *it;
237 : llvm::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
238 : llvm::cerr << "\telts: " << IndependentElementSet(*it) << "\n";
239 : }
240 : llvm::cerr << "elts closure: " << eltsClosure << "\n";
241 : }
242 :
243 3130: return eltsClosure;
244 : }
245 :
246 : class IndependentSolver : public SolverImpl {
247 : private:
248 : Solver *solver;
249 :
250 : public:
251 : IndependentSolver(Solver *_solver)
252 208: : solver(_solver) {}
104: branch 0 taken
0: branch 1 not taken
104: branch 5 taken
0: branch 6 not taken
104: branch 8 taken
104: branch 9 taken
0: branch 13 not taken
0: branch 14 not taken
253 104: ~IndependentSolver() { delete solver; }
254 :
255 : bool computeTruth(const Query&, bool &isValid);
256 : bool computeValidity(const Query&, Solver::Validity &result);
257 : bool computeValue(const Query&, ref<Expr> &result);
258 : bool computeInitialValues(const Query& query,
259 : const std::vector<const MemoryObject*> &objects,
260 : std::vector< std::vector<unsigned char> > &values,
261 634: bool &hasSolution) {
262 : return solver->impl->computeInitialValues(query, objects, values,
263 634: hasSolution);
264 : }
265 : };
266 :
267 : bool IndependentSolver::computeValidity(const Query& query,
268 736: Solver::Validity &result) {
269 : std::vector< ref<Expr> > required;
270 : IndependentElementSet eltsClosure =
271 736: getIndependentConstraints(query, required);
272 736: ConstraintManager tmp(required);
273 : return solver->impl->computeValidity(Query(tmp, query.expr),
274 2944: result);
275 : }
276 :
277 2228: bool IndependentSolver::computeTruth(const Query& query, bool &isValid) {
278 : std::vector< ref<Expr> > required;
279 : IndependentElementSet eltsClosure =
280 2228: getIndependentConstraints(query, required);
281 2228: ConstraintManager tmp(required);
282 : return solver->impl->computeTruth(Query(tmp, query.expr),
283 8912: isValid);
284 : }
285 :
286 166: bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
287 : std::vector< ref<Expr> > required;
288 : IndependentElementSet eltsClosure =
289 166: getIndependentConstraints(query, required);
290 166: ConstraintManager tmp(required);
291 664: return solver->impl->computeValue(Query(tmp, query.expr), result);
292 : }
293 :
294 104: Solver *klee::createIndependentSolver(Solver *s) {
295 312: return new Solver(new IndependentSolver(s));
296 : }
Generated: 2009-05-17 22:47 by zcov