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