klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprRangeEvaluator.h
Go to the documentation of this file.
1 //===-- ExprRangeEvaluator.h ------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_EXPRRANGEEVALUATOR_H
11 #define KLEE_EXPRRANGEEVALUATOR_H
12 
13 #include "klee/Expr.h"
14 #include "klee/util/Bits.h"
15 
16 namespace klee {
17 
18 /*
19 class ValueType {
20 public:
21  ValueType(); // empty range
22  ValueType(uint64_t value);
23  ValueType(uint64_t min, uint64_t max);
24 
25  bool mustEqual(const uint64_t b);
26  bool mustEqual(const ValueType &b);
27  bool mayEqual(const uint64_t b);
28  bool mayEqual(const ValueType &b);
29 
30  bool isFullRange(unsigned width);
31 
32  ValueType set_union(ValueType &);
33  ValueType set_intersection(ValueType &);
34  ValueType set_difference(ValueType &);
35 
36  ValueType binaryAnd(ValueType &);
37  ValueType binaryOr(ValueType &);
38  ValueType binaryXor(ValueType &);
39  ValueType concat(ValueType &, unsigned width);
40  ValueType add(ValueType &, unsigned width);
41  ValueType sub(ValueType &, unsigned width);
42  ValueType mul(ValueType &, unsigned width);
43  ValueType udiv(ValueType &, unsigned width);
44  ValueType sdiv(ValueType &, unsigned width);
45  ValueType urem(ValueType &, unsigned width);
46  ValueType srem(ValueType &, unsigned width);
47 
48  uint64_t min();
49  uint64_t max();
50  int64_t minSigned(unsigned width);
51  int64_t maxSigned(unsigned width);
52 }
53 */
54 
55 template<class T>
57 protected:
60  virtual T getInitialReadRange(const Array &os, T index) = 0;
61 
62  T evalRead(const UpdateList &ul, T index);
63 
64 public:
66  virtual ~ExprRangeEvaluator() {}
67 
68  T evaluate(const ref<Expr> &e);
69 };
70 
71 template<class T>
73  T index) {
74  T res;
75 
76  for (const UpdateNode *un=ul.head; un; un=un->next) {
77  T ui = evaluate(un->index);
78 
79  if (ui.mustEqual(index)) {
80  return res.set_union(evaluate(un->value));
81  } else if (ui.mayEqual(index)) {
82  res = res.set_union(evaluate(un->value));
83  if (res.isFullRange(8)) {
84  return res;
85  }
86  }
87  }
88 
89  return res.set_union(getInitialReadRange(*ul.root, index));
90 }
91 
92 template<class T>
94  switch (e->getKind()) {
95  case Expr::Constant:
96  return T(cast<ConstantExpr>(e));
97 
98  case Expr::NotOptimized:
99  break;
100 
101  case Expr::Read: {
102  const ReadExpr *re = cast<ReadExpr>(e);
103  T index = evaluate(re->index);
104 
105  assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read");
106 
107  return evalRead(re->updates, index);
108  }
109 
110  case Expr::Select: {
111  const SelectExpr *se = cast<SelectExpr>(e);
112  T cond = evaluate(se->cond);
113 
114  if (cond.mustEqual(1)) {
115  return evaluate(se->trueExpr);
116  } else if (cond.mustEqual(0)) {
117  return evaluate(se->falseExpr);
118  } else {
119  return evaluate(se->trueExpr).set_union(evaluate(se->falseExpr));
120  }
121  }
122 
123  // XXX these should be unrolled to ensure nice inline
124  case Expr::Concat: {
125  const Expr *ep = e.get();
126  T res(0);
127  for (unsigned i=0; i<ep->getNumKids(); i++)
128  res = res.concat(evaluate(ep->getKid(i)),8);
129  return res;
130  }
131 
132  // Arithmetic
133 
134  case Expr::Add: {
135  const BinaryExpr *be = cast<BinaryExpr>(e);
136  unsigned width = be->left->getWidth();
137  return evaluate(be->left).add(evaluate(be->right), width);
138  }
139  case Expr::Sub: {
140  const BinaryExpr *be = cast<BinaryExpr>(e);
141  unsigned width = be->left->getWidth();
142  return evaluate(be->left).sub(evaluate(be->right), width);
143  }
144  case Expr::Mul: {
145  const BinaryExpr *be = cast<BinaryExpr>(e);
146  unsigned width = be->left->getWidth();
147  return evaluate(be->left).mul(evaluate(be->right), width);
148  }
149  case Expr::UDiv: {
150  const BinaryExpr *be = cast<BinaryExpr>(e);
151  unsigned width = be->left->getWidth();
152  return evaluate(be->left).udiv(evaluate(be->right), width);
153  }
154  case Expr::SDiv: {
155  const BinaryExpr *be = cast<BinaryExpr>(e);
156  unsigned width = be->left->getWidth();
157  return evaluate(be->left).sdiv(evaluate(be->right), width);
158  }
159  case Expr::URem: {
160  const BinaryExpr *be = cast<BinaryExpr>(e);
161  unsigned width = be->left->getWidth();
162  return evaluate(be->left).urem(evaluate(be->right), width);
163  }
164  case Expr::SRem: {
165  const BinaryExpr *be = cast<BinaryExpr>(e);
166  unsigned width = be->left->getWidth();
167  return evaluate(be->left).srem(evaluate(be->right), width);
168  }
169 
170  // Binary
171 
172  case Expr::And: {
173  const BinaryExpr *be = cast<BinaryExpr>(e);
174  return evaluate(be->left).binaryAnd(evaluate(be->right));
175  }
176  case Expr::Or: {
177  const BinaryExpr *be = cast<BinaryExpr>(e);
178  return evaluate(be->left).binaryOr(evaluate(be->right));
179  }
180  case Expr::Xor: {
181  const BinaryExpr *be = cast<BinaryExpr>(e);
182  return evaluate(be->left).binaryXor(evaluate(be->right));
183  }
184  case Expr::Shl: {
185  // BinaryExpr *be = cast<BinaryExpr>(e);
186  // unsigned width = be->left->getWidth();
187  // return evaluate(be->left).shl(evaluate(be->right), width);
188  break;
189  }
190  case Expr::LShr: {
191  // BinaryExpr *be = cast<BinaryExpr>(e);
192  // unsigned width = be->left->getWidth();
193  // return evaluate(be->left).lshr(evaluate(be->right), width);
194  break;
195  }
196  case Expr::AShr: {
197  // BinaryExpr *be = cast<BinaryExpr>(e);
198  // unsigned width = be->left->getWidth();
199  // return evaluate(be->left).ashr(evaluate(be->right), width);
200  break;
201  }
202 
203  // Comparison
204 
205  case Expr::Eq: {
206  const BinaryExpr *be = cast<BinaryExpr>(e);
207  T left = evaluate(be->left);
208  T right = evaluate(be->right);
209 
210  if (left.mustEqual(right)) {
211  return T(1);
212  } else if (!left.mayEqual(right)) {
213  return T(0);
214  }
215  break;
216  }
217 
218  case Expr::Ult: {
219  const BinaryExpr *be = cast<BinaryExpr>(e);
220  T left = evaluate(be->left);
221  T right = evaluate(be->right);
222 
223  if (left.max() < right.min()) {
224  return T(1);
225  } else if (left.min() >= right.max()) {
226  return T(0);
227  }
228  break;
229  }
230  case Expr::Ule: {
231  const BinaryExpr *be = cast<BinaryExpr>(e);
232  T left = evaluate(be->left);
233  T right = evaluate(be->right);
234 
235  if (left.max() <= right.min()) {
236  return T(1);
237  } else if (left.min() > right.max()) {
238  return T(0);
239  }
240  break;
241  }
242  case Expr::Slt: {
243  const BinaryExpr *be = cast<BinaryExpr>(e);
244  T left = evaluate(be->left);
245  T right = evaluate(be->right);
246  unsigned bits = be->left->getWidth();
247 
248  if (left.maxSigned(bits) < right.minSigned(bits)) {
249  return T(1);
250  } else if (left.minSigned(bits) >= right.maxSigned(bits)) {
251  return T(0);
252  }
253  break;
254  }
255  case Expr::Sle: {
256  const BinaryExpr *be = cast<BinaryExpr>(e);
257  T left = evaluate(be->left);
258  T right = evaluate(be->right);
259  unsigned bits = be->left->getWidth();
260 
261  if (left.maxSigned(bits) <= right.minSigned(bits)) {
262  return T(1);
263  } else if (left.minSigned(bits) > right.maxSigned(bits)) {
264  return T(0);
265  }
266  break;
267  }
268 
269  case Expr::Ne:
270  case Expr::Ugt:
271  case Expr::Uge:
272  case Expr::Sgt:
273  case Expr::Sge:
274  assert(0 && "invalid expressions (uncanonicalized)");
275 
276  default:
277  break;
278  }
279 
280  return T(0, bits64::maxValueOfNBits(e->getWidth()));
281 }
282 
283 }
284 
285 #endif
T * get() const
Definition: Ref.h:69
uint64_t maxValueOfNBits(unsigned N)
Definition: Bits.h:64
ref< Expr > left
Definition: Expr.h:494
Not used in canonical form.
Definition: Expr.h:151
virtual unsigned getNumKids() const =0
ref< Expr > trueExpr
Definition: Expr.h:732
Class representing a complete list of updates into an array.
Definition: Expr.h:655
UpdateList updates
Definition: Expr.h:687
Not used in canonical form.
Definition: Expr.h:155
Expr::Width range
Definition: Expr.h:612
Class representing an if-then-else expression.
Definition: Expr.h:726
Not used in canonical form.
Definition: Expr.h:154
Class representing symbolic expressions.
Definition: Expr.h:88
Not used in canonical form.
Definition: Expr.h:158
virtual T getInitialReadRange(const Array &os, T index)=0
virtual Width getWidth() const =0
virtual ref< Expr > getKid(unsigned i) const =0
Width getWidth() const
Definition: Expr.h:699
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
T evalRead(const UpdateList &ul, T index)
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
Class representing a one byte read from an array.
Definition: Expr.h:681
T evaluate(const ref< Expr > &e)
ref< Expr > index
Definition: Expr.h:688
Class representing a byte update of an array.
Definition: Expr.h:569
ref< Expr > cond
Definition: Expr.h:732
Not used in canonical form.
Definition: Expr.h:159
ref< Expr > falseExpr
Definition: Expr.h:732