 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
2.6% |
2 / 77 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
5.2% |
4 / 77 |
| |
|
Line Coverage: |
1.1% |
1 / 87 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "ImpliedValue.h"
4 :
5 : // FIXME: This should not be here.
6 : #include "klee/ExecutionState.h"
7 : #include "klee/Expr.h"
8 : // FIXME: This should not be here.
9 : #include "klee/Memory.h"
10 : #include "klee/Solver.h"
11 : // FIXME: Use APInt.
12 : #include "klee/Internal/Support/IntEvaluation.h"
13 :
14 : #include "klee/util/ExprUtil.h"
15 :
16 : #include <iostream>
17 : #include <set>
18 :
19 : #include "klee/Internal/FIXME/sugar.h"
20 :
21 : using namespace klee;
22 :
23 : // XXX we really want to do some sort of canonicalization of exprs
24 : // globally so that cases below become simpler
25 : static void _getImpliedValue(ref<Expr> e,
26 : uint64_t value,
27 0: ImpliedValueList &results) {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 9 not taken
0: branch 10 not taken
0: branch 11 not taken
0: branch 12 not taken
28 0: switch (e.getKind()) {
29 :
30 : case Expr::Constant: {
0: branch 1 not taken
0: branch 2 not taken
31 0: assert(value == e.getConstantValue() && "error in implied value calculation");
32 : break;
33 : }
34 :
35 : // Special
36 :
37 : case Expr::NotOptimized: break;
38 :
39 : case Expr::Read: {
40 : // XXX in theory it is possible to descend into a symbolic index
41 : // under certain circumstances (all values known, known value
42 : // unique, or range known, max / min hit). Seems unlikely this
43 : // would work often enough to be worth the effort.
44 0: ReadExpr *re = static_ref_cast<ReadExpr>(e);
45 : results.push_back(std::make_pair(re,
46 0: ConstantExpr::create(value, e.getWidth())));
47 0: break;
48 : }
49 :
50 : case Expr::Select: {
51 : // not much to do, could improve with range analysis
52 0: SelectExpr *se = static_ref_cast<SelectExpr>(e);
53 :
0: branch 1 not taken
0: branch 2 not taken
54 0: if (se->trueExpr.isConstant()) {
0: branch 1 not taken
0: branch 2 not taken
55 0: if (se->falseExpr.isConstant()) {
0: branch 2 not taken
0: branch 3 not taken
56 0: if (se->trueExpr.getConstantValue() != se->falseExpr.getConstantValue()) {
0: branch 1 not taken
0: branch 2 not taken
57 0: if (value == se->trueExpr.getConstantValue()) {
58 0: _getImpliedValue(se->cond, 1, results);
59 : } else {
60 : assert(value == se->falseExpr.getConstantValue() &&
0: branch 1 not taken
0: branch 2 not taken
61 0: "err in implied value calculation");
62 0: _getImpliedValue(se->cond, 0, results);
63 : }
64 : }
65 : }
66 : }
67 : break;
68 : }
69 :
70 : case Expr::Concat: {
71 0: ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
72 0: _getImpliedValue(ce->getKid(0), (value >> ce->getKid(1).getWidth()) & ((1 << ce->getKid(0).getWidth()) - 1), results);
73 0: _getImpliedValue(ce->getKid(1), value & ((1 << ce->getKid(1).getWidth()) - 1), results);
74 0: break;
75 : }
76 :
77 : case Expr::Extract: {
78 : // XXX, could do more here with "some bits" mask
79 : break;
80 : }
81 :
82 : // Casting
83 :
84 : case Expr::ZExt:
85 : case Expr::SExt: {
86 0: CastExpr *ce = static_ref_cast<CastExpr>(e);
87 : _getImpliedValue(ce->src,
88 : bits64::truncateToNBits(value,
89 : ce->src.getWidth()),
90 0: results);
91 0: break;
92 : }
93 :
94 : // Arithmetic
95 :
96 : case Expr::Add: { // constants on left
97 0: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
0: branch 1 not taken
0: branch 2 not taken
98 0: if (be->left.isConstant()) {
99 : uint64_t nvalue = ints::sub(value,
100 : be->left.getConstantValue(),
101 0: be->left.getWidth());
102 0: _getImpliedValue(be->right, nvalue, results);
103 : }
104 : break;
105 : }
106 : case Expr::Sub: { // constants on left
107 0: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
0: branch 1 not taken
0: branch 2 not taken
108 0: if (be->left.isConstant()) {
109 : uint64_t nvalue = ints::sub(be->left.getConstantValue(),
110 : value,
111 0: be->left.getWidth());
112 0: _getImpliedValue(be->right, nvalue, results);
113 : }
114 : break;
115 : }
116 : case Expr::Mul: {
117 : // XXX can do stuff here, but need valid mask and other things
118 : // because of 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 : // no, no, no
127 : break;
128 :
129 : // Binary
130 :
131 : case Expr::And: {
132 0: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
0: branch 1 not taken
0: branch 2 not taken
133 0: if (be->getWidth() == Expr::Bool) {
0: branch 0 not taken
0: branch 1 not taken
134 0: if (value) {
135 0: _getImpliedValue(be->left, value, results);
136 0: _getImpliedValue(be->right, value, results);
137 : }
138 : } else {
139 : // XXX, we can basically propogate a mask here
140 : // where we know "some bits". may or may not be
141 : // useful.
142 : }
143 : break;
144 : }
145 : case Expr::Or: {
146 0: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
0: branch 0 not taken
0: branch 1 not taken
147 0: if (!value) {
148 0: _getImpliedValue(be->left, 0, results);
149 0: _getImpliedValue(be->right, 0, results);
150 : } else {
151 : // XXX, can do more?
152 : }
153 : break;
154 : }
155 : case Expr::Xor: { // constants on left
156 0: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
0: branch 1 not taken
0: branch 2 not taken
157 0: if (be->left.isConstant()) {
158 0: _getImpliedValue(be->right, value ^ be->left.getConstantValue(), results);
159 : }
160 : break;
161 : }
162 :
163 : // Comparison
164 : case Expr::Ne:
165 0: value = !value;
166 : /* fallthru */
167 : case Expr::Eq: {
168 0: EqExpr *ee = static_ref_cast<EqExpr>(e);
0: branch 0 not taken
0: branch 1 not taken
169 0: if (value) {
0: branch 1 not taken
0: branch 2 not taken
170 0: if (ee->left.isConstant())
171 0: _getImpliedValue(ee->right, ee->left.getConstantValue(), results);
172 : } else {
173 : // look for limited value range, woohoo
174 : //
175 : // in general anytime one side was restricted to two values we
176 : // can apply this trick. the only obvious case where this
177 : // occurs, aside from booleans, is as the result of a select
178 : // expression where the true and false branches are single
179 : // valued and distinct.
180 :
0: branch 1 not taken
0: branch 2 not taken
181 0: if (ee->left.isConstant()) {
0: branch 1 not taken
0: branch 2 not taken
182 0: if (ee->left.getWidth() == Expr::Bool) {
183 0: _getImpliedValue(ee->right, !ee->left.getConstantValue(), results);
184 : }
185 : }
186 : }
187 : break;
188 : }
189 :
190 : default:
191 : break;
192 : }
193 0: }
194 :
195 : void ImpliedValue::getImpliedValues(ref<Expr> e,
196 : ref<Expr> value,
197 0: ImpliedValueList &results) {
0: branch 1 not taken
0: branch 2 not taken
198 0: assert(value.isConstant() && "non-constant in place of constant");
199 0: _getImpliedValue(e, value.getConstantValue(), results);
200 0: }
201 :
202 : void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
203 0: ref<Expr> value) {
0: branch 1 not taken
0: branch 2 not taken
204 0: assert(value.isConstant() && "non-constant in place of constant");
205 :
206 : std::vector<ref<ReadExpr> > reads;
207 : std::map<ref<ReadExpr>, ref<Expr> > found;
208 : ImpliedValueList results;
209 :
210 0: getImpliedValues(e, value, results);
211 :
0: branch 0 not taken
0: branch 1 not taken
212 0: foreach(i, results.begin(), results.end()) {
213 0: let(it, found.find(i->first));
0: branch 0 not taken
0: branch 1 not taken
214 0: if (it != found.end()) {
215 : assert(it->second.getConstantValue() == i->second.getConstantValue() &&
0: branch 2 not taken
0: branch 3 not taken
216 0: "I don't think so Scott");
217 : } else {
218 0: found.insert(std::make_pair(i->first, i->second));
219 : }
220 : }
221 :
222 0: findReads(e, false, reads);
223 0: std::set< ref<ReadExpr> > readsSet(reads.begin(), reads.end());
224 0: reads = std::vector< ref<ReadExpr> >(readsSet.begin(), readsSet.end());
225 :
226 : std::vector<ref<Expr> > assumption;
227 0: assumption.push_back(EqExpr::create(e, value));
228 :
229 : // obscure... we need to make sure that all the read indices are
230 : // bounds checked. if we don't do this we can end up constructing
231 : // invalid counterexamples because STP will happily make out of
232 : // bounds indices which will not get picked up. this is of utmost
233 : // importance if we are being backed by the CexCachingSolver.
0: branch 0 not taken
0: branch 1 not taken
234 0: foreach(i, reads.begin(), reads.end()) {
235 0: ReadExpr *re = i->get();
236 0: const MemoryObject *mo = re->updates.root;
237 0: assumption.push_back(mo->getBoundsCheckOffset(re->index));
238 : }
239 :
240 : ConstraintManager assume(assumption);
0: branch 2 not taken
0: branch 3 not taken
241 0: foreach(i, reads.begin(), reads.end()) {
242 : ref<ReadExpr> var = *i;
243 : ref<Expr> possible;
244 0: bool success = S->getValue(Query(assume, var), possible);
0: branch 0 not taken
0: branch 1 not taken
245 0: assert(success && "FIXME: Unhandled solver failure");
246 0: let(it, found.find(var));
247 : bool res;
248 0: success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res);
0: branch 0 not taken
0: branch 1 not taken
249 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
250 0: if (res) {
0: branch 0 not taken
0: branch 1 not taken
251 0: if (it != found.end()) {
0: branch 2 not taken
0: branch 3 not taken
252 0: assert(possible.getConstantValue() == it->second.getConstantValue());
253 0: found.erase(it);
254 : }
255 : } else {
0: branch 0 not taken
0: branch 1 not taken
256 0: if (it!=found.end()) {
257 0: ref<Expr> binding = it->second;
258 0: ExecutionState tmp(assumption);
259 : llvm::cerr << "checkForImpliedValues: " << e << " = " << value << "\n"
260 : << "\t\t implies " << var << " == " << binding
261 0: << " (error)\n";
262 0: assert(0);
263 : }
264 : }
265 : }
266 :
0: branch 0 not taken
0: branch 1 not taken
267 0: assert(found.empty());
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
268 206: }
Generated: 2009-05-17 22:47 by zcov