klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprBuilder.cpp
Go to the documentation of this file.
1 //===-- ExprBuilder.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 "klee/ExprBuilder.h"
11 
12 using namespace klee;
13 
15 }
16 
18 }
19 
20 namespace {
21  class DefaultExprBuilder : public ExprBuilder {
22  virtual ref<Expr> Constant(const llvm::APInt &Value) {
23  return ConstantExpr::alloc(Value);
24  }
25 
26  virtual ref<Expr> NotOptimized(const ref<Expr> &Index) {
27  return NotOptimizedExpr::alloc(Index);
28  }
29 
30  virtual ref<Expr> Read(const UpdateList &Updates,
31  const ref<Expr> &Index) {
32  return ReadExpr::alloc(Updates, Index);
33  }
34 
35  virtual ref<Expr> Select(const ref<Expr> &Cond,
36  const ref<Expr> &LHS, const ref<Expr> &RHS) {
37  return SelectExpr::alloc(Cond, LHS, RHS);
38  }
39 
40  virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) {
41  return ConcatExpr::alloc(LHS, RHS);
42  }
43 
44  virtual ref<Expr> Extract(const ref<Expr> &LHS,
45  unsigned Offset, Expr::Width W) {
46  return ExtractExpr::alloc(LHS, Offset, W);
47  }
48 
49  virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) {
50  return ZExtExpr::alloc(LHS, W);
51  }
52 
53  virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) {
54  return SExtExpr::alloc(LHS, W);
55  }
56 
57  virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) {
58  return AddExpr::alloc(LHS, RHS);
59  }
60 
61  virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) {
62  return SubExpr::alloc(LHS, RHS);
63  }
64 
65  virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) {
66  return MulExpr::alloc(LHS, RHS);
67  }
68 
69  virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
70  return UDivExpr::alloc(LHS, RHS);
71  }
72 
73  virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
74  return SDivExpr::alloc(LHS, RHS);
75  }
76 
77  virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
78  return URemExpr::alloc(LHS, RHS);
79  }
80 
81  virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
82  return SRemExpr::alloc(LHS, RHS);
83  }
84 
85  virtual ref<Expr> Not(const ref<Expr> &LHS) {
86  return NotExpr::alloc(LHS);
87  }
88 
89  virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
90  return AndExpr::alloc(LHS, RHS);
91  }
92 
93  virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) {
94  return OrExpr::alloc(LHS, RHS);
95  }
96 
97  virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) {
98  return XorExpr::alloc(LHS, RHS);
99  }
100 
101  virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) {
102  return ShlExpr::alloc(LHS, RHS);
103  }
104 
105  virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
106  return LShrExpr::alloc(LHS, RHS);
107  }
108 
109  virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
110  return AShrExpr::alloc(LHS, RHS);
111  }
112 
113  virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) {
114  return EqExpr::alloc(LHS, RHS);
115  }
116 
117  virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
118  return NeExpr::alloc(LHS, RHS);
119  }
120 
121  virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) {
122  return UltExpr::alloc(LHS, RHS);
123  }
124 
125  virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) {
126  return UleExpr::alloc(LHS, RHS);
127  }
128 
129  virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
130  return UgtExpr::alloc(LHS, RHS);
131  }
132 
133  virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
134  return UgeExpr::alloc(LHS, RHS);
135  }
136 
137  virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
138  return SltExpr::alloc(LHS, RHS);
139  }
140 
141  virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) {
142  return SleExpr::alloc(LHS, RHS);
143  }
144 
145  virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
146  return SgtExpr::alloc(LHS, RHS);
147  }
148 
149  virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
150  return SgeExpr::alloc(LHS, RHS);
151  }
152  };
153 
157  class ChainedBuilder {
158  protected:
161  ExprBuilder *Builder;
162 
164  ExprBuilder *Base;
165 
166  public:
167  ChainedBuilder(ExprBuilder *_Builder, ExprBuilder *_Base)
168  : Builder(_Builder), Base(_Base) {}
169  ~ChainedBuilder() { delete Base; }
170 
171  ref<Expr> Constant(const llvm::APInt &Value) {
172  return Base->Constant(Value);
173  }
174 
175  ref<Expr> NotOptimized(const ref<Expr> &Index) {
176  return Base->NotOptimized(Index);
177  }
178 
179  ref<Expr> Read(const UpdateList &Updates,
180  const ref<Expr> &Index) {
181  return Base->Read(Updates, Index);
182  }
183 
184  ref<Expr> Select(const ref<Expr> &Cond,
185  const ref<Expr> &LHS, const ref<Expr> &RHS) {
186  return Base->Select(Cond, LHS, RHS);
187  }
188 
189  ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) {
190  return Base->Concat(LHS, RHS);
191  }
192 
193  ref<Expr> Extract(const ref<Expr> &LHS,
194  unsigned Offset, Expr::Width W) {
195  return Base->Extract(LHS, Offset, W);
196  }
197 
198  ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) {
199  return Base->ZExt(LHS, W);
200  }
201 
202  ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) {
203  return Base->SExt(LHS, W);
204  }
205 
206  ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) {
207  return Base->Add(LHS, RHS);
208  }
209 
210  ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) {
211  return Base->Sub(LHS, RHS);
212  }
213 
214  ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) {
215  return Base->Mul(LHS, RHS);
216  }
217 
218  ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
219  return Base->UDiv(LHS, RHS);
220  }
221 
222  ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
223  return Base->SDiv(LHS, RHS);
224  }
225 
226  ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
227  return Base->URem(LHS, RHS);
228  }
229 
230  ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
231  return Base->SRem(LHS, RHS);
232  }
233 
234  ref<Expr> Not(const ref<Expr> &LHS) {
235  return Base->Not(LHS);
236  }
237 
238  ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
239  return Base->And(LHS, RHS);
240  }
241 
242  ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) {
243  return Base->Or(LHS, RHS);
244  }
245 
246  ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) {
247  return Base->Xor(LHS, RHS);
248  }
249 
250  ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) {
251  return Base->Shl(LHS, RHS);
252  }
253 
254  ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
255  return Base->LShr(LHS, RHS);
256  }
257 
258  ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
259  return Base->AShr(LHS, RHS);
260  }
261 
262  ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) {
263  return Base->Eq(LHS, RHS);
264  }
265 
266  ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
267  return Base->Ne(LHS, RHS);
268  }
269 
270  ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) {
271  return Base->Ult(LHS, RHS);
272  }
273 
274  ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) {
275  return Base->Ule(LHS, RHS);
276  }
277 
278  ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
279  return Base->Ugt(LHS, RHS);
280  }
281 
282  ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
283  return Base->Uge(LHS, RHS);
284  }
285 
286  ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
287  return Base->Slt(LHS, RHS);
288  }
289 
290  ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) {
291  return Base->Sle(LHS, RHS);
292  }
293 
294  ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
295  return Base->Sgt(LHS, RHS);
296  }
297 
298  ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
299  return Base->Sge(LHS, RHS);
300  }
301  };
302 
310  template<typename SpecializedBuilder>
311  class ConstantSpecializedExprBuilder : public ExprBuilder {
312  SpecializedBuilder Builder;
313 
314  public:
315  ConstantSpecializedExprBuilder(ExprBuilder *Base) : Builder(this, Base) {}
316  ~ConstantSpecializedExprBuilder() {}
317 
318  virtual ref<Expr> Constant(const llvm::APInt &Value) {
319  return Builder.Constant(Value);
320  }
321 
322  virtual ref<Expr> NotOptimized(const ref<Expr> &Index) {
323  return Builder.NotOptimized(Index);
324  }
325 
326  virtual ref<Expr> Read(const UpdateList &Updates,
327  const ref<Expr> &Index) {
328  // Roll back through writes when possible.
329  const UpdateNode *UN = Updates.head;
330  while (UN && Eq(Index, UN->index)->isFalse())
331  UN = UN->next;
332 
333  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Index))
334  return Builder.Read(UpdateList(Updates.root, UN), CE);
335 
336  return Builder.Read(UpdateList(Updates.root, UN), Index);
337  }
338 
339  virtual ref<Expr> Select(const ref<Expr> &Cond,
340  const ref<Expr> &LHS, const ref<Expr> &RHS) {
341  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Cond))
342  return CE->isTrue() ? LHS : RHS;
343 
344  return Builder.Select(cast<NonConstantExpr>(Cond), LHS, RHS);
345  }
346 
347  virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) {
348  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
349  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
350  return LCE->Concat(RCE);
351  return Builder.Concat(LCE, cast<NonConstantExpr>(RHS));
352  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
353  return Builder.Concat(cast<NonConstantExpr>(LHS), RCE);
354  }
355 
356  return Builder.Concat(cast<NonConstantExpr>(LHS),
357  cast<NonConstantExpr>(RHS));
358  }
359 
360  virtual ref<Expr> Extract(const ref<Expr> &LHS,
361  unsigned Offset, Expr::Width W) {
362  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS))
363  return CE->Extract(Offset, W);
364 
365  return Builder.Extract(cast<NonConstantExpr>(LHS), Offset, W);
366  }
367 
368  virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) {
369  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS))
370  return CE->ZExt(W);
371 
372  return Builder.ZExt(cast<NonConstantExpr>(LHS), W);
373  }
374 
375  virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) {
376  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS))
377  return CE->SExt(W);
378 
379  return Builder.SExt(cast<NonConstantExpr>(LHS), W);
380  }
381 
382  virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) {
383  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
384  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
385  return LCE->Add(RCE);
386  return Builder.Add(LCE, cast<NonConstantExpr>(RHS));
387  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
388  return Builder.Add(cast<NonConstantExpr>(LHS), RCE);
389  }
390 
391  return Builder.Add(cast<NonConstantExpr>(LHS),
392  cast<NonConstantExpr>(RHS));
393  }
394 
395  virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) {
396  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
397  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
398  return LCE->Sub(RCE);
399  return Builder.Sub(LCE, cast<NonConstantExpr>(RHS));
400  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
401  return Builder.Sub(cast<NonConstantExpr>(LHS), RCE);
402  }
403 
404  return Builder.Sub(cast<NonConstantExpr>(LHS),
405  cast<NonConstantExpr>(RHS));
406  }
407 
408  virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) {
409  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
410  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
411  return LCE->Mul(RCE);
412  return Builder.Mul(LCE, cast<NonConstantExpr>(RHS));
413  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
414  return Builder.Mul(cast<NonConstantExpr>(LHS), RCE);
415  }
416 
417  return Builder.Mul(cast<NonConstantExpr>(LHS),
418  cast<NonConstantExpr>(RHS));
419  }
420 
421  virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
422  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
423  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
424  return LCE->UDiv(RCE);
425  return Builder.UDiv(LCE, cast<NonConstantExpr>(RHS));
426  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
427  return Builder.UDiv(cast<NonConstantExpr>(LHS), RCE);
428  }
429 
430  return Builder.UDiv(cast<NonConstantExpr>(LHS),
431  cast<NonConstantExpr>(RHS));
432  }
433 
434  virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
435  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
436  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
437  return LCE->SDiv(RCE);
438  return Builder.SDiv(LCE, cast<NonConstantExpr>(RHS));
439  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
440  return Builder.SDiv(cast<NonConstantExpr>(LHS), RCE);
441  }
442 
443  return Builder.SDiv(cast<NonConstantExpr>(LHS),
444  cast<NonConstantExpr>(RHS));
445  }
446 
447  virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
448  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
449  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
450  return LCE->URem(RCE);
451  return Builder.URem(LCE, cast<NonConstantExpr>(RHS));
452  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
453  return Builder.URem(cast<NonConstantExpr>(LHS), RCE);
454  }
455 
456  return Builder.URem(cast<NonConstantExpr>(LHS),
457  cast<NonConstantExpr>(RHS));
458  }
459 
460  virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
461  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
462  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
463  return LCE->SRem(RCE);
464  return Builder.SRem(LCE, cast<NonConstantExpr>(RHS));
465  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
466  return Builder.SRem(cast<NonConstantExpr>(LHS), RCE);
467  }
468 
469  return Builder.SRem(cast<NonConstantExpr>(LHS),
470  cast<NonConstantExpr>(RHS));
471  }
472 
473  virtual ref<Expr> Not(const ref<Expr> &LHS) {
474  // !!X ==> X
475  if (NotExpr *DblNot = dyn_cast<NotExpr>(LHS))
476  return DblNot->getKid(0);
477 
478  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS))
479  return CE->Not();
480 
481  return Builder.Not(cast<NonConstantExpr>(LHS));
482  }
483 
484  virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
485  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
486  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
487  return LCE->And(RCE);
488  return Builder.And(LCE, cast<NonConstantExpr>(RHS));
489  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
490  return Builder.And(cast<NonConstantExpr>(LHS), RCE);
491  }
492 
493  return Builder.And(cast<NonConstantExpr>(LHS),
494  cast<NonConstantExpr>(RHS));
495  }
496 
497  virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) {
498  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
499  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
500  return LCE->Or(RCE);
501  return Builder.Or(LCE, cast<NonConstantExpr>(RHS));
502  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
503  return Builder.Or(cast<NonConstantExpr>(LHS), RCE);
504  }
505 
506  return Builder.Or(cast<NonConstantExpr>(LHS),
507  cast<NonConstantExpr>(RHS));
508  }
509 
510  virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) {
511  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
512  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
513  return LCE->Xor(RCE);
514  return Builder.Xor(LCE, cast<NonConstantExpr>(RHS));
515  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
516  return Builder.Xor(cast<NonConstantExpr>(LHS), RCE);
517  }
518 
519  return Builder.Xor(cast<NonConstantExpr>(LHS),
520  cast<NonConstantExpr>(RHS));
521  }
522 
523  virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) {
524  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
525  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
526  return LCE->Shl(RCE);
527  return Builder.Shl(LCE, cast<NonConstantExpr>(RHS));
528  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
529  return Builder.Shl(cast<NonConstantExpr>(LHS), RCE);
530  }
531 
532  return Builder.Shl(cast<NonConstantExpr>(LHS),
533  cast<NonConstantExpr>(RHS));
534  }
535 
536  virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
537  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
538  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
539  return LCE->LShr(RCE);
540  return Builder.LShr(LCE, cast<NonConstantExpr>(RHS));
541  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
542  return Builder.LShr(cast<NonConstantExpr>(LHS), RCE);
543  }
544 
545  return Builder.LShr(cast<NonConstantExpr>(LHS),
546  cast<NonConstantExpr>(RHS));
547  }
548 
549  virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
550  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
551  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
552  return LCE->AShr(RCE);
553  return Builder.AShr(LCE, cast<NonConstantExpr>(RHS));
554  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
555  return Builder.AShr(cast<NonConstantExpr>(LHS), RCE);
556  }
557 
558  return Builder.AShr(cast<NonConstantExpr>(LHS),
559  cast<NonConstantExpr>(RHS));
560  }
561 
562  virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) {
563  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
564  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
565  return LCE->Eq(RCE);
566  return Builder.Eq(LCE, cast<NonConstantExpr>(RHS));
567  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
568  return Builder.Eq(cast<NonConstantExpr>(LHS), RCE);
569  }
570 
571  return Builder.Eq(cast<NonConstantExpr>(LHS),
572  cast<NonConstantExpr>(RHS));
573  }
574 
575  virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
576  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
577  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
578  return LCE->Ne(RCE);
579  return Builder.Ne(LCE, cast<NonConstantExpr>(RHS));
580  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
581  return Builder.Ne(cast<NonConstantExpr>(LHS), RCE);
582  }
583 
584  return Builder.Ne(cast<NonConstantExpr>(LHS),
585  cast<NonConstantExpr>(RHS));
586  }
587 
588  virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) {
589  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
590  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
591  return LCE->Ult(RCE);
592  return Builder.Ult(LCE, cast<NonConstantExpr>(RHS));
593  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
594  return Builder.Ult(cast<NonConstantExpr>(LHS), RCE);
595  }
596 
597  return Builder.Ult(cast<NonConstantExpr>(LHS),
598  cast<NonConstantExpr>(RHS));
599  }
600 
601  virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) {
602  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
603  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
604  return LCE->Ule(RCE);
605  return Builder.Ule(LCE, cast<NonConstantExpr>(RHS));
606  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
607  return Builder.Ule(cast<NonConstantExpr>(LHS), RCE);
608  }
609 
610  return Builder.Ule(cast<NonConstantExpr>(LHS),
611  cast<NonConstantExpr>(RHS));
612  }
613 
614  virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
615  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
616  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
617  return LCE->Ugt(RCE);
618  return Builder.Ugt(LCE, cast<NonConstantExpr>(RHS));
619  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
620  return Builder.Ugt(cast<NonConstantExpr>(LHS), RCE);
621  }
622 
623  return Builder.Ugt(cast<NonConstantExpr>(LHS),
624  cast<NonConstantExpr>(RHS));
625  }
626 
627  virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
628  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
629  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
630  return LCE->Uge(RCE);
631  return Builder.Uge(LCE, cast<NonConstantExpr>(RHS));
632  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
633  return Builder.Uge(cast<NonConstantExpr>(LHS), RCE);
634  }
635 
636  return Builder.Uge(cast<NonConstantExpr>(LHS),
637  cast<NonConstantExpr>(RHS));
638  }
639 
640  virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
641  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
642  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
643  return LCE->Slt(RCE);
644  return Builder.Slt(LCE, cast<NonConstantExpr>(RHS));
645  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
646  return Builder.Slt(cast<NonConstantExpr>(LHS), RCE);
647  }
648 
649  return Builder.Slt(cast<NonConstantExpr>(LHS),
650  cast<NonConstantExpr>(RHS));
651  }
652 
653  virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) {
654  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
655  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
656  return LCE->Sle(RCE);
657  return Builder.Sle(LCE, cast<NonConstantExpr>(RHS));
658  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
659  return Builder.Sle(cast<NonConstantExpr>(LHS), RCE);
660  }
661 
662  return Builder.Sle(cast<NonConstantExpr>(LHS),
663  cast<NonConstantExpr>(RHS));
664  }
665 
666  virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
667  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
668  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
669  return LCE->Sgt(RCE);
670  return Builder.Sgt(LCE, cast<NonConstantExpr>(RHS));
671  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
672  return Builder.Sgt(cast<NonConstantExpr>(LHS), RCE);
673  }
674 
675  return Builder.Sgt(cast<NonConstantExpr>(LHS),
676  cast<NonConstantExpr>(RHS));
677  }
678 
679  virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
680  if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
681  if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
682  return LCE->Sge(RCE);
683  return Builder.Sge(LCE, cast<NonConstantExpr>(RHS));
684  } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) {
685  return Builder.Sge(cast<NonConstantExpr>(LHS), RCE);
686  }
687 
688  return Builder.Sge(cast<NonConstantExpr>(LHS),
689  cast<NonConstantExpr>(RHS));
690  }
691  };
692 
693  class ConstantFoldingBuilder :
694  public ChainedBuilder {
695  public:
696  ConstantFoldingBuilder(ExprBuilder *Builder, ExprBuilder *Base)
697  : ChainedBuilder(Builder, Base) {}
698 
699  ref<Expr> Add(const ref<ConstantExpr> &LHS,
700  const ref<NonConstantExpr> &RHS) {
701  // 0 + X ==> X
702  if (LHS->isZero())
703  return RHS;
704 
705  switch (RHS->getKind()) {
706  default: break;
707 
708  case Expr::Add: {
709  BinaryExpr *BE = cast<BinaryExpr>(RHS);
710  // C_0 + (C_1 + X) ==> (C_0 + C1) + X
711  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
712  return Builder->Add(LHS->Add(CE), BE->right);
713  // C_0 + (X + C_1) ==> (C_0 + C1) + X
714  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
715  return Builder->Add(LHS->Add(CE), BE->left);
716  break;
717  }
718 
719  case Expr::Sub: {
720  BinaryExpr *BE = cast<BinaryExpr>(RHS);
721  // C_0 + (C_1 - X) ==> (C_0 + C1) - X
722  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
723  return Builder->Sub(LHS->Add(CE), BE->right);
724  // C_0 + (X - C_1) ==> (C_0 - C1) + X
725  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
726  return Builder->Add(LHS->Sub(CE), BE->left);
727  break;
728  }
729  }
730 
731  return Base->Add(LHS, RHS);
732  }
733 
734  ref<Expr> Add(const ref<NonConstantExpr> &LHS,
735  const ref<ConstantExpr> &RHS) {
736  return Add(RHS, LHS);
737  }
738 
739  ref<Expr> Add(const ref<NonConstantExpr> &LHS,
740  const ref<NonConstantExpr> &RHS) {
741  switch (LHS->getKind()) {
742  default: break;
743 
744  case Expr::Add: {
745  BinaryExpr *BE = cast<BinaryExpr>(LHS);
746  // (X + Y) + Z ==> X + (Y + Z)
747  return Builder->Add(BE->left,
748  Builder->Add(BE->right, RHS));
749  }
750 
751  case Expr::Sub: {
752  BinaryExpr *BE = cast<BinaryExpr>(LHS);
753  // (X - Y) + Z ==> X + (Z - Y)
754  return Builder->Add(BE->left,
755  Builder->Sub(RHS, BE->right));
756  }
757  }
758 
759  switch (RHS->getKind()) {
760  default: break;
761 
762  case Expr::Add: {
763  BinaryExpr *BE = cast<BinaryExpr>(RHS);
764  // X + (C_0 + Y) ==> C_0 + (X + Y)
765  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
766  return Builder->Add(CE, Builder->Add(LHS, BE->right));
767  // X + (Y + C_0) ==> C_0 + (X + Y)
768  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
769  return Builder->Add(CE, Builder->Add(LHS, BE->left));
770  break;
771  }
772 
773  case Expr::Sub: {
774  BinaryExpr *BE = cast<BinaryExpr>(RHS);
775  // X + (C_0 - Y) ==> C_0 + (X - Y)
776  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
777  return Builder->Add(CE, Builder->Sub(LHS, BE->right));
778  // X + (Y - C_0) ==> -C_0 + (X + Y)
779  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
780  return Builder->Add(CE->Neg(), Builder->Add(LHS, BE->left));
781  break;
782  }
783  }
784 
785  return Base->Add(LHS, RHS);
786  }
787 
788  ref<Expr> Sub(const ref<ConstantExpr> &LHS,
789  const ref<NonConstantExpr> &RHS) {
790  switch (RHS->getKind()) {
791  default: break;
792 
793  case Expr::Add: {
794  BinaryExpr *BE = cast<BinaryExpr>(RHS);
795  // C_0 - (C_1 + X) ==> (C_0 - C1) - X
796  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
797  return Builder->Sub(LHS->Sub(CE), BE->right);
798  // C_0 - (X + C_1) ==> (C_0 + C1) + X
799  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
800  return Builder->Sub(LHS->Sub(CE), BE->left);
801  break;
802  }
803 
804  case Expr::Sub: {
805  BinaryExpr *BE = cast<BinaryExpr>(RHS);
806  // C_0 - (C_1 - X) ==> (C_0 - C1) + X
807  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
808  return Builder->Add(LHS->Sub(CE), BE->right);
809  // C_0 - (X - C_1) ==> (C_0 + C1) - X
810  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
811  return Builder->Sub(LHS->Add(CE), BE->left);
812  break;
813  }
814  }
815 
816  return Base->Sub(LHS, RHS);
817  }
818 
819  ref<Expr> Sub(const ref<NonConstantExpr> &LHS,
820  const ref<ConstantExpr> &RHS) {
821  // X - C_0 ==> -C_0 + X
822  return Add(RHS->Neg(), LHS);
823  }
824 
825  ref<Expr> Sub(const ref<NonConstantExpr> &LHS,
826  const ref<NonConstantExpr> &RHS) {
827  switch (LHS->getKind()) {
828  default: break;
829 
830  case Expr::Add: {
831  BinaryExpr *BE = cast<BinaryExpr>(LHS);
832  // (X + Y) - Z ==> X + (Y - Z)
833  return Builder->Add(BE->left, Builder->Sub(BE->right, RHS));
834  }
835 
836  case Expr::Sub: {
837  BinaryExpr *BE = cast<BinaryExpr>(LHS);
838  // (X - Y) - Z ==> X - (Y + Z)
839  return Builder->Sub(BE->left, Builder->Add(BE->right, RHS));
840  }
841  }
842 
843  switch (RHS->getKind()) {
844  default: break;
845 
846  case Expr::Add: {
847  BinaryExpr *BE = cast<BinaryExpr>(RHS);
848  // X - (C + Y) ==> -C + (X - Y)
849  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
850  return Builder->Add(CE->Neg(), Builder->Sub(LHS, BE->right));
851  // X - (Y + C) ==> -C + (X + Y)
852  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
853  return Builder->Add(CE->Neg(), Builder->Sub(LHS, BE->left));
854  break;
855  }
856 
857  case Expr::Sub: {
858  BinaryExpr *BE = cast<BinaryExpr>(RHS);
859  // X - (C - Y) ==> -C + (X + Y)
860  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
861  return Builder->Add(CE->Neg(), Builder->Add(LHS, BE->right));
862  // X - (Y - C) ==> C + (X - Y)
863  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
864  return Builder->Add(CE, Builder->Sub(LHS, BE->left));
865  break;
866  }
867  }
868 
869  return Base->Sub(LHS, RHS);
870  }
871 
872  ref<Expr> Mul(const ref<ConstantExpr> &LHS,
873  const ref<NonConstantExpr> &RHS) {
874  if (LHS->isZero())
875  return LHS;
876  if (LHS->isOne())
877  return RHS;
878  // FIXME: Unbalance nested muls, fold constants through
879  // {sub,add}-with-constant, etc.
880  return Base->Mul(LHS, RHS);
881  }
882 
883  ref<Expr> Mul(const ref<NonConstantExpr> &LHS,
884  const ref<ConstantExpr> &RHS) {
885  return Mul(RHS, LHS);
886  }
887 
888  ref<Expr> Mul(const ref<NonConstantExpr> &LHS,
889  const ref<NonConstantExpr> &RHS) {
890  return Base->Mul(LHS, RHS);
891  }
892 
893  ref<Expr> And(const ref<ConstantExpr> &LHS,
894  const ref<NonConstantExpr> &RHS) {
895  if (LHS->isZero())
896  return LHS;
897  if (LHS->isAllOnes())
898  return RHS;
899  // FIXME: Unbalance nested ands, fold constants through
900  // {and,or}-with-constant, etc.
901  return Base->And(LHS, RHS);
902  }
903 
904  ref<Expr> And(const ref<NonConstantExpr> &LHS,
905  const ref<ConstantExpr> &RHS) {
906  return And(RHS, LHS);
907  }
908 
909  ref<Expr> And(const ref<NonConstantExpr> &LHS,
910  const ref<NonConstantExpr> &RHS) {
911  return Base->And(LHS, RHS);
912  }
913 
914  ref<Expr> Or(const ref<ConstantExpr> &LHS,
915  const ref<NonConstantExpr> &RHS) {
916  if (LHS->isZero())
917  return RHS;
918  if (LHS->isAllOnes())
919  return LHS;
920  // FIXME: Unbalance nested ors, fold constants through
921  // {and,or}-with-constant, etc.
922  return Base->Or(LHS, RHS);
923  }
924 
925  ref<Expr> Or(const ref<NonConstantExpr> &LHS,
926  const ref<ConstantExpr> &RHS) {
927  return Or(RHS, LHS);
928  }
929 
930  ref<Expr> Or(const ref<NonConstantExpr> &LHS,
931  const ref<NonConstantExpr> &RHS) {
932  return Base->Or(LHS, RHS);
933  }
934 
935  ref<Expr> Xor(const ref<ConstantExpr> &LHS,
936  const ref<NonConstantExpr> &RHS) {
937  if (LHS->isZero())
938  return RHS;
939  // FIXME: Unbalance nested ors, fold constants through
940  // {and,or}-with-constant, etc.
941  return Base->Xor(LHS, RHS);
942  }
943 
944  ref<Expr> Xor(const ref<NonConstantExpr> &LHS,
945  const ref<ConstantExpr> &RHS) {
946  return Xor(RHS, LHS);
947  }
948 
949  ref<Expr> Xor(const ref<NonConstantExpr> &LHS,
950  const ref<NonConstantExpr> &RHS) {
951  return Base->Xor(LHS, RHS);
952  }
953 
954  ref<Expr> Eq(const ref<ConstantExpr> &LHS,
955  const ref<NonConstantExpr> &RHS) {
956  Expr::Width Width = LHS->getWidth();
957 
958  if (Width == Expr::Bool) {
959  // true == X ==> X
960  if (LHS->isTrue())
961  return RHS;
962 
963  // false == ... (not)
964  return Base->Not(RHS);
965  }
966 
967  return Base->Eq(LHS, RHS);
968  }
969 
970  ref<Expr> Eq(const ref<NonConstantExpr> &LHS,
971  const ref<ConstantExpr> &RHS) {
972  return Eq(RHS, LHS);
973  }
974 
975  ref<Expr> Eq(const ref<NonConstantExpr> &LHS,
976  const ref<NonConstantExpr> &RHS) {
977  return Base->Eq(LHS, RHS);
978  }
979  };
980 
981  typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder>
982  ConstantFoldingExprBuilder;
983 
984  class SimplifyingBuilder : public ChainedBuilder {
985  public:
986  SimplifyingBuilder(ExprBuilder *Builder, ExprBuilder *Base)
987  : ChainedBuilder(Builder, Base) {}
988 
989  ref<Expr> Eq(const ref<ConstantExpr> &LHS,
990  const ref<NonConstantExpr> &RHS) {
991  Expr::Width Width = LHS->getWidth();
992 
993  if (Width == Expr::Bool) {
994  // true == X ==> X
995  if (LHS->isTrue())
996  return RHS;
997 
998  // false == X (not)
999  return Base->Not(RHS);
1000  }
1001 
1002  return Base->Eq(LHS, RHS);
1003  }
1004 
1005  ref<Expr> Eq(const ref<NonConstantExpr> &LHS,
1006  const ref<ConstantExpr> &RHS) {
1007  return Eq(RHS, LHS);
1008  }
1009 
1010  ref<Expr> Eq(const ref<NonConstantExpr> &LHS,
1011  const ref<NonConstantExpr> &RHS) {
1012  // X == X ==> true
1013  if (LHS == RHS)
1014  return Builder->True();
1015 
1016  return Base->Eq(LHS, RHS);
1017  }
1018 
1019  ref<Expr> Not(const ref<NonConstantExpr> &LHS) {
1020  // Transform !(a or b) ==> !a and !b.
1021  if (const OrExpr *OE = dyn_cast<OrExpr>(LHS))
1022  return Builder->And(Builder->Not(OE->left),
1023  Builder->Not(OE->right));
1024  return Base->Not(LHS);
1025  }
1026 
1027  ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
1028  // X != Y ==> !(X == Y)
1029  return Builder->Not(Builder->Eq(LHS, RHS));
1030  }
1031 
1032  ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
1033  // X u> Y ==> Y u< X
1034  return Builder->Ult(RHS, LHS);
1035  }
1036 
1037  ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
1038  // X u>= Y ==> Y u<= X
1039  return Builder->Ule(RHS, LHS);
1040  }
1041 
1042  ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
1043  // X s> Y ==> Y s< X
1044  return Builder->Slt(RHS, LHS);
1045  }
1046 
1047  ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
1048  // X s>= Y ==> Y s<= X
1049  return Builder->Sle(RHS, LHS);
1050  }
1051  };
1052 
1053  typedef ConstantSpecializedExprBuilder<SimplifyingBuilder>
1054  SimplifyingExprBuilder;
1055 }
1056 
1058  return new DefaultExprBuilder();
1059 }
1060 
1062  return new ConstantFoldingExprBuilder(Base);
1063 }
1064 
1066  return new SimplifyingExprBuilder(Base);
1067 }
static ref< Expr > alloc(const ref< Expr > &src)
Definition: Expr.h:541
static ref< Expr > alloc(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.h:793
ref< Expr > left
Definition: Expr.h:494
ref< ConstantExpr > Neg()
Definition: Expr.cpp:380
ref< ConstantExpr > Sub(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:384
Not used in canonical form.
Definition: Expr.h:151
ExprBuilder * createSimplifyingExprBuilder(ExprBuilder *Base)
ExprBuilder * createDefaultExprBuilder()
ref< Expr > index
Definition: Expr.h:578
ref< ConstantExpr > Or(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:412
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
bool isOne() const
isOne - Is this a constant one.
Definition: Expr.h:429
virtual ~ExprBuilder()
Definition: ExprBuilder.cpp:17
bool isZero() const
isZero - Is this a constant zero.
Definition: Expr.h:426
Class representing a complete list of updates into an array.
Definition: Expr.h:655
Not used in canonical form.
Definition: Expr.h:155
Not used in canonical form.
Definition: Expr.h:154
bool isAllOnes() const
isAllOnes - Is this constant all ones.
Definition: Expr.h:442
Not used in canonical form.
Definition: Expr.h:158
virtual ref< Expr > getKid(unsigned i) const =0
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:432
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
static ref< Expr > alloc(const ref< Expr > &e)
Definition: Expr.h:903
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1094
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
ref< Expr > right
Definition: Expr.h:494
const UpdateNode * next
Definition: Expr.h:577
const Array * root
Definition: Expr.h:659
virtual Kind getKind() const =0
static ref< Expr > alloc(const UpdateList &updates, const ref< Expr > &index)
Definition: Expr.h:691
Width getWidth() const
Definition: Expr.h:340
Class representing a byte update of an array.
Definition: Expr.h:569
static ref< Expr > alloc(const ref< Expr > &c, const ref< Expr > &t, const ref< Expr > &f)
Definition: Expr.h:735
static const Width Bool
Definition: Expr.h:97
Not used in canonical form.
Definition: Expr.h:159
ExprBuilder * createConstantFoldingExprBuilder(ExprBuilder *Base)
static ref< Expr > alloc(const ref< Expr > &e, unsigned o, Width w)
Definition: Expr.h:852
ref< ConstantExpr > Add(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:376