 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
5.2% |
3 / 58 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
10.3% |
6 / 58 |
| |
|
Line Coverage: |
13.3% |
6 / 45 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Executor.h"
4 :
5 : #include "MemoryManager.h"
6 : #include "TimingSolver.h"
7 :
8 : #include "klee/ExecutionState.h"
9 : #include "klee/Memory.h"
10 : #include "klee/Solver.h"
11 : #include "klee/Internal/Module/KInstruction.h"
12 : #include "klee/Internal/Module/KModule.h"
13 :
14 : #include "llvm/Function.h"
15 :
16 : #include <cassert>
17 : #include <iostream>
18 :
19 : using namespace llvm;
20 : using namespace klee;
21 :
22 : klee::MemoryObject *klee::selectReferent(klee::MemoryObject *r1,
23 1148908: klee::MemoryObject *r2) {
24 : #ifdef KLEE_TRACK_REFERENTS
25 : #else
0: branch 0 not taken
1148908: branch 1 taken
26 1148908: assert(!r1 && !r2 && "nonono: should not have referents if not tracking them.");
27 1148908: return 0;
28 : #endif
29 :
30 : if(!r1)
31 : return r2;
32 : if(!r2)
33 : return r1;
34 : if(r1 != r2) {
35 : llvm::cerr << "XXX: Don't understand this tree! L=" << r1
36 : << " R=" << r2 <<"\n";
37 : assert(0);
38 : }
39 : return r1;
40 : }
41 :
42 :
43 : MemoryObject *Executor::recoverReferent(ExecutionState &state,
44 : ref<Expr> base,
45 3427568: Value *ptr) {
46 : #ifdef KLEE_TRACK_REFERENTS
47 : #else
48 3427568: return 0;
49 : #endif
50 :
51 : if(state.underConstrained) {
52 : printFileLine(state, state.prevPC);
53 : llvm::cerr << "About to make up object : pointer=" << ptr
54 : << " base=" << base << " inst:" << *state.prevPC->inst << "\n";
55 : return lazyAllocate(state, base, ptr);
56 : }
57 :
58 : ResolutionList rl;
59 : ObjectPair op;
60 : bool success;
61 : assert(state.addressSpace.resolveOne(state, solver, base, op, success) &&
62 : "resolveOne error");
63 : assert(success && "out of bounds / multiple resolution unhandled");
64 : MemoryObject * referent = (MemoryObject*) op.first;
65 : bool res;
66 : assert(solver->mustBeTrue(state, referent->getBoundsCheckPointer(base),
67 : res) &&
68 : res &&
69 : "out of bounds unhandled");
70 : if(referent->fake_object) {
71 : llvm::cerr << "Recovered fake referent: " << referent
72 : << " for addr=" << base << "\n";
73 : return referent;
74 : }
75 :
76 : // Push this into executeMemoryOp?
77 : printFileLine(state, state.prevPC);
78 : llvm::cerr << "XXX: no referent for base=" << base
79 : << "inst=" << *state.prevPC->inst << "\n";
80 : assert(0 && "Check this out");
81 : return 0;
82 : }
83 :
84 :
85 : MemoryObject * Executor::lazyAllocate(ExecutionState &state, ref<Expr> base,
86 0: Value *ptr) {
0: branch 0 not taken
0: branch 1 not taken
87 0: assert(state.underConstrained > 64);
88 : // XXX:DRE: Need to make sure:
89 : // if(!p)
90 : // *p
91 : // gives an error.
92 :
93 : // How do we find the base object that the thing is in and store
94 : // into it? We can't right? We don't have it?
95 :
96 : // It might not seem like it, but I'm pretty sure this is the right
97 : // thing to check.
98 0: MemoryObject *mo = 0;
99 : ref<Expr> eq = EqExpr::create(base,
100 0: ConstantExpr::create(0x12345678, kMachinePointerType));
101 : bool res;
102 0: bool success = solver->mustBeTrue(state, Expr::createNot(eq), res);
0: branch 0 not taken
0: branch 1 not taken
103 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
104 0: if (res) {
105 : ObjectPair op;
106 : bool success;
107 : assert(state.addressSpace.resolveOne(state, solver, base, op, success) &&
0: branch 1 not taken
0: branch 2 not taken
0: branch 4 not taken
0: branch 5 not taken
108 0: "timeout");
0: branch 0 not taken
0: branch 1 not taken
109 0: assert(success && "out of bounds / multiple resolution unhandled");
110 0: mo = (MemoryObject*) op.first;
111 : assert(solver->mustBeTrue(state, mo->getBoundsCheckPointer(base), res) &&
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 10 not taken
0: branch 11 not taken
112 0: res && "out of bounds unhandled");
113 : // XXX: DWD: I'd like to make this happen less often.
114 0: llvm::cerr << "Expr: " << base << " already bound to: " << mo << "\n";
115 : } else {
116 0: mo = memory->allocate((uint64_t)state.underConstrained, false, false, 0);
0: branch 0 not taken
0: branch 1 not taken
117 0: assert(mo && "out of memory");
118 0: mo->fake_object = true;
119 0: ObjectState *os = bindObjectInState(state, mo, false);
120 0: os->makeSymbolic();
121 0: state.addSymbolic(mo);
122 :
123 0: ref<Expr> eq = EqExpr::create(base, mo->getBaseExpr());
124 : assert(solver->mustBeTrue(state, Expr::createNot(eq), res) &&
125 : !res &&
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 10 not taken
0: branch 11 not taken
126 0: "Fix the check: just need to see if there is a unique value?");
127 :
128 0: llvm::cerr << "Binding to: " << mo << " via: " << eq << "\n";
129 0: addConstraint(state, eq);
130 : llvm::cerr << "Made object up for: pointer=" << ptr
131 0: << " base=" << base << "\n";
132 :
133 : ObjectPair op;
134 : bool success;
135 : assert(state.addressSpace.resolveOne(state, solver, base, op, success) &&
0: branch 1 not taken
0: branch 2 not taken
0: branch 4 not taken
0: branch 5 not taken
136 0: "timeout");
0: branch 0 not taken
0: branch 1 not taken
137 0: assert(success && "out of bounds / multiple resolution unhandled");
138 0: MemoryObject *ptr_mo = (MemoryObject*) op.first;
139 : bool res;
140 : assert(solver->mustBeTrue(state, ptr_mo->getBoundsCheckPointer(base),
141 : res) &&
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 10 not taken
0: branch 11 not taken
142 0: res && "out of bounds unhandled");
0: branch 0 not taken
0: branch 1 not taken
143 0: assert(ptr_mo == mo && "what is up?");
144 0: state.cloneObject(os, mo);
145 :
146 : // XXX have to enable multibyte reads at all times. Or recreate.
0: branch 0 not taken
0: branch 1 not taken
147 0: if (base.getKind() == Expr::Read) {
148 0: llvm::cerr << "base is a readexpr: " << base << "\n";
149 : } else {
150 : llvm::cerr << "base is NOT readexpr: " << base << " kind = " <<
151 0: base.getKind() << "\n";
152 :
153 0: assert(0);
154 0: }
155 : }
156 : // Not strictly necessary? This isn't valid anyway?
157 :
158 : // XXX I took this out, it doesn't make sense and is completely
159 : // illegal (you are overwriting a register with different
160 : // contents). - DWD
161 :
162 : // bindLocal(target, state, mo->getBaseExpr(), mo);
163 :
164 0: return mo;
165 : }
166 :
167 : // XXX: Not quite sure the right thing to do here. If we check for an
168 : // MO than if its a pointer that happens to have a legitimate value then
169 : // we get a false hit. If we use referents then we have to hack things
170 : // since otherwise I'm not real clear on how to get the referent: if it's
171 : // a fake object we seem to have a tendency to lose them, in which was
172 : // we have to re-resolve things. Which isn't such a great thing since it
173 : // runs into the problem above.
174 : void Executor::handlePointsToObj(ExecutionState &state,
175 : KInstruction *target,
176 : const std::vector< ref<Expr> > &arguments,
177 0: const std::vector<MemoryObject *> &argReferents) {
178 :
179 : // XXX should type check args
180 : assert(arguments.size()==1 &&
0: branch 0 not taken
0: branch 1 not taken
181 0: "invalid number of arguments to handlePointsToObj");
0: branch 0 not taken
0: branch 1 not taken
182 0: assert(!state.underConstrained && "Invalid call");
183 : #ifndef KLEE_TRACK_REFERENTS
184 0: assert(0 && "Not tracking refs");
185 : #endif
186 :
187 : const MemoryObject *mo = argReferents[0];
188 : if(!mo) {
189 : ObjectPair op;
190 : bool success;
191 : assert(state.addressSpace.resolveOne(state, solver, arguments[0],
192 : op, success) &&
193 : "timeout");
194 : if (success) {
195 : mo = op.first;
196 : assert(mo->fake_object && "lost referent for non-fake obj");
197 : }
198 : }
199 : int live = (mo != 0);
200 : bindLocal(target, state, ConstantExpr::create(live, Expr::Int32));
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
201 206: }
202 :
203 : #ifdef KLEE_TRACK_REFERENTS
204 : void Executor::writeReferent(ExecutionState &state, ObjectState *os,
205 : ref<Expr> offset, MemoryObject *mo) {
206 : if(!os->referents) {
207 : ref<Expr> size =
208 : ConstantExpr::create((unsigned long)os->size, Expr::Int32);
209 : MemoryObject *mo2 = memory->allocate(state, size, false, false, 0);
210 : assert(mo2 && "out of memory");
211 : os->referents = bindObjectInState(state, mo2, false);
212 : os->referents->initializeToZero();
213 : }
214 : ref<Expr> v = Expr::createPointer((uint64_t)(unsigned)mo);
215 : os->referents->write(offset, v);
216 : }
217 : #endif
218 :
Generated: 2009-05-17 22:47 by zcov