 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
56.3% |
196 / 348 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
67.2% |
234 / 348 |
| |
|
Line Coverage: |
69.5% |
237 / 341 |
| |
 |
|
 |
1 : #include "klee/Solver.h"
2 :
3 : #include "klee/Constraints.h"
4 : #include "klee/Expr.h"
5 : #include "klee/IncompleteSolver.h"
6 : // FIXME: This should not be here.
7 : #include "klee/Memory.h"
8 : #include "klee/util/ExprEvaluator.h"
9 : #include "klee/util/ExprRangeEvaluator.h"
10 : #include "klee/util/ExprVisitor.h"
11 : // FIXME: Use APInt.
12 : #include "klee/Internal/Support/IntEvaluation.h"
13 :
14 : #include "klee/Internal/FIXME/sugar.h"
15 :
16 : #include <iostream>
17 : #include <sstream>
18 : #include <cassert>
19 : #include <map>
20 : #include <vector>
21 :
22 : using namespace klee;
23 :
24 : /***/
25 :
26 : //#define LOG
27 : #ifdef LOG
28 : std::ostream *theLog;
29 : #endif
30 :
31 : // Hacker's Delight, pgs 58-63
32 : static uint64_t minOR(uint64_t a, uint64_t b,
33 : uint64_t c, uint64_t d) {
34 710: uint64_t temp, m = ((uint64_t) 1)<<63;
45440: branch 0 taken
710: branch 1 taken
35 46150: while (m) {
0: branch 0 not taken
45440: branch 1 taken
36 45440: if (~a & c & m) {
37 0: temp = (a | m) & -m;
0: branch 0 not taken
0: branch 1 not taken
38 0: if (temp <= b) { a = temp; break; }
0: branch 0 not taken
45440: branch 1 taken
39 45440: } else if (a & ~c & m) {
40 0: temp = (c | m) & -m;
0: branch 0 not taken
0: branch 1 not taken
41 0: if (temp <= d) { c = temp; break; }
42 : }
43 45440: m >>= 1;
44 : }
45 :
46 710: return a | c;
47 : }
48 : static uint64_t maxOR(uint64_t a, uint64_t b,
49 : uint64_t c, uint64_t d) {
50 710: uint64_t temp, m = ((uint64_t) 1)<<63;
51 :
45440: branch 0 taken
24: branch 1 taken
52 45464: while (m) {
686: branch 0 taken
44754: branch 1 taken
53 45440: if (b & d & m) {
54 686: temp = (b - m) | (m - 1);
686: branch 0 taken
0: branch 1 not taken
55 686: if (temp >= a) { b = temp; break; }
56 0: temp = (d - m) | (m -1);
0: branch 0 not taken
0: branch 1 not taken
57 0: if (temp >= c) { d = temp; break; }
58 : }
59 44754: m >>= 1;
60 : }
61 :
62 710: return b | d;
63 : }
64 : static uint64_t minAND(uint64_t a, uint64_t b,
65 : uint64_t c, uint64_t d) {
66 428: uint64_t temp, m = ((uint64_t) 1)<<63;
27392: branch 0 taken
0: branch 1 not taken
67 27392: while (m) {
27392: branch 0 taken
0: branch 1 not taken
68 27392: if (~a & ~c & m) {
69 27392: temp = (a | m) & -m;
428: branch 0 taken
26964: branch 1 taken
70 27392: if (temp <= b) { a = temp; break; }
71 26964: temp = (c | m) & -m;
0: branch 0 not taken
26964: branch 1 taken
72 26964: if (temp <= d) { c = temp; break; }
73 : }
74 26964: m >>= 1;
75 : }
76 :
77 428: return a & c;
78 : }
79 : static uint64_t maxAND(uint64_t a, uint64_t b,
80 : uint64_t c, uint64_t d) {
81 428: uint64_t temp, m = ((uint64_t) 1)<<63;
27392: branch 0 taken
428: branch 1 taken
82 27820: while (m) {
0: branch 0 not taken
27392: branch 1 taken
83 27392: if (b & ~d & m) {
84 0: temp = (b & ~m) | (m - 1);
0: branch 0 not taken
0: branch 1 not taken
85 0: if (temp >= a) { b = temp; break; }
0: branch 0 not taken
27392: branch 1 taken
86 27392: } else if (~b & d & m) {
87 0: temp = (d & ~m) | (m - 1);
0: branch 0 not taken
0: branch 1 not taken
88 0: if (temp >= c) { d = temp; break; }
89 : }
90 27392: m >>= 1;
91 : }
92 :
93 428: return b & d;
94 : }
95 :
96 : ///
97 :
98 : class ValueRange {
99 : private:
100 : uint64_t m_min, m_max;
101 :
102 : public:
103 28413: ValueRange() : m_min(1),m_max(0) {}
104 31978: ValueRange(uint64_t value) : m_min(value), m_max(value) {}
105 48045: ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {}
106 3903: ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {}
107 :
108 : void print(std::ostream &os) const {
109 : if (isFixed()) {
110 : os << m_min;
111 : } else {
112 : os << "[" << m_min << "," << m_max << "]";
113 : }
114 : }
115 :
116 : bool isEmpty() const {
117 97739: return m_min>m_max;
118 : }
119 : bool contains(uint64_t value) const {
120 : return this->intersects(ValueRange(value));
121 : }
122 : bool intersects(const ValueRange &b) const {
123 2654: return !this->set_intersection(b).isEmpty();
124 : }
125 :
126 : bool isFullRange(unsigned bits) {
24: branch 0 taken
48: branch 1 taken
24: branch 2 taken
0: branch 3 not taken
127 96: return m_min==0 && m_max==bits64::maxValueOfNBits(bits);
128 : }
129 :
130 : ValueRange set_intersection(const ValueRange &b) const {
131 12801: return ValueRange(std::max(m_min,b.m_min), std::min(m_max,b.m_max));
132 : }
133 : ValueRange set_union(const ValueRange &b) const {
134 5943: return ValueRange(std::min(m_min,b.m_min), std::max(m_max,b.m_max));
135 : }
136 : ValueRange set_difference(const ValueRange &b) const {
0: branch 0 not taken
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
0: branch 7 not taken
137 0: if (b.isEmpty() || b.m_min > m_max || b.m_max < m_min) { // no intersection
138 0: return *this;
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
139 0: } else if (b.m_min <= m_min && b.m_max >= m_max) { // empty
140 0: return ValueRange(1,0);
0: branch 0 not taken
0: branch 1 not taken
141 0: } else if (b.m_min <= m_min) { // one range out
142 : // cannot overflow because b.m_max < m_max
143 0: return ValueRange(b.m_max+1, m_max);
0: branch 0 not taken
0: branch 1 not taken
144 0: } else if (b.m_max >= m_max) {
145 : // cannot overflow because b.min > m_min
146 0: return ValueRange(m_min, b.m_min-1);
147 : } else {
148 : // two ranges, take bottom
149 0: return ValueRange(m_min, b.m_min-1);
150 : }
151 : }
152 428: ValueRange binaryAnd(const ValueRange &b) const {
153 : // XXX
428: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
428: branch 3 taken
154 856: assert(!isEmpty() && !b.isEmpty() && "XXX");
0: branch 0 not taken
428: branch 1 taken
428: branch 2 taken
428: branch 3 taken
0: branch 4 not taken
428: branch 5 taken
155 428: if (isFixed() && b.isFixed()) {
156 0: return ValueRange(m_min & b.m_min);
157 : } else {
158 : return ValueRange(minAND(m_min, m_max, b.m_min, b.m_max),
159 1284: maxAND(m_min, m_max, b.m_min, b.m_max));
160 : }
161 : }
162 0: ValueRange binaryAnd(uint64_t b) const { return binaryAnd(ValueRange(b)); }
163 710: ValueRange binaryOr(ValueRange b) const {
164 : // XXX
710: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
710: branch 3 taken
165 1420: assert(!isEmpty() && !b.isEmpty() && "XXX");
12: branch 0 taken
698: branch 1 taken
0: branch 2 not taken
12: branch 3 taken
0: branch 4 not taken
710: branch 5 taken
166 722: if (isFixed() && b.isFixed()) {
167 0: return ValueRange(m_min | b.m_min);
168 : } else {
169 : return ValueRange(minOR(m_min, m_max, b.m_min, b.m_max),
170 2130: maxOR(m_min, m_max, b.m_min, b.m_max));
171 : }
172 : }
173 : ValueRange binaryOr(uint64_t b) const { return binaryOr(ValueRange(b)); }
174 : ValueRange binaryXor(ValueRange b) const {
0: branch 0 not taken
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
175 0: if (isFixed() && b.isFixed()) {
176 0: return ValueRange(m_min ^ b.m_min);
177 : } else {
178 0: uint64_t t = m_max | b.m_max;
0: branch 0 not taken
0: branch 1 not taken
179 0: while (!bits64::isPowerOfTwo(t))
180 0: t = bits64::withoutRightmostBit(t);
181 0: return ValueRange(0, (t<<1)-1);
182 : }
183 : }
184 :
185 : ValueRange binaryShiftLeft(unsigned bits) const {
186 24: return ValueRange(m_min<<bits, m_max<<bits);
187 : }
188 : ValueRange binaryShiftRight(unsigned bits) const {
189 0: return ValueRange(m_min>>bits, m_max>>bits);
190 : }
191 :
192 : ValueRange concat(const ValueRange &b, unsigned bits) const {
193 48: return binaryShiftLeft(bits).binaryOr(b);
194 : }
195 0: ValueRange extract(uint64_t lowBit, uint64_t maxBit) const {
196 0: return binaryShiftRight(lowBit).binaryAnd(bits64::maxValueOfNBits(maxBit-lowBit));
197 : }
198 :
199 : ValueRange add(const ValueRange &b, unsigned width) const {
200 356: return ValueRange(0, bits64::maxValueOfNBits(width));
201 : }
202 : ValueRange sub(const ValueRange &b, unsigned width) const {
203 72: return ValueRange(0, bits64::maxValueOfNBits(width));
204 : }
205 : ValueRange mul(const ValueRange &b, unsigned width) const {
206 25: return ValueRange(0, bits64::maxValueOfNBits(width));
207 : }
208 : ValueRange udiv(const ValueRange &b, unsigned width) const {
209 0: return ValueRange(0, bits64::maxValueOfNBits(width));
210 : }
211 : ValueRange sdiv(const ValueRange &b, unsigned width) const {
212 2: return ValueRange(0, bits64::maxValueOfNBits(width));
213 : }
214 : ValueRange urem(const ValueRange &b, unsigned width) const {
215 0: return ValueRange(0, bits64::maxValueOfNBits(width));
216 : }
217 : ValueRange srem(const ValueRange &b, unsigned width) const {
218 0: return ValueRange(0, bits64::maxValueOfNBits(width));
219 : }
220 :
221 : // use min() to get value if true (XXX should we add a method to
222 : // make code clearer?)
223 12961: bool isFixed() const { return m_min==m_max; }
224 :
225 : bool operator==(const ValueRange &b) const { return m_min==b.m_min && m_max==b.m_max; }
226 : bool operator!=(const ValueRange &b) const { return !(*this==b); }
227 :
873: branch 0 taken
873: branch 1 taken
873: branch 2 taken
873: branch 3 taken
873: branch 4 taken
873: branch 5 taken
873: branch 6 taken
873: branch 7 taken
0: branch 8 not taken
31: branch 9 taken
31: branch 10 taken
31: branch 11 taken
0: branch 12 not taken
31: branch 13 taken
31: branch 14 taken
31: branch 15 taken
0: branch 16 not taken
31: branch 17 taken
31: branch 18 taken
31: branch 19 taken
0: branch 20 not taken
69: branch 21 taken
69: branch 22 taken
69: branch 23 taken
0: branch 24 not taken
69: branch 25 taken
69: branch 26 taken
69: branch 27 taken
0: branch 28 not taken
214: branch 29 taken
214: branch 30 taken
214: branch 31 taken
0: branch 32 not taken
214: branch 33 taken
214: branch 34 taken
214: branch 35 taken
0: branch 36 not taken
214: branch 37 taken
214: branch 38 taken
214: branch 39 taken
214: branch 40 taken
214: branch 41 taken
214: branch 42 taken
214: branch 43 taken
214: branch 44 taken
214: branch 45 taken
214: branch 46 taken
214: branch 47 taken
228 873: bool mustEqual(const uint64_t b) const { return m_min==m_max && m_min==b; }
229 : bool mayEqual(const uint64_t b) const { return m_min<=b && m_max>=b; }
230 :
2582: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
2582: branch 3 taken
2582: branch 4 taken
2582: branch 5 taken
72: branch 6 taken
0: branch 7 not taken
0: branch 8 not taken
72: branch 9 taken
72: branch 10 taken
72: branch 11 taken
231 5308: bool mustEqual(const ValueRange &b) const { return isFixed() && b.isFixed() && m_min==b.m_min; }
232 2654: bool mayEqual(const ValueRange &b) const { return this->intersects(b); }
233 :
234 62709: uint64_t min() const {
0: branch 0 not taken
62709: branch 1 taken
235 62709: assert(!isEmpty() && "cannot get minimum of empty range");
236 62709: return m_min;
237 : }
238 :
239 28488: uint64_t max() const {
0: branch 0 not taken
28488: branch 1 taken
240 28488: assert(!isEmpty() && "cannot get maximum of empty range");
241 28488: return m_max;
242 : }
243 :
244 4: int64_t minSigned(unsigned bits) const {
245 : assert((m_min>>bits)==0 && (m_max>>bits)==0 &&
4: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
4: branch 3 taken
246 4: "range is outside given number of bits");
247 :
248 : // if max allows sign bit to be set then it can be smallest value,
249 : // otherwise since the range is not empty, min cannot have a sign
250 : // bit
251 :
252 4: uint64_t smallest = ((uint64_t) 1 << (bits-1));
2: branch 0 taken
2: branch 1 taken
253 4: if (m_max >= smallest) {
254 2: return ints::sext(smallest, 64, bits);
255 : } else {
256 2: return m_min;
257 : }
258 : }
259 :
260 4: int64_t maxSigned(unsigned bits) const {
261 : assert((m_min>>bits)==0 && (m_max>>bits)==0 &&
4: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
4: branch 3 taken
262 4: "range is outside given number of bits");
263 :
264 4: uint64_t smallest = ((uint64_t) 1 << (bits-1));
265 :
266 : // if max and min have sign bit then max is max, otherwise if only
267 : // max has sign bit then max is largest signed integer, otherwise
268 : // max is max
269 :
4: branch 0 taken
0: branch 1 not taken
2: branch 2 taken
2: branch 3 taken
270 4: if (m_min < smallest && m_max >= smallest) {
271 2: return smallest - 1;
272 : } else {
273 4: return ints::sext(m_max, 64, bits);
274 : }
275 : }
276 : };
277 :
278 : inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) {
279 : vr.print(os);
280 : return os;
281 : }
282 :
283 : // used to find all memory object ids and the maximum size of any
284 : // object state that references them (for symbolic size).
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
371: branch 6 taken
285 1484: class ObjectFinder : public ExprVisitor {
286 : protected:
287 791: Action visitRead(const ReadExpr &re) {
288 791: addUpdates(re.updates);
289 791: return Action::doChildren();
290 : }
291 :
292 : // XXX nice if this information was cached somewhere, used by
293 : // independence as well right?
294 : void addUpdates(const UpdateList &ul) {
45620: branch 0 taken
791: branch 1 taken
295 46411: for (const UpdateNode *un=ul.head; un; un=un->next) {
296 45620: visit(un->index);
297 45620: visit(un->value);
298 : }
299 :
300 791: addObject(*ul.root);
301 : }
302 :
303 : public:
304 1161: void addObject(const MemoryObject &mo) {
305 1161: unsigned id = mo.id;
306 1161: std::map<unsigned,unsigned>::iterator it = results.find(id);
307 :
525: branch 0 taken
636: branch 1 taken
308 2322: if (it == results.end()) {
309 1050: results[id] = mo.size;
0: branch 0 not taken
636: branch 1 taken
310 1272: } else if (mo.size > it->second) {
311 0: it->second = mo.size;
312 : }
313 1161: }
314 :
315 : public:
316 : std::map<unsigned, unsigned> results;
317 : };
318 :
319 : // XXX waste of space, rather have ByteValueRange
320 : typedef ValueRange CexValueData;
321 :
322 : class CexObjectData {
323 : public:
324 : unsigned size;
325 : CexValueData *values;
326 :
327 : public:
26480: branch 1 taken
525: branch 2 taken
328 27005: CexObjectData(unsigned _size) : size(_size), values(new CexValueData[size]) {
26480: branch 0 taken
525: branch 1 taken
329 27005: for (unsigned i=0; i<size; i++)
330 52960: values[i] = ValueRange(0, 255);
331 : }
332 : };
333 :
3074: branch 0 taken
3074: branch 1 taken
0: branch 3 not taken
1537: branch 4 taken
334 3074: class CexRangeEvaluator : public ExprRangeEvaluator<ValueRange> {
335 : public:
336 : std::map<unsigned, CexObjectData> &objectValues;
337 : CexRangeEvaluator(std::map<unsigned, CexObjectData> &_objectValues)
338 3074: : objectValues(_objectValues) {}
339 :
340 1909: ValueRange getInitialReadRange(const MemoryObject &os, ValueRange index) {
341 1909: return ValueRange(0, 255);
342 : }
343 : };
344 :
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
1657: branch 6 taken
345 1657: class CexConstifier : public ExprEvaluator {
346 : protected:
347 1884: ref<Expr> getInitialValue(const MemoryObject &mo, unsigned index) {
348 1884: let(it, objectValues.find(mo.id));
0: branch 0 not taken
1884: branch 1 taken
349 3768: assert(it != objectValues.end() && "missing object?");
350 1884: CexObjectData &cod = it->second;
351 :
0: branch 0 not taken
1884: branch 1 taken
352 1884: if (index >= cod.size) {
353 0: return ReadExpr::create(UpdateList(&mo, true, 0), ref<Expr>(index, Expr::Int32));
354 : } else {
355 1884: CexValueData &cvd = cod.values[index];
0: branch 2 not taken
1884: branch 3 taken
356 1884: assert(cvd.min() == cvd.max() && "value is not fixed");
357 1884: return ref<Expr>(cvd.min(), Expr::Int8);
358 : }
359 : }
360 :
361 : public:
362 : std::map<unsigned, CexObjectData> &objectValues;
363 : CexConstifier(std::map<unsigned, CexObjectData> &_objectValues)
364 3314: : objectValues(_objectValues) {}
365 : };
366 :
367 : class CexData {
368 : public:
369 : std::map<unsigned, CexObjectData> objectValues;
370 :
371 : public:
372 371: CexData(ObjectFinder &finder) {
525: branch 0 taken
371: branch 1 taken
373 1638: foreach(it, finder.results.begin(), finder.results.end()) {
374 : objectValues.insert(std::pair<unsigned, CexObjectData>(it->first,
375 1575: CexObjectData(it->second)));
376 : }
377 371: }
378 371: ~CexData() {
525: branch 0 taken
371: branch 1 taken
379 1638: foreach(it, objectValues.begin(), objectValues.end()) {
525: branch 0 taken
0: branch 1 not taken
380 525: delete[] it->second.values;
381 : }
382 742: }
383 :
384 6238: void forceExprToValue(ref<Expr> e, uint64_t value) {
385 6238: forceExprToRange(e, CexValueData(value,value));
386 6238: }
387 :
388 8723: void forceExprToRange(ref<Expr> e, CexValueData range) {
389 : #ifdef LOG
390 : // *theLog << "force: " << e << " to " << range << "\n";
391 : #endif
1612: branch 0 taken
0: branch 1 not taken
508: branch 2 taken
1: branch 3 taken
0: branch 4 not taken
129: branch 5 taken
214: branch 6 taken
4879: branch 7 taken
16: branch 8 taken
316: branch 9 taken
0: branch 10 not taken
1048: branch 11 taken
392 8723: switch (e.getKind()) {
393 : case Expr::Constant: {
394 : // rather a pity if the constant isn't in the range, but how can
395 : // we use this?
396 : break;
397 : }
398 :
399 : // Special
400 :
401 : case Expr::NotOptimized: break;
402 :
403 : case Expr::Read: {
404 1612: ReadExpr *re = static_ref_cast<ReadExpr>(e);
405 1612: const MemoryObject *mo = re->updates.root;
406 3224: CexObjectData &cod = objectValues.find(mo->id)->second;
407 :
408 : // XXX we need to respect the version here and object state chain
409 :
1612: branch 1 taken
0: branch 2 not taken
1612: branch 3 taken
0: branch 4 not taken
1612: branch 5 taken
0: branch 6 not taken
410 3224: if (re->index.isConstant() && re->index.getConstantValue()<mo->size) {
411 3224: CexValueData &cvd = cod.values[re->index.getConstantValue()];
412 : CexValueData tmp = cvd.set_intersection(range);
413 :
326: branch 0 taken
1286: branch 1 taken
414 1612: if (tmp.isEmpty()) {
269: branch 0 taken
57: branch 1 taken
415 326: if (range.isFixed()) // ranges conflict, if new one is fixed use that
416 269: cvd = range;
417 : } else {
418 1286: cvd = tmp;
419 : }
420 : } else {
421 : // XXX fatal("XXX not implemented");
422 : }
423 :
424 : break;
425 : }
426 :
427 : case Expr::Select: {
428 0: SelectExpr *se = static_ref_cast<SelectExpr>(e);
429 0: ValueRange cond = evalRangeForExpr(se->cond);
0: branch 0 not taken
0: branch 1 not taken
430 0: if (cond.isFixed()) {
0: branch 1 not taken
0: branch 2 not taken
431 0: if (cond.min()) {
432 0: forceExprToRange(se->trueExpr, range);
433 : } else {
434 0: forceExprToRange(se->falseExpr, range);
435 : }
436 : } else {
437 : // XXX imprecise... we have a choice here. One method is to
438 : // simply force both sides into the specified range (since the
439 : // condition is indetermined). This may lose in two ways, the
440 : // first is that the condition chosen may limit further
441 : // restrict the range in each of the children, however this is
442 : // less of a problem as the range will be a superset of legal
443 : // values. The other is if the condition ends up being forced
444 : // by some other constraints, then we needlessly forced one
445 : // side into the given range.
446 : //
447 : // The other method would be to force the condition to one
448 : // side and force that side into the given range. This loses
449 : // when we force the condition to an unsatisfiable value
450 : // (either because the condition cannot be that, or the
451 : // resulting range given that condition is not in the required
452 : // range).
453 : //
454 : // Currently we just force both into the range. A hybrid would
455 : // be to evaluate the ranges for each of the children... if
456 : // one of the ranges happens to already be a subset of the
457 : // required range then it may be preferable to force the
458 : // condition to that side.
459 0: forceExprToRange(se->trueExpr, range);
460 0: forceExprToRange(se->falseExpr, range);
461 : }
462 : break;
463 : }
464 :
465 : // XXX imprecise... the problem here is that extracting bits
466 : // loses information about what bits are connected across the
467 : // bytes. if a value can be 1 or 256 then either the top or
468 : // lower byte is 0, but just extraction loses this information
469 : // and will allow neither,one,or both to be 1.
470 : //
471 : // we can protect against this in a limited fashion by writing
472 : // the extraction a byte at a time, then checking the evaluated
473 : // value, isolating for that range, and continuing.
474 : case Expr::Concat: {
475 508: ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
0: branch 0 not taken
508: branch 1 taken
476 508: if (ce->is2ByteConcat()) {
477 0: forceExprToRange(ce->getKid(0), range.extract( 8, 16));
478 0: forceExprToRange(ce->getKid(1), range.extract( 0, 8));
479 : }
0: branch 0 not taken
508: branch 1 taken
480 508: else if (ce->is4ByteConcat()) {
481 0: forceExprToRange(ce->getKid(0), range.extract(24, 32));
482 0: forceExprToRange(ce->getKid(1), range.extract(16, 24));
483 0: forceExprToRange(ce->getKid(2), range.extract( 8, 16));
484 0: forceExprToRange(ce->getKid(3), range.extract( 0, 8));
485 : }
0: branch 0 not taken
508: branch 1 taken
486 508: else if (ce->is8ByteConcat()) {
487 0: forceExprToRange(ce->getKid(0), range.extract(56, 64));
488 0: forceExprToRange(ce->getKid(1), range.extract(48, 56));
489 0: forceExprToRange(ce->getKid(2), range.extract(40, 48));
490 0: forceExprToRange(ce->getKid(3), range.extract(32, 40));
491 0: forceExprToRange(ce->getKid(4), range.extract(24, 32));
492 0: forceExprToRange(ce->getKid(5), range.extract(16, 24));
493 0: forceExprToRange(ce->getKid(6), range.extract( 8, 16));
494 0: forceExprToRange(ce->getKid(7), range.extract( 0, 8));
495 : }
496 :
497 : break;
498 : }
499 :
500 : case Expr::Extract: {
501 : // XXX
502 : break;
503 : }
504 :
505 : // Casting
506 :
507 : // Simply intersect the output range with the range of all
508 : // possible outputs and then truncate to the desired number of
509 : // bits.
510 :
511 : // For ZExt this simplifies to just intersection with the
512 : // possible input range.
513 : case Expr::ZExt: {
514 1: CastExpr *ce = static_ref_cast<CastExpr>(e);
515 1: unsigned inBits = ce->src.getWidth();
516 : ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits)));
517 2: forceExprToRange(ce->src, input);
518 1: break;
519 : }
520 : // For SExt instead of doing the intersection we just take the output range
521 : // minus the impossible values. This is nicer since it is a single interval.
522 : case Expr::SExt: {
523 0: CastExpr *ce = static_ref_cast<CastExpr>(e);
524 0: unsigned inBits = ce->src.getWidth();
525 0: unsigned outBits = ce->width;
526 : ValueRange output = range.set_difference(ValueRange(1<<(inBits-1),
527 : (bits64::maxValueOfNBits(outBits)-
528 0: bits64::maxValueOfNBits(inBits-1)-1)));
529 : ValueRange input = output.binaryAnd(bits64::maxValueOfNBits(inBits));
530 0: forceExprToRange(ce->src, input);
531 0: break;
532 : }
533 :
534 : // Binary
535 :
536 : case Expr::And: {
537 129: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
100: branch 1 taken
29: branch 2 taken
538 129: if (be->getWidth()==Expr::Bool) {
100: branch 0 taken
0: branch 1 not taken
539 100: if (range.isFixed()) {
540 100: ValueRange left = evalRangeForExpr(be->left);
541 100: ValueRange right = evalRangeForExpr(be->right);
542 :
31: branch 1 taken
69: branch 2 taken
543 100: if (!range.min()) {
31: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
31: branch 3 taken
31: branch 4 taken
0: branch 5 not taken
544 62: if (left.mustEqual(0) || right.mustEqual(0)) {
545 : // all is well
546 : } else {
547 : // XXX heuristic, which order
548 :
549 62: forceExprToValue(be->left, 0);
550 31: left = evalRangeForExpr(be->left);
551 :
552 : // see if that worked
31: branch 0 taken
0: branch 1 not taken
553 31: if (!left.mustEqual(1))
554 62: forceExprToValue(be->right, 0);
555 : }
556 : } else {
69: branch 0 taken
0: branch 1 not taken
557 138: if (!left.mustEqual(1)) forceExprToValue(be->left, 1);
69: branch 0 taken
0: branch 1 not taken
558 138: if (!right.mustEqual(1)) forceExprToValue(be->right, 1);
559 : }
560 : }
561 : } else {
562 : // XXX
563 : }
564 : break;
565 : }
566 :
567 : case Expr::Or: {
568 214: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
214: branch 1 taken
0: branch 2 not taken
569 214: if (be->getWidth()==Expr::Bool) {
214: branch 0 taken
0: branch 1 not taken
570 214: if (range.isFixed()) {
571 214: ValueRange left = evalRangeForExpr(be->left);
572 214: ValueRange right = evalRangeForExpr(be->right);
573 :
214: branch 1 taken
0: branch 2 not taken
574 214: if (range.min()) {
214: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
214: branch 3 taken
214: branch 4 taken
0: branch 5 not taken
575 428: if (left.mustEqual(1) || right.mustEqual(1)) {
576 : // all is well
577 : } else {
578 : // XXX heuristic, which order?
579 :
580 : // force left to value we need
581 428: forceExprToValue(be->left, 1);
582 214: left = evalRangeForExpr(be->left);
583 :
584 : // see if that worked
214: branch 0 taken
0: branch 1 not taken
585 214: if (!left.mustEqual(1))
586 428: forceExprToValue(be->right, 1);
587 : }
588 : } else {
0: branch 0 not taken
0: branch 1 not taken
589 0: if (!left.mustEqual(0)) forceExprToValue(be->left, 0);
0: branch 0 not taken
0: branch 1 not taken
590 0: if (!right.mustEqual(0)) forceExprToValue(be->right, 0);
591 : }
592 : }
593 : } else {
594 : // XXX
595 : }
596 : break;
597 : }
598 :
599 : case Expr::Xor: break;
600 :
601 : // Comparison
602 :
603 : case Expr::Eq: {
604 4879: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
4879: branch 0 taken
0: branch 1 not taken
605 4879: if (range.isFixed()) {
4879: branch 1 taken
0: branch 2 not taken
606 4879: if (be->left.isConstant()) {
607 9758: uint64_t value = be->left.getConstantValue();
2727: branch 1 taken
2152: branch 2 taken
608 4879: if (range.min()) {
609 5454: forceExprToValue(be->right, value);
610 : } else {
631: branch 0 taken
1521: branch 1 taken
611 2152: if (value==0) {
612 : forceExprToRange(be->right,
613 : CexValueData(1,
614 : ints::sext(1,
615 : be->right.getWidth(),
616 1893: 1)));
617 : } else {
618 : // XXX heuristic / lossy, could be better to pick larger range?
619 4563: forceExprToRange(be->right, CexValueData(0, value-1));
620 : }
621 : }
622 : } else {
623 : // XXX what now
624 : }
625 : }
626 : break;
627 : }
628 :
629 : case Expr::Ult: {
630 16: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
631 :
632 : // XXX heuristic / lossy, what order if conflict
633 :
16: branch 0 taken
0: branch 1 not taken
634 16: if (range.isFixed()) {
635 16: ValueRange left = evalRangeForExpr(be->left);
636 16: ValueRange right = evalRangeForExpr(be->right);
637 :
638 32: uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
639 :
640 : // XXX should deal with overflow (can lead to empty range)
641 :
12: branch 0 taken
4: branch 1 taken
642 16: if (left.isFixed()) {
8: branch 1 taken
4: branch 2 taken
643 12: if (range.min()) {
644 24: forceExprToRange(be->right, CexValueData(left.min()+1, maxValue));
645 : } else {
646 12: forceExprToRange(be->right, CexValueData(0, left.min()));
647 : }
4: branch 0 taken
0: branch 1 not taken
648 4: } else if (right.isFixed()) {
0: branch 1 not taken
4: branch 2 taken
649 4: if (range.min()) {
650 0: forceExprToRange(be->left, CexValueData(0, right.min()-1));
651 : } else {
652 12: forceExprToRange(be->left, CexValueData(right.min(), maxValue));
653 : }
654 : } else {
655 : // XXX ???
656 : }
657 : }
658 : break;
659 : }
660 : case Expr::Ule: {
661 316: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
662 :
663 : // XXX heuristic / lossy, what order if conflict
664 :
316: branch 0 taken
0: branch 1 not taken
665 316: if (range.isFixed()) {
666 316: ValueRange left = evalRangeForExpr(be->left);
667 316: ValueRange right = evalRangeForExpr(be->right);
668 :
669 : // XXX should deal with overflow (can lead to empty range)
670 :
671 632: uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
0: branch 0 not taken
316: branch 1 taken
672 316: if (left.isFixed()) {
0: branch 1 not taken
0: branch 2 not taken
673 0: if (range.min()) {
674 0: forceExprToRange(be->right, CexValueData(left.min(), maxValue));
675 : } else {
676 0: forceExprToRange(be->right, CexValueData(0, left.min()-1));
677 : }
316: branch 0 taken
0: branch 1 not taken
678 316: } else if (right.isFixed()) {
221: branch 1 taken
95: branch 2 taken
679 316: if (range.min()) {
680 663: forceExprToRange(be->left, CexValueData(0, right.min()));
681 : } else {
682 285: forceExprToRange(be->left, CexValueData(right.min()+1, maxValue));
683 : }
684 : } else {
685 : // XXX ???
686 : }
687 : }
688 : break;
689 : }
690 :
691 : case Expr::Ne:
692 : case Expr::Ugt:
693 : case Expr::Uge:
694 : case Expr::Sgt:
695 : case Expr::Sge:
696 0: assert(0 && "invalid expressions (uncanonicalized");
697 :
698 : default:
699 : break;
700 : }
701 8723: }
702 :
703 371: void fixValues() {
525: branch 0 taken
371: branch 1 taken
704 1638: foreach(it, objectValues.begin(), objectValues.end()) {
705 525: CexObjectData &cod = it->second;
26480: branch 0 taken
525: branch 1 taken
706 27005: for (unsigned i=0; i<cod.size; i++) {
707 26480: CexValueData &cvd = cod.values[i];
708 52960: cvd = CexValueData(cvd.min() + (cvd.max()-cvd.min())/2);
709 : }
710 : }
711 371: }
712 :
713 1537: ValueRange evalRangeForExpr(ref<Expr> &e) {
714 1537: CexRangeEvaluator ce(objectValues);
715 1537: return ce.evaluate(e);
716 : }
717 :
718 1480: bool exprMustBeValue(ref<Expr> e, uint64_t value) {
719 1480: CexConstifier cc(objectValues);
720 1480: ref<Expr> v = cc.visit(e);
0: branch 1 not taken
1480: branch 2 taken
721 1480: if (!v.isConstant()) return false;
722 : // XXX reenable once all reads and vars are fixed
723 : // assert(v.isConstant() && "not all values have been fixed");
724 1480: return v.getConstantValue()==value;
725 : }
726 : };
727 :
728 : /* *** */
729 :
730 :
731 : class FastCexSolver : public IncompleteSolver {
732 : public:
733 : FastCexSolver();
734 : ~FastCexSolver();
735 :
736 : IncompleteSolver::PartialValidity computeTruth(const Query&);
737 : bool computeValue(const Query&, ref<Expr> &result);
738 : bool computeInitialValues(const Query&,
739 : const std::vector<const MemoryObject*> &objects,
740 : std::vector< std::vector<unsigned char> > &values,
741 : bool &hasSolution);
742 : };
743 :
744 2: FastCexSolver::FastCexSolver() { }
745 :
1: branch 0 taken
0: branch 1 not taken
1: branch 3 taken
1: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
746 2: FastCexSolver::~FastCexSolver() { }
747 :
748 : IncompleteSolver::PartialValidity
749 0: FastCexSolver::computeTruth(const Query& query) {
750 : #ifdef LOG
751 : std::ostringstream log;
752 : theLog = &log;
753 : // log << "------ start FastCexSolver::mustBeTrue ------\n";
754 : log << "-- QUERY --\n";
755 : unsigned i=0;
756 : foreach(c, query.constraints.begin(), query.constraints.end())
757 : log << " C" << i++ << ": " << *c << ", \n";
758 : log << " Q : " << query.expr << "\n";
759 : #endif
760 :
761 0: ObjectFinder of;
0: branch 0 not taken
0: branch 1 not taken
762 0: foreach(c, query.constraints.begin(), query.constraints.end())
763 0: of.visit(*c);
764 0: of.visit(query.expr);
765 0: CexData cd(of);
766 :
0: branch 0 not taken
0: branch 1 not taken
767 0: foreach(c, query.constraints.begin(), query.constraints.end())
768 0: cd.forceExprToValue(*c, 1);
769 0: cd.forceExprToValue(query.expr, 0);
770 :
771 : #ifdef LOG
772 : log << " -- ranges --\n";
773 : foreach(it, cd.objectValues.begin(), cd.objectValues.end()) {
774 : CexObjectData &cod = it->second;
775 : log << " arr" << it->first << "[" << cod.size << "] = [";
776 : unsigned continueFrom=cod.size-1;
777 : for (; continueFrom>0; continueFrom--)
778 : if (cod.values[continueFrom-1]!=cod.values[continueFrom])
779 : break;
780 : for (unsigned i=0; i<cod.size; i++) {
781 : log << cod.values[i];
782 : if (i<cod.size-1) {
783 : log << ", ";
784 : if (i==continueFrom) {
785 : log << "...";
786 : break;
787 : }
788 : }
789 : }
790 : log << "]\n";
791 : }
792 : #endif
793 :
794 : // this could be done lazily of course
795 0: cd.fixValues();
796 :
797 : #ifdef LOG
798 : log << " -- fixed values --\n";
799 : foreach(it, cd.objectValues.begin(), cd.objectValues.end()) {
800 : CexObjectData &cod = it->second;
801 : log << " arr" << it->first << "[" << cod.size << "] = [";
802 : unsigned continueFrom=cod.size-1;
803 : for (; continueFrom>0; continueFrom--)
804 : if (cod.values[continueFrom-1]!=cod.values[continueFrom])
805 : break;
806 : for (unsigned i=0; i<cod.size; i++) {
807 : log << cod.values[i];
808 : if (i<cod.size-1) {
809 : log << ", ";
810 : if (i==continueFrom) {
811 : log << "...";
812 : break;
813 : }
814 : }
815 : }
816 : log << "]\n";
817 : }
818 : #endif
819 :
820 : // check the result
821 :
822 0: bool isGood = true;
823 :
0: branch 2 not taken
0: branch 3 not taken
824 0: if (!cd.exprMustBeValue(query.expr, 0)) isGood = false;
825 :
0: branch 0 not taken
0: branch 1 not taken
826 0: foreach(c, query.constraints.begin(), query.constraints.end())
0: branch 2 not taken
0: branch 3 not taken
827 0: if (!cd.exprMustBeValue(*c, 1)) isGood = false;
828 :
829 : #ifdef LOG
830 : log << " -- evaluating result --\n";
831 :
832 : i=0;
833 : foreach(c, query.constraints.begin(), query.constraints.end()) {
834 : bool res = cd.exprMustBeValue(*c, 1);
835 : log << " C" << i++ << ": " << (res?"true":"false") << "\n";
836 : }
837 : log << " Q : "
838 : << (cd.exprMustBeValue(query.expr, 0)?"true":"false") << "\n";
839 :
840 : log << "\n\n";
841 : #endif
842 :
0: branch 0 not taken
0: branch 1 not taken
843 0: return isGood ? IncompleteSolver::MayBeFalse : IncompleteSolver::None;
844 : }
845 :
846 0: bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) {
847 0: ObjectFinder of;
0: branch 0 not taken
0: branch 1 not taken
848 0: foreach(c, query.constraints.begin(), query.constraints.end())
849 0: of.visit(*c);
850 0: of.visit(query.expr);
851 0: CexData cd(of);
852 :
0: branch 0 not taken
0: branch 1 not taken
853 0: foreach(c, query.constraints.begin(), query.constraints.end())
854 0: cd.forceExprToValue(*c, 1);
855 :
856 : // this could be done lazily of course
857 0: cd.fixValues();
858 :
859 : // check the result
0: branch 0 not taken
0: branch 1 not taken
860 0: foreach(c, query.constraints.begin(), query.constraints.end())
0: branch 2 not taken
0: branch 3 not taken
861 0: if (!cd.exprMustBeValue(*c, 1))
862 0: return false;
863 :
864 : CexConstifier cc(cd.objectValues);
865 0: ref<Expr> value = cc.visit(query.expr);
866 :
0: branch 1 not taken
0: branch 2 not taken
867 0: if (value.isConstant()) {
868 : result = value;
869 0: return true;
870 : } else {
871 0: return false;
872 0: }
873 : }
874 :
875 : bool FastCexSolver::computeInitialValues(const Query& query,
876 : const std::vector<const MemoryObject*> &objects,
877 : std::vector< std::vector<unsigned char> > &values,
878 371: bool &hasSolution) {
879 371: ObjectFinder of;
2512: branch 0 taken
371: branch 1 taken
880 3625: foreach(c, query.constraints.begin(), query.constraints.end())
881 2512: of.visit(*c);
882 371: of.visit(query.expr);
370: branch 0 taken
371: branch 1 taken
883 741: foreach(it, objects.begin(), objects.end())
884 370: of.addObject(**it);
885 371: CexData cd(of);
886 :
2512: branch 0 taken
371: branch 1 taken
887 3625: foreach(c, query.constraints.begin(), query.constraints.end())
888 2512: cd.forceExprToValue(*c, 1);
889 742: cd.forceExprToValue(query.expr, 0);
890 :
891 : // this could be done lazily of course
892 371: cd.fixValues();
893 :
894 : // check the result
1269: branch 0 taken
211: branch 1 taken
895 2222: foreach(c, query.constraints.begin(), query.constraints.end())
160: branch 2 taken
1109: branch 3 taken
896 1269: if (!cd.exprMustBeValue(*c, 1))
897 160: return false;
34: branch 2 taken
177: branch 3 taken
898 422: if (!cd.exprMustBeValue(query.expr, 0))
899 34: return false;
900 :
901 177: hasSolution = true;
902 : CexConstifier cc(cd.objectValues);
176: branch 0 taken
177: branch 1 taken
903 353: foreach(it, objects.begin(), objects.end()) {
904 176: const MemoryObject *mo = *it;
905 : std::vector<unsigned char> data;
906 176: data.reserve(mo->size);
907 :
528: branch 2 taken
176: branch 3 taken
908 1408: for (unsigned i=0; i<mo->size; i++) {
909 : ref<Expr> value =
910 : cc.visit(ReadExpr::create(UpdateList(mo, true, 0),
911 : ConstantExpr::create(i,
912 1056: kMachinePointerType)));
913 :
528: branch 1 taken
0: branch 2 not taken
914 528: if (value.isConstant()) {
915 528: data.push_back(value.getConstantValue());
916 : } else {
917 : // FIXME: When does this happen?
918 0: return false;
919 : }
920 : }
921 :
922 : values.push_back(data);
923 : }
924 :
925 177: return true;
926 : }
927 :
928 :
929 1: Solver *klee::createFastCexSolver(Solver *s) {
930 2: return new Solver(new StagedSolverImpl(new FastCexSolver(), s));
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
931 206: }
Generated: 2009-05-17 22:47 by zcov