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