diff options
Diffstat (limited to 'lib/Core/Searcher.cpp')
| -rw-r--r-- | lib/Core/Searcher.cpp | 575 |
1 files changed, 575 insertions, 0 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp new file mode 100644 index 00000000..4c94c59b --- /dev/null +++ b/lib/Core/Searcher.cpp @@ -0,0 +1,575 @@ +//===-- Searcher.cpp ------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "Common.h" + +#include "Searcher.h" + +#include "CoreStats.h" +#include "Executor.h" +#include "PTree.h" +#include "StatsTracker.h" + +#include "klee/ExecutionState.h" +#include "klee/Statistics.h" +#include "klee/Internal/Module/InstructionInfoTable.h" +#include "klee/Internal/Module/KInstruction.h" +#include "klee/Internal/Module/KModule.h" +#include "klee/Internal/ADT/DiscretePDF.h" +#include "klee/Internal/ADT/RNG.h" +#include "klee/Internal/Support/ModuleUtil.h" +#include "klee/Internal/System/Time.h" + +#include "llvm/Constants.h" +#include "llvm/Instructions.h" +#include "llvm/Module.h" +#include "llvm/Support/CallSite.h" +#include "llvm/Support/CFG.h" +#include "llvm/Support/CommandLine.h" + +#include <cassert> +#include <fstream> +#include <climits> + +using namespace klee; +using namespace llvm; + +namespace { + cl::opt<bool> + DebugLogMerge("debug-log-merge"); +} + +namespace klee { + extern RNG theRNG; +} + +Searcher::~Searcher() { +} + +/// + +ExecutionState &DFSSearcher::selectState() { + return *states.back(); +} + +void DFSSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + states.insert(states.end(), + addedStates.begin(), + addedStates.end()); + for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { + ExecutionState *es = *it; + if (es == states.back()) { + states.pop_back(); + } else { + bool ok = false; + + for (std::vector<ExecutionState*>::iterator it = states.begin(), + ie = states.end(); it != ie; ++it) { + if (es==*it) { + states.erase(it); + ok = true; + break; + } + } + + assert(ok && "invalid state removed"); + } + } +} + +/// + +ExecutionState &RandomSearcher::selectState() { + return *states[theRNG.getInt32()%states.size()]; +} + +void RandomSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + states.insert(states.end(), + addedStates.begin(), + addedStates.end()); + for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { + ExecutionState *es = *it; + bool ok = false; + + for (std::vector<ExecutionState*>::iterator it = states.begin(), + ie = states.end(); it != ie; ++it) { + if (es==*it) { + states.erase(it); + ok = true; + break; + } + } + + assert(ok && "invalid state removed"); + } +} + +/// + +WeightedRandomSearcher::WeightedRandomSearcher(Executor &_executor, + WeightType _type) + : executor(_executor), + states(new DiscretePDF<ExecutionState*>()), + type(_type) { + switch(type) { + case Depth: + updateWeights = false; + break; + case InstCount: + case CPInstCount: + case QueryCost: + case MinDistToUncovered: + case CoveringNew: + updateWeights = true; + break; + default: + assert(0 && "invalid weight type"); + } +} + +WeightedRandomSearcher::~WeightedRandomSearcher() { + delete states; +} + +ExecutionState &WeightedRandomSearcher::selectState() { + return *states->choose(theRNG.getDoubleL()); +} + +double WeightedRandomSearcher::getWeight(ExecutionState *es) { + switch(type) { + default: + case Depth: + return es->weight; + case InstCount: { + uint64_t count = theStatisticManager->getIndexedValue(stats::instructions, + es->pc->info->id); + double inv = 1. / std::max((uint64_t) 1, count); + return inv * inv; + } + case CPInstCount: { + StackFrame &sf = es->stack.back(); + uint64_t count = sf.callPathNode->statistics.getValue(stats::instructions); + double inv = 1. / std::max((uint64_t) 1, count); + return inv; + } + case QueryCost: + return (es->queryCost < .1) ? 1. : 1./es->queryCost; + case CoveringNew: + case MinDistToUncovered: { + uint64_t md2u = computeMinDistToUncovered(es->pc, + es->stack.back().minDistToUncoveredOnReturn); + + double invMD2U = 1. / (md2u ? md2u : 10000); + if (type==CoveringNew) { + double invCovNew = 0.; + if (es->instsSinceCovNew) + invCovNew = 1. / std::max(1, (int) es->instsSinceCovNew - 1000); + return (invCovNew * invCovNew + invMD2U * invMD2U); + } else { + return invMD2U * invMD2U; + } + } + } +} + +void WeightedRandomSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + if (current && updateWeights && !removedStates.count(current)) + states->update(current, getWeight(current)); + + for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(), + ie = addedStates.end(); it != ie; ++it) { + ExecutionState *es = *it; + states->insert(es, getWeight(es)); + } + + for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { + states->remove(*it); + } +} + +bool WeightedRandomSearcher::empty() { + return states->empty(); +} + +/// + +RandomPathSearcher::RandomPathSearcher(Executor &_executor) + : executor(_executor) { +} + +RandomPathSearcher::~RandomPathSearcher() { +} + +ExecutionState &RandomPathSearcher::selectState() { + unsigned flips=0, bits=0; + PTree::Node *n = executor.processTree->root; + + while (!n->data) { + if (!n->left) { + n = n->right; + } else if (!n->right) { + n = n->left; + } else { + if (bits==0) { + flips = theRNG.getInt32(); + bits = 32; + } + --bits; + n = (flips&(1<<bits)) ? n->left : n->right; + } + } + + return *n->data; +} + +void RandomPathSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { +} + +bool RandomPathSearcher::empty() { + return executor.states.empty(); +} + +/// + +BumpMergingSearcher::BumpMergingSearcher(Executor &_executor, Searcher *_baseSearcher) + : executor(_executor), + baseSearcher(_baseSearcher), + mergeFunction(executor.kmodule->kleeMergeFn) { +} + +BumpMergingSearcher::~BumpMergingSearcher() { + delete baseSearcher; +} + +/// + +Instruction *BumpMergingSearcher::getMergePoint(ExecutionState &es) { + if (mergeFunction) { + Instruction *i = es.pc->inst; + + if (i->getOpcode()==Instruction::Call) { + CallSite cs(cast<CallInst>(i)); + if (mergeFunction==cs.getCalledFunction()) + return i; + } + } + + return 0; +} + +ExecutionState &BumpMergingSearcher::selectState() { +entry: + // out of base states, pick one to pop + if (baseSearcher->empty()) { + std::map<llvm::Instruction*, ExecutionState*>::iterator it = + statesAtMerge.begin(); + ExecutionState *es = it->second; + statesAtMerge.erase(it); + ++es->pc; + + baseSearcher->addState(es); + } + + ExecutionState &es = baseSearcher->selectState(); + + if (Instruction *mp = getMergePoint(es)) { + std::map<llvm::Instruction*, ExecutionState*>::iterator it = + statesAtMerge.find(mp); + + baseSearcher->removeState(&es); + + if (it==statesAtMerge.end()) { + statesAtMerge.insert(std::make_pair(mp, &es)); + } else { + ExecutionState *mergeWith = it->second; + if (mergeWith->merge(es)) { + // hack, because we are terminating the state we need to let + // the baseSearcher know about it again + baseSearcher->addState(&es); + executor.terminateState(es); + } else { + it->second = &es; // the bump + ++mergeWith->pc; + + baseSearcher->addState(mergeWith); + } + } + + goto entry; + } else { + return es; + } +} + +void BumpMergingSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + baseSearcher->update(current, addedStates, removedStates); +} + +/// + +MergingSearcher::MergingSearcher(Executor &_executor, Searcher *_baseSearcher) + : executor(_executor), + baseSearcher(_baseSearcher), + mergeFunction(executor.kmodule->kleeMergeFn) { +} + +MergingSearcher::~MergingSearcher() { + delete baseSearcher; +} + +/// + +Instruction *MergingSearcher::getMergePoint(ExecutionState &es) { + if (mergeFunction) { + Instruction *i = es.pc->inst; + + if (i->getOpcode()==Instruction::Call) { + CallSite cs(cast<CallInst>(i)); + if (mergeFunction==cs.getCalledFunction()) + return i; + } + } + + return 0; +} + +ExecutionState &MergingSearcher::selectState() { + while (!baseSearcher->empty()) { + ExecutionState &es = baseSearcher->selectState(); + if (getMergePoint(es)) { + baseSearcher->removeState(&es, &es); + statesAtMerge.insert(&es); + } else { + return es; + } + } + + // build map of merge point -> state list + std::map<Instruction*, std::vector<ExecutionState*> > merges; + for (std::set<ExecutionState*>::const_iterator it = statesAtMerge.begin(), + ie = statesAtMerge.end(); it != ie; ++it) { + ExecutionState &state = **it; + Instruction *mp = getMergePoint(state); + + merges[mp].push_back(&state); + } + + if (DebugLogMerge) + llvm::cerr << "-- all at merge --\n"; + for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator + it = merges.begin(), ie = merges.end(); it != ie; ++it) { + if (DebugLogMerge) { + llvm::cerr << "\tmerge: " << it->first << " ["; + for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(), + ie2 = it->second.end(); it2 != ie2; ++it2) { + ExecutionState *state = *it2; + llvm::cerr << state << ", "; + } + llvm::cerr << "]\n"; + } + + // merge states + std::set<ExecutionState*> toMerge(it->second.begin(), it->second.end()); + while (!toMerge.empty()) { + ExecutionState *base = *toMerge.begin(); + toMerge.erase(toMerge.begin()); + + std::set<ExecutionState*> toErase; + for (std::set<ExecutionState*>::iterator it = toMerge.begin(), + ie = toMerge.end(); it != ie; ++it) { + ExecutionState *mergeWith = *it; + + if (base->merge(*mergeWith)) { + toErase.insert(mergeWith); + } + } + if (DebugLogMerge && !toErase.empty()) { + llvm::cerr << "\t\tmerged: " << base << " with ["; + for (std::set<ExecutionState*>::iterator it = toErase.begin(), + ie = toErase.end(); it != ie; ++it) { + if (it!=toErase.begin()) llvm::cerr << ", "; + llvm::cerr << *it; + } + llvm::cerr << "]\n"; + } + for (std::set<ExecutionState*>::iterator it = toErase.begin(), + ie = toErase.end(); it != ie; ++it) { + std::set<ExecutionState*>::iterator it2 = toMerge.find(*it); + assert(it2!=toMerge.end()); + executor.terminateState(**it); + toMerge.erase(it2); + } + + // step past merge and toss base back in pool + statesAtMerge.erase(statesAtMerge.find(base)); + ++base->pc; + baseSearcher->addState(base); + } + } + + if (DebugLogMerge) + llvm::cerr << "-- merge complete, continuing --\n"; + + return selectState(); +} + +void MergingSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + if (!removedStates.empty()) { + std::set<ExecutionState *> alt = removedStates; + for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { + ExecutionState *es = *it; + std::set<ExecutionState*>::const_iterator it = statesAtMerge.find(es); + if (it!=statesAtMerge.end()) { + statesAtMerge.erase(it); + alt.erase(alt.find(es)); + } + } + baseSearcher->update(current, addedStates, alt); + } else { + baseSearcher->update(current, addedStates, removedStates); + } +} + +/// + +BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher, + double _timeBudget, + unsigned _instructionBudget) + : baseSearcher(_baseSearcher), + timeBudget(_timeBudget), + instructionBudget(_instructionBudget), + lastState(0) { + +} + +BatchingSearcher::~BatchingSearcher() { + delete baseSearcher; +} + +ExecutionState &BatchingSearcher::selectState() { + if (!lastState || + (util::getWallTime()-lastStartTime)>timeBudget || + (stats::instructions-lastStartInstructions)>instructionBudget) { + if (lastState) { + double delta = util::getWallTime()-lastStartTime; + if (delta>timeBudget*1.1) { + llvm::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n"; + timeBudget = delta; + } + } + lastState = &baseSearcher->selectState(); + lastStartTime = util::getWallTime(); + lastStartInstructions = stats::instructions; + return *lastState; + } else { + return *lastState; + } +} + +void BatchingSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + if (removedStates.count(lastState)) + lastState = 0; + baseSearcher->update(current, addedStates, removedStates); +} + +/***/ + +IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *_baseSearcher) + : baseSearcher(_baseSearcher), + time(1.) { +} + +IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() { + delete baseSearcher; +} + +ExecutionState &IterativeDeepeningTimeSearcher::selectState() { + ExecutionState &res = baseSearcher->selectState(); + startTime = util::getWallTime(); + return res; +} + +void IterativeDeepeningTimeSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + double elapsed = util::getWallTime() - startTime; + + if (!removedStates.empty()) { + std::set<ExecutionState *> alt = removedStates; + for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { + ExecutionState *es = *it; + std::set<ExecutionState*>::const_iterator it = pausedStates.find(es); + if (it!=pausedStates.end()) { + pausedStates.erase(it); + alt.erase(alt.find(es)); + } + } + baseSearcher->update(current, addedStates, alt); + } else { + baseSearcher->update(current, addedStates, removedStates); + } + + if (current && !removedStates.count(current) && elapsed>time) { + pausedStates.insert(current); + baseSearcher->removeState(current); + } + + if (baseSearcher->empty()) { + time *= 2; + llvm::cerr << "KLEE: increasing time budget to: " << time << "\n"; + baseSearcher->update(0, pausedStates, std::set<ExecutionState*>()); + pausedStates.clear(); + } +} + +/***/ + +InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers) + : searchers(_searchers), + index(1) { +} + +InterleavedSearcher::~InterleavedSearcher() { + for (std::vector<Searcher*>::const_iterator it = searchers.begin(), + ie = searchers.end(); it != ie; ++it) + delete *it; +} + +ExecutionState &InterleavedSearcher::selectState() { + Searcher *s = searchers[--index]; + if (index==0) index = searchers.size(); + return s->selectState(); +} + +void InterleavedSearcher::update(ExecutionState *current, + const std::set<ExecutionState*> &addedStates, + const std::set<ExecutionState*> &removedStates) { + for (std::vector<Searcher*>::const_iterator it = searchers.begin(), + ie = searchers.end(); it != ie; ++it) + (*it)->update(current, addedStates, removedStates); +} |