ExecutionState.cpp

Go to the documentation of this file.
00001 //===-- ExecutionState.cpp ------------------------------------------------===//
00002 //
00003 //                     The KLEE Symbolic Virtual Machine
00004 //
00005 // This file is distributed under the University of Illinois Open Source
00006 // License. See LICENSE.TXT for details.
00007 //
00008 //===----------------------------------------------------------------------===//
00009 
00010 #include "klee/ExecutionState.h"
00011 
00012 #include "klee/Internal/Module/Cell.h"
00013 #include "klee/Internal/Module/InstructionInfoTable.h"
00014 #include "klee/Internal/Module/KInstruction.h"
00015 #include "klee/Internal/Module/KModule.h"
00016 
00017 #include "klee/Expr.h"
00018 
00019 #include "Memory.h"
00020 
00021 #include "llvm/Function.h"
00022 #include "llvm/Support/CommandLine.h"
00023 
00024 #include <iostream>
00025 #include <cassert>
00026 #include <map>
00027 #include <set>
00028 #include <stdarg.h>
00029 
00030 using namespace llvm;
00031 using namespace klee;
00032 
00033 namespace { 
00034   cl::opt<bool>
00035   DebugLogStateMerge("debug-log-state-merge");
00036 }
00037 
00038 /***/
00039 
00040 StackFrame::StackFrame(KInstIterator _caller, KFunction *_kf)
00041   : caller(_caller), kf(_kf), callPathNode(0), 
00042     minDistToUncoveredOnReturn(0), varargs(0) {
00043   locals = new Cell[kf->numRegisters];
00044 }
00045 
00046 StackFrame::StackFrame(const StackFrame &s) 
00047   : caller(s.caller),
00048     kf(s.kf),
00049     callPathNode(s.callPathNode),
00050     allocas(s.allocas),
00051     minDistToUncoveredOnReturn(s.minDistToUncoveredOnReturn),
00052     varargs(s.varargs) {
00053   locals = new Cell[s.kf->numRegisters];
00054   for (unsigned i=0; i<s.kf->numRegisters; i++)
00055     locals[i] = s.locals[i];
00056 }
00057 
00058 StackFrame::~StackFrame() { 
00059   delete[] locals; 
00060 }
00061 
00062 /***/
00063 
00064 ExecutionState::ExecutionState(KFunction *kf) 
00065   : fakeState(false),
00066     underConstrained(false),
00067     depth(0),
00068     pc(kf->instructions),
00069     prevPC(pc),
00070     queryCost(0.), 
00071     weight(1),
00072     instsSinceCovNew(0),
00073     coveredNew(false),
00074     forkDisabled(false),
00075     ptreeNode(0) {
00076   pushFrame(0, kf);
00077 }
00078 
00079 ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) 
00080   : fakeState(true),
00081     underConstrained(false),
00082     constraints(assumptions),
00083     queryCost(0.),
00084     ptreeNode(0) {
00085 }
00086 
00087 ExecutionState::~ExecutionState() {
00088   while (!stack.empty()) popFrame();
00089 }
00090 
00091 ExecutionState *ExecutionState::branch() {
00092   depth++;
00093 
00094   ExecutionState *falseState = new ExecutionState(*this);
00095   falseState->coveredNew = false;
00096   falseState->coveredLines.clear();
00097 
00098   weight *= .5;
00099   falseState->weight -= weight;
00100 
00101   return falseState;
00102 }
00103 
00104 void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) {
00105   stack.push_back(StackFrame(caller,kf));
00106 }
00107 
00108 void ExecutionState::popFrame() {
00109   StackFrame &sf = stack.back();
00110   for (std::vector<const MemoryObject*>::iterator it = sf.allocas.begin(), 
00111          ie = sf.allocas.end(); it != ie; ++it)
00112     addressSpace.unbindObject(*it);
00113   stack.pop_back();
00114 }
00115 
00117 
00118 std::string ExecutionState::getFnAlias(std::string fn) {
00119   std::map < std::string, std::string >::iterator it = fnAliases.find(fn);
00120   if (it != fnAliases.end())
00121     return it->second;
00122   else return "";
00123 }
00124 
00125 void ExecutionState::addFnAlias(std::string old_fn, std::string new_fn) {
00126   fnAliases[old_fn] = new_fn;
00127 }
00128 
00129 void ExecutionState::removeFnAlias(std::string fn) {
00130   fnAliases.erase(fn);
00131 }
00132 
00133 
00134 
00135 std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) {
00136   os << "{";
00137   MemoryMap::iterator it = mm.begin();
00138   MemoryMap::iterator ie = mm.end();
00139   if (it!=ie) {
00140     os << "MO" << it->first->id << ":" << it->second;
00141     for (++it; it!=ie; ++it)
00142       os << ", MO" << it->first->id << ":" << it->second;
00143   }
00144   os << "}";
00145   return os;
00146 }
00147 
00148 bool ExecutionState::merge(const ExecutionState &b) {
00149   if (DebugLogStateMerge)
00150     llvm::cerr << "-- attempting merge of A:" 
00151                << this << " with B:" << &b << "--\n";
00152   if (pc != b.pc)
00153     return false;
00154 
00155   // XXX is it even possible for these to differ? does it matter? probably
00156   // implies difference in object states?
00157   if (symbolics!=b.symbolics)
00158     return false;
00159 
00160   {
00161     std::vector<StackFrame>::const_iterator itA = stack.begin();
00162     std::vector<StackFrame>::const_iterator itB = b.stack.begin();
00163     while (itA!=stack.end() && itB!=b.stack.end()) {
00164       // XXX vaargs?
00165       if (itA->caller!=itB->caller || itA->kf!=itB->kf)
00166         return false;
00167       ++itA;
00168       ++itB;
00169     }
00170     if (itA!=stack.end() || itB!=b.stack.end())
00171       return false;
00172   }
00173 
00174   std::set< ref<Expr> > aConstraints(constraints.begin(), constraints.end());
00175   std::set< ref<Expr> > bConstraints(b.constraints.begin(), 
00176                                      b.constraints.end());
00177   std::set< ref<Expr> > commonConstraints, aSuffix, bSuffix;
00178   std::set_intersection(aConstraints.begin(), aConstraints.end(),
00179                         bConstraints.begin(), bConstraints.end(),
00180                         std::inserter(commonConstraints, commonConstraints.begin()));
00181   std::set_difference(aConstraints.begin(), aConstraints.end(),
00182                       commonConstraints.begin(), commonConstraints.end(),
00183                       std::inserter(aSuffix, aSuffix.end()));
00184   std::set_difference(bConstraints.begin(), bConstraints.end(),
00185                       commonConstraints.begin(), commonConstraints.end(),
00186                       std::inserter(bSuffix, bSuffix.end()));
00187   if (DebugLogStateMerge) {
00188     llvm::cerr << "\tconstraint prefix: [";
00189     for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(), 
00190            ie = commonConstraints.end(); it != ie; ++it)
00191       llvm::cerr << *it << ", ";
00192     llvm::cerr << "]\n";
00193     llvm::cerr << "\tA suffix: [";
00194     for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), 
00195            ie = aSuffix.end(); it != ie; ++it)
00196       llvm::cerr << *it << ", ";
00197     llvm::cerr << "]\n";
00198     llvm::cerr << "\tB suffix: [";
00199     for (std::set< ref<Expr> >::iterator it = bSuffix.begin(), 
00200            ie = bSuffix.end(); it != ie; ++it)
00201       llvm::cerr << *it << ", ";
00202     llvm::cerr << "]\n";
00203   }
00204 
00205   // We cannot merge if addresses would resolve differently in the
00206   // states. This means:
00207   // 
00208   // 1. Any objects created since the branch in either object must
00209   // have been free'd.
00210   //
00211   // 2. We cannot have free'd any pre-existing object in one state
00212   // and not the other
00213 
00214   if (DebugLogStateMerge) {
00215     llvm::cerr << "\tchecking object states\n";
00216     llvm::cerr << "A: " << addressSpace.objects << "\n";
00217     llvm::cerr << "B: " << b.addressSpace.objects << "\n";
00218   }
00219     
00220   std::set<const MemoryObject*> mutated;
00221   MemoryMap::iterator ai = addressSpace.objects.begin();
00222   MemoryMap::iterator bi = b.addressSpace.objects.begin();
00223   MemoryMap::iterator ae = addressSpace.objects.end();
00224   MemoryMap::iterator be = b.addressSpace.objects.end();
00225   for (; ai!=ae && bi!=be; ++ai, ++bi) {
00226     if (ai->first != bi->first) {
00227       if (DebugLogStateMerge) {
00228         if (ai->first < bi->first) {
00229           llvm::cerr << "\t\tB misses binding for: " << ai->first->id << "\n";
00230         } else {
00231           llvm::cerr << "\t\tA misses binding for: " << bi->first->id << "\n";
00232         }
00233       }
00234       return false;
00235     }
00236     if (ai->second != bi->second) {
00237       if (DebugLogStateMerge)
00238         llvm::cerr << "\t\tmutated: " << ai->first->id << "\n";
00239       mutated.insert(ai->first);
00240     }
00241   }
00242   if (ai!=ae || bi!=be) {
00243     if (DebugLogStateMerge)
00244       llvm::cerr << "\t\tmappings differ\n";
00245     return false;
00246   }
00247   
00248   // merge stack
00249 
00250   ref<Expr> inA = ConstantExpr::alloc(1, Expr::Bool);
00251   ref<Expr> inB = ConstantExpr::alloc(1, Expr::Bool);
00252   for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), 
00253          ie = aSuffix.end(); it != ie; ++it)
00254     inA = AndExpr::create(inA, *it);
00255   for (std::set< ref<Expr> >::iterator it = bSuffix.begin(), 
00256          ie = bSuffix.end(); it != ie; ++it)
00257     inB = AndExpr::create(inB, *it);
00258 
00259   // XXX should we have a preference as to which predicate to use?
00260   // it seems like it can make a difference, even though logically
00261   // they must contradict each other and so inA => !inB
00262 
00263   std::vector<StackFrame>::iterator itA = stack.begin();
00264   std::vector<StackFrame>::const_iterator itB = b.stack.begin();
00265   for (; itA!=stack.end(); ++itA, ++itB) {
00266     StackFrame &af = *itA;
00267     const StackFrame &bf = *itB;
00268     for (unsigned i=0; i<af.kf->numRegisters; i++) {
00269       ref<Expr> &av = af.locals[i].value;
00270       const ref<Expr> &bv = bf.locals[i].value;
00271       if (av.isNull() || bv.isNull()) {
00272         // if one is null then by implication (we are at same pc)
00273         // we cannot reuse this local, so just ignore
00274       } else {
00275         av = SelectExpr::create(inA, av, bv);
00276       }
00277     }
00278   }
00279 
00280   for (std::set<const MemoryObject*>::iterator it = mutated.begin(), 
00281          ie = mutated.end(); it != ie; ++it) {
00282     const MemoryObject *mo = *it;
00283     const ObjectState *os = addressSpace.findObject(mo);
00284     const ObjectState *otherOS = b.addressSpace.findObject(mo);
00285     assert(os && !os->readOnly && 
00286            "objects mutated but not writable in merging state");
00287     assert(otherOS);
00288 
00289     ObjectState *wos = addressSpace.getWriteable(mo, os);
00290     for (unsigned i=0; i<mo->size; i++) {
00291       ref<Expr> av = wos->read8(i);
00292       ref<Expr> bv = otherOS->read8(i);
00293       wos->write(i, SelectExpr::create(inA, av, bv));
00294     }
00295   }
00296 
00297   constraints = ConstraintManager();
00298   for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(), 
00299          ie = commonConstraints.end(); it != ie; ++it)
00300     constraints.addConstraint(*it);
00301   constraints.addConstraint(OrExpr::create(inA, inB));
00302 
00303   return true;
00304 }
00305 
00306 
00307 
00308 /*
00309    Used for tainting: create a clone of os that we can revirt to with
00310    the behavior that all constraints are preserved, but writes are 
00311    discarded.  When we revirt it will be at the same address.
00312  */
00313 ObjectState *ExecutionState::cloneObject(ObjectState *os, 
00314                                          MemoryObject *mo) {
00315   MemoryMap::iterator it = shadowObjects.find(mo);
00316   if (it != shadowObjects.end())
00317     assert(0 && "Cannot exist already!");
00318 
00319   llvm::cerr << "DRE: Inserting a cloned object: " << mo << "\n";
00320   shadowObjects = shadowObjects.replace(std::make_pair(mo, os));
00321   os = new ObjectState(*os);
00322   addressSpace.bindObject(mo, os);
00323   return os;
00324 }
00325 
00326 /***/
00327 
00328 
00329 ExecutionTraceEvent::ExecutionTraceEvent(ExecutionState& state, 
00330                                          KInstruction* ki)
00331   : consecutiveCount(1) 
00332 {
00333   file = ki->info->file;
00334   line = ki->info->line;
00335   funcName = state.stack.back().kf->function->getName();
00336   stackDepth = state.stack.size();
00337 }
00338 
00339 bool ExecutionTraceEvent::ignoreMe() const {
00340   // ignore all events occurring in certain pesky uclibc files:
00341   if (file.find("libc/stdio/") != std::string::npos) {
00342     return true;
00343   }
00344 
00345   return false;
00346 }
00347 
00348 void ExecutionTraceEvent::print(std::ostream &os) const {
00349   os.width(stackDepth);
00350   os << ' ';
00351   printDetails(os);
00352   os << ' ' << file << ':' << line << ':' << funcName;
00353   if (consecutiveCount > 1)
00354     os << " (" << consecutiveCount << "x)\n";
00355   else
00356     os << '\n';
00357 }
00358 
00359 
00360 bool ExecutionTraceEventEquals(ExecutionTraceEvent* e1, ExecutionTraceEvent* e2) {
00361   // first see if their base class members are identical:
00362   if (!((e1->file == e2->file) &&
00363         (e1->line == e2->line) &&
00364         (e1->funcName == e2->funcName)))
00365     return false;
00366 
00367   // fairly ugly, but i'm no OOP master, so this is the way i'm
00368   // doing it for now ... lemme know if there's a cleaner way:
00369   BranchTraceEvent* be1 = dynamic_cast<BranchTraceEvent*>(e1);
00370   BranchTraceEvent* be2 = dynamic_cast<BranchTraceEvent*>(e2);
00371   if (be1 && be2) {
00372     return ((be1->trueTaken == be2->trueTaken) &&
00373             (be1->canForkGoBothWays == be2->canForkGoBothWays));
00374   }
00375 
00376   // don't tolerate duplicates in anything else:
00377   return false;
00378 }
00379 
00380 
00381 void BranchTraceEvent::printDetails(std::ostream &os) const {
00382   os << "BRANCH " << (trueTaken ? "T" : "F") << ' ' <<
00383         (canForkGoBothWays ? "2-way" : "1-way");
00384 }
00385 
00386 void ExecutionTraceManager::addEvent(ExecutionTraceEvent* evt) {
00387   // don't trace anything before __user_main, except for global events
00388   if (!hasSeenUserMain) {
00389     if (evt->funcName == "__user_main") {
00390       hasSeenUserMain = true;
00391     }
00392     else if (evt->funcName != "global_def") {
00393       return;
00394     }
00395   }
00396 
00397   // custom ignore events:
00398   if (evt->ignoreMe())
00399     return;
00400 
00401   if (events.size() > 0) {
00402     // compress consecutive duplicates:
00403     ExecutionTraceEvent* last = events.back();
00404     if (ExecutionTraceEventEquals(last, evt)) {
00405       last->consecutiveCount++;
00406       return;
00407     }
00408   }
00409 
00410   events.push_back(evt);
00411 }
00412 
00413 void ExecutionTraceManager::printAllEvents(std::ostream &os) const {
00414   for (unsigned i = 0; i != events.size(); ++i)
00415     events[i]->print(os);
00416 }
00417 
00418 /***/

Generated on Fri Jun 5 03:31:31 2009 for klee by  doxygen 1.5.8