 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
67.1% |
497 / 741 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
95.1% |
705 / 741 |
| |
|
Line Coverage: |
85.4% |
461 / 540 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Expr.h"
4 :
5 :
6 : #include "klee/Machine.h"
7 : // FIXME: This shouldn't be here.
8 : #include "klee/Memory.h"
9 : #include "llvm/Type.h"
10 : #include "llvm/DerivedTypes.h"
11 : #include "llvm/Support/CommandLine.h"
12 : #include "llvm/Support/Streams.h"
13 : // FIXME: We shouldn't need this once fast constant support moves into
14 : // Core. If we need to do arithmetic, we probably want to use APInt.
15 : #include "klee/Internal/Support/IntEvaluation.h"
16 :
17 : #include "klee/util/ExprPPrinter.h"
18 :
19 : using namespace klee;
20 : using namespace llvm;
21 :
22 : namespace {
23 : cl::opt<bool>
24 108: ConstArrayOpt("const-array-opt",
25 : cl::init(false),
26 108: cl::desc("Enable various optimizations involving all-constant arrays."));
27 : }
28 :
29 : /***/
30 :
31 : unsigned Expr::count = 0;
32 :
33 1023: ref<Expr> Expr::createTempRead(const MemoryObject *mo, Expr::Width w) {
34 1023: UpdateList ul(mo, true, 0);
35 :
195: branch 0 taken
256: branch 1 taken
200: branch 2 taken
191: branch 3 taken
181: branch 4 taken
0: branch 5 not taken
36 1023: switch (w) {
37 : case Expr::Bool: return ZExtExpr::create(ReadExpr::create(ul,
38 : ref<Expr>(0,kMachinePointerType)),
39 390: Expr::Bool);
40 : case Expr::Int8: return ReadExpr::create(ul,
41 512: ref<Expr>(0,kMachinePointerType));
42 : case Expr::Int16: return ConcatExpr::create(ReadExpr::create(ul,
43 : ref<Expr>(1,kMachinePointerType)),
44 : ReadExpr::create(ul,
45 600: ref<Expr>(0,kMachinePointerType)));
46 : case Expr::Int32: return ConcatExpr::create4(ReadExpr::create(ul,
47 : ref<Expr>(3,kMachinePointerType)),
48 : ReadExpr::create(ul,
49 : ref<Expr>(2,kMachinePointerType)),
50 : ReadExpr::create(ul,
51 : ref<Expr>(1,kMachinePointerType)),
52 : ReadExpr::create(ul,
53 955: ref<Expr>(0,kMachinePointerType)));
54 : case Expr::Int64: return ConcatExpr::create8(ReadExpr::create(ul,
55 : ref<Expr>(7,kMachinePointerType)),
56 : ReadExpr::create(ul,
57 : ref<Expr>(6,kMachinePointerType)),
58 : ReadExpr::create(ul,
59 : ref<Expr>(5,kMachinePointerType)),
60 : ReadExpr::create(ul,
61 : ref<Expr>(4,kMachinePointerType)),
62 : ReadExpr::create(ul,
63 : ref<Expr>(3,kMachinePointerType)),
64 : ReadExpr::create(ul,
65 : ref<Expr>(2,kMachinePointerType)),
66 : ReadExpr::create(ul,
67 : ref<Expr>(1,kMachinePointerType)),
68 : ReadExpr::create(ul,
69 1629: ref<Expr>(0,kMachinePointerType)));
70 0: default: assert(0 && "invalid width");
71 1023: }
72 : }
73 :
74 : // returns 0 if b is structurally equal to *this
75 6657325: int Expr::compare(const Expr &b) const {
748355: branch 0 taken
5908970: branch 1 taken
76 6657325: if (this == &b) return 0;
77 :
78 5908970: Kind ak = getKind(), bk = b.getKind();
357084: branch 0 taken
5551886: branch 1 taken
79 5908970: if (ak!=bk)
330031: branch 0 taken
27053: branch 1 taken
80 357084: return (ak < bk) ? -1 : 1;
81 :
3375184: branch 0 taken
2176702: branch 1 taken
82 5551886: if (hashValue != b.hashValue)
1746885: branch 0 taken
1628299: branch 1 taken
83 3375184: return (hashValue < b.hashValue) ? -1 : 1;
84 :
1410: branch 1 taken
2175292: branch 2 taken
85 2176702: if (int res = compareContents(b))
86 1410: return res;
87 :
88 2175292: unsigned aN = getNumKids();
3132481: branch 0 taken
2175292: branch 1 taken
89 5307773: for (unsigned i=0; i<aN; i++)
0: branch 5 not taken
3132481: branch 6 taken
90 3132481: if (int res = getKid(i).compare(b.getKid(i)))
91 0: return res;
92 :
93 2175292: return 0;
94 : }
95 :
96 2525: void Expr::printKind(std::ostream &os, Kind k) {
0: branch 0 not taken
2: branch 1 taken
735: branch 2 taken
0: branch 3 not taken
477: branch 4 taken
64: branch 5 taken
0: branch 6 not taken
16: branch 7 taken
87: branch 8 taken
1: branch 9 taken
45: branch 10 taken
0: branch 11 not taken
0: branch 12 not taken
0: branch 13 not taken
0: branch 14 not taken
513: branch 15 taken
97: branch 16 taken
0: branch 17 not taken
0: branch 18 not taken
0: branch 19 not taken
0: branch 20 not taken
371: branch 21 taken
0: branch 22 not taken
97: branch 23 taken
8: branch 24 taken
0: branch 25 not taken
0: branch 26 not taken
11: branch 27 taken
1: branch 28 taken
0: branch 29 not taken
0: branch 30 not taken
0: branch 31 not taken
97 2525: switch(k) {
98 : #define X(C) case C: os << #C; break
99 0: X(Constant);
100 2: X(NotOptimized);
101 735: X(Read);
102 0: X(Select);
103 477: X(Concat);
104 64: X(Extract);
105 0: X(ZExt);
106 16: X(SExt);
107 87: X(Add);
108 1: X(Sub);
109 45: X(Mul);
110 0: X(UDiv);
111 0: X(SDiv);
112 0: X(URem);
113 0: X(SRem);
114 513: X(And);
115 97: X(Or);
116 0: X(Xor);
117 0: X(Shl);
118 0: X(LShr);
119 0: X(AShr);
120 371: X(Eq);
121 0: X(Ne);
122 97: X(Ult);
123 8: X(Ule);
124 0: X(Ugt);
125 0: X(Uge);
126 11: X(Slt);
127 1: X(Sle);
128 0: X(Sgt);
129 0: X(Sge);
130 : #undef X
131 : default:
132 0: assert(0 && "invalid kind");
133 : }
134 2525: }
135 :
136 : ////////
137 : //
138 : // Simple hash functions for various kinds of Exprs
139 : //
140 : ///////
141 :
142 31745: unsigned Expr::computeHash() {
143 31745: unsigned res = getKind() * Expr::MAGIC_HASH_CONSTANT;
144 :
145 31745: int n = getNumKids();
62895: branch 0 taken
31745: branch 1 taken
146 94640: for (int i = 0; i < n; i++) {
147 62895: res <<= 1;
148 62895: res ^= getKid(i).hash() * Expr::MAGIC_HASH_CONSTANT;
149 : }
150 :
151 31745: hashValue = res;
152 31745: return hashValue;
153 : }
154 :
155 643: unsigned ConstantExpr::computeHash() {
156 1286: hashValue = Expr::hashConstant(asUInt64, width);
157 643: return hashValue;
158 : }
159 :
160 1324: unsigned CastExpr::computeHash() {
161 1324: unsigned res = getWidth() * Expr::MAGIC_HASH_CONSTANT;
162 1324: hashValue = res ^ src.hash() * Expr::MAGIC_HASH_CONSTANT;
163 1324: return hashValue;
164 : }
165 :
166 24125: unsigned ExtractExpr::computeHash() {
167 24125: unsigned res = offset * Expr::MAGIC_HASH_CONSTANT;
168 24125: res ^= getWidth() * Expr::MAGIC_HASH_CONSTANT;
169 24125: hashValue = res ^ expr.hash() * Expr::MAGIC_HASH_CONSTANT;
170 24125: return hashValue;
171 : }
172 :
173 5512: unsigned ReadExpr::computeHash() {
174 5512: unsigned res = index.hash() * Expr::MAGIC_HASH_CONSTANT;
175 5512: res ^= updates.hash();
176 5512: hashValue = res;
177 5512: return hashValue;
178 : }
179 :
180 0: uint64_t Expr::getConstantValue() const {
0: branch 1 not taken
0: branch 2 not taken
181 0: assert(getKind() == Constant);
182 0: return static_cast<const ConstantExpr*>(this)->asUInt64;
183 : }
184 :
185 1568: ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
186 1568: unsigned numArgs = args.size();
187 :
0: branch 0 not taken
20: branch 1 taken
0: branch 2 not taken
90: branch 3 taken
90: branch 4 taken
75: branch 5 taken
75: branch 6 taken
15: branch 7 taken
12: branch 8 taken
12: branch 9 taken
12: branch 10 taken
12: branch 11 taken
75: branch 12 taken
75: branch 13 taken
75: branch 14 taken
60: branch 15 taken
60: branch 16 taken
60: branch 17 taken
75: branch 18 taken
75: branch 19 taken
75: branch 20 taken
75: branch 21 taken
75: branch 22 taken
75: branch 23 taken
75: branch 24 taken
75: branch 25 taken
75: branch 26 taken
75: branch 27 taken
0: branch 28 not taken
188 1568: switch(k) {
189 : case NotOptimized:
190 : assert(numArgs == 1 && args[0].isExpr() &&
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
191 0: "invalid args array for given opcode");
192 0: return NotOptimizedExpr::create(args[0].expr);
193 :
194 : case Select:
195 : assert(numArgs == 3 && args[0].isExpr() &&
196 : args[1].isExpr() && args[2].isExpr() &&
20: branch 0 taken
0: branch 1 not taken
20: branch 2 taken
0: branch 3 not taken
20: branch 4 taken
0: branch 5 not taken
0: branch 6 not taken
20: branch 7 taken
197 80: "invalid args array for Select opcode");
198 : return SelectExpr::create(args[0].expr,
199 : args[1].expr,
200 100: args[2].expr);
201 :
202 : case Concat: {
203 : assert(numArgs == 2 && args[0].isExpr() && args[1].isExpr() &&
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
204 0: "invalid args array for Concat opcode");
205 :
206 0: return ConcatExpr::create(args[0].expr, args[1].expr);
207 : }
208 :
209 : #define CAST_EXPR_CASE(T) \
210 : case T: \
211 : assert(numArgs == 2 && \
212 : args[0].isExpr() && args[1].isWidth() && \
213 : "invalid args array for given opcode"); \
214 : return T ## Expr::create(args[0].expr, args[1].width); \
215 :
216 : #define BINARY_EXPR_CASE(T) \
217 : case T: \
218 : assert(numArgs == 2 && \
219 : args[0].isExpr() && args[1].isExpr() && \
220 : "invalid args array for given opcode"); \
221 : return T ## Expr::create(args[0].expr, args[1].expr); \
222 :
90: branch 0 taken
0: branch 1 not taken
90: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
90: branch 5 taken
223 450: CAST_EXPR_CASE(ZExt);
90: branch 0 taken
0: branch 1 not taken
90: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
90: branch 5 taken
224 450: CAST_EXPR_CASE(SExt);
225 :
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
226 375: BINARY_EXPR_CASE(Add);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
227 375: BINARY_EXPR_CASE(Sub);
15: branch 0 taken
0: branch 1 not taken
15: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
15: branch 5 taken
228 75: BINARY_EXPR_CASE(Mul);
12: branch 0 taken
0: branch 1 not taken
12: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
12: branch 5 taken
229 60: BINARY_EXPR_CASE(UDiv);
12: branch 0 taken
0: branch 1 not taken
12: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
12: branch 5 taken
230 60: BINARY_EXPR_CASE(SDiv);
12: branch 0 taken
0: branch 1 not taken
12: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
12: branch 5 taken
231 60: BINARY_EXPR_CASE(URem);
12: branch 0 taken
0: branch 1 not taken
12: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
12: branch 5 taken
232 60: BINARY_EXPR_CASE(SRem);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
233 375: BINARY_EXPR_CASE(And);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
234 375: BINARY_EXPR_CASE(Or);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
235 375: BINARY_EXPR_CASE(Xor);
60: branch 0 taken
0: branch 1 not taken
60: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
60: branch 5 taken
236 300: BINARY_EXPR_CASE(Shl);
60: branch 0 taken
0: branch 1 not taken
60: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
60: branch 5 taken
237 300: BINARY_EXPR_CASE(LShr);
60: branch 0 taken
0: branch 1 not taken
60: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
60: branch 5 taken
238 300: BINARY_EXPR_CASE(AShr);
239 :
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
240 375: BINARY_EXPR_CASE(Eq);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
241 375: BINARY_EXPR_CASE(Ne);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
242 375: BINARY_EXPR_CASE(Ult);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
243 375: BINARY_EXPR_CASE(Ule);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
244 375: BINARY_EXPR_CASE(Ugt);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
245 375: BINARY_EXPR_CASE(Uge);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
246 375: BINARY_EXPR_CASE(Slt);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
247 375: BINARY_EXPR_CASE(Sle);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
248 375: BINARY_EXPR_CASE(Sgt);
75: branch 0 taken
0: branch 1 not taken
75: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
75: branch 5 taken
249 375: BINARY_EXPR_CASE(Sge);
250 :
251 : case Constant:
252 : case Extract:
253 : case Read:
254 : default:
255 0: assert(0 && "invalid kind");
256 : }
257 :
258 : }
259 :
260 :
261 0: void Expr::printWidth(std::ostream &os, Width width) {
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
262 0: switch(width) {
263 0: case Expr::Bool: os << "Expr::Bool"; break;
264 0: case Expr::Int8: os << "Expr::Int8"; break;
265 0: case Expr::Int16: os << "Expr::Int16"; break;
266 0: case Expr::Int32: os << "Expr::Int32"; break;
267 0: case Expr::Int64: os << "Expr::Int64"; break;
268 0: default: os << "<invalid type: " << (unsigned) width << ">";
269 : }
270 0: }
271 :
272 2159457: Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) {
2099933: branch 0 taken
0: branch 1 not taken
3: branch 2 taken
6: branch 3 taken
59515: branch 4 taken
0: branch 5 not taken
273 4318914: switch (t->getTypeID()) {
274 : case llvm::Type::IntegerTyID: {
275 4199866: Width w = cast<IntegerType>(t)->getBitWidth();
276 :
277 : // should remove this limitation soon
2075416: branch 0 taken
24517: branch 1 taken
17: branch 2 taken
2075399: branch 3 taken
17: branch 4 taken
0: branch 5 not taken
278 2099933: if (w == 1 || w == 8 || w == 16 || w == 32 || w == 64)
279 2099933: return w;
280 : else {
281 0: assert(0 && "XXX arbitrary bit widths unsupported");
282 : abort();
283 : }
284 : }
285 0: case llvm::Type::FloatTyID: return Expr::Int32;
286 3: case llvm::Type::DoubleTyID: return Expr::Int64;
287 6: case llvm::Type::X86_FP80TyID: return Expr::Int64; // XXX: needs to be fixed
288 59515: case llvm::Type::PointerTyID: return kMachinePointerType;
289 : default:
290 : cerr << "non-primitive type argument to Expr::getTypeForLLVMType()\n";
291 0: abort();
292 : }
293 : }
294 :
295 0: ref<Expr> Expr::createImplies(ref<Expr> hyp, ref<Expr> conc) {
296 0: return OrExpr::create(Expr::createNot(hyp), conc);
297 : }
298 :
299 18260: ref<Expr> Expr::createIsZero(ref<Expr> e) {
300 36520: return EqExpr::create(e, ConstantExpr::create(0, e.getWidth()));
301 : }
302 :
303 25590: ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
304 25590: return ZExtExpr::create(e, kMachinePointerType);
305 : }
306 :
307 18219: ref<Expr> Expr::createNot(ref<Expr> e) {
308 36438: return createIsZero(e);
309 : }
310 :
311 272481: ref<Expr> Expr::createPointer(uint64_t v) {
312 544962: return ConstantExpr::create(v, kMachinePointerType);
313 : }
314 :
315 643: Expr* Expr::createConstant(uint64_t val, Width w) {
316 1286: Expr *r = new ConstantExpr(val, w);
317 643: r->computeHash();
318 643: return r;
319 : }
320 :
321 206: void Expr::print(std::ostream &os) const {
322 206: const ref<Expr> tmp((Expr*)this);
323 206: ExprPPrinter::printOne(os, "", tmp);
324 206: }
325 :
326 : /***/
327 :
328 287: ref<ConstantExpr> ConstantExpr::fromMemory(void *address, Width width) {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
287: branch 3 taken
0: branch 4 not taken
0: branch 5 not taken
329 287: switch (width) {
330 0: case Expr::Bool: return ConstantExpr::create(*(( uint8_t*) address), width);
331 0: case Expr::Int8: return ConstantExpr::create(*(( uint8_t*) address), width);
332 0: case Expr::Int16: return ConstantExpr::create(*((uint16_t*) address), width);
333 287: case Expr::Int32: return ConstantExpr::create(*((uint32_t*) address), width);
334 0: case Expr::Int64: return ConstantExpr::create(*((uint64_t*) address), width);
335 0: default: assert(0 && "invalid type");
336 : }
337 : }
338 :
339 643: void ConstantExpr::toMemory(void *address) {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
638: branch 3 taken
5: branch 4 taken
0: branch 5 not taken
340 643: switch (width) {
341 0: case Expr::Bool: *(( uint8_t*) address) = asUInt64; break;
342 0: case Expr::Int8: *(( uint8_t*) address) = asUInt64; break;
343 0: case Expr::Int16: *((uint16_t*) address) = asUInt64; break;
344 638: case Expr::Int32: *((uint32_t*) address) = asUInt64; break;
345 5: case Expr::Int64: *((uint64_t*) address) = asUInt64; break;
346 0: default: assert(0 && "invalid type");
347 : }
348 643: }
349 :
350 : /***/
351 :
352 1020: ref<Expr> NotOptimizedExpr::create(ref<Expr> src) {
353 1020: return NotOptimizedExpr::alloc(src);
354 : }
355 :
356 5319: ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
357 : // rollback index when possible...
358 :
359 : // XXX this doesn't really belong here... there are basically two
360 : // cases, one is rebuild, where we want to optimistically try various
361 : // optimizations when the index has changed, and the other is
362 : // initial creation, where we expect the ObjectState to have constructed
363 : // a smart UpdateList so it is not worth rescanning.
364 :
365 5319: const UpdateNode *un = ul.head;
7768: branch 3 taken
4981: branch 4 taken
366 25578: for (; un; un=un->next) {
367 7768: ref<Expr> cond = EqExpr::create(index, un->index);
368 :
7510: branch 1 taken
258: branch 2 taken
369 7768: if (cond.isConstant()) {
80: branch 1 taken
7430: branch 2 taken
370 7510: if (cond.getConstantValue())
371 160: return un->value;
372 : } else {
373 258: break;
374 : }
375 : }
376 :
377 10478: return ReadExpr::alloc(ul, index);
378 : }
379 :
380 1194003: int ReadExpr::compareContents(const Expr &b) const {
381 1194003: return updates.compare(static_cast<const ReadExpr&>(b).updates);
382 : }
383 :
384 2888: ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
385 2888: Expr::Width kt = t.getWidth();
386 :
0: branch 1 not taken
2888: branch 2 taken
387 2888: assert(c.getWidth()==Bool && "type mismatch");
0: branch 1 not taken
2888: branch 2 taken
388 2888: assert(kt==f.getWidth() && "type mismatch");
389 :
353: branch 1 taken
2535: branch 2 taken
390 2888: if (c.isConstant()) {
349: branch 1 taken
4: branch 2 taken
391 353: return c.getConstantValue() ? t : f;
2100: branch 0 taken
435: branch 1 taken
392 2535: } else if (t==f) {
393 2100: return t;
85: branch 0 taken
350: branch 1 taken
394 435: } else if (kt==Expr::Bool) { // c ? t : f <=> (c and t) or (not c and f)
5: branch 1 taken
80: branch 2 taken
395 85: if (t.isConstant()) {
3: branch 1 taken
2: branch 2 taken
396 5: if (t.getConstantValue()) {
397 3: return OrExpr::create(c, f);
398 : } else {
399 4: return AndExpr::create(Expr::createNot(c), f);
400 : }
5: branch 1 taken
75: branch 2 taken
401 80: } else if (f.isConstant()) {
3: branch 1 taken
2: branch 2 taken
402 5: if (f.getConstantValue()) {
403 6: return OrExpr::create(Expr::createNot(c), t);
404 : } else {
405 2: return AndExpr::create(c, t);
406 : }
407 : }
408 : }
409 :
410 850: return SelectExpr::alloc(c, t, f);
411 : }
412 :
413 : /***/
414 :
415 :
416 6385244: ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
417 6385244: Expr::Width w = l.getWidth() + r.getWidth();
418 :
419 : /* Constant folding */
6369136: branch 1 taken
16108: branch 2 taken
6369131: branch 4 taken
5: branch 5 taken
6369131: branch 6 taken
16113: branch 7 taken
420 6385244: if (l.getKind() == Expr::Constant && r.getKind() == Expr::Constant) {
421 : // XXX: should fix this constant limitation soon
0: branch 0 not taken
6369131: branch 1 taken
422 6369131: assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
423 :
424 6369131: uint64_t res = (l.getConstantValue() << r.getWidth()) + r.getConstantValue();
425 12738262: return ConstantExpr::create(res, w);
426 : }
427 :
428 : // Merge contiguous Extracts
12784: branch 1 taken
3329: branch 2 taken
12779: branch 4 taken
5: branch 5 taken
12779: branch 6 taken
3334: branch 7 taken
429 16113: if (l.getKind() == Expr::Extract && r.getKind() == Expr::Extract) {
430 12779: const ExtractExpr* ee_left = static_ref_cast<ExtractExpr>(l);
431 12779: const ExtractExpr* ee_right = static_ref_cast<ExtractExpr>(r);
12777: branch 0 taken
2: branch 1 taken
12777: branch 2 taken
0: branch 3 not taken
12777: branch 4 taken
2: branch 5 taken
432 25558: if (ee_left->expr == ee_right->expr &&
433 : ee_right->offset + ee_right->width == ee_left->offset) {
434 25554: return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
435 : }
436 : }
437 :
438 6672: return ConcatExpr::alloc(l, r);
439 : }
440 :
441 : /// Shortcut to concat N kids. The chain returned is unbalanced to the right
442 200: ref<Expr> ConcatExpr::createN(unsigned n_kids, const ref<Expr> kids[]) {
0: branch 0 not taken
200: branch 1 taken
443 200: assert(n_kids > 0);
0: branch 0 not taken
200: branch 1 taken
444 200: if (n_kids == 1)
445 0: return kids[0];
446 :
447 200: ref<Expr> r = ConcatExpr::create(kids[n_kids-2], kids[n_kids-1]);
5: branch 0 taken
200: branch 1 taken
448 205: for (int i=n_kids-3; i>=0; i--)
449 5: r = ConcatExpr::create(kids[i], r);
450 400: return r;
451 : }
452 :
453 : /// Shortcut to concat 4 kids. The chain returned is unbalanced to the right
454 : ref<Expr> ConcatExpr::create4(const ref<Expr> &kid1, const ref<Expr> &kid2,
455 2124763: const ref<Expr> &kid3, const ref<Expr> &kid4) {
456 2124763: return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3, kid4)));
457 : }
458 :
459 : /// Shortcut to concat 8 kids. The chain returned is unbalanced to the right
460 : ref<Expr> ConcatExpr::create8(const ref<Expr> &kid1, const ref<Expr> &kid2,
461 : const ref<Expr> &kid3, const ref<Expr> &kid4,
462 : const ref<Expr> &kid5, const ref<Expr> &kid6,
463 193: const ref<Expr> &kid7, const ref<Expr> &kid8) {
464 : return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3,
465 193: ConcatExpr::create(kid4, ConcatExpr::create4(kid5, kid6, kid7, kid8)))));
466 : }
467 :
468 : /***/
469 :
470 40064: ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
471 40064: unsigned kw = expr.getWidth();
40064: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
40064: branch 3 taken
472 40064: assert(w > 0 && off + w <= kw && "invalid extract");
473 :
4453: branch 0 taken
35611: branch 1 taken
474 40064: if (w == kw)
475 4453: return expr;
11130: branch 1 taken
24481: branch 2 taken
476 35611: else if (expr.isConstant()) {
477 33390: return ConstantExpr::create(ints::trunc(expr.getConstantValue() >> off, w, kw), w);
478 : }
479 : else
480 : // Extract(Concat)
388: branch 0 taken
24093: branch 1 taken
481 24481: if (ConcatExpr *ce = dyn_ref_cast<ConcatExpr>(expr)) {
482 : // if the extract skips the right side of the concat
126: branch 2 taken
262: branch 3 taken
483 388: if (off >= ce->getRight().getWidth())
484 378: return ExtractExpr::create(ce->getLeft(), off - ce->getRight().getWidth(), w);
485 :
486 : // if the extract skips the left side of the concat
253: branch 2 taken
9: branch 3 taken
487 524: if (off + w <= ce->getRight().getWidth())
488 506: return ExtractExpr::create(ce->getRight(), off, w);
489 :
490 : // E(C(x,y)) = C(E(x), E(y))
491 : return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1).getWidth() + off),
492 9: ExtractExpr::create(ce->getKid(1), off, ce->getKid(1).getWidth() - off));
493 : }
494 :
495 48186: return ExtractExpr::alloc(expr, off, w);
496 : }
497 :
498 :
499 26356: ref<Expr> ExtractExpr::createByteOff(ref<Expr> expr, unsigned offset, Width bits) {
500 52712: return ExtractExpr::create(expr, 8*offset, bits);
501 : }
502 :
503 : /***/
504 :
505 37907: ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
506 37907: unsigned kBits = e.getWidth();
27611: branch 0 taken
10296: branch 1 taken
507 37907: if (w == kBits) {
508 27611: return e;
263: branch 0 taken
10033: branch 1 taken
509 10296: } else if (w < kBits) { // trunc
510 526: return ExtractExpr::createByteOff(e, 0, w);
511 : } else {
8783: branch 1 taken
1250: branch 2 taken
512 10033: if (e.isConstant()) {
513 : return ConstantExpr::create(ints::zext(e.getConstantValue(), w, kBits),
514 26349: w);
515 : }
516 :
517 2500: return ZExtExpr::alloc(e, w);
518 : }
519 : }
520 :
521 583: ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
522 583: unsigned kBits = e.getWidth();
0: branch 0 not taken
583: branch 1 taken
523 583: if (w == kBits) {
524 0: return e;
0: branch 0 not taken
583: branch 1 taken
525 583: } else if (w < kBits) { // trunc
526 0: return ExtractExpr::createByteOff(e, 0, w);
527 : } else {
517: branch 1 taken
66: branch 2 taken
528 583: if (e.isConstant()) {
529 : return ConstantExpr::create(ints::sext(e.getConstantValue(), w, kBits),
530 1551: w);
531 : }
532 :
533 132: return SExtExpr::alloc(e, w);
534 : }
535 : }
536 :
537 : /***/
538 :
539 : static ref<Expr> AndExpr_create(Expr *l, Expr *r);
540 : static ref<Expr> XorExpr_create(Expr *l, Expr *r);
541 :
542 : static ref<Expr> EqExpr_createPartial(Expr *l, const ref<Expr> &cr);
543 : static ref<Expr> AndExpr_createPartialR(const ref<Expr> &cl, Expr *r);
544 : static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r);
545 : static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r);
546 :
547 935: static ref<Expr> AddExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
0: branch 1 not taken
935: branch 2 taken
548 935: assert(cl.isConstant() && "non-constant passed in place of constant");
549 935: uint64_t value = cl.getConstantValue();
550 935: Expr::Width type = cl.getWidth();
551 :
15: branch 0 taken
920: branch 1 taken
552 935: if (type==Expr::Bool) {
553 15: return XorExpr_createPartialR(cl, r);
162: branch 0 taken
758: branch 1 taken
554 920: } else if (!value) {
555 162: return r;
556 : } else {
557 758: Expr::Kind rk = r->getKind();
153: branch 0 taken
605: branch 1 taken
153: branch 4 taken
0: branch 5 not taken
153: branch 6 taken
605: branch 7 taken
153: branch 9 taken
605: branch 10 taken
558 758: if (rk==Expr::Add && r->getKid(0).isConstant()) { // A + (B+c) == (A+B) + c
559 : return AddExpr::create(AddExpr::create(cl, r->getKid(0)),
560 153: r->getKid(1));
0: branch 0 not taken
605: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
605: branch 7 taken
0: branch 9 not taken
605: branch 10 taken
561 605: } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // A + (B-c) == (A+B) - c
562 : return SubExpr::create(AddExpr::create(cl, r->getKid(0)),
563 0: r->getKid(1));
564 : } else {
565 1210: return AddExpr::alloc(cl, r);
566 : }
567 : }
568 : }
569 : static ref<Expr> AddExpr_createPartial(Expr *l, const ref<Expr> &cr) {
570 671: return AddExpr_createPartialR(cr, l);
571 : }
572 25: static ref<Expr> AddExpr_create(Expr *l, Expr *r) {
573 25: Expr::Width type = l->getWidth();
574 :
5: branch 0 taken
20: branch 1 taken
575 25: if (type == Expr::Bool) {
576 5: return XorExpr_create(l, r);
577 : } else {
578 20: Expr::Kind lk = l->getKind(), rk = r->getKind();
0: branch 0 not taken
20: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
20: branch 7 taken
0: branch 9 not taken
20: branch 10 taken
579 20: if (lk==Expr::Add && l->getKid(0).isConstant()) { // (k+a)+b = k+(a+b)
580 : return AddExpr::create(l->getKid(0),
581 0: AddExpr::create(l->getKid(1), r));
0: branch 0 not taken
20: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
20: branch 7 taken
0: branch 9 not taken
20: branch 10 taken
582 20: } else if (lk==Expr::Sub && l->getKid(0).isConstant()) { // (k-a)+b = k+(b-a)
583 : return AddExpr::create(l->getKid(0),
584 0: SubExpr::create(r, l->getKid(1)));
0: branch 0 not taken
20: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
20: branch 7 taken
0: branch 9 not taken
20: branch 10 taken
585 20: } else if (rk==Expr::Add && r->getKid(0).isConstant()) { // a + (k+b) = k+(a+b)
586 : return AddExpr::create(r->getKid(0),
587 0: AddExpr::create(l, r->getKid(1)));
0: branch 0 not taken
20: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
20: branch 7 taken
0: branch 9 not taken
20: branch 10 taken
588 20: } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // a + (k-b) = k+(a-b)
589 : return AddExpr::create(r->getKid(0),
590 0: SubExpr::create(l, r->getKid(1)));
591 : } else {
592 40: return AddExpr::alloc(l, r);
593 : }
594 : }
595 : }
596 :
597 50: static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
0: branch 1 not taken
50: branch 2 taken
598 50: assert(cl.isConstant() && "non-constant passed in place of constant");
599 50: Expr::Width type = cl.getWidth();
600 :
5: branch 0 taken
45: branch 1 taken
601 50: if (type==Expr::Bool) {
602 5: return XorExpr_createPartialR(cl, r);
603 : } else {
604 45: Expr::Kind rk = r->getKind();
0: branch 0 not taken
45: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
45: branch 7 taken
0: branch 9 not taken
45: branch 10 taken
605 45: if (rk==Expr::Add && r->getKid(0).isConstant()) { // A - (B+c) == (A-B) - c
606 : return SubExpr::create(SubExpr::create(cl, r->getKid(0)),
607 0: r->getKid(1));
6: branch 0 taken
39: branch 1 taken
6: branch 4 taken
0: branch 5 not taken
6: branch 6 taken
39: branch 7 taken
6: branch 9 taken
39: branch 10 taken
608 45: } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // A - (B-c) == (A-B) + c
609 : return AddExpr::create(SubExpr::create(cl, r->getKid(0)),
610 6: r->getKid(1));
611 : } else {
612 78: return SubExpr::alloc(cl, r);
613 : }
614 : }
615 : }
616 230: static ref<Expr> SubExpr_createPartial(Expr *l, const ref<Expr> &cr) {
0: branch 1 not taken
230: branch 2 taken
617 230: assert(cr.isConstant() && "non-constant passed in place of constant");
618 230: uint64_t value = cr.getConstantValue();
619 230: Expr::Width width = cr.getWidth();
620 230: uint64_t nvalue = ints::sub(0, value, width);
621 :
622 460: return AddExpr_createPartial(l, ConstantExpr::create(nvalue, width));
623 : }
624 77: static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
625 77: Expr::Width type = l->getWidth();
626 :
5: branch 0 taken
72: branch 1 taken
627 77: if (type == Expr::Bool) {
628 5: return XorExpr_create(l, r);
26: branch 0 taken
46: branch 1 taken
629 72: } else if (*l==*r) {
630 26: return ref<Expr>(0, type);
631 : } else {
632 46: Expr::Kind lk = l->getKind(), rk = r->getKind();
0: branch 0 not taken
46: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
46: branch 7 taken
0: branch 9 not taken
46: branch 10 taken
633 46: if (lk==Expr::Add && l->getKid(0).isConstant()) { // (k+a)-b = k+(a-b)
634 : return AddExpr::create(l->getKid(0),
635 0: SubExpr::create(l->getKid(1), r));
0: branch 0 not taken
46: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
46: branch 7 taken
0: branch 9 not taken
46: branch 10 taken
636 46: } else if (lk==Expr::Sub && l->getKid(0).isConstant()) { // (k-a)-b = k-(a+b)
637 : return SubExpr::create(l->getKid(0),
638 0: AddExpr::create(l->getKid(1), r));
26: branch 0 taken
20: branch 1 taken
26: branch 4 taken
0: branch 5 not taken
26: branch 6 taken
20: branch 7 taken
26: branch 9 taken
20: branch 10 taken
639 46: } else if (rk==Expr::Add && r->getKid(0).isConstant()) { // a - (k+b) = (a-c) - k
640 : return SubExpr::create(SubExpr::create(l, r->getKid(1)),
641 52: r->getKid(0));
0: branch 0 not taken
20: branch 1 taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
20: branch 7 taken
0: branch 9 not taken
20: branch 10 taken
642 20: } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // a - (k-b) = (a+b) - k
643 : return SubExpr::create(AddExpr::create(l, r->getKid(1)),
644 0: r->getKid(0));
645 : } else {
646 40: return SubExpr::alloc(l, r);
647 : }
648 : }
649 : }
650 :
651 84: static ref<Expr> MulExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
0: branch 1 not taken
84: branch 2 taken
652 84: assert(cl.isConstant() && "non-constant passed in place of constant");
653 84: uint64_t value = cl.getConstantValue();
654 84: Expr::Width type = cl.getWidth();
655 :
0: branch 0 not taken
84: branch 1 taken
656 84: if (type == Expr::Bool) {
657 0: return AndExpr_createPartialR(cl, r);
44: branch 0 taken
40: branch 1 taken
658 84: } else if (value == 1) {
659 44: return r;
2: branch 0 taken
38: branch 1 taken
660 40: } else if (!value) {
661 2: return cl;
662 : } else {
663 76: return MulExpr::alloc(cl, r);
664 : }
665 : }
666 : static ref<Expr> MulExpr_createPartial(Expr *l, const ref<Expr> &cr) {
667 79: return MulExpr_createPartialR(cr, l);
668 : }
669 5: static ref<Expr> MulExpr_create(Expr *l, Expr *r) {
670 5: Expr::Width type = l->getWidth();
671 :
0: branch 0 not taken
5: branch 1 taken
672 5: if (type == Expr::Bool) {
673 0: return AndExpr::alloc(l, r);
674 : } else {
675 10: return MulExpr::alloc(l, r);
676 : }
677 : }
678 :
679 737: static ref<Expr> AndExpr_createPartial(Expr *l, const ref<Expr> &cr) {
0: branch 1 not taken
737: branch 2 taken
680 737: assert(cr.isConstant() && "non-constant passed in place of constant");
681 737: uint64_t value = cr.getConstantValue();
682 737: Expr::Width width = cr.getWidth();;
683 :
389: branch 0 taken
348: branch 1 taken
684 737: if (value==ints::sext(1, width, 1)) {
685 389: return l;
210: branch 0 taken
138: branch 1 taken
686 348: } else if (!value) {
687 210: return cr;
688 : } else {
689 276: return AndExpr::alloc(l, cr);
690 : }
691 : }
692 : static ref<Expr> AndExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
693 311: return AndExpr_createPartial(r, cl);
694 : }
695 : static ref<Expr> AndExpr_create(Expr *l, Expr *r) {
696 8810: return AndExpr::alloc(l, r);
697 : }
698 :
699 434: static ref<Expr> OrExpr_createPartial(Expr *l, const ref<Expr> &cr) {
0: branch 1 not taken
434: branch 2 taken
700 434: assert(cr.isConstant() && "non-constant passed in place of constant");
701 434: uint64_t value = cr.getConstantValue();
702 434: Expr::Width width = cr.getWidth();
703 :
34: branch 0 taken
400: branch 1 taken
704 434: if (value == ints::sext(1, width, 1)) {
705 34: return cr;
375: branch 0 taken
25: branch 1 taken
706 400: } else if (!value) {
707 375: return l;
708 : } else {
709 50: return OrExpr::alloc(l, cr);
710 : }
711 : }
712 : static ref<Expr> OrExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
713 78: return OrExpr_createPartial(r, cl);
714 : }
715 : static ref<Expr> OrExpr_create(Expr *l, Expr *r) {
716 2402: return OrExpr::alloc(l, r);
717 : }
718 :
719 74: static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
0: branch 1 not taken
74: branch 2 taken
720 74: assert(cl.isConstant() && "non-constant passed in place of constant");
721 74: uint64_t value = cl.getConstantValue();
722 74: Expr::Width type = cl.getWidth();
723 :
30: branch 0 taken
44: branch 1 taken
724 74: if (type==Expr::Bool) {
18: branch 0 taken
12: branch 1 taken
725 30: if (value) {
726 36: return EqExpr_createPartial(r, ConstantExpr::create(0, Expr::Bool));
727 : } else {
728 12: return r;
729 : }
8: branch 0 taken
36: branch 1 taken
730 44: } else if (!value) {
731 8: return r;
732 : } else {
733 72: return XorExpr::alloc(cl, r);
734 : }
735 : }
736 :
737 : static ref<Expr> XorExpr_createPartial(Expr *l, const ref<Expr> &cr) {
738 27: return XorExpr_createPartialR(cr, l);
739 : }
740 35: static ref<Expr> XorExpr_create(Expr *l, Expr *r) {
741 70: return XorExpr::alloc(l, r);
742 : }
743 :
744 : static ref<Expr> UDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
13: branch 2 taken
745 13: if (l.getWidth() == Expr::Bool) { // r must be 1
746 0: return l;
747 : } else{
748 13: return UDivExpr::alloc(l, r);
749 : }
750 : }
751 :
752 : static ref<Expr> SDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
15: branch 2 taken
753 15: if (l.getWidth() == Expr::Bool) { // r must be 1
754 0: return l;
755 : } else{
756 15: return SDivExpr::alloc(l, r);
757 : }
758 : }
759 :
760 12: static ref<Expr> URemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
12: branch 2 taken
761 12: if (l.getWidth() == Expr::Bool) { // r must be 1
762 0: return ConstantExpr::create(0, Expr::Bool);
763 : } else{
764 24: return URemExpr::alloc(l, r);
765 : }
766 : }
767 :
768 12: static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
12: branch 2 taken
769 12: if (l.getWidth() == Expr::Bool) { // r must be 1
770 0: return ConstantExpr::create(0, Expr::Bool);
771 : } else{
772 24: return SRemExpr::alloc(l, r);
773 : }
774 : }
775 :
776 81: static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
81: branch 2 taken
777 81: if (l.getWidth() == Expr::Bool) { // l & !r
778 0: return AndExpr::create(l, Expr::createNot(r));
779 : } else{
780 162: return ShlExpr::alloc(l, r);
781 : }
782 : }
783 :
784 105: static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
105: branch 2 taken
785 105: if (l.getWidth() == Expr::Bool) { // l & !r
786 0: return AndExpr::create(l, Expr::createNot(r));
787 : } else{
788 210: return LShrExpr::alloc(l, r);
789 : }
790 : }
791 :
792 : static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
0: branch 1 not taken
60: branch 2 taken
793 60: if (l.getWidth() == Expr::Bool) { // l
794 0: return l;
795 : } else{
796 60: return AShrExpr::alloc(l, r);
797 : }
798 : }
799 :
800 : #define BCREATE_R(_e_op, _op, partialL, partialR) \
801 : ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
802 : assert(l.getWidth()==r.getWidth() && "type mismatch"); \
803 : if (l.isConstant()) { \
804 : if (r.isConstant()) { \
805 : Expr::Width width = l.getWidth(); \
806 : uint64_t val = ints::_op(l.getConstantValue(), \
807 : r.getConstantValue(), width); \
808 : return ConstantExpr::create(val, width); \
809 : } else { \
810 : return _e_op ## _createPartialR(l, r.get()); \
811 : } \
812 : } else if (r.isConstant()) { \
813 : return _e_op ## _createPartial(l.get(), r); \
814 : } \
815 : return _e_op ## _create(l.get(), r.get()); \
816 : }
817 :
818 : #define BCREATE(_e_op, _op) \
819 : ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
820 : assert(l.getWidth()==r.getWidth() && "type mismatch"); \
821 : if (l.isConstant()) { \
822 : if (r.isConstant()) { \
823 : Expr::Width width = l.getWidth(); \
824 : uint64_t val = ints::_op(l.getConstantValue(), \
825 : r.getConstantValue(), width); \
826 : return ConstantExpr::create(val, width); \
827 : } \
828 : } \
829 : return _e_op ## _create(l, r); \
830 : }
831 :
0: branch 2 not taken
1182654: branch 3 taken
1182188: branch 6 taken
466: branch 7 taken
1181924: branch 9 taken
264: branch 10 taken
441: branch 19 taken
25: branch 20 taken
832 3546527: BCREATE_R(AddExpr, add, AddExpr_createPartial, AddExpr_createPartialR)
0: branch 2 not taken
3408982: branch 3 taken
3408675: branch 6 taken
307: branch 7 taken
3408625: branch 9 taken
50: branch 10 taken
230: branch 19 taken
77: branch 20 taken
833 10226232: BCREATE_R(SubExpr, sub, SubExpr_createPartial, SubExpr_createPartialR)
0: branch 2 not taken
27245: branch 3 taken
27161: branch 6 taken
84: branch 7 taken
27156: branch 9 taken
5: branch 10 taken
79: branch 19 taken
5: branch 20 taken
834 81562: BCREATE_R(MulExpr, mul, MulExpr_createPartial, MulExpr_createPartialR)
0: branch 2 not taken
11444: branch 3 taken
6613: branch 6 taken
4831: branch 7 taken
6302: branch 9 taken
311: branch 10 taken
426: branch 18 taken
4405: branch 19 taken
835 33284: BCREATE_R(AndExpr, land, AndExpr_createPartial, AndExpr_createPartialR)
0: branch 2 not taken
6854: branch 3 taken
5297: branch 6 taken
1557: branch 7 taken
5219: branch 9 taken
78: branch 10 taken
356: branch 18 taken
1201: branch 19 taken
836 20050: BCREATE_R(OrExpr, lor, OrExpr_createPartial, OrExpr_createPartialR)
0: branch 2 not taken
250: branch 3 taken
198: branch 6 taken
52: branch 7 taken
171: branch 9 taken
27: branch 10 taken
27: branch 19 taken
25: branch 20 taken
837 617: BCREATE_R(XorExpr, lxor, XorExpr_createPartial, XorExpr_createPartialR)
0: branch 2 not taken
18: branch 3 taken
9: branch 6 taken
9: branch 7 taken
5: branch 9 taken
4: branch 10 taken
838 28: BCREATE(UDivExpr, udiv)
0: branch 2 not taken
27: branch 3 taken
16: branch 6 taken
11: branch 7 taken
12: branch 9 taken
4: branch 10 taken
839 51: BCREATE(SDivExpr, sdiv)
0: branch 2 not taken
16: branch 3 taken
8: branch 6 taken
8: branch 7 taken
4: branch 9 taken
4: branch 10 taken
840 24: BCREATE(URemExpr, urem)
0: branch 2 not taken
12: branch 3 taken
4: branch 6 taken
8: branch 7 taken
0: branch 9 not taken
4: branch 10 taken
841 12: BCREATE(SRemExpr, srem)
0: branch 2 not taken
523: branch 3 taken
467: branch 6 taken
56: branch 7 taken
442: branch 9 taken
25: branch 10 taken
842 1407: BCREATE(ShlExpr, shl)
0: branch 2 not taken
676: branch 3 taken
591: branch 6 taken
85: branch 7 taken
571: branch 9 taken
20: branch 10 taken
843 1818: BCREATE(LShrExpr, lshr)
0: branch 2 not taken
60: branch 3 taken
20: branch 6 taken
40: branch 7 taken
0: branch 9 not taken
20: branch 10 taken
844 60: BCREATE(AShrExpr, ashr)
845 :
846 : #define CMPCREATE(_e_op, _op) \
847 : ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
848 : assert(l.getWidth()==r.getWidth() && "type mismatch"); \
849 : reduce(&l, &r); \
850 : if (l.isConstant()) { \
851 : if (r.isConstant()) { \
852 : Expr::Width width = l.getWidth(); \
853 : uint64_t val = ints::_op(l.getConstantValue(), \
854 : r.getConstantValue(), width); \
855 : return ConstantExpr::create(val, Expr::Bool); \
856 : } \
857 : } \
858 : return _e_op ## _create(l, r); \
859 : }
860 :
861 : #define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR) \
862 : ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
863 : assert(l.getWidth()==r.getWidth() && "type mismatch"); \
864 : if (l.isConstant()) { \
865 : if (r.isConstant()) { \
866 : Expr::Width width = l.getWidth(); \
867 : uint64_t val = ints::_op(l.getConstantValue(), \
868 : r.getConstantValue(), width); \
869 : return ConstantExpr::create(val, Expr::Bool); \
870 : } else { \
871 : return partialR(l, r.get()); \
872 : } \
873 : } else if (r.isConstant()) { \
874 : return partialL(l.get(), r); \
875 : } else { \
876 : return _e_op ## _create(l.get(), r.get()); \
877 : } \
878 : }
879 :
880 :
881 18542: static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
1: branch 0 taken
18541: branch 1 taken
882 18542: if (l == r) {
883 1: return ref<Expr>(1, Expr::Bool);
884 : } else {
885 37082: return EqExpr::alloc(l, r);
886 : }
887 : }
888 :
889 :
890 : /// Tries to optimize EqExpr cl == rd, where cl is a ConstantExpr and
891 : /// rd a ReadExpr. If rd is a read into an all-constant array,
892 : /// returns a disjunction of equalities on the index. Otherwise,
893 : /// returns the initial equality expression.
894 : static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
895 16: ReadExpr *rd) {
0: branch 1 not taken
16: branch 2 taken
896 16: assert(cl.isConstant() && "constant expression required");
0: branch 1 not taken
16: branch 2 taken
897 16: assert(rd->getKind() == Expr::Read && "read expression required");
898 :
899 16: uint64_t ct = cl.getConstantValue();
900 : ref<Expr> first_idx_match;
901 :
902 : // number of positions in the array that contain value ct
903 16: unsigned matches = 0;
904 :
905 : //llvm::cerr << "Size updates/root: " << rd->updates.getSize() << " / " << (rd->updates.root)->size << "\n";
906 :
907 : // for now, just assume standard "flushing" of a concrete array,
908 : // where the concrete array has one update for each index, in order
909 16: bool all_const = true;
16: branch 0 taken
0: branch 1 not taken
910 32: if (rd->updates.getSize() == (rd->updates.root)->size) {
911 32: unsigned k = rd->updates.getSize();
131072: branch 4 taken
16: branch 5 taken
912 262176: for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
0: branch 0 not taken
131072: branch 1 taken
913 131072: assert(k > 0);
914 131072: k--;
915 :
916 131072: ref<Expr> idx = un->index;
917 131072: ref<Expr> val = un->value;
131072: branch 1 taken
0: branch 2 not taken
0: branch 4 not taken
131072: branch 5 taken
0: branch 6 not taken
131072: branch 7 taken
918 131072: if (!idx.isConstant() || !val.isConstant()) {
919 0: all_const = false;
920 : //llvm::cerr << "Idx or val not constant\n";
921 0: break;
922 : }
923 : else {
0: branch 1 not taken
131072: branch 2 taken
924 131072: if (idx.getConstantValue() != k) {
925 0: all_const = false;
926 : //llvm::cerr << "Wrong constant\n";
927 : break;
928 : }
512: branch 1 taken
130560: branch 2 taken
929 131072: if (val.getConstantValue() == ct) {
930 512: matches++;
16: branch 0 taken
496: branch 1 taken
931 512: if (matches == 1)
932 16: first_idx_match = un->index;
933 : }
934 : }
935 : }
936 : }
937 0: else all_const = false;
938 :
16: branch 0 taken
0: branch 1 not taken
16: branch 2 taken
0: branch 3 not taken
939 16: if (all_const && matches <= 100) {
940 : // apply optimization
941 : //llvm::cerr << "\n\n=== Applying const array optimization ===\n\n";
942 :
0: branch 0 not taken
16: branch 1 taken
943 16: if (matches == 0)
944 0: return ref<Expr>(0, Expr::Bool);
945 :
946 16: ref<Expr> res = EqExpr::create(first_idx_match, rd->index);
0: branch 0 not taken
16: branch 1 taken
947 16: if (matches == 1)
948 0: return res;
949 :
131072: branch 0 taken
16: branch 1 taken
950 131088: for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
131056: branch 0 taken
16: branch 1 taken
496: branch 3 taken
130560: branch 4 taken
496: branch 5 taken
130576: branch 6 taken
951 262144: if (un->index != first_idx_match && un->value.getConstantValue() == ct) {
952 496: ref<Expr> curr_eq = EqExpr::create(un->index, rd->index);
953 496: res = OrExpr::create(curr_eq, res);
954 : }
955 : }
956 :
957 32: return res;
958 : }
959 :
960 0: return EqExpr_create(cl, ref<Expr>(rd));
961 : }
962 :
963 :
964 26238: static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
0: branch 1 not taken
26238: branch 2 taken
965 26238: assert(cl.isConstant() && "non-constant passed in place of constant");
966 26238: uint64_t value = cl.getConstantValue();
967 26238: Expr::Width width = cl.getWidth();
968 :
969 26238: Expr::Kind rk = r->getKind();
19010: branch 0 taken
7228: branch 1 taken
970 26238: if (width == Expr::Bool) {
173: branch 0 taken
18837: branch 1 taken
971 19010: if (value) {
972 173: return r;
973 : } else {
974 : // 0 != ...
975 :
13547: branch 0 taken
5290: branch 1 taken
976 18837: if (rk == Expr::Eq) {
977 13547: const EqExpr *ree = static_ref_cast<EqExpr>(r);
978 :
979 : // eliminate double negation
10960: branch 1 taken
2587: branch 2 taken
3175: branch 4 taken
7785: branch 5 taken
3175: branch 6 taken
10372: branch 7 taken
980 13547: if (ree->left.isConstant() &&
981 : ree->left.getWidth()==Expr::Bool) {
0: branch 1 not taken
3175: branch 2 taken
982 3175: assert(!ree->left.getConstantValue());
983 3175: return ree->right;
984 : }
2676: branch 0 taken
2614: branch 1 taken
985 5290: } else if (rk == Expr::Or) {
986 2676: const OrExpr *roe = static_ref_cast<OrExpr>(r);
987 :
988 : // transform not(or(a,b)) to and(not a, not b)
989 : return AndExpr::create(Expr::createNot(roe->left),
990 8028: Expr::createNot(roe->right));
991 : }
992 : }
87: branch 0 taken
7141: branch 1 taken
993 7228: } else if (rk == Expr::SExt) {
994 : // (sext(a,T)==c) == (a==c)
995 87: const SExtExpr *see = static_ref_cast<SExtExpr>(r);
996 87: Expr::Width fromBits = see->src.getWidth();
997 87: uint64_t trunc = bits64::truncateToNBits(value, fromBits);
998 :
999 : // pathological check, make sure it is possible to
1000 : // sext to this value *from any value*
87: branch 0 taken
0: branch 1 not taken
1001 87: if (value == ints::sext(trunc, width, fromBits)) {
1002 174: return EqExpr::create(see->src, ConstantExpr::create(trunc, fromBits));
1003 : } else {
1004 0: return ConstantExpr::create(0, Expr::Bool);
1005 : }
1939: branch 0 taken
5202: branch 1 taken
1006 7141: } else if (rk == Expr::ZExt) {
1007 : // (zext(a,T)==c) == (a==c)
1008 1939: const ZExtExpr *zee = static_ref_cast<ZExtExpr>(r);
1009 1939: Expr::Width fromBits = zee->src.getWidth();
1010 1939: uint64_t trunc = bits64::truncateToNBits(value, fromBits);
1011 :
1012 : // pathological check, make sure it is possible to
1013 : // zext to this value *from any value*
1917: branch 0 taken
22: branch 1 taken
1014 1939: if (value == ints::zext(trunc, width, fromBits)) {
1015 3834: return EqExpr::create(zee->src, ConstantExpr::create(trunc, fromBits));
1016 : } else {
1017 44: return ConstantExpr::create(0, Expr::Bool);
1018 : }
387: branch 0 taken
4815: branch 1 taken
1019 5202: } else if (rk==Expr::Add) {
1020 387: const AddExpr *ae = static_ref_cast<AddExpr>(r);
387: branch 1 taken
0: branch 2 not taken
1021 387: if (ae->left.isConstant()) {
1022 : // c0 = c1 + b => c0 - c1 = b
1023 : return EqExpr_createPartialR(SubExpr::create(cl, ae->left),
1024 387: ae->right.get());
1025 : }
158: branch 0 taken
4657: branch 1 taken
1026 4815: } else if (rk==Expr::Sub) {
1027 158: const SubExpr *se = static_ref_cast<SubExpr>(r);
158: branch 1 taken
0: branch 2 not taken
1028 158: if (se->left.isConstant()) {
1029 : // c0 = c1 - b => c1 - c0 = b
1030 : return EqExpr_createPartialR(SubExpr::create(se->left, cl),
1031 158: se->right.get());
1032 : }
2287: branch 0 taken
2370: branch 1 taken
16: branch 2 taken
2271: branch 3 taken
16: branch 4 taken
4641: branch 5 taken
1033 6944: } else if (rk == Expr::Read && ConstArrayOpt) {
1034 16: return TryConstArrayOpt(cl, static_cast<ReadExpr*>(r));
1035 : }
1036 :
1037 35254: return EqExpr_create(cl, r);
1038 : }
1039 :
1040 : static ref<Expr> EqExpr_createPartial(Expr *l, const ref<Expr> &cr) {
1041 22821: return EqExpr_createPartialR(cr, l);
1042 : }
1043 :
1044 7623: ref<Expr> NeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1045 : return EqExpr::create(ConstantExpr::create(0, Expr::Bool),
1046 15246: EqExpr::create(l, r));
1047 : }
1048 :
1049 442: ref<Expr> UgtExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1050 442: return UltExpr::create(r, l);
1051 : }
1052 229: ref<Expr> UgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1053 229: return UleExpr::create(r, l);
1054 : }
1055 :
1056 630: ref<Expr> SgtExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1057 630: return SltExpr::create(r, l);
1058 : }
1059 303: ref<Expr> SgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1060 303: return SleExpr::create(r, l);
1061 : }
1062 :
1063 : // XXX:FIXME:DRE: this is broken. I am just doing this so can merge.
1064 : // This is just a (broken) hack to eliminate overflow when we add constraints
1065 : // from under-constrained execution.
1066 : #ifndef KLEE_TRACK_REFERENTS
1067 : # define reduce(_c, _x) do { } while(0)
1068 : #else
1069 : // Given: "(X op Y == X op W)" factor out X. Currently "op" just is *
1070 : static void reduce(ref<Expr> *c, ref<Expr> *x) {
1071 : ref<Expr> *t;
1072 :
1073 : if(x->getKind() == Expr::Constant) {
1074 : t = x;
1075 : x = c;
1076 : c = t;
1077 : }
1078 : //llvm::cerr << "Trying to do something smart w/ " << **c << " and " << **x << "\n";
1079 : if(c->getKind() != Expr::Constant)
1080 : return;
1081 : if(x->getKind() != Expr::Mul)
1082 : return;
1083 :
1084 : ref<Expr> k0 = (*x)->getKid(0);
1085 : ref<Expr> k1 = (*x)->getKid(1);
1086 : ref<Expr> mc, mv;
1087 :
1088 : // llvm::cerr << "preconditions a go. k0=" << *k0 << "\n";
1089 : if(k0->getKind() == Expr::Constant) {
1090 : mc = k0;
1091 : mv = k1;
1092 : } else if(k1->getKind() == Expr::Constant) {
1093 : mc = k1;
1094 : mv = k0;
1095 : } else
1096 : return;
1097 :
1098 : assert(mc->getConstantValue() && "Unexpected value");
1099 :
1100 : if(c->getConstantValue() % mc->getConstantValue() == 0) {
1101 : // llvm::cerr << "Simplified: can divide " << **c << " by " << *mc << "\n";
1102 : *c = ConstantExpr::create(
1103 : c->getConstantValue() / mc->getConstantValue(),
1104 : mc->getWidth());
1105 : *x = mv;
1106 : // llvm::cerr << "Got: " << **c << " and " << **x << "\n";
1107 : } // else llvm::cerr << "cannot divide " << **c << " by " << *mc << "\n";
1108 : }
1109 : #endif
1110 :
1111 418: static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
1112 418: Expr::Width t = l.getWidth();
30: branch 0 taken
388: branch 1 taken
1113 418: if (t == Expr::Bool) { // !l && r
1114 60: return AndExpr::create(Expr::createNot(l), r);
1115 : } else {
282: branch 1 taken
106: branch 2 taken
1116 388: if (r.isConstant()) {
1117 282: uint64_t value = r.getConstantValue();
110: branch 0 taken
172: branch 1 taken
1118 282: if (value <= 8) {
1119 : ref<Expr> res(0,Expr::Bool);
377: branch 0 taken
110: branch 1 taken
1120 487: for (unsigned i=0; i<value; i++) {
1121 754: res = OrExpr::create(EqExpr::create(l, ref<Expr>(i,t)), res);
1122 : }
1123 : // llvm::cerr << l << "<" << r << " <=> " << res << "\n";
1124 220: return res;
1125 : }
1126 : }
1127 556: return UltExpr::alloc(l, r);
1128 : }
1129 : }
1130 :
1131 722: static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
30: branch 1 taken
692: branch 2 taken
1132 722: if (l.getWidth() == Expr::Bool) { // !(l && !r)
1133 60: return OrExpr::create(Expr::createNot(l), r);
1134 : } else {
1135 1384: return UleExpr::alloc(l, r);
1136 : }
1137 : }
1138 :
1139 250: static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
30: branch 1 taken
220: branch 2 taken
1140 250: if (l.getWidth() == Expr::Bool) { // l && !r
1141 60: return AndExpr::create(l, Expr::createNot(r));
1142 : } else {
1143 440: return SltExpr::alloc(l, r);
1144 : }
1145 : }
1146 :
1147 163: static ref<Expr> SleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
30: branch 1 taken
133: branch 2 taken
1148 163: if (l.getWidth() == Expr::Bool) { // !(!l && r)
1149 60: return OrExpr::create(l, Expr::createNot(r));
1150 : } else {
1151 266: return SleExpr::alloc(l, r);
1152 : }
1153 : }
1154 :
0: branch 2 not taken
113458: branch 3 taken
89740: branch 6 taken
23718: branch 7 taken
86868: branch 9 taken
2872: branch 10 taken
22803: branch 19 taken
915: branch 20 taken
1155 289939: CMPCREATE_T(EqExpr, eq, EqExpr, EqExpr_createPartial, EqExpr_createPartialR)
0: branch 2 not taken
3407334: branch 3 taken
3406992: branch 6 taken
342: branch 7 taken
3406916: branch 9 taken
76: branch 10 taken
1156 10221166: CMPCREATE(UltExpr, ult)
0: branch 2 not taken
11165: branch 3 taken
10533: branch 6 taken
632: branch 7 taken
10443: branch 9 taken
90: branch 10 taken
1157 32051: CMPCREATE(UleExpr, ule)
0: branch 2 not taken
1638: branch 3 taken
1492: branch 6 taken
146: branch 7 taken
1388: branch 9 taken
104: branch 10 taken
1158 4414: CMPCREATE(SltExpr, slt)
108: branch 0 taken
0: branch 1 not taken
108: branch 2 taken
0: branch 3 not taken
0: branch 6 not taken
827547: branch 7 taken
827435: branch 10 taken
112: branch 11 taken
827384: branch 13 taken
51: branch 14 taken
1159 2482531: CMPCREATE(SleExpr, sle)
Generated: 2009-05-17 22:47 by zcov