 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
71.7% |
142 / 198 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
89.4% |
177 / 198 |
| |
|
Line Coverage: |
80.9% |
304 / 376 |
| |
 |
|
 |
1 : #include "STPBuilder.h"
2 :
3 : #include "klee/Expr.h"
4 : // FIXME: This should not be here.
5 : #include "klee/Memory.h"
6 : #include "klee/Solver.h"
7 : #include "klee/util/Bits.h"
8 :
9 : #include "ConstantDivision.h"
10 : #include "SolverStats.h"
11 :
12 : #include "llvm/Support/CommandLine.h"
13 :
14 : #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
15 : // unclear return
16 : #define vc_bvLeftShiftExpr IAMTHESPAWNOFSATAN
17 : #define vc_bvRightShiftExpr IAMTHESPAWNOFSATAN
18 : // bad refcnt'ng
19 : #define vc_bvVar32LeftShiftExpr IAMTHESPAWNOFSATAN
20 : #define vc_bvVar32RightShiftExpr IAMTHESPAWNOFSATAN
21 : #define vc_bvVar32DivByPowOfTwoExpr IAMTHESPAWNOFSATAN
22 : #define vc_bvCreateMemoryArray IAMTHESPAWNOFSATAN
23 : #define vc_bvReadMemoryArray IAMTHESPAWNOFSATAN
24 : #define vc_bvWriteToMemoryArray IAMTHESPAWNOFSATAN
25 :
26 : #include <algorithm> // max, min
27 : #include <cassert>
28 : #include <iostream>
29 : #include <map>
30 : #include <sstream>
31 : #include <vector>
32 :
33 : #include "klee/Internal/FIXME/sugar.h"
34 :
35 : using namespace klee;
36 :
37 : namespace {
38 : llvm::cl::opt<bool>
39 1: UseConstructHash("use-construct-hash",
40 : llvm::cl::desc("Use hash-consing during STP query construction."),
41 1: llvm::cl::init(true));
42 : }
43 :
44 : ///
45 :
46 : /***/
47 :
48 1: STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides)
4: branch 0 taken
1: branch 1 taken
1: branch 3 taken
1: branch 4 taken
49 5: : vc(_vc), optimizeDivides(_optimizeDivides)
50 : {
51 1: tempVars[0] = buildVar("__tmpInt8", 8);
52 1: tempVars[1] = buildVar("__tmpInt16", 16);
53 1: tempVars[2] = buildVar("__tmpInt32", 32);
54 1: tempVars[3] = buildVar("__tmpInt64", 64);
55 1: }
56 :
57 1: STPBuilder::~STPBuilder() {
1: branch 1 taken
0: branch 2 not taken
4: branch 3 taken
1: branch 4 taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 9 not taken
0: branch 10 not taken
58 1: }
59 :
60 : ///
61 :
62 : /* Warning: be careful about what c_interface functions you use. Some of
63 : them look like they cons memory but in fact don't, which is bad when
64 : you call vc_DeleteExpr on them. */
65 :
66 4: ::VCExpr STPBuilder::buildVar(const char *name, unsigned width) {
67 : // XXX don't rebuild if this stuff cons's
0: branch 0 not taken
4: branch 1 taken
68 4: ::Type t = (width==1) ? vc_boolType(vc) : vc_bvType(vc, width);
69 4: ::VCExpr res = vc_varExpr(vc, (char*) name, t);
70 4: vc_DeleteExpr(t);
71 4: return res;
72 : }
73 :
74 1017: ::VCExpr STPBuilder::buildArray(const char *name, unsigned indexWidth, unsigned valueWidth) {
75 : // XXX don't rebuild if this stuff cons's
76 1017: ::Type t1 = vc_bvType(vc, indexWidth);
77 1017: ::Type t2 = vc_bvType(vc, valueWidth);
78 1017: ::Type t = vc_arrayType(vc, t1, t2);
79 1017: ::VCExpr res = vc_varExpr(vc, (char*) name, t);
80 1017: vc_DeleteExpr(t);
81 1017: vc_DeleteExpr(t2);
82 1017: vc_DeleteExpr(t1);
83 1017: return res;
84 : }
85 :
86 0: ExprHandle STPBuilder::getTempVar(Expr::Width w) {
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
87 0: switch (w) {
88 0: case Expr::Int8: return tempVars[0];
89 0: case Expr::Int16: return tempVars[1];
90 0: case Expr::Int32: return tempVars[2];
91 0: case Expr::Int64: return tempVars[3];
92 : default:
93 0: assert(0 && "invalid type");
94 : }
95 : }
96 :
97 0: ExprHandle STPBuilder::getTrue() {
98 0: return vc_trueExpr(vc);
99 : }
100 325: ExprHandle STPBuilder::getFalse() {
101 325: return vc_falseExpr(vc);
102 : }
103 650: ExprHandle STPBuilder::bvOne(unsigned width) {
104 650: return bvConst32(width, 1);
105 : }
106 5395: ExprHandle STPBuilder::bvZero(unsigned width) {
107 5395: return bvConst32(width, 0);
108 : }
109 1756: ExprHandle STPBuilder::bvMinusOne(unsigned width) {
110 1756: return bvConst64(width, (int64_t) -1);
111 : }
112 21613: ExprHandle STPBuilder::bvConst32(unsigned width, uint32_t value) {
113 21613: return vc_bvConstExprFromInt(vc, width, value);
114 : }
115 2096: ExprHandle STPBuilder::bvConst64(unsigned width, uint64_t value) {
116 2096: return vc_bvConstExprFromLL(vc, width, value);
117 : }
118 :
119 650: ExprHandle STPBuilder::bvBoolExtract(ExprHandle expr, int bit) {
120 2600: return vc_eqExpr(vc, bvExtract(expr, bit, bit), bvOne(1));
121 : }
122 7540: ExprHandle STPBuilder::bvExtract(ExprHandle expr, unsigned top, unsigned bottom) {
123 15080: return vc_bvExtract(vc, expr, top, bottom);
124 : }
125 5340: ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) {
126 10680: return vc_eqExpr(vc, a, b);
127 : }
128 :
129 : // logical right shift
130 3512: ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits) {
131 3512: unsigned width = vc_getBVLength(vc, expr);
132 3512: unsigned shift = amount & ((1<<shiftBits) - 1);
133 :
65: branch 0 taken
3447: branch 1 taken
134 3512: if (shift==0) {
135 65: return expr;
4: branch 0 taken
3443: branch 1 taken
136 3447: } else if (shift>=width) {
137 4: return bvZero(width);
138 : } else {
139 : return vc_bvConcatExpr(vc,
140 : bvZero(shift),
141 13772: bvExtract(expr, width - 1, shift));
142 : }
143 : }
144 :
145 : // logical left shift
146 1828: ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned shiftBits) {
147 1828: unsigned width = vc_getBVLength(vc, expr);
148 1828: unsigned shift = amount & ((1<<shiftBits) - 1);
149 :
68: branch 0 taken
1760: branch 1 taken
150 1828: if (shift==0) {
151 68: return expr;
4: branch 0 taken
1756: branch 1 taken
152 1760: } else if (shift>=width) {
153 4: return bvZero(width);
154 : } else {
155 : // stp shift does "expr @ [0 x s]" which we then have to extract,
156 : // rolling our own gives slightly smaller exprs
157 : return vc_bvConcatExpr(vc,
158 : bvExtract(expr, width - shift - 1, 0),
159 7024: bvZero(shift));
160 : }
161 : }
162 :
163 : // left shift by a variable amount on an expression of the specified width
164 60: ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width) {
165 60: ExprHandle res = bvZero(width);
166 :
167 60: int shiftBits = getShiftBits( width );
168 :
169 : //get the shift amount (looking only at the bits appropriate for the given width)
170 120: ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 );
171 :
172 : //construct a big if-then-elif-elif-... with one case per possible shift amount
1800: branch 0 taken
60: branch 1 taken
173 1860: for( int i=width-1; i>=0; i-- ) {
174 : res = vc_iteExpr(vc,
175 : eqExpr(shift, bvConst32(shiftBits, i)),
176 : bvLeftShift(expr, i, shiftBits),
177 10800: res);
178 : }
179 60: return res;
180 : }
181 :
182 : // logical right shift by a variable amount on an expression of the specified width
183 60: ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width) {
184 60: ExprHandle res = bvZero(width);
185 :
186 60: int shiftBits = getShiftBits( width );
187 :
188 : //get the shift amount (looking only at the bits appropriate for the given width)
189 120: ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 );
190 :
191 : //construct a big if-then-elif-elif-... with one case per possible shift amount
1800: branch 0 taken
60: branch 1 taken
192 1860: for( int i=width-1; i>=0; i-- ) {
193 : res = vc_iteExpr(vc,
194 : eqExpr(shift, bvConst32(shiftBits, i)),
195 : bvRightShift(expr, i, shiftBits),
196 10800: res);
197 : }
198 :
199 60: return res;
200 : }
201 :
202 : // arithmetic right shift by a variable amount on an expression of the specified width
203 60: ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width) {
204 60: int shiftBits = getShiftBits( width );
205 :
206 : //get the shift amount (looking only at the bits appropriate for the given width)
207 120: ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 );
208 :
209 : //get the sign bit to fill with
210 120: ExprHandle signedBool = bvBoolExtract(expr, width-1);
211 :
212 : //start with the result if shifting by width-1
213 180: ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, shiftBits);
214 :
215 : //construct a big if-then-elif-elif-... with one case per possible shift amount
216 : // XXX more efficient to move the ite on the sign outside all exprs?
217 : // XXX more efficient to sign extend, right shift, then extract lower bits?
1740: branch 0 taken
60: branch 1 taken
218 1800: for( int i=width-2; i>=0; i-- ) {
219 : res = vc_iteExpr(vc,
220 : eqExpr(shift, bvConst32(shiftBits,i)),
221 : constructAShrByConstant(expr,
222 : i,
223 : signedBool,
224 : shiftBits),
225 12180: res);
226 : }
227 :
228 60: return res;
229 : }
230 :
231 : ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr,
232 : unsigned amount,
233 : ExprHandle isSigned,
234 1820: unsigned shiftBits) {
235 1820: unsigned width = vc_getBVLength(vc, expr);
236 1820: unsigned shift = amount & ((1<<shiftBits) - 1);
237 :
64: branch 0 taken
1756: branch 1 taken
238 1820: if (shift==0) {
239 64: return expr;
66: branch 0 taken
1690: branch 1 taken
240 1756: } else if (shift>=width-1) {
241 198: return vc_iteExpr(vc, isSigned, bvMinusOne(width), bvZero(width));
242 : } else {
243 : return vc_iteExpr(vc,
244 : isSigned,
245 : ExprHandle(vc_bvConcatExpr(vc,
246 : bvMinusOne(shift),
247 : bvExtract(expr, width - 1, shift))),
248 11830: bvRightShift(expr, shift, shiftBits));
249 : }
250 : }
251 :
252 6: ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x) {
253 6: unsigned shiftBits = getShiftBits(width);
254 : uint64_t add, sub;
255 6: ExprHandle res = 0;
256 :
257 : // expr*x == expr*(add-sub) == expr*add - expr*sub
258 6: ComputeMultConstants64(x, add, sub);
259 :
260 : // legal, these would overflow completely
261 12: add = bits64::truncateToNBits(add, width);
262 12: sub = bits64::truncateToNBits(sub, width);
263 :
384: branch 0 taken
6: branch 1 taken
264 390: for (int j=63; j>=0; j--) {
265 384: uint64_t bit = 1LL << j;
266 :
378: branch 0 taken
6: branch 1 taken
2: branch 2 taken
376: branch 3 taken
267 384: if ((add&bit) || (sub&bit)) {
6: branch 0 taken
2: branch 1 taken
0: branch 2 not taken
6: branch 3 taken
268 8: assert(!((add&bit) && (sub&bit)) && "invalid mult constants");
269 16: ExprHandle op = bvLeftShift(expr, j, shiftBits);
270 :
6: branch 0 taken
2: branch 1 taken
271 8: if (add&bit) {
2: branch 0 taken
4: branch 1 taken
272 12: if (res) {
273 4: res = vc_bvPlusExpr(vc, width, res, op);
274 : } else {
275 4: res = op;
276 : }
277 : } else {
0: branch 0 not taken
2: branch 1 taken
278 4: if (res) {
279 0: res = vc_bvMinusExpr(vc, width, res, op);
280 : } else {
281 2: res = vc_bvUMinusExpr(vc, op);
282 : }
283 8: }
284 : }
285 : }
286 :
0: branch 0 not taken
6: branch 1 taken
287 12: if (!res)
288 0: res = bvZero(width);
289 :
290 : return res;
291 : }
292 :
293 : /*
294 : * Compute the 32-bit unsigned integer division of n by a divisor d based on
295 : * the constants derived from the constant divisor d.
296 : *
297 : * Returns n/d without doing explicit division. The cost is 2 adds, 3 shifts,
298 : * and a (64-bit) multiply.
299 : *
300 : * @param n numerator (dividend) as an expression
301 : * @param width number of bits used to represent the value
302 : * @param d the divisor
303 : *
304 : * @return n/d without doing explicit division
305 : */
306 0: ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d) {
0: branch 0 not taken
0: branch 1 not taken
307 0: assert(width==32 && "can only compute udiv constants for 32-bit division");
308 :
309 : // Compute the constants needed to compute n/d for constant d w/o
310 : // division by d.
311 : uint32_t mprime, sh1, sh2;
312 0: ComputeUDivConstants32(d, mprime, sh1, sh2);
313 0: ExprHandle expr_sh1 = bvConst32( 32, sh1);
314 0: ExprHandle expr_sh2 = bvConst32( 32, sh2);
315 :
316 : // t1 = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
317 0: ExprHandle expr_n_64 = vc_bvConcatExpr( vc, bvZero(32), expr_n ); //extend to 64 bits
318 0: ExprHandle t1_64bits = constructMulByConstant( expr_n_64, 64, (uint64_t)mprime );
319 0: ExprHandle t1 = vc_bvExtract( vc, t1_64bits, 63, 32 ); //upper 32 bits
320 :
321 : // n/d = (((n - t1) >> sh1) + t1) >> sh2;
322 0: ExprHandle n_minus_t1 = vc_bvMinusExpr( vc, width, expr_n, t1 );
323 0: ExprHandle shift_sh1 = bvVarRightShift( n_minus_t1, expr_sh1, 32 );
324 0: ExprHandle plus_t1 = vc_bvPlusExpr( vc, width, shift_sh1, t1 );
325 0: ExprHandle res = bvVarRightShift( plus_t1, expr_sh2, 32 );
326 :
327 0: return res;
328 : }
329 :
330 : /*
331 : * Compute the 32-bitnsigned integer division of n by a divisor d based on
332 : * the constants derived from the constant divisor d.
333 : *
334 : * Returns n/d without doing explicit division. The cost is 3 adds, 3 shifts,
335 : * a (64-bit) multiply, and an XOR.
336 : *
337 : * @param n numerator (dividend) as an expression
338 : * @param width number of bits used to represent the value
339 : * @param d the divisor
340 : *
341 : * @return n/d without doing explicit division
342 : */
343 0: ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d) {
0: branch 0 not taken
0: branch 1 not taken
344 0: assert(width==32 && "can only compute udiv constants for 32-bit division");
345 :
346 : // Compute the constants needed to compute n/d for constant d w/o division by d.
347 : int32_t mprime, dsign, shpost;
348 0: ComputeSDivConstants32(d, mprime, dsign, shpost);
349 0: ExprHandle expr_dsign = bvConst32( 32, dsign);
350 0: ExprHandle expr_shpost = bvConst32( 32, shpost);
351 :
352 : // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
353 0: int64_t mprime_64 = (int64_t)mprime;
354 :
355 0: ExprHandle expr_n_64 = vc_bvSignExtend( vc, expr_n, 64 );
356 0: ExprHandle mult_64 = constructMulByConstant( expr_n_64, 64, mprime_64 );
357 0: ExprHandle mulsh = vc_bvExtract( vc, mult_64, 63, 32 ); //upper 32-bits
358 0: ExprHandle n_plus_mulsh = vc_bvPlusExpr( vc, width, expr_n, mulsh );
359 :
360 : // Improved variable arithmetic right shift: sign extend, shift,
361 : // extract.
362 0: ExprHandle extend_npm = vc_bvSignExtend( vc, n_plus_mulsh, 64 );
363 0: ExprHandle shift_npm = bvVarRightShift( extend_npm, expr_shpost, 64 );
364 0: ExprHandle shift_shpost = vc_bvExtract( vc, shift_npm, 31, 0 ); //lower 32-bits
365 :
366 : // XSIGN(n) is -1 if n is negative, positive one otherwise
367 0: ExprHandle is_signed = bvBoolExtract( expr_n, 31 );
368 0: ExprHandle neg_one = bvMinusOne(32);
369 0: ExprHandle xsign_of_n = vc_iteExpr( vc, is_signed, neg_one, bvZero(32) );
370 :
371 : // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
372 0: ExprHandle q0 = vc_bvMinusExpr( vc, width, shift_shpost, xsign_of_n );
373 :
374 : // n/d = (q0 ^ dsign) - dsign
375 0: ExprHandle q0_xor_dsign = vc_bvXorExpr( vc, q0, expr_dsign );
376 0: ExprHandle res = vc_bvMinusExpr( vc, width, q0_xor_dsign, expr_dsign );
377 :
378 0: return res;
379 : }
380 :
381 9016: ::VCExpr STPBuilder::getInitialArray(const MemoryObject *root) {
7999: branch 0 taken
1017: branch 1 taken
382 9016: if (root->stpInitialArray) {
383 7999: return root->stpInitialArray;
384 : } else {
385 : char buf[32];
386 1017: sprintf(buf, "arr%d", root->id);
387 1017: root->stpInitialArray = buildArray(buf, 32, 8);
388 1017: return root->stpInitialArray;
389 : }
390 : }
391 :
392 0: ExprHandle STPBuilder::getInitialRead(const MemoryObject *root, unsigned index) {
393 0: return vc_readExpr(vc, getInitialArray(root), bvConst32(32, index));
394 : }
395 :
396 : ::VCExpr STPBuilder::getArrayForUpdate(const MemoryObject *root,
397 9016: const UpdateNode *un) {
9016: branch 0 taken
0: branch 1 not taken
398 9016: if (!un) {
399 9016: return getInitialArray(root);
400 : } else {
0: branch 0 not taken
0: branch 1 not taken
401 0: if (!un->stpArray) {
402 : #if 0
403 : std::vector<const UpdateNode *> indices;
404 : for (; un; un = un->next) {
405 : if (un->stpArray)
406 : break;
407 : indices.push_back(un);
408 : }
409 :
410 : ::VCExpr array = un ? un->stpArray : getInitialArray(root);
411 : foreach(it, indices.rbegin(), indices.rend()) {
412 : un = *it;
413 : un->stpArray = array = vc_writeExpr(vc, array,
414 : construct(un->index, 0),
415 : construct(un->value, 0));
416 : }
417 : #else
418 : un->stpArray = vc_writeExpr(vc,
419 : getArrayForUpdate(root, un->next),
420 : construct(un->index, 0),
421 0: construct(un->value, 0));
422 : #endif
423 : }
424 :
425 0: return un->stpArray;
426 : }
427 : }
428 :
429 : /** if *width_out!=1 then result is a bitvector,
430 : otherwise it is a bool */
431 32180: ExprHandle STPBuilder::construct(ref<Expr> e, int *width_out) {
32180: branch 0 taken
0: branch 1 not taken
10893: branch 3 taken
21287: branch 4 taken
10893: branch 5 taken
21287: branch 6 taken
432 32180: if (!UseConstructHash || e.isConstant()) {
433 21786: return constructActual(e, width_out);
434 : } else {
435 21287: let(it, constructed.find(e));
885: branch 0 taken
20402: branch 1 taken
436 42574: if (it!=constructed.end()) {
885: branch 0 taken
0: branch 1 not taken
437 885: if (width_out)
438 885: *width_out = it->second.second;
439 1770: return it->second.first;
440 : } else {
441 : int width;
14129: branch 0 taken
6273: branch 1 taken
442 20402: if (!width_out) width_out = &width;
443 20402: ExprHandle res = constructActual(e, width_out);
444 122412: constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
445 40804: return res;
446 : }
447 : }
448 : }
449 :
450 :
451 : /** if *width_out!=1 then result is a bitvector,
452 : otherwise it is a bool */
453 31295: ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
454 : int width;
9016: branch 0 taken
22279: branch 1 taken
455 31295: if (!width_out) width_out = &width;
456 :
457 : ++stats::queryConstructs;
458 :
10893: branch 0 taken
1017: branch 1 taken
9016: branch 2 taken
15: branch 3 taken
6040: branch 4 taken
570: branch 5 taken
0: branch 6 not taken
0: branch 7 not taken
88: branch 8 taken
60: branch 9 taken
16: branch 10 taken
16: branch 11 taken
16: branch 12 taken
16: branch 13 taken
16: branch 14 taken
118: branch 15 taken
144: branch 16 taken
102: branch 17 taken
80: branch 18 taken
80: branch 19 taken
80: branch 20 taken
2296: branch 21 taken
136: branch 22 taken
160: branch 23 taken
160: branch 24 taken
160: branch 25 taken
0: branch 26 not taken
459 31295: switch(e.getKind()) {
460 :
461 : case Expr::Constant: {
462 10893: uint64_t asUInt64 = e.getConstantValue();
463 10893: *width_out = e.getWidth();
464 :
0: branch 0 not taken
10893: branch 1 taken
465 10893: if (*width_out > 64)
466 0: assert(0 && "constructActual: width > 64");
467 :
325: branch 0 taken
10568: branch 1 taken
468 10893: if (*width_out == 1)
0: branch 0 not taken
325: branch 1 taken
469 325: return asUInt64 ? getTrue() : getFalse();
10228: branch 0 taken
340: branch 1 taken
470 10568: else if (*width_out <= 32)
471 10228: return bvConst32(*width_out, asUInt64);
472 340: else return bvConst64(*width_out, asUInt64);
473 : }
474 :
475 : // Special
476 : case Expr::NotOptimized: {
477 1017: NotOptimizedExpr *noe = static_ref_cast<NotOptimizedExpr>(e);
478 2034: return construct(noe->src, width_out);
479 : }
480 :
481 : case Expr::Read: {
482 9016: ReadExpr *re = static_ref_cast<ReadExpr>(e);
483 9016: *width_out = 8;
484 : return vc_readExpr(vc,
485 : getArrayForUpdate(re->updates.root,
486 : re->updates.head),
487 27048: construct(re->index, 0));
488 : }
489 :
490 : case Expr::Select: {
491 15: SelectExpr *se = static_ref_cast<SelectExpr>(e);
492 30: ExprHandle cond = construct(se->cond, 0);
493 30: ExprHandle tExpr = construct(se->trueExpr, width_out);
494 30: ExprHandle fExpr = construct(se->falseExpr, width_out);
495 30: return vc_iteExpr(vc, cond, tExpr, fExpr);
496 : }
497 :
498 : case Expr::Concat: {
499 6040: ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
500 6040: unsigned numKids = ce->getNumKids();
501 6040: ExprHandle res = construct(ce->getKid(numKids-1), 0);
6040: branch 0 taken
6040: branch 1 taken
502 12080: for (int i=numKids-2; i>=0; i--) {
503 12080: res = vc_bvConcatExpr(vc, construct(ce->getKid(i), 0), res);
504 : }
505 6040: *width_out = ce->getWidth();
506 12080: return res;
507 : }
508 :
509 : case Expr::Extract: {
510 570: ExtractExpr *ee = static_ref_cast<ExtractExpr>(e);
511 1140: ExprHandle src = construct(ee->expr, width_out);
512 570: *width_out = ee->getWidth();
570: branch 0 taken
0: branch 1 not taken
513 570: if (*width_out==1) {
514 1140: return bvBoolExtract(src, 0);
515 : } else {
516 0: return vc_bvExtract(vc, src, ee->offset + *width_out - 1, ee->offset);
517 570: }
518 : }
519 :
520 : // Casting
521 :
522 : case Expr::ZExt: {
523 : int srcWidth;
524 0: CastExpr *ce = static_ref_cast<CastExpr>(e);
525 0: ExprHandle src = construct(ce->src, &srcWidth);
526 0: *width_out = ce->getWidth();
0: branch 0 not taken
0: branch 1 not taken
527 0: if (srcWidth==1) {
528 0: return vc_iteExpr(vc, src, bvOne(*width_out), bvZero(*width_out));
529 : } else {
530 0: return vc_bvConcatExpr(vc, bvZero(*width_out-srcWidth), src);
531 0: }
532 : }
533 :
534 : case Expr::SExt: {
535 : int srcWidth;
536 0: CastExpr *ce = static_ref_cast<CastExpr>(e);
537 0: ExprHandle src = construct(ce->src, &srcWidth);
538 0: *width_out = ce->getWidth();
0: branch 0 not taken
0: branch 1 not taken
539 0: if (srcWidth==1) {
540 0: return vc_iteExpr(vc, src, bvMinusOne(*width_out), bvZero(*width_out));
541 : } else {
542 0: return vc_bvSignExtend(vc, src, *width_out);
543 0: }
544 : }
545 :
546 : // Arithmetic
547 :
548 : case Expr::Add: {
549 88: AddExpr *ae = static_ref_cast<AddExpr>(e);
550 176: ExprHandle left = construct(ae->left, width_out);
551 176: ExprHandle right = construct(ae->right, width_out);
0: branch 0 not taken
88: branch 1 taken
552 88: assert(*width_out!=1 && "uncanonicalized add");
553 176: return vc_bvPlusExpr(vc, *width_out, left, right);
554 : }
555 :
556 : case Expr::Sub: {
557 60: SubExpr *se = static_ref_cast<SubExpr>(e);
558 120: ExprHandle left = construct(se->left, width_out);
559 120: ExprHandle right = construct(se->right, width_out);
0: branch 0 not taken
60: branch 1 taken
560 60: assert(*width_out!=1 && "uncanonicalized sub");
561 120: return vc_bvMinusExpr(vc, *width_out, left, right);
562 : }
563 :
564 : case Expr::Mul: {
565 16: MulExpr *me = static_ref_cast<MulExpr>(e);
566 32: ExprHandle right = construct(me->right, width_out);
0: branch 0 not taken
16: branch 1 taken
567 16: assert(*width_out!=1 && "uncanonicalized mul");
568 :
6: branch 1 taken
10: branch 2 taken
569 16: if (me->left.isConstant()) {
570 12: return constructMulByConstant(right, *width_out, me->left.getConstantValue());
571 : } else {
572 20: ExprHandle left = construct(me->left, width_out);
573 20: return vc_bvMultExpr(vc, *width_out, left, right);
574 16: }
575 : }
576 :
577 : case Expr::UDiv: {
578 16: UDivExpr *de = static_ref_cast<UDivExpr>(e);
579 32: ExprHandle left = construct(de->left, width_out);
0: branch 0 not taken
16: branch 1 taken
580 16: assert(*width_out!=1 && "uncanonicalized udiv");
581 :
4: branch 1 taken
12: branch 2 taken
582 16: if (de->right.isConstant()) {
583 4: uint64_t divisor = de->right.getConstantValue();
584 :
2: branch 0 taken
2: branch 1 taken
585 4: if (bits64::isPowerOfTwo(divisor)) {
586 : return bvRightShift(left,
587 : bits64::indexOfSingleBit(divisor),
588 4: getShiftBits(*width_out));
2: branch 0 taken
0: branch 1 not taken
589 2: } else if (optimizeDivides) {
0: branch 0 not taken
2: branch 1 taken
590 2: if (*width_out == 32) //only works for 32-bit division
591 0: return constructUDivByConstant( left, *width_out, (uint32_t)divisor );
592 : }
593 : }
594 :
595 28: ExprHandle right = construct(de->right, width_out);
596 28: return vc_bvDivExpr(vc, *width_out, left, right);
597 : }
598 :
599 : case Expr::SDiv: {
600 16: SDivExpr *de = static_ref_cast<SDivExpr>(e);
601 32: ExprHandle left = construct(de->left, width_out);
0: branch 0 not taken
16: branch 1 taken
602 16: assert(*width_out!=1 && "uncanonicalized sdiv");
603 :
4: branch 1 taken
12: branch 2 taken
604 16: if (de->right.isConstant()) {
605 4: uint64_t divisor = de->right.getConstantValue();
606 :
4: branch 0 taken
0: branch 1 not taken
607 4: if (optimizeDivides) {
0: branch 0 not taken
4: branch 1 taken
608 4: if (*width_out == 32) //only works for 32-bit division
609 0: return constructSDivByConstant( left, *width_out, divisor);
610 : }
611 : }
612 :
613 : // XXX need to test for proper handling of sign, not sure I
614 : // trust STP
615 32: ExprHandle right = construct(de->right, width_out);
616 32: return vc_sbvDivExpr(vc, *width_out, left, right);
617 : }
618 :
619 : case Expr::URem: {
620 16: URemExpr *de = static_ref_cast<URemExpr>(e);
621 32: ExprHandle left = construct(de->left, width_out);
0: branch 0 not taken
16: branch 1 taken
622 16: assert(*width_out!=1 && "uncanonicalized urem");
623 :
4: branch 1 taken
12: branch 2 taken
624 16: if (de->right.isConstant()) {
625 4: uint64_t divisor = de->right.getConstantValue();
626 :
2: branch 0 taken
2: branch 1 taken
627 4: if (bits64::isPowerOfTwo(divisor)) {
628 2: unsigned bits = bits64::indexOfSingleBit(divisor);
629 :
630 : // special case for modding by 1 or else we bvExtract -1:0
1: branch 0 taken
1: branch 1 taken
631 2: if (bits == 0) {
632 1: return bvZero(*width_out);
633 : } else {
634 : return vc_bvConcatExpr(vc,
635 : bvZero(*width_out - bits),
636 4: bvExtract(left, bits - 1, 0));
637 : }
638 : }
639 :
640 : //use fast division to compute modulo without explicit division for constant divisor
2: branch 0 taken
0: branch 1 not taken
641 2: if (optimizeDivides) {
0: branch 0 not taken
2: branch 1 taken
642 2: if (*width_out == 32) { //only works for 32-bit division
643 0: ExprHandle quotient = constructUDivByConstant( left, *width_out, (uint32_t)divisor );
644 0: ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
645 0: ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
646 0: return rem;
647 : }
648 : }
649 : }
650 :
651 28: ExprHandle right = construct(de->right, width_out);
652 28: return vc_bvModExpr(vc, *width_out, left, right);
653 : }
654 :
655 : case Expr::SRem: {
656 16: SRemExpr *de = static_ref_cast<SRemExpr>(e);
657 32: ExprHandle left = construct(de->left, width_out);
658 32: ExprHandle right = construct(de->right, width_out);
0: branch 0 not taken
16: branch 1 taken
659 16: assert(*width_out!=1 && "uncanonicalized srem");
660 :
661 : #if 0 //not faster per first benchmark
662 : if (optimizeDivides) {
663 : if (ConstantExpr *cre = de->right->asConstant()) {
664 : uint64_t divisor = cre->asUInt64;
665 :
666 : //use fast division to compute modulo without explicit division for constant divisor
667 : if( *width_out == 32 ) { //only works for 32-bit division
668 : ExprHandle quotient = constructSDivByConstant( left, *width_out, divisor );
669 : ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
670 : ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
671 : return rem;
672 : }
673 : }
674 : }
675 : #endif
676 :
677 : // XXX implement my fast path and test for proper handling of sign
678 32: return vc_sbvModExpr(vc, *width_out, left, right);
679 : }
680 :
681 : // Binary
682 :
683 : case Expr::And: {
684 118: AndExpr *ae = static_ref_cast<AndExpr>(e);
685 236: ExprHandle left = construct(ae->left, width_out);
686 236: ExprHandle right = construct(ae->right, width_out);
54: branch 0 taken
64: branch 1 taken
687 118: if (*width_out==1) {
688 108: return vc_andExpr(vc, left, right);
689 : } else {
690 128: return vc_bvAndExpr(vc, left, right);
691 118: }
692 : }
693 : case Expr::Or: {
694 144: OrExpr *oe = static_ref_cast<OrExpr>(e);
695 288: ExprHandle left = construct(oe->left, width_out);
696 288: ExprHandle right = construct(oe->right, width_out);
80: branch 0 taken
64: branch 1 taken
697 144: if (*width_out==1) {
698 160: return vc_orExpr(vc, left, right);
699 : } else {
700 128: return vc_bvOrExpr(vc, left, right);
701 144: }
702 : }
703 :
704 : case Expr::Xor: {
705 102: XorExpr *xe = static_ref_cast<XorExpr>(e);
706 204: ExprHandle left = construct(xe->left, width_out);
707 204: ExprHandle right = construct(xe->right, width_out);
708 :
30: branch 0 taken
72: branch 1 taken
709 102: if (*width_out==1) {
710 : // XXX check for most efficient?
711 : return vc_iteExpr(vc, left,
712 90: ExprHandle(vc_notExpr(vc, right)), right);
713 : } else {
714 144: return vc_bvXorExpr(vc, left, right);
715 102: }
716 : }
717 :
718 : case Expr::Shl: {
719 80: ShlExpr *se = static_ref_cast<ShlExpr>(e);
720 160: ExprHandle left = construct(se->left, width_out);
0: branch 0 not taken
80: branch 1 taken
721 80: assert(*width_out!=1 && "uncanonicalized shl");
722 :
20: branch 1 taken
60: branch 2 taken
723 80: if (se->right.isConstant()) {
724 60: return bvLeftShift(left, se->right.getConstantValue(), getShiftBits(*width_out));
725 : } else {
726 : int shiftWidth;
727 120: ExprHandle amount = construct(se->right, &shiftWidth);
728 120: return bvVarLeftShift( left, amount, *width_out );
729 80: }
730 : }
731 :
732 : case Expr::LShr: {
733 80: LShrExpr *lse = static_ref_cast<LShrExpr>(e);
734 160: ExprHandle left = construct(lse->left, width_out);
735 160: unsigned shiftBits = getShiftBits(*width_out);
0: branch 0 not taken
80: branch 1 taken
736 80: assert(*width_out!=1 && "uncanonicalized lshr");
737 :
20: branch 1 taken
60: branch 2 taken
738 80: if (lse->right.isConstant()) {
739 40: return bvRightShift(left, (unsigned) lse->right.getConstantValue(), shiftBits);
740 : } else {
741 : int shiftWidth;
742 120: ExprHandle amount = construct(lse->right, &shiftWidth);
743 120: return bvVarRightShift( left, amount, *width_out );
744 80: }
745 : }
746 :
747 : case Expr::AShr: {
748 80: AShrExpr *ase = static_ref_cast<AShrExpr>(e);
749 160: ExprHandle left = construct(ase->left, width_out);
0: branch 0 not taken
80: branch 1 taken
750 80: assert(*width_out!=1 && "uncanonicalized ashr");
751 :
20: branch 1 taken
60: branch 2 taken
752 80: if (ase->right.isConstant()) {
753 20: unsigned shift = (unsigned) ase->right.getConstantValue();
754 40: ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
755 40: return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
756 : } else {
757 : int shiftWidth;
758 120: ExprHandle amount = construct(ase->right, &shiftWidth);
759 120: return bvVarArithRightShift( left, amount, *width_out );
760 80: }
761 : }
762 :
763 : // Comparison
764 :
765 : case Expr::Eq: {
766 2296: EqExpr *ee = static_ref_cast<EqExpr>(e);
767 4592: ExprHandle left = construct(ee->left, width_out);
768 4592: ExprHandle right = construct(ee->right, width_out);
852: branch 0 taken
1444: branch 1 taken
769 2296: if (*width_out==1) {
325: branch 1 taken
527: branch 2 taken
770 852: if (ee->left.isConstant()) {
0: branch 1 not taken
325: branch 2 taken
771 325: assert(!ee->left.getConstantValue() && "uncanonicalized eq");
772 650: return vc_notExpr(vc, right);
773 : } else {
774 1054: return vc_iffExpr(vc, left, right);
775 : }
776 : } else {
777 1444: *width_out = 1;
778 2888: return vc_eqExpr(vc, left, right);
779 2296: }
780 : }
781 :
782 : case Expr::Ult: {
783 136: UltExpr *ue = static_ref_cast<UltExpr>(e);
784 272: ExprHandle left = construct(ue->left, width_out);
785 272: ExprHandle right = construct(ue->right, width_out);
0: branch 0 not taken
136: branch 1 taken
786 136: assert(*width_out!=1 && "uncanonicalized ult");
787 136: *width_out = 1;
788 272: return vc_bvLtExpr(vc, left, right);
789 : }
790 :
791 : case Expr::Ule: {
792 160: UleExpr *ue = static_ref_cast<UleExpr>(e);
793 320: ExprHandle left = construct(ue->left, width_out);
794 320: ExprHandle right = construct(ue->right, width_out);
0: branch 0 not taken
160: branch 1 taken
795 160: assert(*width_out!=1 && "uncanonicalized ule");
796 160: *width_out = 1;
797 320: return vc_bvLeExpr(vc, left, right);
798 : }
799 :
800 : case Expr::Slt: {
801 160: SltExpr *se = static_ref_cast<SltExpr>(e);
802 320: ExprHandle left = construct(se->left, width_out);
803 320: ExprHandle right = construct(se->right, width_out);
0: branch 0 not taken
160: branch 1 taken
804 160: assert(*width_out!=1 && "uncanonicalized slt");
805 160: *width_out = 1;
806 320: return vc_sbvLtExpr(vc, left, right);
807 : }
808 :
809 : case Expr::Sle: {
810 160: SleExpr *se = static_ref_cast<SleExpr>(e);
811 320: ExprHandle left = construct(se->left, width_out);
812 320: ExprHandle right = construct(se->right, width_out);
0: branch 0 not taken
160: branch 1 taken
813 160: assert(*width_out!=1 && "uncanonicalized sle");
814 160: *width_out = 1;
815 320: return vc_sbvLeExpr(vc, left, right);
816 : }
817 :
818 : // unused due to canonicalization
819 : #if 0
820 : case Expr::Ne:
821 : case Expr::Ugt:
822 : case Expr::Uge:
823 : case Expr::Sgt:
824 : case Expr::Sge:
825 : #endif
826 :
827 : default:
828 0: assert(0 && "unhandled Expr type");
829 : return vc_trueExpr(vc);
830 : }
1: branch 0 taken
0: branch 1 not taken
1: branch 2 taken
0: branch 3 not taken
831 3: }
Generated: 2009-05-17 22:47 by zcov