klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ImpliedValue.cpp
Go to the documentation of this file.
1 //===-- ImpliedValue.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 "ImpliedValue.h"
11 
12 #include "Context.h"
13 #include "klee/Constraints.h"
14 #include "klee/Expr.h"
15 #include "klee/Solver.h"
16 // FIXME: Use APInt.
18 
19 #include "klee/util/ExprUtil.h"
20 
21 #include <map>
22 #include <set>
23 
24 using namespace klee;
25 
26 // XXX we really want to do some sort of canonicalization of exprs
27 // globally so that cases below become simpler
29  ref<ConstantExpr> value,
30  ImpliedValueList &results) {
31  switch (e->getKind()) {
32  case Expr::Constant: {
33  assert(value == cast<ConstantExpr>(e) &&
34  "error in implied value calculation");
35  break;
36  }
37 
38  // Special
39 
40  case Expr::NotOptimized: break;
41 
42  case Expr::Read: {
43  // XXX in theory it is possible to descend into a symbolic index
44  // under certain circumstances (all values known, known value
45  // unique, or range known, max / min hit). Seems unlikely this
46  // would work often enough to be worth the effort.
47  ReadExpr *re = cast<ReadExpr>(e);
48  results.push_back(std::make_pair(re, value));
49  break;
50  }
51 
52  case Expr::Select: {
53  // not much to do, could improve with range analysis
54  SelectExpr *se = cast<SelectExpr>(e);
55 
56  if (ConstantExpr *TrueCE = dyn_cast<ConstantExpr>(se->trueExpr)) {
57  if (ConstantExpr *FalseCE = dyn_cast<ConstantExpr>(se->falseExpr)) {
58  if (TrueCE != FalseCE) {
59  if (value == TrueCE) {
61  results);
62  } else {
63  assert(value == FalseCE &&
64  "err in implied value calculation");
66  results);
67  }
68  }
69  }
70  }
71  break;
72  }
73 
74  case Expr::Concat: {
75  ConcatExpr *ce = cast<ConcatExpr>(e);
76  getImpliedValues(ce->getKid(0), value->Extract(ce->getKid(1)->getWidth(),
77  ce->getKid(0)->getWidth()),
78  results);
79  getImpliedValues(ce->getKid(1), value->Extract(0,
80  ce->getKid(1)->getWidth()),
81  results);
82  break;
83  }
84 
85  case Expr::Extract: {
86  // XXX, could do more here with "some bits" mask
87  break;
88  }
89 
90  // Casting
91 
92  case Expr::ZExt:
93  case Expr::SExt: {
94  CastExpr *ce = cast<CastExpr>(e);
95  getImpliedValues(ce->src, value->Extract(0, ce->src->getWidth()),
96  results);
97  break;
98  }
99 
100  // Arithmetic
101 
102  case Expr::Add: { // constants on left
103  BinaryExpr *be = cast<BinaryExpr>(e);
104  // C_0 + A = C => A = C - C_0
105  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left))
106  getImpliedValues(be->right, value->Sub(CE), results);
107  break;
108  }
109  case Expr::Sub: { // constants on left
110  BinaryExpr *be = cast<BinaryExpr>(e);
111  // C_0 - A = C => A = C_0 - C
112  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left))
113  getImpliedValues(be->right, CE->Sub(value), results);
114  break;
115  }
116  case Expr::Mul: {
117  // FIXME: Can do stuff here, but need valid mask and other things because of
118  // bits that might be lost.
119  break;
120  }
121 
122  case Expr::UDiv:
123  case Expr::SDiv:
124  case Expr::URem:
125  case Expr::SRem:
126  break;
127 
128  // Binary
129 
130  case Expr::And: {
131  BinaryExpr *be = cast<BinaryExpr>(e);
132  if (be->getWidth() == Expr::Bool) {
133  if (value->isTrue()) {
134  getImpliedValues(be->left, value, results);
135  getImpliedValues(be->right, value, results);
136  }
137  } else {
138  // FIXME; We can propogate a mask here where we know "some bits". May or
139  // may not be useful.
140  }
141  break;
142  }
143  case Expr::Or: {
144  BinaryExpr *be = cast<BinaryExpr>(e);
145  if (value->isZero()) {
146  getImpliedValues(be->left, 0, results);
147  getImpliedValues(be->right, 0, results);
148  } else {
149  // FIXME: Can do more?
150  }
151  break;
152  }
153  case Expr::Xor: {
154  BinaryExpr *be = cast<BinaryExpr>(e);
155  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left))
156  getImpliedValues(be->right, value->Xor(CE), results);
157  break;
158  }
159 
160  // Comparison
161  case Expr::Ne:
162  value = value->Not();
163  /* fallthru */
164  case Expr::Eq: {
165  EqExpr *ee = cast<EqExpr>(e);
166  if (value->isTrue()) {
167  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left))
168  getImpliedValues(ee->right, CE, results);
169  } else {
170  // Look for limited value range.
171  //
172  // In general anytime one side was restricted to two values we can apply
173  // this trick. The only obvious case where this occurs, aside from
174  // booleans, is as the result of a select expression where the true and
175  // false branches are single valued and distinct.
176 
177  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left))
178  if (CE->getWidth() == Expr::Bool)
179  getImpliedValues(ee->right, CE->Not(), results);
180  }
181  break;
182  }
183 
184  default:
185  break;
186  }
187 }
188 
190  ref<ConstantExpr> value) {
191  std::vector<ref<ReadExpr> > reads;
192  std::map<ref<ReadExpr>, ref<ConstantExpr> > found;
193  ImpliedValueList results;
194 
195  getImpliedValues(e, value, results);
196 
197  for (ImpliedValueList::iterator i = results.begin(), ie = results.end();
198  i != ie; ++i) {
199  std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it =
200  found.find(i->first);
201  if (it != found.end()) {
202  assert(it->second == i->second && "Invalid ImpliedValue!");
203  } else {
204  found.insert(std::make_pair(i->first, i->second));
205  }
206  }
207 
208  findReads(e, false, reads);
209  std::set< ref<ReadExpr> > readsSet(reads.begin(), reads.end());
210  reads = std::vector< ref<ReadExpr> >(readsSet.begin(), readsSet.end());
211 
212  std::vector<ref<Expr> > assumption;
213  assumption.push_back(EqExpr::create(e, value));
214 
215  // obscure... we need to make sure that all the read indices are
216  // bounds checked. if we don't do this we can end up constructing
217  // invalid counterexamples because STP will happily make out of
218  // bounds indices which will not get picked up. this is of utmost
219  // importance if we are being backed by the CexCachingSolver.
220 
221  for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(),
222  ie = reads.end(); i != ie; ++i) {
223  ReadExpr *re = i->get();
224  assumption.push_back(UltExpr::create(re->index,
227  }
228 
229  ConstraintManager assume(assumption);
230  for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(),
231  ie = reads.end(); i != ie; ++i) {
232  ref<ReadExpr> var = *i;
233  ref<ConstantExpr> possible;
234  bool success = S->getValue(Query(assume, var), possible);
235  assert(success && "FIXME: Unhandled solver failure");
236  std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = found.find(var);
237  bool res;
238  success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res);
239  assert(success && "FIXME: Unhandled solver failure");
240  if (res) {
241  if (it != found.end()) {
242  assert(possible == it->second && "Invalid ImpliedValue!");
243  found.erase(it);
244  }
245  } else {
246  if (it!=found.end()) {
247  ref<Expr> binding = it->second;
248  llvm::errs() << "checkForImpliedValues: " << e << " = " << value << "\n"
249  << "\t\t implies " << var << " == " << binding
250  << " (error)\n";
251  assert(0);
252  }
253  }
254  }
255 
256  assert(found.empty());
257 }
void checkForImpliedValues(Solver *S, ref< Expr > e, ref< ConstantExpr > cvalue)
ref< ConstantExpr > Extract(unsigned offset, Width W)
Definition: Expr.cpp:364
bool getValue(const Query &, ref< ConstantExpr > &result)
Definition: Solver.cpp:176
ref< Expr > left
Definition: Expr.h:494
ref< ConstantExpr > Sub(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:384
Not used in canonical form.
Definition: Expr.h:151
unsigned size
Definition: Expr.h:605
ref< Expr > trueExpr
Definition: Expr.h:732
ref< ConstantExpr > Not()
Definition: Expr.cpp:432
ref< ConstantExpr > Xor(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:416
bool isZero() const
isZero - Is this a constant zero.
Definition: Expr.h:426
std::vector< std::pair< ref< ReadExpr >, ref< ConstantExpr > > > ImpliedValueList
Definition: ImpliedValue.h:27
UpdateList updates
Definition: Expr.h:687
Expr::Width getPointerWidth() const
Definition: Context.h:40
Class representing an if-then-else expression.
Definition: Expr.h:726
bool mustBeTrue(const Query &, bool &result)
Definition: Solver.cpp:144
ref< Expr > src
Definition: Expr.h:945
virtual Width getWidth() const =0
static const Context & get()
get - Return the global singleton instance of the Context.
Definition: Context.cpp:35
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:432
void findReads(ref< Expr > e, bool visitUpdates, std::vector< ref< ReadExpr > > &result)
Definition: ExprUtil.cpp:21
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
ref< Expr > right
Definition: Expr.h:494
void getImpliedValues(ref< Expr > e, ref< ConstantExpr > cvalue, ImpliedValueList &result)
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
ref< Expr > index
Definition: Expr.h:688
ref< Expr > cond
Definition: Expr.h:732
static const Width Bool
Definition: Expr.h:97
ref< Expr > falseExpr
Definition: Expr.h:732
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:807