klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExecutionState.cpp
Go to the documentation of this file.
1 //===-- ExecutionState.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 "klee/ExecutionState.h"
11 
16 
17 #include "klee/Expr.h"
18 
19 #include "Memory.h"
20 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
21 #include "llvm/IR/Function.h"
22 #else
23 #include "llvm/Function.h"
24 #endif
25 #include "llvm/Support/CommandLine.h"
26 #include "llvm/Support/raw_ostream.h"
27 
28 #include <iomanip>
29 #include <sstream>
30 #include <cassert>
31 #include <map>
32 #include <set>
33 #include <stdarg.h>
34 
35 using namespace llvm;
36 using namespace klee;
37 
38 namespace {
39  cl::opt<bool>
40  DebugLogStateMerge("debug-log-state-merge");
41 }
42 
43 /***/
44 
45 StackFrame::StackFrame(KInstIterator _caller, KFunction *_kf)
46  : caller(_caller), kf(_kf), callPathNode(0),
47  minDistToUncoveredOnReturn(0), varargs(0) {
48  locals = new Cell[kf->numRegisters];
49 }
50 
52  : caller(s.caller),
53  kf(s.kf),
54  callPathNode(s.callPathNode),
55  allocas(s.allocas),
56  minDistToUncoveredOnReturn(s.minDistToUncoveredOnReturn),
57  varargs(s.varargs) {
58  locals = new Cell[s.kf->numRegisters];
59  for (unsigned i=0; i<s.kf->numRegisters; i++)
60  locals[i] = s.locals[i];
61 }
62 
64  delete[] locals;
65 }
66 
67 /***/
68 
70  : fakeState(false),
71  underConstrained(false),
72  depth(0),
73  pc(kf->instructions),
74  prevPC(pc),
75  queryCost(0.),
76  weight(1),
77  instsSinceCovNew(0),
78  coveredNew(false),
79  forkDisabled(false),
80  ptreeNode(0) {
81  pushFrame(0, kf);
82 }
83 
84 ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
85  : fakeState(true),
86  underConstrained(false),
87  constraints(assumptions),
88  queryCost(0.),
89  ptreeNode(0) {
90 }
91 
93  for (unsigned int i=0; i<symbolics.size(); i++)
94  {
95  const MemoryObject *mo = symbolics[i].first;
96  assert(mo->refCount > 0);
97  mo->refCount--;
98  if (mo->refCount == 0)
99  delete mo;
100  }
101 
102  while (!stack.empty()) popFrame();
103 }
104 
106  : fnAliases(state.fnAliases),
107  fakeState(state.fakeState),
108  underConstrained(state.underConstrained),
109  depth(state.depth),
110  pc(state.pc),
111  prevPC(state.prevPC),
112  stack(state.stack),
113  constraints(state.constraints),
114  queryCost(state.queryCost),
115  weight(state.weight),
116  addressSpace(state.addressSpace),
117  pathOS(state.pathOS),
118  symPathOS(state.symPathOS),
119  instsSinceCovNew(state.instsSinceCovNew),
120  coveredNew(state.coveredNew),
121  forkDisabled(state.forkDisabled),
122  coveredLines(state.coveredLines),
123  ptreeNode(state.ptreeNode),
124  symbolics(state.symbolics),
125  arrayNames(state.arrayNames),
126  shadowObjects(state.shadowObjects),
127  incomingBBIndex(state.incomingBBIndex)
128 {
129  for (unsigned int i=0; i<symbolics.size(); i++)
130  symbolics[i].first->refCount++;
131 }
132 
134  depth++;
135 
136  ExecutionState *falseState = new ExecutionState(*this);
137  falseState->coveredNew = false;
138  falseState->coveredLines.clear();
139 
140  weight *= .5;
141  falseState->weight -= weight;
142 
143  return falseState;
144 }
145 
147  stack.push_back(StackFrame(caller,kf));
148 }
149 
151  StackFrame &sf = stack.back();
152  for (std::vector<const MemoryObject*>::iterator it = sf.allocas.begin(),
153  ie = sf.allocas.end(); it != ie; ++it)
155  stack.pop_back();
156 }
157 
158 void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) {
159  mo->refCount++;
160  symbolics.push_back(std::make_pair(mo, array));
161 }
163 
164 std::string ExecutionState::getFnAlias(std::string fn) {
165  std::map < std::string, std::string >::iterator it = fnAliases.find(fn);
166  if (it != fnAliases.end())
167  return it->second;
168  else return "";
169 }
170 
171 void ExecutionState::addFnAlias(std::string old_fn, std::string new_fn) {
172  fnAliases[old_fn] = new_fn;
173 }
174 
175 void ExecutionState::removeFnAlias(std::string fn) {
176  fnAliases.erase(fn);
177 }
178 
179 
180 
181 llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm) {
182  os << "{";
183  MemoryMap::iterator it = mm.begin();
184  MemoryMap::iterator ie = mm.end();
185  if (it!=ie) {
186  os << "MO" << it->first->id << ":" << it->second;
187  for (++it; it!=ie; ++it)
188  os << ", MO" << it->first->id << ":" << it->second;
189  }
190  os << "}";
191  return os;
192 }
193 
195  if (DebugLogStateMerge)
196  llvm::errs() << "-- attempting merge of A:" << this << " with B:" << &b
197  << "--\n";
198  if (pc != b.pc)
199  return false;
200 
201  // XXX is it even possible for these to differ? does it matter? probably
202  // implies difference in object states?
203  if (symbolics!=b.symbolics)
204  return false;
205 
206  {
207  std::vector<StackFrame>::const_iterator itA = stack.begin();
208  std::vector<StackFrame>::const_iterator itB = b.stack.begin();
209  while (itA!=stack.end() && itB!=b.stack.end()) {
210  // XXX vaargs?
211  if (itA->caller!=itB->caller || itA->kf!=itB->kf)
212  return false;
213  ++itA;
214  ++itB;
215  }
216  if (itA!=stack.end() || itB!=b.stack.end())
217  return false;
218  }
219 
220  std::set< ref<Expr> > aConstraints(constraints.begin(), constraints.end());
221  std::set< ref<Expr> > bConstraints(b.constraints.begin(),
222  b.constraints.end());
223  std::set< ref<Expr> > commonConstraints, aSuffix, bSuffix;
224  std::set_intersection(aConstraints.begin(), aConstraints.end(),
225  bConstraints.begin(), bConstraints.end(),
226  std::inserter(commonConstraints, commonConstraints.begin()));
227  std::set_difference(aConstraints.begin(), aConstraints.end(),
228  commonConstraints.begin(), commonConstraints.end(),
229  std::inserter(aSuffix, aSuffix.end()));
230  std::set_difference(bConstraints.begin(), bConstraints.end(),
231  commonConstraints.begin(), commonConstraints.end(),
232  std::inserter(bSuffix, bSuffix.end()));
233  if (DebugLogStateMerge) {
234  llvm::errs() << "\tconstraint prefix: [";
235  for (std::set<ref<Expr> >::iterator it = commonConstraints.begin(),
236  ie = commonConstraints.end();
237  it != ie; ++it)
238  llvm::errs() << *it << ", ";
239  llvm::errs() << "]\n";
240  llvm::errs() << "\tA suffix: [";
241  for (std::set<ref<Expr> >::iterator it = aSuffix.begin(),
242  ie = aSuffix.end();
243  it != ie; ++it)
244  llvm::errs() << *it << ", ";
245  llvm::errs() << "]\n";
246  llvm::errs() << "\tB suffix: [";
247  for (std::set<ref<Expr> >::iterator it = bSuffix.begin(),
248  ie = bSuffix.end();
249  it != ie; ++it)
250  llvm::errs() << *it << ", ";
251  llvm::errs() << "]\n";
252  }
253 
254  // We cannot merge if addresses would resolve differently in the
255  // states. This means:
256  //
257  // 1. Any objects created since the branch in either object must
258  // have been free'd.
259  //
260  // 2. We cannot have free'd any pre-existing object in one state
261  // and not the other
262 
263  if (DebugLogStateMerge) {
264  llvm::errs() << "\tchecking object states\n";
265  llvm::errs() << "A: " << addressSpace.objects << "\n";
266  llvm::errs() << "B: " << b.addressSpace.objects << "\n";
267  }
268 
269  std::set<const MemoryObject*> mutated;
274  for (; ai!=ae && bi!=be; ++ai, ++bi) {
275  if (ai->first != bi->first) {
276  if (DebugLogStateMerge) {
277  if (ai->first < bi->first) {
278  llvm::errs() << "\t\tB misses binding for: " << ai->first->id << "\n";
279  } else {
280  llvm::errs() << "\t\tA misses binding for: " << bi->first->id << "\n";
281  }
282  }
283  return false;
284  }
285  if (ai->second != bi->second) {
286  if (DebugLogStateMerge)
287  llvm::errs() << "\t\tmutated: " << ai->first->id << "\n";
288  mutated.insert(ai->first);
289  }
290  }
291  if (ai!=ae || bi!=be) {
292  if (DebugLogStateMerge)
293  llvm::errs() << "\t\tmappings differ\n";
294  return false;
295  }
296 
297  // merge stack
298 
301  for (std::set< ref<Expr> >::iterator it = aSuffix.begin(),
302  ie = aSuffix.end(); it != ie; ++it)
303  inA = AndExpr::create(inA, *it);
304  for (std::set< ref<Expr> >::iterator it = bSuffix.begin(),
305  ie = bSuffix.end(); it != ie; ++it)
306  inB = AndExpr::create(inB, *it);
307 
308  // XXX should we have a preference as to which predicate to use?
309  // it seems like it can make a difference, even though logically
310  // they must contradict each other and so inA => !inB
311 
312  std::vector<StackFrame>::iterator itA = stack.begin();
313  std::vector<StackFrame>::const_iterator itB = b.stack.begin();
314  for (; itA!=stack.end(); ++itA, ++itB) {
315  StackFrame &af = *itA;
316  const StackFrame &bf = *itB;
317  for (unsigned i=0; i<af.kf->numRegisters; i++) {
318  ref<Expr> &av = af.locals[i].value;
319  const ref<Expr> &bv = bf.locals[i].value;
320  if (av.isNull() || bv.isNull()) {
321  // if one is null then by implication (we are at same pc)
322  // we cannot reuse this local, so just ignore
323  } else {
324  av = SelectExpr::create(inA, av, bv);
325  }
326  }
327  }
328 
329  for (std::set<const MemoryObject*>::iterator it = mutated.begin(),
330  ie = mutated.end(); it != ie; ++it) {
331  const MemoryObject *mo = *it;
332  const ObjectState *os = addressSpace.findObject(mo);
333  const ObjectState *otherOS = b.addressSpace.findObject(mo);
334  assert(os && !os->readOnly &&
335  "objects mutated but not writable in merging state");
336  assert(otherOS);
337 
338  ObjectState *wos = addressSpace.getWriteable(mo, os);
339  for (unsigned i=0; i<mo->size; i++) {
340  ref<Expr> av = wos->read8(i);
341  ref<Expr> bv = otherOS->read8(i);
342  wos->write(i, SelectExpr::create(inA, av, bv));
343  }
344  }
345 
347  for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(),
348  ie = commonConstraints.end(); it != ie; ++it)
350  constraints.addConstraint(OrExpr::create(inA, inB));
351 
352  return true;
353 }
354 
355 void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
356  unsigned idx = 0;
357  const KInstruction *target = prevPC;
358  for (ExecutionState::stack_ty::const_reverse_iterator
359  it = stack.rbegin(), ie = stack.rend();
360  it != ie; ++it) {
361  const StackFrame &sf = *it;
362  Function *f = sf.kf->function;
363  const InstructionInfo &ii = *target->info;
364  out << "\t#" << idx++;
365  std::stringstream AssStream;
366  AssStream << std::setw(8) << std::setfill('0') << ii.assemblyLine;
367  out << AssStream.str();
368  out << " in " << f->getName().str() << " (";
369  // Yawn, we could go up and print varargs if we wanted to.
370  unsigned index = 0;
371  for (Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
372  ai != ae; ++ai) {
373  if (ai!=f->arg_begin()) out << ", ";
374 
375  out << ai->getName().str();
376  // XXX should go through function
377  ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value;
378  if (isa<ConstantExpr>(value))
379  out << "=" << value;
380  }
381  out << ")";
382  if (ii.file != "")
383  out << " at " << ii.file << ":" << ii.line;
384  out << "\n";
385  target = sf.caller;
386  }
387 }
bool merge(const ExecutionState &b)
void dumpStack(llvm::raw_ostream &out) const
constraint_iterator end() const
Definition: Constraints.h:57
StackFrame(KInstIterator caller, KFunction *kf)
ExecutionState * branch()
const InstructionInfo * info
Definition: KInstruction.h:31
unsigned getArgRegister(unsigned index)
Definition: KModule.h:65
void addConstraint(ref< Expr > e)
llvm::raw_ostream & operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
ref< Expr > value
Definition: Cell.h:19
static ref< Expr > create(ref< Expr > c, ref< Expr > t, ref< Expr > f)
Definition: Expr.cpp:527
std::vector< std::pair< const MemoryObject *, const Array * > > symbolics
ordered list of symbolics: used to generate test cases.
std::map< const std::string *, std::set< unsigned > > coveredLines
unsigned size
size in bytes
Definition: Memory.h:45
std::vector< const MemoryObject * > allocas
ObjectState * getWriteable(const MemoryObject *mo, const ObjectState *os)
Obtain an ObjectState suitable for writing.
void write(unsigned offset, ref< Expr > value)
Definition: Memory.cpp:529
void addFnAlias(std::string old_fn, std::string new_fn)
AddressSpace addressSpace
bool isNull() const
Definition: Ref.h:99
std::string getFnAlias(std::string fn)
constraint_iterator begin() const
Definition: Constraints.h:54
KFunction * kf
llvm::Function * function
Definition: KModule.h:44
void pushFrame(KInstIterator caller, KFunction *kf)
std::map< std::string, std::string > fnAliases
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
void removeFnAlias(std::string fn)
ConstraintManager constraints
KInstIterator prevPC
const std::string & file
KInstIterator caller
unsigned refCount
Definition: Memory.h:38
static const Width Bool
Definition: Expr.h:97
unsigned numRegisters
Definition: KModule.h:46
const ObjectState * findObject(const MemoryObject *mo) const
Lookup a binding from a MemoryObject.
iterator end() const
Definition: ImmutableMap.h:86
void unbindObject(const MemoryObject *mo)
Remove a binding from the address space.
void addSymbolic(const MemoryObject *mo, const Array *array)
Statistic instructions
iterator begin() const
Definition: ImmutableMap.h:83
ref< Expr > read8(unsigned offset) const
Definition: Memory.cpp:387