klee
AddressSpace.cpp
Go to the documentation of this file.
1//===-- AddressSpace.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 "AddressSpace.h"
11
12#include "ExecutionState.h"
13#include "Memory.h"
14#include "TimingSolver.h"
15
16#include "klee/Expr/Expr.h"
18
19#include "CoreStats.h"
20
21using namespace klee;
22
24
25void AddressSpace::bindObject(const MemoryObject *mo, ObjectState *os) {
26 assert(os->copyOnWriteOwner==0 && "object already has owner");
28 objects = objects.replace(std::make_pair(mo, os));
29}
30
33}
34
36 const auto res = objects.lookup(mo);
37 return res ? res->second.get() : nullptr;
38}
39
41 const ObjectState *os) {
42 assert(!os->readOnly);
43
44 // If this address space owns they object, return it
45 if (cowKey == os->copyOnWriteOwner)
46 return const_cast<ObjectState*>(os);
47
48 // Add a copy of this object state that can be updated
49 ref<ObjectState> newObjectState(new ObjectState(*os));
50 newObjectState->copyOnWriteOwner = cowKey;
51 objects = objects.replace(std::make_pair(mo, newObjectState));
52 return newObjectState.get();
53}
54
56
58 ObjectPair &result) const {
59 uint64_t address = addr->getZExtValue();
60 MemoryObject hack(address);
61
62 if (const auto res = objects.lookup_previous(&hack)) {
63 const auto &mo = res->first;
64 // Check if the provided address is between start and end of the object
65 // [mo->address, mo->address + mo->size) or the object is a 0-sized object.
66 if ((mo->size==0 && address==mo->address) ||
67 (address - mo->address < mo->size)) {
68 result.first = res->first;
69 result.second = res->second.get();
70 return true;
71 }
72 }
73
74 return false;
75}
76
78 TimingSolver *solver,
79 ref<Expr> address,
80 ObjectPair &result,
81 bool &success) const {
82 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
83 success = resolveOne(CE, result);
84 return true;
85 } else {
87
88 // try cheap search, will succeed for any inbounds pointer
89
91 if (!solver->getValue(state.constraints, address, cex, state.queryMetaData))
92 return false;
93 uint64_t example = cex->getZExtValue();
94 MemoryObject hack(example);
95 const auto res = objects.lookup_previous(&hack);
96
97 if (res) {
98 const MemoryObject *mo = res->first;
99 if (example - mo->address < mo->size) {
100 result.first = res->first;
101 result.second = res->second.get();
102 success = true;
103 return true;
104 }
105 }
106
107 // didn't work, now we have to search
108
112
113 MemoryMap::iterator start = oi;
114 while (oi!=begin) {
115 --oi;
116 const auto &mo = oi->first;
117
118 bool mayBeTrue;
119 if (!solver->mayBeTrue(state.constraints,
120 mo->getBoundsCheckPointer(address), mayBeTrue,
121 state.queryMetaData))
122 return false;
123 if (mayBeTrue) {
124 result.first = oi->first;
125 result.second = oi->second.get();
126 success = true;
127 return true;
128 } else {
129 bool mustBeTrue;
130 if (!solver->mustBeTrue(state.constraints,
131 UgeExpr::create(address, mo->getBaseExpr()),
132 mustBeTrue, state.queryMetaData))
133 return false;
134 if (mustBeTrue)
135 break;
136 }
137 }
138
139 // search forwards
140 for (oi=start; oi!=end; ++oi) {
141 const auto &mo = oi->first;
142
143 bool mustBeTrue;
144 if (!solver->mustBeTrue(state.constraints,
145 UltExpr::create(address, mo->getBaseExpr()),
146 mustBeTrue, state.queryMetaData))
147 return false;
148 if (mustBeTrue) {
149 break;
150 } else {
151 bool mayBeTrue;
152
153 if (!solver->mayBeTrue(state.constraints,
154 mo->getBoundsCheckPointer(address), mayBeTrue,
155 state.queryMetaData))
156 return false;
157 if (mayBeTrue) {
158 result.first = oi->first;
159 result.second = oi->second.get();
160 success = true;
161 return true;
162 }
163 }
164 }
165
166 success = false;
167 return true;
168 }
169}
170
172 TimingSolver *solver, ref<Expr> p,
173 const ObjectPair &op, ResolutionList &rl,
174 unsigned maxResolutions) const {
175 // XXX in the common case we can save one query if we ask
176 // mustBeTrue before mayBeTrue for the first result. easy
177 // to add I just want to have a nice symbolic test case first.
178 const MemoryObject *mo = op.first;
179 ref<Expr> inBounds = mo->getBoundsCheckPointer(p);
180 bool mayBeTrue;
181 if (!solver->mayBeTrue(state.constraints, inBounds, mayBeTrue,
182 state.queryMetaData)) {
183 return 1;
184 }
185
186 if (mayBeTrue) {
187 rl.push_back(op);
188
189 // fast path check
190 auto size = rl.size();
191 if (size == 1) {
192 bool mustBeTrue;
193 if (!solver->mustBeTrue(state.constraints, inBounds, mustBeTrue,
194 state.queryMetaData))
195 return 1;
196 if (mustBeTrue)
197 return 0;
198 }
199 else
200 if (size == maxResolutions)
201 return 1;
202 }
203
204 return 2;
205}
206
209 unsigned maxResolutions, time::Span timeout) const {
210 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) {
211 ObjectPair res;
212 if (resolveOne(CE, res))
213 rl.push_back(res);
214 return false;
215 } else {
217
218 // XXX in general this isn't exactly what we want... for
219 // a multiple resolution case (or for example, a \in {b,c,0})
220 // we want to find the first object, find a cex assuming
221 // not the first, find a cex assuming not the second...
222 // etc.
223
224 // XXX how do we smartly amortize the cost of checking to
225 // see if we need to keep searching up/down, in bad cases?
226 // maybe we don't care?
227
228 // XXX we really just need a smart place to start (although
229 // if its a known solution then the code below is guaranteed
230 // to hit the fast path with exactly 2 queries). we could also
231 // just get this by inspection of the expr.
232
234 if (!solver->getValue(state.constraints, p, cex, state.queryMetaData))
235 return true;
236 uint64_t example = cex->getZExtValue();
237 MemoryObject hack(example);
238
242
243 MemoryMap::iterator start = oi;
244 // search backwards, start with one minus because this
245 // is the object that p *should* be within, which means we
246 // get write off the end with 4 queries
247 while (oi != begin) {
248 --oi;
249 const MemoryObject *mo = oi->first;
250 if (timeout && timeout < timer.delta())
251 return true;
252
253 auto op = std::make_pair<>(mo, oi->second.get());
254
255 int incomplete =
256 checkPointerInObject(state, solver, p, op, rl, maxResolutions);
257 if (incomplete != 2)
258 return incomplete ? true : false;
259
260 bool mustBeTrue;
261 if (!solver->mustBeTrue(state.constraints,
262 UgeExpr::create(p, mo->getBaseExpr()), mustBeTrue,
263 state.queryMetaData))
264 return true;
265 if (mustBeTrue)
266 break;
267 }
268
269 // search forwards
270 for (oi = start; oi != end; ++oi) {
271 const MemoryObject *mo = oi->first;
272 if (timeout && timeout < timer.delta())
273 return true;
274
275 bool mustBeTrue;
276 if (!solver->mustBeTrue(state.constraints,
277 UltExpr::create(p, mo->getBaseExpr()), mustBeTrue,
278 state.queryMetaData))
279 return true;
280 if (mustBeTrue)
281 break;
282 auto op = std::make_pair<>(mo, oi->second.get());
283
284 int incomplete =
285 checkPointerInObject(state, solver, p, op, rl, maxResolutions);
286 if (incomplete != 2)
287 return incomplete ? true : false;
288 }
289 }
290
291 return false;
292}
293
294// These two are pretty big hack so we can sort of pass memory back
295// and forth to externals. They work by abusing the concrete cache
296// store inside of the object states, which allows them to
297// transparently avoid screwing up symbolics (if the byte is symbolic
298// then its concrete cache byte isn't being used) but is just a hack.
299
301 for (MemoryMap::iterator it = objects.begin(), ie = objects.end();
302 it != ie; ++it) {
303 const MemoryObject *mo = it->first;
304
305 if (!mo->isUserSpecified) {
306 const auto &os = it->second;
307 auto address = reinterpret_cast<std::uint8_t*>(mo->address);
308
309 if (!os->readOnly)
310 memcpy(address, os->concreteStore, mo->size);
311 }
312 }
313}
314
316 for (auto &obj : objects) {
317 const MemoryObject *mo = obj.first;
318
319 if (!mo->isUserSpecified) {
320 const auto &os = obj.second;
321
322 if (!copyInConcrete(mo, os.get(), mo->address))
323 return false;
324 }
325 }
326
327 return true;
328}
329
331 uint64_t src_address) {
332 auto address = reinterpret_cast<std::uint8_t*>(src_address);
333 if (memcmp(address, os->concreteStore, mo->size) != 0) {
334 if (os->readOnly) {
335 return false;
336 } else {
337 ObjectState *wos = getWriteable(mo, os);
338 memcpy(wos->concreteStore, address, mo->size);
339 }
340 }
341 return true;
342}
343
344/***/
345
347 return a->address < b->address;
348}
349
void unbindObject(const MemoryObject *mo)
Remove a binding from the address space.
int checkPointerInObject(ExecutionState &state, TimingSolver *solver, ref< Expr > p, const ObjectPair &op, ResolutionList &rl, unsigned maxResolutions) const
bool resolveOne(const ref< ConstantExpr > &address, ObjectPair &result) const
bool copyInConcrete(const MemoryObject *mo, const ObjectState *os, uint64_t src_address)
bool resolve(ExecutionState &state, TimingSolver *solver, ref< Expr > p, ResolutionList &rl, unsigned maxResolutions=0, time::Span timeout=time::Span()) const
unsigned cowKey
Epoch counter used to control ownership of objects.
Definition: AddressSpace.h:41
const ObjectState * findObject(const MemoryObject *mo) const
Lookup a binding from a MemoryObject.
ObjectState * getWriteable(const MemoryObject *mo, const ObjectState *os)
Obtain an ObjectState suitable for writing.
ExecutionState representing a path under exploration.
SolverQueryMetaData queryMetaData
Statistics and information.
ConstraintSet constraints
Constraints collected so far.
iterator begin() const
Definition: ImmutableMap.h:83
const value_type * lookup(const key_type &key) const
Definition: ImmutableMap.h:51
ImmutableMap replace(const value_type &value) const
Definition: ImmutableMap.h:70
ImmutableMap remove(const key_type &key) const
Definition: ImmutableMap.h:73
const value_type * lookup_previous(const key_type &key) const
Definition: ImmutableMap.h:54
iterator upper_bound(const key_type &key) const
Definition: ImmutableMap.h:95
iterator end() const
Definition: ImmutableMap.h:86
unsigned size
size in bytes
Definition: Memory.h:52
bool isUserSpecified
Definition: Memory.h:59
ref< Expr > getBoundsCheckPointer(ref< Expr > pointer) const
Definition: Memory.h:118
uint64_t address
Definition: Memory.h:49
ref< ConstantExpr > getBaseExpr() const
Definition: Memory.h:109
unsigned copyOnWriteOwner
Definition: Memory.h:168
uint8_t * concreteStore
Holds all known concrete bytes.
Definition: Memory.h:176
bool getValue(const ConstraintSet &, ref< Expr > expr, ref< ConstantExpr > &result, SolverQueryMetaData &metaData)
bool mayBeTrue(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
bool mustBeTrue(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
Definition: Ref.h:82
T * get() const
Definition: Ref.h:129
Statistic resolveTime
Definition: main.cpp:291
std::vector< ObjectPair > ResolutionList
Definition: AddressSpace.h:28
std::pair< const MemoryObject *, const ObjectState * > ObjectPair
Definition: AddressSpace.h:25
bool operator()(const MemoryObject *a, const MemoryObject *b) const