aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Searcher.cpp211
-rw-r--r--lib/Core/Searcher.h46
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp7
-rw-r--r--lib/Core/SpecialFunctionHandler.h1
-rw-r--r--lib/Core/UserSearcher.cpp22
-rw-r--r--lib/Module/KModule.cpp53
6 files changed, 0 insertions, 340 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 0e7aa685..b9f22538 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -301,217 +301,6 @@ bool RandomPathSearcher::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::vector<ExecutionState *> &addedStates,
- const std::vector<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() {
- // FIXME: this loop is endless if baseSearcher includes RandomPathSearcher.
- // The reason is that RandomPathSearcher::removeState() does nothing...
- 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::errs() << "-- all at merge --\n";
- for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator
- it = merges.begin(), ie = merges.end(); it != ie; ++it) {
- if (DebugLogMerge) {
- llvm::errs() << "\tmerge: " << it->first << " [";
- for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(),
- ie2 = it->second.end(); it2 != ie2; ++it2) {
- ExecutionState *state = *it2;
- llvm::errs() << state << ", ";
- }
- llvm::errs() << "]\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::errs() << "\t\tmerged: " << base << " with [";
- for (std::set<ExecutionState*>::iterator it = toErase.begin(),
- ie = toErase.end(); it != ie; ++it) {
- if (it!=toErase.begin()) llvm::errs() << ", ";
- llvm::errs() << *it;
- }
- llvm::errs() << "]\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::errs() << "-- merge complete, continuing --\n";
-
- return selectState();
-}
-
-void
-MergingSearcher::update(ExecutionState *current,
- const std::vector<ExecutionState *> &addedStates,
- const std::vector<ExecutionState *> &removedStates) {
- if (!removedStates.empty()) {
- std::vector<ExecutionState *> alt = removedStates;
- for (std::vector<ExecutionState *>::const_iterator
- it = removedStates.begin(),
- ie = removedStates.end();
- it != ie; ++it) {
- ExecutionState *es = *it;
- std::set<ExecutionState*>::const_iterator it2 = statesAtMerge.find(es);
- if (it2 != statesAtMerge.end()) {
- statesAtMerge.erase(it2);
- alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end());
- }
- }
- baseSearcher->update(current, addedStates, alt);
- } else {
- baseSearcher->update(current, addedStates, removedStates);
- }
-}
-
-///
-
BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
double _timeBudget,
unsigned _instructionBudget)
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 4ede3640..27c8aed1 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -180,52 +180,6 @@ namespace klee {
}
};
- class MergingSearcher : public Searcher {
- Executor &executor;
- std::set<ExecutionState*> statesAtMerge;
- Searcher *baseSearcher;
- llvm::Function *mergeFunction;
-
- private:
- llvm::Instruction *getMergePoint(ExecutionState &es);
-
- public:
- MergingSearcher(Executor &executor, Searcher *baseSearcher);
- ~MergingSearcher();
-
- ExecutionState &selectState();
- void update(ExecutionState *current,
- const std::vector<ExecutionState *> &addedStates,
- const std::vector<ExecutionState *> &removedStates);
- bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
- void printName(llvm::raw_ostream &os) {
- os << "MergingSearcher\n";
- }
- };
-
- class BumpMergingSearcher : public Searcher {
- Executor &executor;
- std::map<llvm::Instruction*, ExecutionState*> statesAtMerge;
- Searcher *baseSearcher;
- llvm::Function *mergeFunction;
-
- private:
- llvm::Instruction *getMergePoint(ExecutionState &es);
-
- public:
- BumpMergingSearcher(Executor &executor, Searcher *baseSearcher);
- ~BumpMergingSearcher();
-
- ExecutionState &selectState();
- void update(ExecutionState *current,
- const std::vector<ExecutionState *> &addedStates,
- const std::vector<ExecutionState *> &removedStates);
- bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
- void printName(llvm::raw_ostream &os) {
- os << "BumpMergingSearcher\n";
- }
- };
-
class BatchingSearcher : public Searcher {
Searcher *baseSearcher;
double timeBudget;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index aaa26922..74d36f27 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -93,7 +93,6 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
add("klee_is_symbolic", handleIsSymbolic, true),
add("klee_make_symbolic", handleMakeSymbolic, false),
add("klee_mark_global", handleMarkGlobal, false),
- add("klee_merge", handleMerge, false),
add("klee_prefer_cex", handlePreferCex, false),
add("klee_posix_prefer_cex", handlePosixPreferCex, false),
add("klee_print_expr", handlePrintExpr, false),
@@ -325,12 +324,6 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
readStringAtAddress(state, arguments[3]).c_str());
}
-void SpecialFunctionHandler::handleMerge(ExecutionState &state,
- KInstruction *target,
- std::vector<ref<Expr> > &arguments) {
- // nop
-}
-
void SpecialFunctionHandler::handleNew(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 2dfdde43..394b649a 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -116,7 +116,6 @@ namespace klee {
HANDLER(handleMakeSymbolic);
HANDLER(handleMalloc);
HANDLER(handleMarkGlobal);
- HANDLER(handleMerge);
HANDLER(handleNew);
HANDLER(handleNewArray);
HANDLER(handlePreferCex);
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 2bbbe747..4275f3a5 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -52,15 +52,6 @@ namespace {
cl::desc("Amount of time to batch when using --use-batching-search"),
cl::init(5.0));
-
- cl::opt<bool>
- UseMerge("use-merge",
- cl::desc("Enable support for klee_merge() (experimental)"));
-
- cl::opt<bool>
- UseBumpMerge("use-bump-merge",
- cl::desc("Enable support for klee_merge() (extra experimental)"));
-
}
@@ -115,19 +106,6 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
}
- // merge support is experimental
- if (UseMerge) {
- if (UseBumpMerge)
- klee_error("use-merge and use-bump-merge cannot be used together");
- // RandomPathSearcher cannot be used in conjunction with MergingSearcher,
- // see MergingSearcher::selectState() for explanation.
- if (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end())
- klee_error("use-merge currently does not support random-path, please use another search strategy");
- searcher = new MergingSearcher(executor, searcher);
- } else if (UseBumpMerge) {
- searcher = new BumpMergingSearcher(executor, searcher);
- }
-
if (UseIterativeDeepeningTimeSearch) {
searcher = new IterativeDeepeningTimeSearcher(searcher);
}
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 751776b9..bb34dcad 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -54,9 +54,6 @@ namespace {
eSwitchTypeLLVM,
eSwitchTypeInternal
};
-
- cl::list<std::string>
- MergeAtExit("merge-at-exit");
cl::opt<bool>
NoTruncateSourceLines("no-truncate-source-lines",
@@ -91,7 +88,6 @@ namespace {
KModule::KModule(Module *_module)
: module(_module),
targetData(new DataLayout(module)),
- kleeMergeFn(0),
infos(0),
constantTable(0) {
}
@@ -206,53 +202,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
InterpreterHandler *ih) {
LLVMContext &ctx = module->getContext();
- if (!MergeAtExit.empty()) {
- Function *mergeFn = module->getFunction("klee_merge");
- if (!mergeFn) {
- llvm::FunctionType *Ty =
- FunctionType::get(Type::getVoidTy(ctx), std::vector<Type *>(), false);
- mergeFn = Function::Create(Ty, GlobalVariable::ExternalLinkage,
- "klee_merge",
- module);
- }
-
- for (cl::list<std::string>::iterator it = MergeAtExit.begin(),
- ie = MergeAtExit.end(); it != ie; ++it) {
- std::string &name = *it;
- Function *f = module->getFunction(name);
- if (!f) {
- klee_error("cannot insert merge-at-exit for: %s (cannot find)",
- name.c_str());
- } else if (f->isDeclaration()) {
- klee_error("cannot insert merge-at-exit for: %s (external)",
- name.c_str());
- }
-
- BasicBlock *exit = BasicBlock::Create(ctx, "exit", f);
- PHINode *result = 0;
- if (f->getReturnType() != Type::getVoidTy(ctx))
- result = PHINode::Create(f->getReturnType(), 0, "retval", exit);
- CallInst::Create(mergeFn, "", exit);
- ReturnInst::Create(ctx, result, exit);
-
- llvm::errs() << "KLEE: adding klee_merge at exit of: " << name << "\n";
- for (llvm::Function::iterator bbit = f->begin(), bbie = f->end();
- bbit != bbie; ++bbit) {
- BasicBlock *bb = &*bbit;
- if (bb != exit) {
- Instruction *i = bbit->getTerminator();
- if (i->getOpcode()==Instruction::Ret) {
- if (result) {
- result->addIncoming(i->getOperand(0), bb);
- }
- i->eraseFromParent();
- BranchInst::Create(exit, bb);
- }
- }
- }
- }
- }
-
// Inject checks prior to optimization... we also perform the
// invariant transformations that we will end up doing later so that
// optimize is seeing what is as close as possible to the final
@@ -373,8 +322,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
delete f;
}
- kleeMergeFn = module->getFunction("klee_merge");
-
/* Build shadow structures */
infos = new InstructionInfoTable(module);
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-22 20:41:52 +0000