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