klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
STPBuilder.cpp
Go to the documentation of this file.
1 //===-- STPBuilder.cpp ----------------------------------------------------===//
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 #include "STPBuilder.h"
11 
12 #include "klee/Expr.h"
13 #include "klee/Solver.h"
14 #include "klee/util/Bits.h"
15 
16 #include "ConstantDivision.h"
17 #include "SolverStats.h"
18 
19 #include "llvm/Support/CommandLine.h"
20 
21 #include <cstdio>
22 
23 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
24 // unclear return
25 #define vc_bvLeftShiftExpr IAMTHESPAWNOFSATAN
26 #define vc_bvRightShiftExpr IAMTHESPAWNOFSATAN
27 // bad refcnt'ng
28 #define vc_bvVar32LeftShiftExpr IAMTHESPAWNOFSATAN
29 #define vc_bvVar32RightShiftExpr IAMTHESPAWNOFSATAN
30 #define vc_bvVar32DivByPowOfTwoExpr IAMTHESPAWNOFSATAN
31 #define vc_bvCreateMemoryArray IAMTHESPAWNOFSATAN
32 #define vc_bvReadMemoryArray IAMTHESPAWNOFSATAN
33 #define vc_bvWriteToMemoryArray IAMTHESPAWNOFSATAN
34 
35 #include <algorithm> // max, min
36 #include <cassert>
37 #include <map>
38 #include <sstream>
39 #include <vector>
40 
41 using namespace klee;
42 
43 namespace {
44  llvm::cl::opt<bool>
45  UseConstructHash("use-construct-hash",
46  llvm::cl::desc("Use hash-consing during STP query construction."),
47  llvm::cl::init(true));
48 }
49 
51 
52 
54 
55  // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run;
56  // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled.
57 
58  /*
59  for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) {
60  ::VCExpr array_expr = it->second;
61  if (array_expr) {
62  ::vc_DeleteExpr(array_expr);
63  array_expr = 0;
64  }
65  }
66 
67 
68  for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) {
69  ::VCExpr un_expr = it->second;
70  if (un_expr) {
71  ::vc_DeleteExpr(un_expr);
72  un_expr = 0;
73  }
74  }
75  */
76 }
77 
78 /***/
79 
80 STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides)
81  : vc(_vc), optimizeDivides(_optimizeDivides)
82 {
83  tempVars[0] = buildVar("__tmpInt8", 8);
84  tempVars[1] = buildVar("__tmpInt16", 16);
85  tempVars[2] = buildVar("__tmpInt32", 32);
86  tempVars[3] = buildVar("__tmpInt64", 64);
87 }
88 
90 
91 }
92 
94 
95 /* Warning: be careful about what c_interface functions you use. Some of
96  them look like they cons memory but in fact don't, which is bad when
97  you call vc_DeleteExpr on them. */
98 
99 ::VCExpr STPBuilder::buildVar(const char *name, unsigned width) {
100  // XXX don't rebuild if this stuff cons's
101  ::Type t = (width==1) ? vc_boolType(vc) : vc_bvType(vc, width);
102  ::VCExpr res = vc_varExpr(vc, const_cast<char*>(name), t);
103  vc_DeleteExpr(t);
104  return res;
105 }
106 
107 ::VCExpr STPBuilder::buildArray(const char *name, unsigned indexWidth, unsigned valueWidth) {
108  // XXX don't rebuild if this stuff cons's
109  ::Type t1 = vc_bvType(vc, indexWidth);
110  ::Type t2 = vc_bvType(vc, valueWidth);
111  ::Type t = vc_arrayType(vc, t1, t2);
112  ::VCExpr res = vc_varExpr(vc, const_cast<char*>(name), t);
113  vc_DeleteExpr(t);
114  vc_DeleteExpr(t2);
115  vc_DeleteExpr(t1);
116  return res;
117 }
118 
120  switch (w) {
121  default: assert(0 && "invalid type");
122  case Expr::Int8: return tempVars[0];
123  case Expr::Int16: return tempVars[1];
124  case Expr::Int32: return tempVars[2];
125  case Expr::Int64: return tempVars[3];
126  }
127 }
128 
130  return vc_trueExpr(vc);
131 }
133  return vc_falseExpr(vc);
134 }
135 ExprHandle STPBuilder::bvOne(unsigned width) {
136  return bvZExtConst(width, 1);
137 }
139  return bvZExtConst(width, 0);
140 }
142  return bvSExtConst(width, (int64_t) -1);
143 }
144 ExprHandle STPBuilder::bvConst32(unsigned width, uint32_t value) {
145  return vc_bvConstExprFromInt(vc, width, value);
146 }
147 ExprHandle STPBuilder::bvConst64(unsigned width, uint64_t value) {
148  return vc_bvConstExprFromLL(vc, width, value);
149 }
150 ExprHandle STPBuilder::bvZExtConst(unsigned width, uint64_t value) {
151  if (width <= 64)
152  return bvConst64(width, value);
153 
154  ExprHandle expr = bvConst64(64, value), zero = bvConst64(64, 0);
155  for (width -= 64; width > 64; width -= 64)
156  expr = vc_bvConcatExpr(vc, zero, expr);
157  return vc_bvConcatExpr(vc, bvConst64(width, 0), expr);
158 }
159 ExprHandle STPBuilder::bvSExtConst(unsigned width, uint64_t value) {
160  if (width <= 64)
161  return bvConst64(width, value);
162  return vc_bvSignExtend(vc, bvConst64(64, value), width);
163 }
164 
166  return vc_eqExpr(vc, bvExtract(expr, bit, bit), bvOne(1));
167 }
168 ExprHandle STPBuilder::bvExtract(ExprHandle expr, unsigned top, unsigned bottom) {
169  return vc_bvExtract(vc, expr, top, bottom);
170 }
172  return vc_eqExpr(vc, a, b);
173 }
174 
175 // logical right shift
177  unsigned width = vc_getBVLength(vc, expr);
178 
179  if (shift==0) {
180  return expr;
181  } else if (shift>=width) {
182  return bvZero(width); // Overshift to zero
183  } else {
184  return vc_bvConcatExpr(vc,
185  bvZero(shift),
186  bvExtract(expr, width - 1, shift));
187  }
188 }
189 
190 // logical left shift
192  unsigned width = vc_getBVLength(vc, expr);
193 
194  if (shift==0) {
195  return expr;
196  } else if (shift>=width) {
197  return bvZero(width); // Overshift to zero
198  } else {
199  // stp shift does "expr @ [0 x s]" which we then have to extract,
200  // rolling our own gives slightly smaller exprs
201  return vc_bvConcatExpr(vc,
202  bvExtract(expr, width - shift - 1, 0),
203  bvZero(shift));
204  }
205 }
206 
207 // left shift by a variable amount on an expression of the specified width
209  unsigned width = vc_getBVLength(vc, expr);
210  ExprHandle res = bvZero(width);
211 
212  //construct a big if-then-elif-elif-... with one case per possible shift amount
213  for( int i=width-1; i>=0; i-- ) {
214  res = vc_iteExpr(vc,
215  eqExpr(shift, bvConst32(width, i)),
216  bvLeftShift(expr, i),
217  res);
218  }
219 
220  // If overshifting, shift to zero
221  res = vc_iteExpr(vc,
222  vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
223  res,
224  bvZero(width));
225  return res;
226 }
227 
228 // logical right shift by a variable amount on an expression of the specified width
230  unsigned width = vc_getBVLength(vc, expr);
231  ExprHandle res = bvZero(width);
232 
233  //construct a big if-then-elif-elif-... with one case per possible shift amount
234  for( int i=width-1; i>=0; i-- ) {
235  res = vc_iteExpr(vc,
236  eqExpr(shift, bvConst32(width, i)),
237  bvRightShift(expr, i),
238  res);
239  }
240 
241  // If overshifting, shift to zero
242  res = vc_iteExpr(vc,
243  vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
244  res,
245  bvZero(width));
246  return res;
247 }
248 
249 // arithmetic right shift by a variable amount on an expression of the specified width
251  unsigned width = vc_getBVLength(vc, expr);
252 
253  //get the sign bit to fill with
254  ExprHandle signedBool = bvBoolExtract(expr, width-1);
255 
256  //start with the result if shifting by width-1
257  ExprHandle res = constructAShrByConstant(expr, width-1, signedBool);
258 
259  //construct a big if-then-elif-elif-... with one case per possible shift amount
260  // XXX more efficient to move the ite on the sign outside all exprs?
261  // XXX more efficient to sign extend, right shift, then extract lower bits?
262  for( int i=width-2; i>=0; i-- ) {
263  res = vc_iteExpr(vc,
264  eqExpr(shift, bvConst32(width,i)),
266  i,
267  signedBool),
268  res);
269  }
270 
271  // If overshifting, shift to zero
272  res = vc_iteExpr(vc,
273  vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
274  res,
275  bvZero(width));
276  return res;
277 }
278 
280  unsigned shift,
281  ExprHandle isSigned) {
282  unsigned width = vc_getBVLength(vc, expr);
283 
284  if (shift==0) {
285  return expr;
286  } else if (shift>=width-1) {
287  return bvZero(width); // Overshift to zero
288  } else {
289  return vc_iteExpr(vc,
290  isSigned,
291  ExprHandle(vc_bvConcatExpr(vc,
292  bvMinusOne(shift),
293  bvExtract(expr, width - 1, shift))),
294  bvRightShift(expr, shift));
295  }
296 }
297 
298 ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x) {
299  uint64_t add, sub;
300  ExprHandle res = 0;
301 
302  // expr*x == expr*(add-sub) == expr*add - expr*sub
303  ComputeMultConstants64(x, add, sub);
304 
305  // legal, these would overflow completely
306  add = bits64::truncateToNBits(add, width);
307  sub = bits64::truncateToNBits(sub, width);
308 
309  for (int j=63; j>=0; j--) {
310  uint64_t bit = 1LL << j;
311 
312  if ((add&bit) || (sub&bit)) {
313  assert(!((add&bit) && (sub&bit)) && "invalid mult constants");
314  ExprHandle op = bvLeftShift(expr, j);
315 
316  if (add&bit) {
317  if (res) {
318  res = vc_bvPlusExpr(vc, width, res, op);
319  } else {
320  res = op;
321  }
322  } else {
323  if (res) {
324  res = vc_bvMinusExpr(vc, width, res, op);
325  } else {
326  res = vc_bvUMinusExpr(vc, op);
327  }
328  }
329  }
330  }
331 
332  if (!res)
333  res = bvZero(width);
334 
335  return res;
336 }
337 
338 /*
339  * Compute the 32-bit unsigned integer division of n by a divisor d based on
340  * the constants derived from the constant divisor d.
341  *
342  * Returns n/d without doing explicit division. The cost is 2 adds, 3 shifts,
343  * and a (64-bit) multiply.
344  *
345  * @param n numerator (dividend) as an expression
346  * @param width number of bits used to represent the value
347  * @param d the divisor
348  *
349  * @return n/d without doing explicit division
350  */
351 ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d) {
352  assert(width==32 && "can only compute udiv constants for 32-bit division");
353 
354  // Compute the constants needed to compute n/d for constant d w/o
355  // division by d.
356  uint32_t mprime, sh1, sh2;
357  ComputeUDivConstants32(d, mprime, sh1, sh2);
358  ExprHandle expr_sh1 = bvConst32( 32, sh1);
359  ExprHandle expr_sh2 = bvConst32( 32, sh2);
360 
361  // t1 = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
362  ExprHandle expr_n_64 = vc_bvConcatExpr( vc, bvZero(32), expr_n ); //extend to 64 bits
363  ExprHandle t1_64bits = constructMulByConstant( expr_n_64, 64, (uint64_t)mprime );
364  ExprHandle t1 = vc_bvExtract( vc, t1_64bits, 63, 32 ); //upper 32 bits
365 
366  // n/d = (((n - t1) >> sh1) + t1) >> sh2;
367  ExprHandle n_minus_t1 = vc_bvMinusExpr( vc, width, expr_n, t1 );
368  ExprHandle shift_sh1 = bvVarRightShift( n_minus_t1, expr_sh1);
369  ExprHandle plus_t1 = vc_bvPlusExpr( vc, width, shift_sh1, t1 );
370  ExprHandle res = bvVarRightShift( plus_t1, expr_sh2);
371 
372  return res;
373 }
374 
375 /*
376  * Compute the 32-bitnsigned integer division of n by a divisor d based on
377  * the constants derived from the constant divisor d.
378  *
379  * Returns n/d without doing explicit division. The cost is 3 adds, 3 shifts,
380  * a (64-bit) multiply, and an XOR.
381  *
382  * @param n numerator (dividend) as an expression
383  * @param width number of bits used to represent the value
384  * @param d the divisor
385  *
386  * @return n/d without doing explicit division
387  */
388 ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d) {
389  assert(width==32 && "can only compute udiv constants for 32-bit division");
390 
391  // Compute the constants needed to compute n/d for constant d w/o division by d.
392  int32_t mprime, dsign, shpost;
393  ComputeSDivConstants32(d, mprime, dsign, shpost);
394  ExprHandle expr_dsign = bvConst32( 32, dsign);
395  ExprHandle expr_shpost = bvConst32( 32, shpost);
396 
397  // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
398  int64_t mprime_64 = (int64_t)mprime;
399 
400  ExprHandle expr_n_64 = vc_bvSignExtend( vc, expr_n, 64 );
401  ExprHandle mult_64 = constructMulByConstant( expr_n_64, 64, mprime_64 );
402  ExprHandle mulsh = vc_bvExtract( vc, mult_64, 63, 32 ); //upper 32-bits
403  ExprHandle n_plus_mulsh = vc_bvPlusExpr( vc, width, expr_n, mulsh );
404 
405  // Improved variable arithmetic right shift: sign extend, shift,
406  // extract.
407  ExprHandle extend_npm = vc_bvSignExtend( vc, n_plus_mulsh, 64 );
408  ExprHandle shift_npm = bvVarRightShift( extend_npm, expr_shpost);
409  ExprHandle shift_shpost = vc_bvExtract( vc, shift_npm, 31, 0 ); //lower 32-bits
410 
411  // XSIGN(n) is -1 if n is negative, positive one otherwise
412  ExprHandle is_signed = bvBoolExtract( expr_n, 31 );
413  ExprHandle neg_one = bvMinusOne(32);
414  ExprHandle xsign_of_n = vc_iteExpr( vc, is_signed, neg_one, bvZero(32) );
415 
416  // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
417  ExprHandle q0 = vc_bvMinusExpr( vc, width, shift_shpost, xsign_of_n );
418 
419  // n/d = (q0 ^ dsign) - dsign
420  ExprHandle q0_xor_dsign = vc_bvXorExpr( vc, q0, expr_dsign );
421  ExprHandle res = vc_bvMinusExpr( vc, width, q0_xor_dsign, expr_dsign );
422 
423  return res;
424 }
425 
426 ::VCExpr STPBuilder::getInitialArray(const Array *root) {
427 
428  assert(root);
429  ::VCExpr array_expr;
430  bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
431 
432  if (!hashed) {
433  // STP uniques arrays by name, so we make sure the name is unique by
434  // including the address.
435  char buf[32];
436  unsigned const addrlen = sprintf(buf, "_%p", (const void*)root) + 1; // +1 for null-termination
437  unsigned const space = (root->name.length() > 32 - addrlen)?(32 - addrlen):root->name.length();
438  memmove(buf + space, buf, addrlen); // moving the address part to the end
439  memcpy(buf, root->name.c_str(), space); // filling out the name part
440 
441  array_expr = buildArray(buf, root->getDomain(), root->getRange());
442 
443  if (root->isConstantArray()) {
444  // FIXME: Flush the concrete values into STP. Ideally we would do this
445  // using assertions, which is much faster, but we need to fix the caching
446  // to work correctly in that case.
447  for (unsigned i = 0, e = root->size; i != e; ++i) {
448  ::VCExpr prev = array_expr;
449  array_expr = vc_writeExpr(vc, prev,
450  construct(ConstantExpr::alloc(i, root->getDomain()), 0),
451  construct(root->constantValues[i], 0));
452  vc_DeleteExpr(prev);
453  }
454  }
455 
456  _arr_hash.hashArrayExpr(root, array_expr);
457  }
458 
459  return(array_expr);
460 }
461 
462 ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
463  return vc_readExpr(vc, getInitialArray(root), bvConst32(32, index));
464 }
465 
466 ::VCExpr STPBuilder::getArrayForUpdate(const Array *root,
467  const UpdateNode *un) {
468  if (!un) {
469  return(getInitialArray(root));
470  }
471  else {
472  // FIXME: This really needs to be non-recursive.
473  ::VCExpr un_expr;
474  bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
475 
476  if (!hashed) {
477  un_expr = vc_writeExpr(vc,
478  getArrayForUpdate(root, un->next),
479  construct(un->index, 0),
480  construct(un->value, 0));
481 
482  _arr_hash.hashUpdateNodeExpr(un, un_expr);
483  }
484 
485  return(un_expr);
486  }
487 }
488 
492  if (!UseConstructHash || isa<ConstantExpr>(e)) {
493  return constructActual(e, width_out);
494  } else {
496  constructed.find(e);
497  if (it!=constructed.end()) {
498  if (width_out)
499  *width_out = it->second.second;
500  return it->second.first;
501  } else {
502  int width;
503  if (!width_out) width_out = &width;
504  ExprHandle res = constructActual(e, width_out);
505  constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
506  return res;
507  }
508  }
509 }
510 
511 
515  int width;
516  if (!width_out) width_out = &width;
517 
519 
520  switch (e->getKind()) {
521  case Expr::Constant: {
522  ConstantExpr *CE = cast<ConstantExpr>(e);
523  *width_out = CE->getWidth();
524 
525  // Coerce to bool if necessary.
526  if (*width_out == 1)
527  return CE->isTrue() ? getTrue() : getFalse();
528 
529  // Fast path.
530  if (*width_out <= 32)
531  return bvConst32(*width_out, CE->getZExtValue(32));
532  if (*width_out <= 64)
533  return bvConst64(*width_out, CE->getZExtValue());
534 
535  ref<ConstantExpr> Tmp = CE;
536  ExprHandle Res = bvConst64(64, Tmp->Extract(0, 64)->getZExtValue());
537  while (Tmp->getWidth() > 64) {
538  Tmp = Tmp->Extract(64, Tmp->getWidth()-64);
539  unsigned Width = std::min(64U, Tmp->getWidth());
540  Res = vc_bvConcatExpr(vc, bvConst64(Width,
541  Tmp->Extract(0, Width)->getZExtValue()),
542  Res);
543  }
544  return Res;
545  }
546 
547  // Special
548  case Expr::NotOptimized: {
549  NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
550  return construct(noe->src, width_out);
551  }
552 
553  case Expr::Read: {
554  ReadExpr *re = cast<ReadExpr>(e);
555  assert(re && re->updates.root);
556  *width_out = re->updates.root->getRange();
557  return vc_readExpr(vc,
559  construct(re->index, 0));
560  }
561 
562  case Expr::Select: {
563  SelectExpr *se = cast<SelectExpr>(e);
564  ExprHandle cond = construct(se->cond, 0);
565  ExprHandle tExpr = construct(se->trueExpr, width_out);
566  ExprHandle fExpr = construct(se->falseExpr, width_out);
567  return vc_iteExpr(vc, cond, tExpr, fExpr);
568  }
569 
570  case Expr::Concat: {
571  ConcatExpr *ce = cast<ConcatExpr>(e);
572  unsigned numKids = ce->getNumKids();
573  ExprHandle res = construct(ce->getKid(numKids-1), 0);
574  for (int i=numKids-2; i>=0; i--) {
575  res = vc_bvConcatExpr(vc, construct(ce->getKid(i), 0), res);
576  }
577  *width_out = ce->getWidth();
578  return res;
579  }
580 
581  case Expr::Extract: {
582  ExtractExpr *ee = cast<ExtractExpr>(e);
583  ExprHandle src = construct(ee->expr, width_out);
584  *width_out = ee->getWidth();
585  if (*width_out==1) {
586  return bvBoolExtract(src, ee->offset);
587  } else {
588  return vc_bvExtract(vc, src, ee->offset + *width_out - 1, ee->offset);
589  }
590  }
591 
592  // Casting
593 
594  case Expr::ZExt: {
595  int srcWidth;
596  CastExpr *ce = cast<CastExpr>(e);
597  ExprHandle src = construct(ce->src, &srcWidth);
598  *width_out = ce->getWidth();
599  if (srcWidth==1) {
600  return vc_iteExpr(vc, src, bvOne(*width_out), bvZero(*width_out));
601  } else {
602  return vc_bvConcatExpr(vc, bvZero(*width_out-srcWidth), src);
603  }
604  }
605 
606  case Expr::SExt: {
607  int srcWidth;
608  CastExpr *ce = cast<CastExpr>(e);
609  ExprHandle src = construct(ce->src, &srcWidth);
610  *width_out = ce->getWidth();
611  if (srcWidth==1) {
612  return vc_iteExpr(vc, src, bvMinusOne(*width_out), bvZero(*width_out));
613  } else {
614  return vc_bvSignExtend(vc, src, *width_out);
615  }
616  }
617 
618  // Arithmetic
619 
620  case Expr::Add: {
621  AddExpr *ae = cast<AddExpr>(e);
622  ExprHandle left = construct(ae->left, width_out);
623  ExprHandle right = construct(ae->right, width_out);
624  assert(*width_out!=1 && "uncanonicalized add");
625  return vc_bvPlusExpr(vc, *width_out, left, right);
626  }
627 
628  case Expr::Sub: {
629  SubExpr *se = cast<SubExpr>(e);
630  ExprHandle left = construct(se->left, width_out);
631  ExprHandle right = construct(se->right, width_out);
632  assert(*width_out!=1 && "uncanonicalized sub");
633  return vc_bvMinusExpr(vc, *width_out, left, right);
634  }
635 
636  case Expr::Mul: {
637  MulExpr *me = cast<MulExpr>(e);
638  ExprHandle right = construct(me->right, width_out);
639  assert(*width_out!=1 && "uncanonicalized mul");
640 
641  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left))
642  if (CE->getWidth() <= 64)
643  return constructMulByConstant(right, *width_out,
644  CE->getZExtValue());
645 
646  ExprHandle left = construct(me->left, width_out);
647  return vc_bvMultExpr(vc, *width_out, left, right);
648  }
649 
650  case Expr::UDiv: {
651  UDivExpr *de = cast<UDivExpr>(e);
652  ExprHandle left = construct(de->left, width_out);
653  assert(*width_out!=1 && "uncanonicalized udiv");
654 
655  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
656  if (CE->getWidth() <= 64) {
657  uint64_t divisor = CE->getZExtValue();
658 
659  if (bits64::isPowerOfTwo(divisor)) {
660  return bvRightShift(left,
661  bits64::indexOfSingleBit(divisor));
662  } else if (optimizeDivides) {
663  if (*width_out == 32) //only works for 32-bit division
664  return constructUDivByConstant( left, *width_out,
665  (uint32_t) divisor);
666  }
667  }
668  }
669 
670  ExprHandle right = construct(de->right, width_out);
671  return vc_bvDivExpr(vc, *width_out, left, right);
672  }
673 
674  case Expr::SDiv: {
675  SDivExpr *de = cast<SDivExpr>(e);
676  ExprHandle left = construct(de->left, width_out);
677  assert(*width_out!=1 && "uncanonicalized sdiv");
678 
679  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right))
680  if (optimizeDivides)
681  if (*width_out == 32) //only works for 32-bit division
682  return constructSDivByConstant( left, *width_out,
683  CE->getZExtValue(32));
684 
685  // XXX need to test for proper handling of sign, not sure I
686  // trust STP
687  ExprHandle right = construct(de->right, width_out);
688  return vc_sbvDivExpr(vc, *width_out, left, right);
689  }
690 
691  case Expr::URem: {
692  URemExpr *de = cast<URemExpr>(e);
693  ExprHandle left = construct(de->left, width_out);
694  assert(*width_out!=1 && "uncanonicalized urem");
695 
696  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
697  if (CE->getWidth() <= 64) {
698  uint64_t divisor = CE->getZExtValue();
699 
700  if (bits64::isPowerOfTwo(divisor)) {
701  unsigned bits = bits64::indexOfSingleBit(divisor);
702 
703  // special case for modding by 1 or else we bvExtract -1:0
704  if (bits == 0) {
705  return bvZero(*width_out);
706  } else {
707  return vc_bvConcatExpr(vc,
708  bvZero(*width_out - bits),
709  bvExtract(left, bits - 1, 0));
710  }
711  }
712 
713  // Use fast division to compute modulo without explicit division for
714  // constant divisor.
715 
716  if (optimizeDivides) {
717  if (*width_out == 32) { //only works for 32-bit division
718  ExprHandle quotient = constructUDivByConstant( left, *width_out, (uint32_t)divisor );
719  ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
720  ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
721  return rem;
722  }
723  }
724  }
725  }
726 
727  ExprHandle right = construct(de->right, width_out);
728  return vc_bvModExpr(vc, *width_out, left, right);
729  }
730 
731  case Expr::SRem: {
732  SRemExpr *de = cast<SRemExpr>(e);
733  ExprHandle left = construct(de->left, width_out);
734  ExprHandle right = construct(de->right, width_out);
735  assert(*width_out!=1 && "uncanonicalized srem");
736 
737 #if 0 //not faster per first benchmark
738  if (optimizeDivides) {
739  if (ConstantExpr *cre = de->right->asConstant()) {
740  uint64_t divisor = cre->asUInt64;
741 
742  //use fast division to compute modulo without explicit division for constant divisor
743  if( *width_out == 32 ) { //only works for 32-bit division
744  ExprHandle quotient = constructSDivByConstant( left, *width_out, divisor );
745  ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
746  ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
747  return rem;
748  }
749  }
750  }
751 #endif
752 
753  // XXX implement my fast path and test for proper handling of sign
754  return vc_sbvModExpr(vc, *width_out, left, right);
755  }
756 
757  // Bitwise
758 
759  case Expr::Not: {
760  NotExpr *ne = cast<NotExpr>(e);
761  ExprHandle expr = construct(ne->expr, width_out);
762  if (*width_out==1) {
763  return vc_notExpr(vc, expr);
764  } else {
765  return vc_bvNotExpr(vc, expr);
766  }
767  }
768 
769  case Expr::And: {
770  AndExpr *ae = cast<AndExpr>(e);
771  ExprHandle left = construct(ae->left, width_out);
772  ExprHandle right = construct(ae->right, width_out);
773  if (*width_out==1) {
774  return vc_andExpr(vc, left, right);
775  } else {
776  return vc_bvAndExpr(vc, left, right);
777  }
778  }
779 
780  case Expr::Or: {
781  OrExpr *oe = cast<OrExpr>(e);
782  ExprHandle left = construct(oe->left, width_out);
783  ExprHandle right = construct(oe->right, width_out);
784  if (*width_out==1) {
785  return vc_orExpr(vc, left, right);
786  } else {
787  return vc_bvOrExpr(vc, left, right);
788  }
789  }
790 
791  case Expr::Xor: {
792  XorExpr *xe = cast<XorExpr>(e);
793  ExprHandle left = construct(xe->left, width_out);
794  ExprHandle right = construct(xe->right, width_out);
795 
796  if (*width_out==1) {
797  // XXX check for most efficient?
798  return vc_iteExpr(vc, left,
799  ExprHandle(vc_notExpr(vc, right)), right);
800  } else {
801  return vc_bvXorExpr(vc, left, right);
802  }
803  }
804 
805  case Expr::Shl: {
806  ShlExpr *se = cast<ShlExpr>(e);
807  ExprHandle left = construct(se->left, width_out);
808  assert(*width_out!=1 && "uncanonicalized shl");
809 
810  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
811  return bvLeftShift(left, (unsigned) CE->getLimitedValue());
812  } else {
813  int shiftWidth;
814  ExprHandle amount = construct(se->right, &shiftWidth);
815  return bvVarLeftShift( left, amount);
816  }
817  }
818 
819  case Expr::LShr: {
820  LShrExpr *lse = cast<LShrExpr>(e);
821  ExprHandle left = construct(lse->left, width_out);
822  assert(*width_out!=1 && "uncanonicalized lshr");
823 
824  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
825  return bvRightShift(left, (unsigned) CE->getLimitedValue());
826  } else {
827  int shiftWidth;
828  ExprHandle amount = construct(lse->right, &shiftWidth);
829  return bvVarRightShift( left, amount);
830  }
831  }
832 
833  case Expr::AShr: {
834  AShrExpr *ase = cast<AShrExpr>(e);
835  ExprHandle left = construct(ase->left, width_out);
836  assert(*width_out!=1 && "uncanonicalized ashr");
837 
838  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
839  unsigned shift = (unsigned) CE->getLimitedValue();
840  ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
841  return constructAShrByConstant(left, shift, signedBool);
842  } else {
843  int shiftWidth;
844  ExprHandle amount = construct(ase->right, &shiftWidth);
845  return bvVarArithRightShift( left, amount);
846  }
847  }
848 
849  // Comparison
850 
851  case Expr::Eq: {
852  EqExpr *ee = cast<EqExpr>(e);
853  ExprHandle left = construct(ee->left, width_out);
854  ExprHandle right = construct(ee->right, width_out);
855  if (*width_out==1) {
856  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
857  if (CE->isTrue())
858  return right;
859  return vc_notExpr(vc, right);
860  } else {
861  return vc_iffExpr(vc, left, right);
862  }
863  } else {
864  *width_out = 1;
865  return vc_eqExpr(vc, left, right);
866  }
867  }
868 
869  case Expr::Ult: {
870  UltExpr *ue = cast<UltExpr>(e);
871  ExprHandle left = construct(ue->left, width_out);
872  ExprHandle right = construct(ue->right, width_out);
873  assert(*width_out!=1 && "uncanonicalized ult");
874  *width_out = 1;
875  return vc_bvLtExpr(vc, left, right);
876  }
877 
878  case Expr::Ule: {
879  UleExpr *ue = cast<UleExpr>(e);
880  ExprHandle left = construct(ue->left, width_out);
881  ExprHandle right = construct(ue->right, width_out);
882  assert(*width_out!=1 && "uncanonicalized ule");
883  *width_out = 1;
884  return vc_bvLeExpr(vc, left, right);
885  }
886 
887  case Expr::Slt: {
888  SltExpr *se = cast<SltExpr>(e);
889  ExprHandle left = construct(se->left, width_out);
890  ExprHandle right = construct(se->right, width_out);
891  assert(*width_out!=1 && "uncanonicalized slt");
892  *width_out = 1;
893  return vc_sbvLtExpr(vc, left, right);
894  }
895 
896  case Expr::Sle: {
897  SleExpr *se = cast<SleExpr>(e);
898  ExprHandle left = construct(se->left, width_out);
899  ExprHandle right = construct(se->right, width_out);
900  assert(*width_out!=1 && "uncanonicalized sle");
901  *width_out = 1;
902  return vc_sbvLeExpr(vc, left, right);
903  }
904 
905  // unused due to canonicalization
906 #if 0
907  case Expr::Ne:
908  case Expr::Ugt:
909  case Expr::Uge:
910  case Expr::Sgt:
911  case Expr::Sge:
912 #endif
913 
914  default:
915  assert(0 && "unhandled Expr type");
916  return vc_trueExpr(vc);
917  }
918 }
919 
920 
ExprHandle getTrue()
Definition: STPBuilder.cpp:129
void ComputeMultConstants64(uint64_t multiplicand, uint64_t &add, uint64_t &sub)
Not used in canonical form.
Definition: Expr.h:151
::VCExpr buildVar(const char *name, unsigned width)
Definition: STPBuilder.cpp:99
uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth)
ref< Expr > index
Definition: Expr.h:578
STPArrayExprHash _arr_hash
Definition: STPBuilder.h:79
unsigned size
Definition: Expr.h:605
ref< Expr > trueExpr
Definition: Expr.h:732
ref< Expr > expr
Definition: Expr.h:900
ExprHandle bvConst32(unsigned width, uint32_t value)
Definition: STPBuilder.cpp:144
ExprHandle bvZero(unsigned width)
Definition: STPBuilder.cpp:138
ExprHandle tempVars[4]
Definition: STPBuilder.h:71
ExprHandle getTempVar(Expr::Width w)
Definition: STPBuilder.cpp:119
ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift)
Definition: STPBuilder.cpp:229
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
static const Width Int16
Definition: Expr.h:99
ExprHandle eqExpr(ExprHandle a, ExprHandle b)
Definition: STPBuilder.cpp:171
void hashArrayExpr(const Array *array, T &exp)
Definition: ArrayExprHash.h:94
UpdateList updates
Definition: Expr.h:687
Not used in canonical form.
Definition: Expr.h:155
uint64_t getZExtValue(unsigned bits=64) const
Definition: Expr.h:361
ExprHandle construct(ref< Expr > e, int *width_out)
Definition: STPBuilder.cpp:491
Class representing an if-then-else expression.
Definition: Expr.h:726
ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x)
Definition: STPBuilder.cpp:298
unsigned offset
Definition: Expr.h:848
::VCExpr getInitialArray(const Array *os)
Definition: STPBuilder.cpp:426
::VCExpr buildArray(const char *name, unsigned indexWidth, unsigned valueWidth)
Definition: STPBuilder.cpp:107
Width getWidth() const
Definition: Expr.h:801
ref< Expr > value
Definition: Expr.h:578
uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth)
ExprHandle bvMinusOne(unsigned width)
Definition: STPBuilder.cpp:141
Not used in canonical form.
Definition: Expr.h:154
static const Width Int32
Definition: Expr.h:100
static const Width Int8
Definition: Expr.h:98
Not used in canonical form.
Definition: Expr.h:158
::VCExpr getArrayForUpdate(const Array *root, const UpdateNode *un)
Definition: STPBuilder.cpp:466
ref< Expr > src
Definition: Expr.h:945
ExprHandle bvExtract(ExprHandle expr, unsigned top, unsigned bottom)
Definition: STPBuilder.cpp:168
void hashUpdateNodeExpr(const UpdateNode *un, T &exp)
ExprHandle bvSExtConst(unsigned width, uint64_t value)
Definition: STPBuilder.cpp:159
ref< Expr > src
Definition: Expr.h:539
static const Width Int64
Definition: Expr.h:101
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:432
Width getWidth() const
Definition: Expr.h:861
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
#define add(name, handler, ret)
ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d)
Definition: STPBuilder.cpp:351
ExprHandle bvOne(unsigned width)
Definition: STPBuilder.cpp:135
bool lookupUpdateNodeExpr(const UpdateNode *un, T &exp) const
ExprHandle bvZExtConst(unsigned width, uint64_t value)
Definition: STPBuilder.cpp:150
const std::string name
Definition: Expr.h:603
ExprHashMap< std::pair< ExprHandle, unsigned > > constructed
Definition: STPBuilder.h:72
uint64_t isPowerOfTwo(uint64_t x)
Definition: Bits.h:83
ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift)
Definition: STPBuilder.cpp:208
ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, ExprHandle isSigned)
Definition: STPBuilder.cpp:279
ExprHandle bvLeftShift(ExprHandle expr, unsigned shift)
Definition: STPBuilder.cpp:191
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
void ComputeUDivConstants32(uint32_t d, uint32_t &mprime, uint32_t &sh1, uint32_t &sh2)
ref< Expr > ExprHandle
Definition: Parser.h:27
ref< Expr > expr
Definition: Expr.h:847
ExprHandle constructActual(ref< Expr > e, int *width_out)
Definition: STPBuilder.cpp:514
Expr::Width getRange() const
Definition: Expr.h:645
const UpdateNode * next
Definition: Expr.h:577
bool isConstantArray() const
Definition: Expr.h:642
Expr::Width getDomain() const
Definition: Expr.h:644
virtual ~STPArrayExprHash()
Definition: STPBuilder.cpp:53
ExprHandle bvBoolExtract(ExprHandle expr, int bit)
Definition: STPBuilder.cpp:165
const Array * root
Definition: Expr.h:659
ExprHandle getFalse()
Definition: STPBuilder.cpp:132
ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d)
Definition: STPBuilder.cpp:388
virtual Kind getKind() const =0
Class representing a one byte read from an array.
Definition: Expr.h:681
Width getWidth() const
Definition: Expr.h:340
unsigned indexOfSingleBit(uint64_t x)
Definition: Bits.h:90
ref< Expr > index
Definition: Expr.h:688
Class representing a byte update of an array.
Definition: Expr.h:569
unsigned getNumKids() const
Definition: Expr.h:806
ref< Expr > cond
Definition: Expr.h:732
ExprHandle bvRightShift(ExprHandle expr, unsigned shift)
Definition: STPBuilder.cpp:176
ExprHandle getInitialRead(const Array *os, unsigned index)
Definition: STPBuilder.cpp:462
Not used in canonical form.
Definition: Expr.h:159
uint64_t truncateToNBits(uint64_t x, unsigned N)
Definition: Bits.h:71
ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift)
Definition: STPBuilder.cpp:250
STPBuilder(::VC _vc, bool _optimizeDivides=true)
Definition: STPBuilder.cpp:80
ExprHandle bvConst64(unsigned width, uint64_t value)
Definition: STPBuilder.cpp:147
bool lookupArrayExpr(const Array *array, T &exp) const
Definition: ArrayExprHash.h:77
void ComputeSDivConstants32(int32_t d, int32_t &mprime, int32_t &dsign, int32_t &shpost)
ref< Expr > falseExpr
Definition: Expr.h:732
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:807
void vc_DeleteExpr(void *)
bool optimizeDivides
Definition: STPBuilder.h:77
Width getWidth() const
Definition: Expr.h:951
Statistic queryConstructs