From 078eac2264f8d80961872f77c1925c997a60ef9b Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Fri, 8 Jul 2016 21:54:56 +0200 Subject: Refactoring: Extract method to dump remaining states --- lib/Core/Executor.cpp | 40 ++++++++++++++++++++++++---------------- lib/Core/Executor.h | 1 + 2 files changed, 25 insertions(+), 16 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 46e163ea..2c4e5202 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2580,6 +2580,20 @@ void Executor::checkMemoryUsage() { } } +void Executor::doDumpStates() { + if (!DumpStatesOnHalt || states.empty()) + return; + klee_message("halting execution, dumping remaining states"); + for (std::set::iterator it = states.begin(), + ie = states.end(); + it != ie; ++it) { + ExecutionState &state = **it; + stepInstruction(state); // keep stats rolling + terminateStateEarly(state, "Execution halting."); + } + updateStates(0); +} + void Executor::run(ExecutionState &initialState) { bindModuleConstants(); @@ -2600,7 +2614,10 @@ void Executor::run(ExecutionState &initialState) { double lastTime, startTime = lastTime = util::getWallTime(); ExecutionState *lastState = 0; while (!seedMap.empty()) { - if (haltExecution) goto dump; + if (haltExecution) { + doDumpStates(); + return; + } std::map >::iterator it = seedMap.upper_bound(lastState); @@ -2649,8 +2666,10 @@ void Executor::run(ExecutionState &initialState) { (*it)->weight = 1.; } - if (OnlySeed) - goto dump; + if (OnlySeed) { + doDumpStates(); + return; + } } searcher = constructUserSearcher(*this); @@ -2672,19 +2691,8 @@ void Executor::run(ExecutionState &initialState) { delete searcher; searcher = 0; - - dump: - if (DumpStatesOnHalt && !states.empty()) { - klee_message("halting execution, dumping remaining states"); - for (std::set::iterator - it = states.begin(), ie = states.end(); - it != ie; ++it) { - ExecutionState &state = **it; - stepInstruction(state); // keep stats rolling - terminateStateEarly(state, "Execution halting."); - } - updateStates(0); - } + + doDumpStates(); } std::string Executor::getAddressInfo(ExecutionState &state, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 600c7b90..99f5921b 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -412,6 +412,7 @@ private: double maxInstTime); void checkMemoryUsage(); void printDebugInstructions(ExecutionState &state); + void doDumpStates(); public: Executor(const InterpreterOptions &opts, InterpreterHandler *ie); -- cgit 1.4.1 From 07632e75e21e3c61f1ab46f76618cb1b807bd6c3 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 22 Mar 2016 16:17:24 +0100 Subject: IterativeDeepeningTimeSearcher: Fix using wrong iterator --- lib/Core/Searcher.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index cbb88727..299bb89d 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -566,7 +566,7 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, ExecutionState *es = *it; std::set::const_iterator it2 = pausedStates.find(es); if (it2 != pausedStates.end()) { - pausedStates.erase(it); + pausedStates.erase(it2); alt.erase(alt.find(es)); } } -- cgit 1.4.1 From f3ff3b06318cae93db4d682e6451ddbca4760328 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 22 Mar 2016 16:39:28 +0100 Subject: Use vector instead of set to add/remove states Deterministic adding/removing of states. --- lib/Core/Executor.cpp | 18 +++--- lib/Core/Executor.h | 4 +- lib/Core/ExecutorTimers.cpp | 4 +- lib/Core/Searcher.cpp | 122 +++++++++++++++++++++---------------- lib/Core/Searcher.h | 56 ++++++++--------- test/Feature/DeterministicSwitch.c | 41 +++++++++++++ 6 files changed, 155 insertions(+), 90 deletions(-) create mode 100644 test/Feature/DeterministicSwitch.c diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2c4e5202..49cba67f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -665,7 +665,7 @@ void Executor::branch(ExecutionState &state, for (unsigned i=1; ibranch(); - addedStates.insert(ns); + addedStates.push_back(ns); result.push_back(ns); es->ptreeNode->data = 0; std::pair res = @@ -883,7 +883,7 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { ++stats::forks; falseState = trueState->branch(); - addedStates.insert(falseState); + addedStates.push_back(falseState); if (RandomizeFork && theRNG.getBool()) std::swap(trueState, falseState); @@ -2467,9 +2467,9 @@ void Executor::updateStates(ExecutionState *current) { states.insert(addedStates.begin(), addedStates.end()); addedStates.clear(); - - for (std::set::iterator - it = removedStates.begin(), ie = removedStates.end(); + + for (std::vector::iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { ExecutionState *es = *it; std::set::iterator it2 = states.find(es); @@ -2674,7 +2674,8 @@ void Executor::run(ExecutionState &initialState) { searcher = constructUserSearcher(*this); - searcher->update(0, states, std::set()); + std::vector newStates(states.begin(), states.end()); + searcher->update(0, newStates, std::vector()); while (!states.empty() && !haltExecution) { ExecutionState &state = searcher->selectState(); @@ -2753,11 +2754,12 @@ void Executor::terminateState(ExecutionState &state) { interpreterHandler->incPathsExplored(); - std::set::iterator it = addedStates.find(&state); + std::vector::iterator it = + std::find(addedStates.begin(), addedStates.end(), &state); if (it==addedStates.end()) { state.pc = state.prevPC; - removedStates.insert(&state); + removedStates.push_back(&state); } else { // never reached searcher, just delete immediately std::map< ExecutionState*, std::vector >::iterator it3 = diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 99f5921b..92edc364 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -122,12 +122,12 @@ private: /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set addedStates; + std::vector addedStates; /// Used to track states that have been removed during the current /// instructions step. /// \invariant \ref removedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set removedStates; + std::vector removedStates; /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 480f1cde..f1c45105 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -179,7 +179,9 @@ void Executor::processTimers(ExecutionState *current, dumpStates = 0; } - if (maxInstTime>0 && current && !removedStates.count(current)) { + if (maxInstTime > 0 && current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) { if (timerTicks*kSecondsPerTick > maxInstTime) { klee_warning("max-instruction-time exceeded: %.2fs", timerTicks*kSecondsPerTick); diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 299bb89d..973057c3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -67,13 +67,14 @@ ExecutionState &DFSSearcher::selectState() { } void DFSSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { + const std::vector &addedStates, + const std::vector &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.back()) { states.pop_back(); @@ -101,13 +102,14 @@ ExecutionState &BFSSearcher::selectState() { } void BFSSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { + const std::vector &addedStates, + const std::vector &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.front()) { states.pop_front(); @@ -134,14 +136,16 @@ ExecutionState &RandomSearcher::selectState() { return *states[theRNG.getInt32()%states.size()]; } -void RandomSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { +void +RandomSearcher::update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; bool ok = false; @@ -224,20 +228,24 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { } } -void WeightedRandomSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { - if (current && updateWeights && !removedStates.count(current)) +void WeightedRandomSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { + if (current && updateWeights && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) states->update(current, getWeight(current)); - - for (std::set::const_iterator it = addedStates.begin(), - ie = addedStates.end(); it != ie; ++it) { + + for (std::vector::const_iterator it = addedStates.begin(), + ie = addedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; states->insert(es, getWeight(es)); } - for (std::set::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { states->remove(*it); } } @@ -277,9 +285,10 @@ ExecutionState &RandomPathSearcher::selectState() { return *n->data; } -void RandomPathSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { +void +RandomPathSearcher::update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) { } bool RandomPathSearcher::empty() { @@ -358,9 +367,9 @@ entry: } } -void BumpMergingSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { +void BumpMergingSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { baseSearcher->update(current, addedStates, removedStates); } @@ -472,18 +481,21 @@ ExecutionState &MergingSearcher::selectState() { return selectState(); } -void MergingSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { +void +MergingSearcher::update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) { if (!removedStates.empty()) { - std::set alt = removedStates; - for (std::set::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + std::vector alt = removedStates; + for (std::vector::const_iterator + it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; std::set::const_iterator it2 = statesAtMerge.find(es); if (it2 != statesAtMerge.end()) { statesAtMerge.erase(it2); - alt.erase(alt.find(es)); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -529,10 +541,12 @@ ExecutionState &BatchingSearcher::selectState() { } } -void BatchingSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { - if (removedStates.count(lastState)) +void +BatchingSearcher::update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) { + if (std::find(removedStates.begin(), removedStates.end(), lastState) != + removedStates.end()) lastState = 0; baseSearcher->update(current, addedStates, removedStates); } @@ -554,20 +568,22 @@ ExecutionState &IterativeDeepeningTimeSearcher::selectState() { return res; } -void IterativeDeepeningTimeSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { +void IterativeDeepeningTimeSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { double elapsed = util::getWallTime() - startTime; if (!removedStates.empty()) { - std::set alt = removedStates; - for (std::set::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + std::vector alt = removedStates; + for (std::vector::const_iterator + it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; std::set::const_iterator it2 = pausedStates.find(es); if (it2 != pausedStates.end()) { pausedStates.erase(it2); - alt.erase(alt.find(es)); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -575,7 +591,10 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, baseSearcher->update(current, addedStates, removedStates); } - if (current && !removedStates.count(current) && elapsed>time) { + if (current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end() && + elapsed > time) { pausedStates.insert(current); baseSearcher->removeState(current); } @@ -583,7 +602,8 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, if (baseSearcher->empty()) { time *= 2; llvm::errs() << "KLEE: increasing time budget to: " << time << "\n"; - baseSearcher->update(0, pausedStates, std::set()); + std::vector ps(pausedStates.begin(), pausedStates.end()); + baseSearcher->update(0, ps, std::vector()); pausedStates.clear(); } } @@ -607,9 +627,9 @@ ExecutionState &InterleavedSearcher::selectState() { return s->selectState(); } -void InterleavedSearcher::update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) { +void InterleavedSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { for (std::vector::const_iterator it = searchers.begin(), ie = searchers.end(); it != ie; ++it) (*it)->update(current, addedStates, removedStates); diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index d866f521..4ede3640 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -35,8 +35,8 @@ namespace klee { virtual ExecutionState &selectState() = 0; virtual void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates) = 0; + const std::vector &addedStates, + const std::vector &removedStates) = 0; virtual bool empty() = 0; @@ -55,15 +55,15 @@ namespace klee { // utility functions void addState(ExecutionState *es, ExecutionState *current = 0) { - std::set tmp; - tmp.insert(es); - update(current, tmp, std::set()); + std::vector tmp; + tmp.push_back(es); + update(current, tmp, std::vector()); } void removeState(ExecutionState *es, ExecutionState *current = 0) { - std::set tmp; - tmp.insert(es); - update(current, std::set(), tmp); + std::vector tmp; + tmp.push_back(es); + update(current, std::vector(), tmp); } enum CoreSearchType { @@ -86,8 +86,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; @@ -100,8 +100,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; @@ -114,8 +114,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; @@ -146,8 +146,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "WeightedRandomSearcher::"; @@ -172,8 +172,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; @@ -195,8 +195,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; @@ -218,8 +218,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; @@ -243,8 +243,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return baseSearcher->empty(); } void printName(llvm::raw_ostream &os) { os << " timeBudget: " << timeBudget @@ -266,8 +266,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; @@ -286,8 +286,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set &addedStates, - const std::set &removedStates); + const std::vector &addedStates, + const std::vector &removedStates); bool empty() { return searchers[0]->empty(); } void printName(llvm::raw_ostream &os) { os << " containing " diff --git a/test/Feature/DeterministicSwitch.c b/test/Feature/DeterministicSwitch.c new file mode 100644 index 00000000..0768576c --- /dev/null +++ b/test/Feature/DeterministicSwitch.c @@ -0,0 +1,41 @@ +// The order cases are generated in LLVM 2.9 is different: tab first then space +// as one can see in assembly.ll, skip this test for older versions +// REQUIRES: not-llvm-2.9 +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=dfs %t.bc >%t.switch.log 2>&1 +// RUN: FileCheck %s -input-file=%t.switch.log -check-prefix=CHECK-DFS +// RUN: rm -rf %t.klee-out +// RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=bfs %t.bc >%t.switch.log 2>&1 +// RUN: FileCheck %s -input-file=%t.switch.log -check-prefix=CHECK-BFS + +#include "klee/klee.h" +#include + +int main(int argc, char **argv) { + char c; + + klee_make_symbolic(&c, sizeof(c), "index"); + + switch (c) { + case ' ': + printf("space\n"); + break; + case '\t': + printf("tab\n"); + break; + default: + printf("default\n"); + break; + } + + // CHECK-DFS: default + // CHECK-DFS: tab + // CHECK-DFS: space + + // CHECK-BFS: space + // CHECK-BFS: tab + // CHECK-BFS: default + + return 0; +} -- cgit 1.4.1 From 91af7cdc0521a155a050976eaa8856f04a576826 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 22 Mar 2016 16:39:49 +0100 Subject: Generate forked states for switch instructions deterministically This patch generates the states based on the order of switch-cases. Before, switch-constraints were randomly assigned to forked states. As generated code might be different between LLVM versions, we use the case values, order them, and iterate in that order over the cases. This way we can also support deterministic execution of older LLVM versions. --- lib/Core/Executor.cpp | 112 +++++++++++++++++++++++++++---------- test/Feature/DeterministicSwitch.c | 13 ++--- 2 files changed, 86 insertions(+), 39 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 49cba67f..709eb3a5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1609,58 +1609,108 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { #endif transferToBasicBlock(si->getSuccessor(index), si->getParent(), state); } else { - std::map > targets; - ref isDefault = ConstantExpr::alloc(1, Expr::Bool); -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); - i != e; ++i) { + // Handle possible different branch targets + + // We have the following assumptions: + // - each case value is mutual exclusive to all other values including the + // default value + // - order of case branches is based on the order of the expressions of + // the scase values, still default is handled last + std::vector bbOrder; + std::map > branchTargets; + + std::map, BasicBlock *> expressionOrder; + + // Iterate through all non-default cases and order them by expressions +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); i != e; + ++i) { ref value = evalConstant(i.getCaseValue()); #else - for (unsigned i=1, cases = si->getNumCases(); igetNumCases(); i < cases; ++i) { ref value = evalConstant(si->getCaseValue(i)); #endif - ref match = EqExpr::create(cond, value); - isDefault = AndExpr::create(isDefault, Expr::createIsZero(match)); + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + BasicBlock *caseSuccessor = i.getCaseSuccessor(); +#else + BasicBlock *caseSuccessor = si->getSuccessor(i); +#endif + expressionOrder.insert(std::make_pair(value, caseSuccessor)); + } + + // Track default branch values + ref defaultValue = ConstantExpr::alloc(1, Expr::Bool); + + // iterate through all non-default cases but in order of the expressions + for (std::map, BasicBlock *>::iterator + it = expressionOrder.begin(), + itE = expressionOrder.end(); + it != itE; ++it) { + ref match = EqExpr::create(cond, it->first); + + // Make sure that the default value does not contain this target's value + defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match)); + + // Check if control flow could take this case bool result; bool success = solver->mayBeTrue(state, match, result); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (result) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - BasicBlock *caseSuccessor = i.getCaseSuccessor(); -#else - BasicBlock *caseSuccessor = si->getSuccessor(i); -#endif - std::map >::iterator it = - targets.insert(std::make_pair(caseSuccessor, - ConstantExpr::alloc(0, Expr::Bool))).first; - - it->second = OrExpr::create(match, it->second); + BasicBlock *caseSuccessor = it->second; + + // Handle the case that a basic block might be the target of multiple + // switch cases. + // Currently we generate an expression containing all switch-case + // values for the same target basic block. We spare us forking too + // many times but we generate more complex condition expressions + // TODO Add option to allow to choose between those behaviors + std::pair >::iterator, bool> res = + branchTargets.insert(std::make_pair( + caseSuccessor, ConstantExpr::alloc(0, Expr::Bool))); + + res.first->second = OrExpr::create(match, res.first->second); + + // Only add basic blocks which have not been target of a branch yet + if (res.second) { + bbOrder.push_back(caseSuccessor); + } } } + + // Check if control could take the default case bool res; - bool success = solver->mayBeTrue(state, isDefault, res); + bool success = solver->mayBeTrue(state, defaultValue, res); assert(success && "FIXME: Unhandled solver failure"); (void) success; - if (res) - targets.insert(std::make_pair(si->getDefaultDest(), isDefault)); - + if (res) { + std::pair >::iterator, bool> ret = + branchTargets.insert( + std::make_pair(si->getDefaultDest(), defaultValue)); + if (ret.second) { + bbOrder.push_back(si->getDefaultDest()); + } + } + + // Fork the current state with each state having one of the possible + // successors of this switch std::vector< ref > conditions; - for (std::map >::iterator it = - targets.begin(), ie = targets.end(); - it != ie; ++it) - conditions.push_back(it->second); - + for (std::vector::iterator it = bbOrder.begin(), + ie = bbOrder.end(); + it != ie; ++it) { + conditions.push_back(branchTargets[*it]); + } std::vector branches; branch(state, conditions, branches); - + std::vector::iterator bit = branches.begin(); - for (std::map >::iterator it = - targets.begin(), ie = targets.end(); + for (std::vector::iterator it = bbOrder.begin(), + ie = bbOrder.end(); it != ie; ++it) { ExecutionState *es = *bit; if (es) - transferToBasicBlock(it->first, bb, *es); + transferToBasicBlock(*it, bb, *es); ++bit; } } diff --git a/test/Feature/DeterministicSwitch.c b/test/Feature/DeterministicSwitch.c index 0768576c..b6c186ff 100644 --- a/test/Feature/DeterministicSwitch.c +++ b/test/Feature/DeterministicSwitch.c @@ -1,6 +1,3 @@ -// The order cases are generated in LLVM 2.9 is different: tab first then space -// as one can see in assembly.ll, skip this test for older versions -// REQUIRES: not-llvm-2.9 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=dfs %t.bc >%t.switch.log 2>&1 @@ -18,23 +15,23 @@ int main(int argc, char **argv) { klee_make_symbolic(&c, sizeof(c), "index"); switch (c) { - case ' ': - printf("space\n"); - break; case '\t': printf("tab\n"); break; + case ' ': + printf("space\n"); + break; default: printf("default\n"); break; } // CHECK-DFS: default - // CHECK-DFS: tab // CHECK-DFS: space + // CHECK-DFS: tab - // CHECK-BFS: space // CHECK-BFS: tab + // CHECK-BFS: space // CHECK-BFS: default return 0; -- cgit 1.4.1