00001
00002
00003
00004
00005
00006
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
00156
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
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
00206
00207
00208
00209
00210
00211
00212
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
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
00260
00261
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
00273
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
00310
00311
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
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
00362 if (!((e1->file == e2->file) &&
00363 (e1->line == e2->line) &&
00364 (e1->funcName == e2->funcName)))
00365 return false;
00366
00367
00368
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
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
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
00398 if (evt->ignoreMe())
00399 return;
00400
00401 if (events.size() > 0) {
00402
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