klee
MetaSMTBuilder.h
Go to the documentation of this file.
1//===-- MetaSMTBuilder.h ----------------------------------------*- C++ -*-===//
2//
3// The KLEE Symbolic Virtual Machine
4//
5// This file is distributed under the University of Illinois Open Source
6// License. See LICENSE.TXT for details.
7//
8//===----------------------------------------------------------------------===//
9
10#ifndef KLEE_METASMTBUILDER_H
11#define KLEE_METASMTBUILDER_H
12
13#include "ConstantDivision.h"
14
15#include "klee/Config/config.h"
16#include "klee/Expr/ArrayExprHash.h"
17#include "klee/Expr/Expr.h"
18#include "klee/Expr/ExprHashMap.h"
19#include "klee/Expr/ExprPPrinter.h"
20
21#ifdef ENABLE_METASMT
22
23#include "llvm/Support/CommandLine.h"
24
25#include <metaSMT/frontend/Logic.hpp>
26#include <metaSMT/frontend/QF_BV.hpp>
27#include <metaSMT/frontend/Array.hpp>
28
29using namespace metaSMT;
30using namespace metaSMT::logic::QF_BV;
31
32#define DIRECT_CONTEXT
33
34namespace {
35llvm::cl::opt<bool> UseConstructHashMetaSMT(
36 "use-construct-hash-metasmt",
37 llvm::cl::desc("Use hash-consing during metaSMT query construction."),
38 llvm::cl::init(true));
39}
40
41namespace klee {
42
43typedef metaSMT::logic::Predicate<proto::terminal<
44 metaSMT::logic::tag::true_tag>::type> const MetaSMTConstTrue;
45typedef metaSMT::logic::Predicate<proto::terminal<
46 metaSMT::logic::tag::false_tag>::type> const MetaSMTConstFalse;
47typedef metaSMT::logic::Array::array MetaSMTArray;
48
49template <typename SolverContext> class MetaSMTBuilder;
50
51template <typename SolverContext>
52class MetaSMTArrayExprHash
53 : public ArrayExprHash<typename SolverContext::result_type> {
54
55 friend class MetaSMTBuilder<SolverContext>;
56
57public:
58 MetaSMTArrayExprHash(){};
59 virtual ~MetaSMTArrayExprHash(){};
60};
61
62template <typename SolverContext> class MetaSMTBuilder {
63public:
64 MetaSMTBuilder(SolverContext &solver, bool optimizeDivides)
65 : _solver(solver), _optimizeDivides(optimizeDivides){};
66 virtual ~MetaSMTBuilder(){};
67
68 typename SolverContext::result_type construct(ref<Expr> e);
69
70 typename SolverContext::result_type getInitialRead(const Array *root,
71 unsigned index);
72
73 typename SolverContext::result_type getTrue() {
74 return (evaluate(_solver, metaSMT::logic::True));
75 }
76
77 typename SolverContext::result_type getFalse() {
78 return (evaluate(_solver, metaSMT::logic::False));
79 }
80
81 typename SolverContext::result_type bvOne(unsigned width) {
82 return bvZExtConst(width, 1);
83 }
84
85 typename SolverContext::result_type bvZero(unsigned width) {
86 return bvZExtConst(width, 0);
87 }
88
89 typename SolverContext::result_type bvMinusOne(unsigned width) {
90 return bvSExtConst(width, (int64_t)-1);
91 }
92
93 typename SolverContext::result_type bvConst32(unsigned width,
94 uint32_t value) {
95 return (evaluate(_solver, bvuint(value, width)));
96 }
97
98 typename SolverContext::result_type bvConst64(unsigned width,
99 uint64_t value) {
100 return (evaluate(_solver, bvuint(value, width)));
101 }
102
103 typename SolverContext::result_type bvZExtConst(unsigned width,
104 uint64_t value);
105 typename SolverContext::result_type bvSExtConst(unsigned width,
106 uint64_t value);
107
108 // logical left and right shift (not arithmetic)
109 typename SolverContext::result_type
110 bvLeftShift(typename SolverContext::result_type expr, unsigned width,
111 unsigned shift);
112 typename SolverContext::result_type
113 bvRightShift(typename SolverContext::result_type expr, unsigned width,
114 unsigned shift);
115 typename SolverContext::result_type
116 bvVarLeftShift(typename SolverContext::result_type expr,
117 typename SolverContext::result_type shift, unsigned width);
118 typename SolverContext::result_type
119 bvVarRightShift(typename SolverContext::result_type expr,
120 typename SolverContext::result_type shift, unsigned width);
121 typename SolverContext::result_type
122 bvVarArithRightShift(typename SolverContext::result_type expr,
123 typename SolverContext::result_type shift,
124 unsigned width);
125
126 typename SolverContext::result_type getArrayForUpdate(const Array *root,
127 const UpdateNode *un);
128 typename SolverContext::result_type getInitialArray(const Array *root);
129 MetaSMTArray buildArray(unsigned elem_width, unsigned index_width);
130
131private:
132 typedef ExprHashMap<std::pair<typename SolverContext::result_type, unsigned> >
133 MetaSMTExprHashMap;
134 typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter;
135 typedef typename MetaSMTExprHashMap::const_iterator
136 MetaSMTExprHashMapConstIter;
137
138 SolverContext &_solver;
139 bool _optimizeDivides;
140 MetaSMTArrayExprHash<SolverContext> _arr_hash;
141 MetaSMTExprHashMap _constructed;
142
143 typename SolverContext::result_type constructActual(ref<Expr> e,
144 int *width_out);
145 typename SolverContext::result_type construct(ref<Expr> e, int *width_out);
146
147 typename SolverContext::result_type
148 bvBoolExtract(typename SolverContext::result_type expr, int bit);
149 typename SolverContext::result_type
150 bvExtract(typename SolverContext::result_type expr, unsigned top,
151 unsigned bottom);
152 typename SolverContext::result_type
153 eqExpr(typename SolverContext::result_type a,
154 typename SolverContext::result_type b);
155
156 typename SolverContext::result_type
157 constructAShrByConstant(typename SolverContext::result_type expr,
158 unsigned width, unsigned shift,
159 typename SolverContext::result_type isSigned);
160 typename SolverContext::result_type
161 constructMulByConstant(typename SolverContext::result_type expr,
162 unsigned width, uint64_t x);
163 typename SolverContext::result_type
164 constructUDivByConstant(typename SolverContext::result_type expr_n,
165 unsigned width, uint64_t d);
166 typename SolverContext::result_type
167 constructSDivByConstant(typename SolverContext::result_type expr_n,
168 unsigned width, uint64_t d);
169};
170
171template <typename SolverContext>
172typename SolverContext::result_type
173MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root,
174 const UpdateNode *un) {
175
176 if (!un) {
177 return (getInitialArray(root));
178 } else {
179 typename SolverContext::result_type un_expr;
180 bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
181
182 if (!hashed) {
183 un_expr = evaluate(_solver,
184 metaSMT::logic::Array::store(
185 getArrayForUpdate(root, un->next.get()),
186 construct(un->index, 0), construct(un->value, 0)));
187 _arr_hash.hashUpdateNodeExpr(un, un_expr);
188 }
189 return (un_expr);
190 }
191}
192
193template <typename SolverContext>
194typename SolverContext::result_type
195MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root) {
196 assert(root);
197 typename SolverContext::result_type array_expr;
198 bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
199
200 if (!hashed) {
201
202 array_expr =
203 evaluate(_solver, buildArray(root->getRange(), root->getDomain()));
204
205 if (root->isConstantArray()) {
206 for (unsigned i = 0, e = root->size; i != e; ++i) {
207 typename SolverContext::result_type tmp = evaluate(
208 _solver,
209 metaSMT::logic::Array::store(
210 array_expr,
211 construct(ConstantExpr::alloc(i, root->getDomain()), 0),
212 construct(root->constantValues[i], 0)));
213 array_expr = tmp;
214 }
215 }
216 _arr_hash.hashArrayExpr(root, array_expr);
217 }
218
219 return (array_expr);
220}
221
222template <typename SolverContext>
223MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width,
224 unsigned index_width) {
225 return (metaSMT::logic::Array::new_array(elem_width, index_width));
226}
227
228template <typename SolverContext>
229typename SolverContext::result_type
230MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root,
231 unsigned index) {
232 assert(root);
233 assert(false);
234 typename SolverContext::result_type array_exp = getInitialArray(root);
235 typename SolverContext::result_type res =
236 evaluate(_solver, metaSMT::logic::Array::select(
237 array_exp, bvuint(index, root->getDomain())));
238 return (res);
239}
240
241template <typename SolverContext>
242typename SolverContext::result_type
243MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) {
244
245 typename SolverContext::result_type res;
246
247 if (width <= 64) {
248 res = bvConst64(width, value);
249 } else {
250 typename SolverContext::result_type expr = bvConst64(64, value);
251 typename SolverContext::result_type zero = bvConst64(64, 0);
252
253 for (width -= 64; width > 64; width -= 64) {
254 expr = evaluate(_solver, concat(zero, expr));
255 }
256 res = evaluate(_solver, concat(bvConst64(width, 0), expr));
257 }
258
259 return (res);
260}
261
262template <typename SolverContext>
263typename SolverContext::result_type
264MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) {
265
266 typename SolverContext::result_type res;
267
268 if (width <= 64) {
269 res = bvConst64(width, value);
270 } else {
271 // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend
272 // arguments
273 res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value)));
274 }
275 return (res);
276}
277
278template <typename SolverContext>
279typename SolverContext::result_type
280MetaSMTBuilder<SolverContext>::bvBoolExtract(
281 typename SolverContext::result_type expr, int bit) {
282 return (evaluate(_solver,
283 metaSMT::logic::equal(extract(bit, bit, expr), bvOne(1))));
284}
285
286template <typename SolverContext>
287typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(
288 typename SolverContext::result_type expr, unsigned top, unsigned bottom) {
289 return (evaluate(_solver, extract(top, bottom, expr)));
290}
291
292template <typename SolverContext>
293typename SolverContext::result_type
294MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a,
295 typename SolverContext::result_type b) {
296 return (evaluate(_solver, metaSMT::logic::equal(a, b)));
297}
298
299template <typename SolverContext>
300typename SolverContext::result_type
301MetaSMTBuilder<SolverContext>::constructAShrByConstant(
302 typename SolverContext::result_type expr, unsigned width, unsigned shift,
303 typename SolverContext::result_type isSigned) {
304 typename SolverContext::result_type res;
305
306 if (shift == 0) {
307 res = expr;
308 } else if (shift >= width) {
309 res = bvZero(width);
310 } else {
311 res = evaluate(
312 _solver,
313 metaSMT::logic::Ite(isSigned, concat(bvMinusOne(shift),
314 bvExtract(expr, width - 1, shift)),
315 bvRightShift(expr, width, shift)));
316 }
317
318 return (res);
319}
320
321// width is the width of expr; x -- number of bits to shift with
322template <typename SolverContext>
323typename SolverContext::result_type
324MetaSMTBuilder<SolverContext>::constructMulByConstant(
325 typename SolverContext::result_type expr, unsigned width, uint64_t x) {
326
327 uint64_t add, sub;
328 typename SolverContext::result_type res;
329 bool first = true;
330
331 // expr*x == expr*(add-sub) == expr*add - expr*sub
332 ComputeMultConstants64(x, add, sub);
333
334 // legal, these would overflow completely
335 add = bits64::truncateToNBits(add, width);
336 sub = bits64::truncateToNBits(sub, width);
337
338 for (int j = 63; j >= 0; j--) {
339 uint64_t bit = 1LL << j;
340
341 if ((add & bit) || (sub & bit)) {
342 assert(!((add & bit) && (sub & bit)) && "invalid mult constants");
343
344 typename SolverContext::result_type op = bvLeftShift(expr, width, j);
345
346 if (add & bit) {
347 if (!first) {
348 res = evaluate(_solver, bvadd(res, op));
349 } else {
350 res = op;
351 first = false;
352 }
353 } else {
354 if (!first) {
355 res = evaluate(_solver, bvsub(res, op));
356 } else {
357 // To reconsider: vc_bvUMinusExpr in STP
358 res = evaluate(_solver, bvsub(bvZero(width), op));
359 first = false;
360 }
361 }
362 }
363 }
364
365 if (first) {
366 res = bvZero(width);
367 }
368
369 return (res);
370}
371
372/*
373 * Compute the 32-bit unsigned integer division of n by a divisor d based on
374 * the constants derived from the constant divisor d.
375 *
376 * Returns n/d without doing explicit division. The cost is 2 adds, 3 shifts,
377 * and a (64-bit) multiply.
378 *
379 * @param expr_n numerator (dividend) n as an expression
380 * @param width number of bits used to represent the value
381 * @param d the divisor
382 *
383 * @return n/d without doing explicit division
384 */
385template <typename SolverContext>
386typename SolverContext::result_type
387MetaSMTBuilder<SolverContext>::constructUDivByConstant(
388 typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
389
390 assert(width == 32 && "can only compute udiv constants for 32-bit division");
391
392 // Compute the constants needed to compute n/d for constant d without division
393 // by d.
394 uint32_t mprime, sh1, sh2;
395 ComputeUDivConstants32(d, mprime, sh1, sh2);
396 typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1);
397 typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2);
398
399 // t1 = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
400 typename SolverContext::result_type expr_n_64 =
401 evaluate(_solver, concat(bvZero(32), expr_n)); // extend to 64 bits
402 typename SolverContext::result_type t1_64bits =
403 constructMulByConstant(expr_n_64, 64, (uint64_t)mprime);
404 typename SolverContext::result_type t1 =
405 bvExtract(t1_64bits, 63, 32); // upper 32 bits
406
407 // n/d = (((n - t1) >> sh1) + t1) >> sh2;
408 typename SolverContext::result_type n_minus_t1 =
409 evaluate(_solver, bvsub(expr_n, t1));
410 typename SolverContext::result_type shift_sh1 =
411 bvVarRightShift(n_minus_t1, expr_sh1, 32);
412 typename SolverContext::result_type plus_t1 =
413 evaluate(_solver, bvadd(shift_sh1, t1));
414 typename SolverContext::result_type res =
415 bvVarRightShift(plus_t1, expr_sh2, 32);
416
417 return (res);
418}
419
420/*
421 * Compute the 32-bitnsigned integer division of n by a divisor d based on
422 * the constants derived from the constant divisor d.
423 *
424 * Returns n/d without doing explicit division. The cost is 3 adds, 3 shifts,
425 * a (64-bit) multiply, and an XOR.
426 *
427 * @param n numerator (dividend) as an expression
428 * @param width number of bits used to represent the value
429 * @param d the divisor
430 *
431 * @return n/d without doing explicit division
432 */
433template <typename SolverContext>
434typename SolverContext::result_type
435MetaSMTBuilder<SolverContext>::constructSDivByConstant(
436 typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
437
438 assert(width == 32 && "can only compute udiv constants for 32-bit division");
439
440 // Compute the constants needed to compute n/d for constant d w/o division by
441 // d.
442 int32_t mprime, dsign, shpost;
443 ComputeSDivConstants32(d, mprime, dsign, shpost);
444 typename SolverContext::result_type expr_dsign = bvConst32(32, dsign);
445 typename SolverContext::result_type expr_shpost = bvConst32(64, shpost);
446
447 // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
448 int64_t mprime_64 = (int64_t)mprime;
449
450 // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend
451 // arguments
452 typename SolverContext::result_type expr_n_64 =
453 evaluate(_solver, sign_extend(64 - width, expr_n));
454 typename SolverContext::result_type mult_64 =
455 constructMulByConstant(expr_n_64, 64, mprime_64);
456 typename SolverContext::result_type mulsh =
457 bvExtract(mult_64, 63, 32); // upper 32-bits
458 typename SolverContext::result_type n_plus_mulsh =
459 evaluate(_solver, bvadd(expr_n, mulsh));
460
461 // Improved variable arithmetic right shift: sign extend, shift, extract.
462 typename SolverContext::result_type extend_npm =
463 evaluate(_solver, sign_extend(64 - width, n_plus_mulsh));
464 typename SolverContext::result_type shift_npm =
465 bvVarRightShift(extend_npm, expr_shpost, 64);
466 typename SolverContext::result_type shift_shpost =
467 bvExtract(shift_npm, 31, 0); // lower 32-bits
468
470
471 // XSIGN(n) is -1 if n is negative, positive one otherwise
472 typename SolverContext::result_type is_signed = bvBoolExtract(expr_n, 31);
473 typename SolverContext::result_type neg_one = bvMinusOne(32);
474 typename SolverContext::result_type xsign_of_n =
475 evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32)));
476
477 // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
478 typename SolverContext::result_type q0 =
479 evaluate(_solver, bvsub(shift_shpost, xsign_of_n));
480
481 // n/d = (q0 ^ dsign) - dsign
482 typename SolverContext::result_type q0_xor_dsign =
483 evaluate(_solver, bvxor(q0, expr_dsign));
484 typename SolverContext::result_type res =
485 evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign));
486
487 return (res);
488}
489
490template <typename SolverContext>
491typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(
492 typename SolverContext::result_type expr, unsigned width, unsigned shift) {
493
494 typename SolverContext::result_type res;
495
496 if (shift == 0) {
497 res = expr;
498 } else if (shift >= width) {
499 res = bvZero(width);
500 } else {
501 // stp shift does "expr @ [0 x s]" which we then have to extract,
502 // rolling our own gives slightly smaller exprs
503 res = evaluate(_solver,
504 concat(extract(width - shift - 1, 0, expr), bvZero(shift)));
505 }
506
507 return (res);
508}
509
510template <typename SolverContext>
511typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(
512 typename SolverContext::result_type expr, unsigned width, unsigned shift) {
513
514 typename SolverContext::result_type res;
515
516 if (shift == 0) {
517 res = expr;
518 } else if (shift >= width) {
519 res = bvZero(width);
520 } else {
521 res = evaluate(_solver,
522 concat(bvZero(shift), extract(width - 1, shift, expr)));
523 }
524
525 return (res);
526}
527
528// left shift by a variable amount on an expression of the specified width
529template <typename SolverContext>
530typename SolverContext::result_type
531MetaSMTBuilder<SolverContext>::bvVarLeftShift(
532 typename SolverContext::result_type expr,
533 typename SolverContext::result_type shift, unsigned width) {
534
535 assert(_solver.get_bv_width(expr) == width);
536 assert(_solver.get_bv_width(shift) == width);
537
538 // If overshifting, shift to zero
539 return evaluate(_solver,
540 metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)),
541 bvshl(expr, shift), bvZero(width)));
542}
543
544// logical right shift by a variable amount on an expression of the specified
545// width
546template <typename SolverContext>
547typename SolverContext::result_type
548MetaSMTBuilder<SolverContext>::bvVarRightShift(
549 typename SolverContext::result_type expr,
550 typename SolverContext::result_type shift, unsigned width) {
551
552 assert(_solver.get_bv_width(expr) == width);
553 assert(_solver.get_bv_width(shift) == width);
554
555 // If overshifting, shift to zero
556 return evaluate(_solver,
557 metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)),
558 bvshr(expr, shift), bvZero(width)));
559}
560
561// arithmetic right shift by a variable amount on an expression of the specified
562// width
563template <typename SolverContext>
564typename SolverContext::result_type
565MetaSMTBuilder<SolverContext>::bvVarArithRightShift(
566 typename SolverContext::result_type expr,
567 typename SolverContext::result_type shift, unsigned width) {
568
569 assert(_solver.get_bv_width(expr) == width);
570 assert(_solver.get_bv_width(shift) == width);
571
572 // If overshifting, shift to zero
573 return evaluate(_solver,
574 metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)),
575 bvashr(expr, shift), bvZero(width)));
576}
577
578template <typename SolverContext>
579typename SolverContext::result_type
580MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) {
581 typename SolverContext::result_type res = construct(e, 0);
582 _constructed.clear();
583 return res;
584}
585
588template <typename SolverContext>
589typename SolverContext::result_type
590MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) {
591
592 if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) {
593 return (constructActual(e, width_out));
594 } else {
595 MetaSMTExprHashMapIter it = _constructed.find(e);
596 if (it != _constructed.end()) {
597 if (width_out) {
598 *width_out = it->second.second;
599 }
600 return it->second.first;
601 } else {
602 int width = 0;
603 if (!width_out) {
604 width_out = &width;
605 }
606 typename SolverContext::result_type res = constructActual(e, width_out);
607 _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
608 return res;
609 }
610 }
611}
612
613template <typename SolverContext>
614typename SolverContext::result_type
615MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
616
617 typename SolverContext::result_type res;
618
619 int width = 0;
620 if (!width_out) {
621 // assert(false);
622 width_out = &width;
623 }
624
625 ++stats::queryConstructs;
626
627 // llvm::errs() << "Constructing expression ";
628 // ExprPPrinter::printSingleExpr(llvm::errs(), e);
629 // llvm::errs() << "\n";
630
631 switch (e->getKind()) {
632
633 case Expr::Constant: {
634 ConstantExpr *coe = cast<ConstantExpr>(e);
635 assert(coe);
636 unsigned coe_width = coe->getWidth();
637 *width_out = coe_width;
638
639 // Coerce to bool if necessary.
640 if (coe_width == 1) {
641 res = (coe->isTrue()) ? getTrue() : getFalse();
642 } else if (coe_width <= 32) {
643 res = bvConst32(coe_width, coe->getZExtValue(32));
644 } else if (coe_width <= 64) {
645 res = bvConst64(coe_width, coe->getZExtValue());
646 } else {
647 ref<ConstantExpr> tmp = coe;
648 res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue());
649 while (tmp->getWidth() > 64) {
650 tmp = tmp->Extract(64, tmp->getWidth() - 64);
651 unsigned min_width = std::min(64U, tmp->getWidth());
652 res = evaluate(_solver,
653 concat(bvConst64(min_width, tmp->Extract(0, min_width)
654 ->getZExtValue()),
655 res));
656 }
657 }
658 break;
659 }
660
661 case Expr::NotOptimized: {
662 NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
663 assert(noe);
664 res = construct(noe->src, width_out);
665 break;
666 }
667
668 case Expr::Select: {
669 SelectExpr *se = cast<SelectExpr>(e);
670 assert(se);
671 res = evaluate(_solver,
672 metaSMT::logic::Ite(construct(se->cond, 0),
673 construct(se->trueExpr, width_out),
674 construct(se->falseExpr, width_out)));
675 break;
676 }
677
678 case Expr::Read: {
679 ReadExpr *re = cast<ReadExpr>(e);
680 assert(re && re->updates.root);
681 *width_out = re->updates.root->getRange();
682 // FixMe call method of Array
683 res = evaluate(_solver, metaSMT::logic::Array::select(
684 getArrayForUpdate(re->updates.root,
685 re->updates.head.get()),
686 construct(re->index, 0)));
687 break;
688 }
689
690 case Expr::Concat: {
691 ConcatExpr *ce = cast<ConcatExpr>(e);
692 assert(ce);
693 *width_out = ce->getWidth();
694 unsigned numKids = ce->getNumKids();
695
696 if (numKids > 0) {
697 res = evaluate(_solver, construct(ce->getKid(numKids - 1), 0));
698 for (int i = numKids - 2; i >= 0; i--) {
699 res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res));
700 }
701 }
702 break;
703 }
704
705 case Expr::Extract: {
706 ExtractExpr *ee = cast<ExtractExpr>(e);
707 assert(ee);
708 // ToDo spare evaluate?
709 typename SolverContext::result_type child =
710 evaluate(_solver, construct(ee->expr, width_out));
711
712 unsigned ee_width = ee->getWidth();
713 *width_out = ee_width;
714
715 if (ee_width == 1) {
716 res = bvBoolExtract(child, ee->offset);
717 } else {
718 res = evaluate(_solver,
719 extract(ee->offset + ee_width - 1, ee->offset, child));
720 }
721 break;
722 }
723
724 case Expr::ZExt: {
725 CastExpr *ce = cast<CastExpr>(e);
726 assert(ce);
727
728 int child_width = 0;
729 typename SolverContext::result_type child =
730 evaluate(_solver, construct(ce->src, &child_width));
731
732 unsigned ce_width = ce->getWidth();
733 *width_out = ce_width;
734
735 if (child_width == 1) {
736 res = evaluate(_solver, metaSMT::logic::Ite(child, bvOne(ce_width),
737 bvZero(ce_width)));
738 } else {
739 res = evaluate(_solver, zero_extend(ce_width - child_width, child));
740 }
741
742 // ToDo calculate how many zeros to add
743 // Note: STP and metaSMT differ in the prototype arguments;
744 // STP requires the width of the resulting bv;
745 // whereas metaSMT (and Z3) require the width of the zero vector that is to
746 // be appended
747 // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src)));
748
749 break;
750 }
751
752 case Expr::SExt: {
753 CastExpr *ce = cast<CastExpr>(e);
754 assert(ce);
755
756 int child_width = 0;
757 typename SolverContext::result_type child =
758 evaluate(_solver, construct(ce->src, &child_width));
759
760 unsigned ce_width = ce->getWidth();
761 *width_out = ce_width;
762
763 if (child_width == 1) {
764 res = evaluate(_solver, metaSMT::logic::Ite(child, bvMinusOne(ce_width),
765 bvZero(ce_width)));
766 } else {
767 // ToDo ce_width - child_width? It is only ce_width in STPBuilder
768 res = evaluate(_solver, sign_extend(ce_width - child_width, child));
769 }
770
771 break;
772 }
773
774 case Expr::Add: {
775 AddExpr *ae = cast<AddExpr>(e);
776 assert(ae);
777 res = evaluate(_solver, bvadd(construct(ae->left, width_out),
778 construct(ae->right, width_out)));
779 assert(*width_out != 1 && "uncanonicalized add");
780 break;
781 }
782
783 case Expr::Sub: {
784 SubExpr *se = cast<SubExpr>(e);
785 assert(se);
786 res = evaluate(_solver, bvsub(construct(se->left, width_out),
787 construct(se->right, width_out)));
788 assert(*width_out != 1 && "uncanonicalized sub");
789 break;
790 }
791
792 case Expr::Mul: {
793 MulExpr *me = cast<MulExpr>(e);
794 assert(me);
795
796 typename SolverContext::result_type right_expr =
797 evaluate(_solver, construct(me->right, width_out));
798 assert(*width_out != 1 && "uncanonicalized mul");
799
800 ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left);
801 if (CE && (CE->getWidth() <= 64)) {
802 res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue());
803 } else {
804 res =
805 evaluate(_solver, bvmul(construct(me->left, width_out), right_expr));
806 }
807 break;
808 }
809
810 case Expr::UDiv: {
811 UDivExpr *de = cast<UDivExpr>(e);
812 assert(de);
813
814 typename SolverContext::result_type left_expr =
815 construct(de->left, width_out);
816 assert(*width_out != 1 && "uncanonicalized udiv");
817 bool construct_both = true;
818
819 ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
820 if (CE && (CE->getWidth() <= 64)) {
821 uint64_t divisor = CE->getZExtValue();
822 if (bits64::isPowerOfTwo(divisor)) {
823 res = bvRightShift(left_expr, *width_out,
824 bits64::indexOfSingleBit(divisor));
825 construct_both = false;
826 } else if (_optimizeDivides) {
827 if (*width_out == 32) { // only works for 32-bit division
828 res =
829 constructUDivByConstant(left_expr, *width_out, (uint32_t)divisor);
830 construct_both = false;
831 }
832 }
833 }
834
835 if (construct_both) {
836 res =
837 evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out)));
838 }
839 break;
840 }
841
842 case Expr::SDiv: {
843 SDivExpr *de = cast<SDivExpr>(e);
844 assert(de);
845
846 typename SolverContext::result_type left_expr =
847 construct(de->left, width_out);
848 assert(*width_out != 1 && "uncanonicalized sdiv");
849
850 bool optimized = false;
851 ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
852 if (CE && _optimizeDivides && (*width_out == 32)) {
853 llvm::APInt divisor = CE->getAPValue();
854 if (divisor != llvm::APInt(CE->getWidth(), 1, false /*unsigned*/) &&
855 divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) {
856 res = constructSDivByConstant(left_expr, *width_out,
857 CE->getZExtValue(32));
858 optimized = true;
859 }
860 }
861 if (!optimized) {
862 res =
863 evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out)));
864 }
865 break;
866 }
867
868 case Expr::URem: {
869 URemExpr *de = cast<URemExpr>(e);
870 assert(de);
871
872 typename SolverContext::result_type left_expr =
873 construct(de->left, width_out);
874 assert(*width_out != 1 && "uncanonicalized urem");
875
876 bool construct_both = true;
877 ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
878 if (CE && (CE->getWidth() <= 64)) {
879
880 uint64_t divisor = CE->getZExtValue();
881
882 if (bits64::isPowerOfTwo(divisor)) {
883
884 unsigned bits = bits64::indexOfSingleBit(divisor);
885 // special case for modding by 1 or else we bvExtract -1:0
886 if (bits == 0) {
887 res = bvZero(*width_out);
888 construct_both = false;
889 } else {
890 res = evaluate(_solver, concat(bvZero(*width_out - bits),
891 bvExtract(left_expr, bits - 1, 0)));
892 construct_both = false;
893 }
894 }
895
896 // Use fast division to compute modulo without explicit division for
897 // constant divisor.
898
899 if (_optimizeDivides &&
900 *width_out == 32) { // only works for 32-bit division
901 typename SolverContext::result_type quotient =
902 constructUDivByConstant(left_expr, *width_out, (uint32_t)divisor);
903 typename SolverContext::result_type quot_times_divisor =
904 constructMulByConstant(quotient, *width_out, divisor);
905 res = evaluate(_solver, bvsub(left_expr, quot_times_divisor));
906 construct_both = false;
907 }
908 }
909
910 if (construct_both) {
911 res =
912 evaluate(_solver, bvurem(left_expr, construct(de->right, width_out)));
913 }
914 break;
915 }
916
917 case Expr::SRem: {
918 SRemExpr *de = cast<SRemExpr>(e);
919 assert(de);
920
921 typename SolverContext::result_type left_expr =
922 evaluate(_solver, construct(de->left, width_out));
923 typename SolverContext::result_type right_expr =
924 evaluate(_solver, construct(de->right, width_out));
925 assert(*width_out != 1 && "uncanonicalized srem");
926
927 bool construct_both = true;
928
929#if 0 // not faster per first benchmark
930
931 if (_optimizeDivides) {
932 if (ConstantExpr *cre = de->right->asConstant()) {
933 uint64_t divisor = cre->asUInt64;
934
935 //use fast division to compute modulo without explicit division for constant divisor
936 if( *width_out == 32 ) { //only works for 32-bit division
937 typename SolverContext::result_type quotient = constructSDivByConstant(left, *width_out, divisor);
938 typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor);
939 res = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
940 construct_both = false;
941 }
942 }
943 }
944
945#endif
946
947 if (construct_both) {
948 res = evaluate(_solver, bvsrem(left_expr, right_expr));
949 }
950 break;
951 }
952
953 case Expr::Not: {
954 NotExpr *ne = cast<NotExpr>(e);
955 assert(ne);
956
957 typename SolverContext::result_type child =
958 evaluate(_solver, construct(ne->expr, width_out));
959 if (*width_out == 1) {
960 res = evaluate(_solver, metaSMT::logic::Not(child));
961 } else {
962 res = evaluate(_solver, bvnot(child));
963 }
964 break;
965 }
966
967 case Expr::And: {
968 AndExpr *ae = cast<AndExpr>(e);
969 assert(ae);
970
971 typename SolverContext::result_type left_expr =
972 evaluate(_solver, construct(ae->left, width_out));
973 typename SolverContext::result_type right_expr =
974 evaluate(_solver, construct(ae->right, width_out));
975
976 if (*width_out == 1) {
977 res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr));
978 } else {
979 res = evaluate(_solver, bvand(left_expr, right_expr));
980 }
981
982 break;
983 }
984
985 case Expr::Or: {
986 OrExpr *oe = cast<OrExpr>(e);
987 assert(oe);
988
989 typename SolverContext::result_type left_expr =
990 evaluate(_solver, construct(oe->left, width_out));
991 typename SolverContext::result_type right_expr =
992 evaluate(_solver, construct(oe->right, width_out));
993
994 if (*width_out == 1) {
995 res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr));
996 } else {
997 res = evaluate(_solver, bvor(left_expr, right_expr));
998 }
999
1000 break;
1001 }
1002
1003 case Expr::Xor: {
1004 XorExpr *xe = cast<XorExpr>(e);
1005 assert(xe);
1006
1007 typename SolverContext::result_type left_expr =
1008 evaluate(_solver, construct(xe->left, width_out));
1009 typename SolverContext::result_type right_expr =
1010 evaluate(_solver, construct(xe->right, width_out));
1011
1012 if (*width_out == 1) {
1013 res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr));
1014 } else {
1015 res = evaluate(_solver, bvxor(left_expr, right_expr));
1016 }
1017
1018 break;
1019 }
1020
1021 case Expr::Shl: {
1022 ShlExpr *se = cast<ShlExpr>(e);
1023 assert(se);
1024
1025 typename SolverContext::result_type left_expr =
1026 evaluate(_solver, construct(se->left, width_out));
1027 assert(*width_out != 1 && "uncanonicalized shl");
1028
1029 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
1030 res = bvLeftShift(left_expr, *width_out, (unsigned)CE->getLimitedValue());
1031 } else {
1032 int shiftWidth = 0;
1033 typename SolverContext::result_type right_expr =
1034 evaluate(_solver, construct(se->right, &shiftWidth));
1035 res = bvVarLeftShift(left_expr, right_expr, *width_out);
1036 }
1037
1038 break;
1039 }
1040
1041 case Expr::LShr: {
1042 LShrExpr *lse = cast<LShrExpr>(e);
1043 assert(lse);
1044
1045 typename SolverContext::result_type left_expr =
1046 evaluate(_solver, construct(lse->left, width_out));
1047 assert(*width_out != 1 && "uncanonicalized lshr");
1048
1049 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
1050 res =
1051 bvRightShift(left_expr, *width_out, (unsigned)CE->getLimitedValue());
1052 } else {
1053 int shiftWidth = 0;
1054 typename SolverContext::result_type right_expr =
1055 evaluate(_solver, construct(lse->right, &shiftWidth));
1056 res = bvVarRightShift(left_expr, right_expr, *width_out);
1057 }
1058
1059 break;
1060 }
1061
1062 case Expr::AShr: {
1063 AShrExpr *ase = cast<AShrExpr>(e);
1064 assert(ase);
1065
1066 typename SolverContext::result_type left_expr =
1067 evaluate(_solver, construct(ase->left, width_out));
1068 assert(*width_out != 1 && "uncanonicalized ashr");
1069
1070 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
1071 unsigned shift = (unsigned)CE->getLimitedValue();
1072 typename SolverContext::result_type signedBool =
1073 bvBoolExtract(left_expr, *width_out - 1);
1074 res = constructAShrByConstant(left_expr, *width_out, shift, signedBool);
1075 } else {
1076 int shiftWidth = 0;
1077 typename SolverContext::result_type right_expr =
1078 evaluate(_solver, construct(ase->right, &shiftWidth));
1079 res = bvVarArithRightShift(left_expr, right_expr, *width_out);
1080 }
1081
1082 break;
1083 }
1084
1085 case Expr::Eq: {
1086 EqExpr *ee = cast<EqExpr>(e);
1087 assert(ee);
1088
1089 typename SolverContext::result_type left_expr =
1090 evaluate(_solver, construct(ee->left, width_out));
1091 typename SolverContext::result_type right_expr =
1092 evaluate(_solver, construct(ee->right, width_out));
1093
1094 if (*width_out == 1) {
1095 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
1096 if (CE->isTrue()) {
1097 res = right_expr;
1098 } else {
1099 res = evaluate(_solver, metaSMT::logic::Not(right_expr));
1100 }
1101 } else {
1102 res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
1103 }
1104 } // end of *width_out == 1
1105 else {
1106 *width_out = 1;
1107 res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
1108 }
1109
1110 break;
1111 }
1112
1113 case Expr::Ult: {
1114 UltExpr *ue = cast<UltExpr>(e);
1115 assert(ue);
1116
1117 typename SolverContext::result_type left_expr =
1118 evaluate(_solver, construct(ue->left, width_out));
1119 typename SolverContext::result_type right_expr =
1120 evaluate(_solver, construct(ue->right, width_out));
1121
1122 assert(*width_out != 1 && "uncanonicalized ult");
1123 *width_out = 1;
1124
1125 res = evaluate(_solver, bvult(left_expr, right_expr));
1126 break;
1127 }
1128
1129 case Expr::Ule: {
1130 UleExpr *ue = cast<UleExpr>(e);
1131 assert(ue);
1132
1133 typename SolverContext::result_type left_expr =
1134 evaluate(_solver, construct(ue->left, width_out));
1135 typename SolverContext::result_type right_expr =
1136 evaluate(_solver, construct(ue->right, width_out));
1137
1138 assert(*width_out != 1 && "uncanonicalized ule");
1139 *width_out = 1;
1140
1141 res = evaluate(_solver, bvule(left_expr, right_expr));
1142 break;
1143 }
1144
1145 case Expr::Slt: {
1146 SltExpr *se = cast<SltExpr>(e);
1147 assert(se);
1148
1149 typename SolverContext::result_type left_expr =
1150 evaluate(_solver, construct(se->left, width_out));
1151 typename SolverContext::result_type right_expr =
1152 evaluate(_solver, construct(se->right, width_out));
1153
1154 assert(*width_out != 1 && "uncanonicalized slt");
1155 *width_out = 1;
1156
1157 res = evaluate(_solver, bvslt(left_expr, right_expr));
1158 break;
1159 }
1160
1161 case Expr::Sle: {
1162 SleExpr *se = cast<SleExpr>(e);
1163 assert(se);
1164
1165 typename SolverContext::result_type left_expr =
1166 evaluate(_solver, construct(se->left, width_out));
1167 typename SolverContext::result_type right_expr =
1168 evaluate(_solver, construct(se->right, width_out));
1169
1170 assert(*width_out != 1 && "uncanonicalized sle");
1171 *width_out = 1;
1172
1173 res = evaluate(_solver, bvsle(left_expr, right_expr));
1174 break;
1175 }
1176
1177// unused due to canonicalization
1178#if 0
1179 case Expr::Ne:
1180 case Expr::Ugt:
1181 case Expr::Uge:
1182 case Expr::Sgt:
1183 case Expr::Sge:
1184#endif
1185
1186 default:
1187 assert(false);
1188 break;
1189 };
1190 return res;
1191}
1192
1193} /* end of namespace klee */
1194
1195#endif /* ENABLE_METASMT */
1196
1197#endif /* KLEE_METASMTBUILDER_H */
add
#define add(name, handler, ret)
klee::ConstantExpr::alloc
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
klee::Expr::Xor
@ Xor
Definition: Expr.h:149
klee::Expr::Not
@ Not
Definition: Expr.h:133
klee::Expr::Ule
@ Ule
Definition: Expr.h:158
klee::Expr::LShr
@ LShr
Definition: Expr.h:151
klee::Expr::Sge
@ Sge
Not used in canonical form.
Definition: Expr.h:164
klee::Expr::Add
@ Add
Definition: Expr.h:138
klee::Expr::Select
@ Select
Definition: Expr.h:124
klee::Expr::Ne
@ Ne
Not used in canonical form.
Definition: Expr.h:156
klee::Expr::And
@ And
Definition: Expr.h:147
klee::Expr::ZExt
@ ZExt
Definition: Expr.h:129
klee::Expr::URem
@ URem
Definition: Expr.h:143
klee::Expr::SDiv
@ SDiv
Definition: Expr.h:142
klee::Expr::NotOptimized
@ NotOptimized
Definition: Expr.h:120
klee::Expr::Mul
@ Mul
Definition: Expr.h:140
klee::Expr::AShr
@ AShr
Definition: Expr.h:152
klee::Expr::Extract
@ Extract
Definition: Expr.h:126
klee::Expr::Read
@ Read
Definition: Expr.h:123
klee::Expr::Constant
@ Constant
Definition: Expr.h:113
klee::Expr::Ugt
@ Ugt
Not used in canonical form.
Definition: Expr.h:159
klee::Expr::Sub
@ Sub
Definition: Expr.h:139
klee::Expr::Ult
@ Ult
Definition: Expr.h:157
klee::Expr::Shl
@ Shl
Definition: Expr.h:150
klee::Expr::SRem
@ SRem
Definition: Expr.h:144
klee::Expr::Concat
@ Concat
Definition: Expr.h:125
klee::Expr::Or
@ Or
Definition: Expr.h:148
klee::Expr::Sle
@ Sle
Definition: Expr.h:162
klee::Expr::Sgt
@ Sgt
Not used in canonical form.
Definition: Expr.h:163
klee::Expr::Slt
@ Slt
Definition: Expr.h:161
klee::Expr::Uge
@ Uge
Not used in canonical form.
Definition: Expr.h:160
klee::Expr::SExt
@ SExt
Definition: Expr.h:130
klee::Expr::UDiv
@ UDiv
Definition: Expr.h:141
klee::Expr::Eq
@ Eq
Definition: Expr.h:155
klee::bits64::truncateToNBits
uint64_t truncateToNBits(uint64_t x, unsigned N)
Definition: Bits.h:78
klee::bits64::indexOfSingleBit
unsigned indexOfSingleBit(uint64_t x)
Definition: Bits.h:98
klee::bits64::isPowerOfTwo
uint64_t isPowerOfTwo(uint64_t x)
Definition: Bits.h:91
klee::floats::sub
uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth)
Definition: FloatEvaluation.h:93
klee::floats::ne
uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth)
Definition: FloatEvaluation.h:152
klee::stats::queryConstructs
Statistic queryConstructs
klee
Definition: main.cpp:291
klee::ComputeMultConstants64
void ComputeMultConstants64(uint64_t multiplicand, uint64_t &add, uint64_t &sub)
Definition: ConstantDivision.cpp:82
klee::ComputeUDivConstants32
void ComputeUDivConstants32(uint32_t d, uint32_t &mprime, uint32_t &sh1, uint32_t &sh2)
Definition: ConstantDivision.cpp:118
klee::ComputeSDivConstants32
void ComputeSDivConstants32(int32_t d, int32_t &mprime, int32_t &dsign, int32_t &shpost)
Definition: ConstantDivision.cpp:128