diff options
-rw-r--r-- | include/klee/ExecutionState.h | 4 | ||||
-rw-r--r-- | include/klee/MergeHandler.h | 110 | ||||
-rw-r--r-- | include/klee/klee.h | 5 | ||||
-rw-r--r-- | lib/Core/CMakeLists.txt | 1 | ||||
-rw-r--r-- | lib/Core/ExecutionState.cpp | 3 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 7 | ||||
-rw-r--r-- | lib/Core/Executor.h | 4 | ||||
-rw-r--r-- | lib/Core/MergeHandler.cpp | 76 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 5 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 41 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 2 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 17 | ||||
-rw-r--r-- | test/Merging/batching_break.c | 42 | ||||
-rw-r--r-- | test/Merging/easy_merge.c | 44 | ||||
-rw-r--r-- | test/Merging/indirect_value.c | 32 | ||||
-rw-r--r-- | test/Merging/loop_merge.c | 38 | ||||
-rw-r--r-- | test/Merging/merge_fail.c | 36 | ||||
-rw-r--r-- | test/Merging/nested_merge.c | 48 | ||||
-rw-r--r-- | test/Merging/split_merge.c | 41 | ||||
-rw-r--r-- | test/Merging/unexpected_close.c | 35 | ||||
-rw-r--r-- | tools/klee/main.cpp | 2 |
21 files changed, 579 insertions, 14 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 78ebddac..6aec61ea 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -13,6 +13,7 @@ #include "klee/Constraints.h" #include "klee/Expr.h" #include "klee/Internal/ADT/TreeStream.h" +#include "klee/MergeHandler.h" // FIXME: We do not want to be exposing these? :( #include "../../lib/Core/AddressSpace.h" @@ -145,6 +146,9 @@ public: void addFnAlias(std::string old_fn, std::string new_fn); void removeFnAlias(std::string fn); + // The objects handling the klee_open_merge calls this state ran through + std::vector<ref<MergeHandler> > openMergeStack; + private: ExecutionState() : ptreeNode(0) {} diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h new file mode 100644 index 00000000..d374e168 --- /dev/null +++ b/include/klee/MergeHandler.h @@ -0,0 +1,110 @@ +//===-- MergeHandler.h --------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +/** + * @file MergeHandler.h + * @brief Implementation of the region based merging + * + * ## Basic usage: + * + * @code{.cpp} + * klee_open_merge(); + * + * code containing branches etc. + * + * klee_close_merge(); + * @endcode + * + * Will lead to all states that forked from the state that executed the + * klee_open_merge() being merged in the klee_close_merge(). This allows for + * fine-grained regions to be specified for merging. + * + * # Implementation Structure + * + * The main part of the new functionality is implemented in the class + * klee::MergeHandler. The Special Function Handler generates an instance of + * this class every time a state runs into a klee_open_merge() call. + * + * This instance is appended to a `std::vector<klee::ref<klee::MergeHandler>>` + * in the ExecutionState that passed the merge open point. This stack is also + * copied during forks. We use a stack instead of a single instance to support + * nested merge regions. + * + * Once a state runs into a `klee_close_merge()`, the Special Function Handler + * notifies the top klee::MergeHandler in the state's stack, pauses the state + * from scheduling, and tries to merge it with all other states that already + * arrived at the same close merge point. This top instance is then popped from + * the stack, resulting in a decrease of the ref count of the + * klee::MergeHandler. + * + * Since the only references to this MergeHandler are in the stacks of + * the ExecutionStates currently in the merging region, once the ref count + * reaches zero, every state which ran into the same `klee_open_merge()` is now + * paused and waiting to be merged. The destructor of the MergeHandler + * then continues the scheduling of the corresponding paused states. +*/ + +#ifndef KLEE_MERGEHANDLER_H +#define KLEE_MERGEHANDLER_H + +#include <vector> +#include <map> +#include <stdint.h> +#include "llvm/Support/CommandLine.h" + +namespace llvm { +class Instruction; +} + +namespace klee { +extern llvm::cl::opt<bool> UseMerge; + +extern llvm::cl::opt<bool> DebugLogMerge; + +class Executor; +class ExecutionState; + +/// @brief Represents one `klee_open_merge()` call. +/// Handles merging of states that branched from it +class MergeHandler { +private: + Executor *executor; + + /// @brief Number of states that are tracked by this MergeHandler, that ran + /// into a relevant klee_close_merge + unsigned closedStateCount; + + /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into + /// them + std::map<llvm::Instruction *, std::vector<ExecutionState *> > + reachedMergeClose; + +public: + + /// @brief Called when a state runs into a 'klee_close_merge()' call + void addClosedState(ExecutionState *es, llvm::Instruction *mp); + + /// @brief True, if any states have run into 'klee_close_merge()' and have + /// not been released yet + bool hasMergedStates(); + + /// @brief Immediately release the merged states that have run into a + /// 'klee_merge_close()' + void releaseStates(); + + /// @brief Required by klee::ref objects + unsigned refCount; + + + MergeHandler(Executor *_executor); + ~MergeHandler(); +}; +} + +#endif /* KLEE_MERGEHANDLER_H */ diff --git a/include/klee/klee.h b/include/klee/klee.h index bd3100b5..644c498e 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -152,6 +152,11 @@ extern "C" { /* Print range for given argument and tagged with name */ void klee_print_range(const char * name, int arg ); + /* Open a merge */ + void klee_open_merge(); + + /* Merge all paths of the state that went through klee_open_merge */ + void klee_close_merge(); #ifdef __cplusplus } #endif diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 86ce3cfc..4b14df36 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -8,6 +8,7 @@ #===------------------------------------------------------------------------===# klee_add_component(kleeCore AddressSpace.cpp + MergeHandler.cpp CallPathManager.cpp Context.cpp CoreStats.cpp diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 20b1a162..522bdd15 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -116,7 +116,8 @@ ExecutionState::ExecutionState(const ExecutionState& state): coveredLines(state.coveredLines), ptreeNode(state.ptreeNode), symbolics(state.symbolics), - arrayNames(state.arrayNames) + arrayNames(state.arrayNames), + openMergeStack(state.openMergeStack) { for (unsigned int i=0; i<symbolics.size(); i++) symbolics[i].first->refCount++; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e79d6a2c..be92b16a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2456,7 +2456,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { void Executor::updateStates(ExecutionState *current) { if (searcher) { searcher->update(current, addedStates, removedStates); - searcher->update(0, continuedStates, pausedStates); + searcher->update(nullptr, continuedStates, pausedStates); pausedStates.clear(); continuedStates.clear(); } @@ -2745,7 +2745,7 @@ std::string Executor::getAddressInfo(ExecutionState &state, } void Executor::pauseState(ExecutionState &state){ - std::vector<ExecutionState *>::iterator it = std::find(continuedStates.begin(), continuedStates.end(), &state); + auto it = std::find(continuedStates.begin(), continuedStates.end(), &state); // If the state was to be continued, but now gets paused again if (it != continuedStates.end()){ // ...just don't continue it @@ -2757,7 +2757,7 @@ void Executor::pauseState(ExecutionState &state){ } void Executor::continueState(ExecutionState &state){ - std::vector<ExecutionState *>::iterator it = std::find(pausedStates.begin(), pausedStates.end(), &state); + auto it = std::find(pausedStates.begin(), pausedStates.end(), &state); // If the state was to be paused, but now gets continued again if (it != pausedStates.end()){ // ...don't pause it @@ -2768,7 +2768,6 @@ void Executor::continueState(ExecutionState &state){ } } - void Executor::terminateState(ExecutionState &state) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c6f01179..71b1f5f7 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -69,6 +69,7 @@ namespace klee { class StatsTracker; class TimingSolver; class TreeStreamWriter; + class MergeHandler; template<class T> class ref; @@ -78,13 +79,12 @@ namespace klee { /// removedStates, and haltExecution, among others. class Executor : public Interpreter { - friend class BumpMergingSearcher; - friend class MergingSearcher; friend class RandomPathSearcher; friend class OwningSearcher; friend class WeightedRandomSearcher; friend class SpecialFunctionHandler; friend class StatsTracker; + friend class MergeHandler; public: class Timer { diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp new file mode 100644 index 00000000..ad8ffd62 --- /dev/null +++ b/lib/Core/MergeHandler.cpp @@ -0,0 +1,76 @@ +//===-- MergeHandler.cpp --------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/MergeHandler.h" + +#include "CoreStats.h" +#include "Executor.h" +#include "klee/ExecutionState.h" + +namespace klee { +llvm::cl::opt<bool> + UseMerge("use-merge", + llvm::cl::init(false), + llvm::cl::desc("Enable support for klee_open_merge() and klee_close_merge() (experimental)")); + +llvm::cl::opt<bool> + DebugLogMerge("debug-log-merge", + llvm::cl::init(false), + llvm::cl::desc("Enhanced verbosity for region based merge operations")); + +void MergeHandler::addClosedState(ExecutionState *es, + llvm::Instruction *mp) { + auto closePoint = reachedMergeClose.find(mp); + + // If no other state has yet encountered this klee_close_merge instruction, + // add a new element to the map + if (closePoint == reachedMergeClose.end()) { + reachedMergeClose[mp].push_back(es); + executor->pauseState(*es); + } else { + // Otherwise try to merge with any state in the map element for this + // instruction + auto &cpv = closePoint->second; + bool mergedSuccessful = false; + + for (auto& mState: cpv) { + if (mState->merge(*es)) { + executor->terminateState(*es); + mergedSuccessful = true; + break; + } + } + if (!mergedSuccessful) { + cpv.push_back(es); + executor->pauseState(*es); + } + } +} + +void MergeHandler::releaseStates() { + for (auto& curMergeGroup: reachedMergeClose) { + for (auto curState: curMergeGroup.second) { + executor->continueState(*curState); + } + } + reachedMergeClose.clear(); +} + +bool MergeHandler::hasMergedStates() { + return (!reachedMergeClose.empty()); +} + +MergeHandler::MergeHandler(Executor *_executor) + : executor(_executor), refCount(0) { +} + +MergeHandler::~MergeHandler() { + releaseStates(); +} +} diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index d5d35e8f..05ebe6a6 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -42,11 +42,6 @@ using namespace klee; using namespace llvm; -namespace { - cl::opt<bool> - DebugLogMerge("debug-log-merge"); -} - namespace klee { extern RNG theRNG; } diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 1c2b245c..a8d6edec 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -10,6 +10,7 @@ #include "Memory.h" #include "SpecialFunctionHandler.h" #include "TimingSolver.h" +#include "klee/MergeHandler.h" #include "klee/ExecutionState.h" @@ -28,6 +29,7 @@ #include "llvm/IR/DataLayout.h" #include <errno.h> +#include <sstream> using namespace llvm; using namespace klee; @@ -92,6 +94,8 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), add("klee_mark_global", handleMarkGlobal, false), + add("klee_open_merge", handleOpenMerge, false), + add("klee_close_merge", handleCloseMerge, false), add("klee_prefer_cex", handlePreferCex, false), add("klee_posix_prefer_cex", handlePosixPreferCex, false), add("klee_print_expr", handlePrintExpr, false), @@ -324,6 +328,43 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, readStringAtAddress(state, arguments[3]).c_str()); } +void SpecialFunctionHandler::handleOpenMerge(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (!UseMerge) { + klee_warning_once(0, "klee_open_merge ignored, use '-use-merge'"); + return; + } + + state.openMergeStack.push_back( + ref<MergeHandler>(new MergeHandler(&executor))); + + if (DebugLogMerge) + llvm::errs() << "open merge: " << &state << "\n"; +} + +void SpecialFunctionHandler::handleCloseMerge(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (!UseMerge) { + klee_warning_once(0, "klee_close_merge ignored, use '-use-merge'"); + return; + } + Instruction *i = target->inst; + + if (DebugLogMerge) + llvm::errs() << "close merge: " << &state << " at " << i << '\n'; + + if (state.openMergeStack.empty()) { + std::ostringstream warning; + warning << &state << " ran into a close at " << i << " without a preceding open\n"; + klee_warning(warning.str().c_str()); + } else { + state.openMergeStack.back()->addClosedState(&state, i); + state.openMergeStack.pop_back(); + } +} + 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 394b649a..7e58018f 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -116,6 +116,8 @@ namespace klee { HANDLER(handleMakeSymbolic); HANDLER(handleMalloc); HANDLER(handleMarkGlobal); + HANDLER(handleOpenMerge); + HANDLER(handleCloseMerge); HANDLER(handleNew); HANDLER(handleNewArray); HANDLER(handlePreferCex); diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 6158f722..f0b2f85a 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -13,6 +13,8 @@ #include "Executor.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/CommandLine.h" + #include "llvm/Support/CommandLine.h" using namespace llvm; @@ -58,8 +60,13 @@ namespace { void klee::initializeSearchOptions() { // default values if (CoreSearch.empty()) { - CoreSearch.push_back(Searcher::RandomPath); - CoreSearch.push_back(Searcher::NURS_CovNew); + if (UseMerge){ + CoreSearch.push_back(Searcher::NURS_CovNew); + klee_warning("--use-merge enabled. Using NURS_CovNew as default searcher."); + } else { + CoreSearch.push_back(Searcher::RandomPath); + CoreSearch.push_back(Searcher::NURS_CovNew); + } } } @@ -104,6 +111,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) { searcher = new InterleavedSearcher(s); } + if (UseMerge) { + 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"); + } + } + if (UseBatchingSearch) { searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions); } diff --git a/test/Merging/batching_break.c b/test/Merging/batching_break.c new file mode 100644 index 00000000..67570734 --- /dev/null +++ b/test/Merging/batching_break.c @@ -0,0 +1,42 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// CHECK: close merge: +// CHECK: KLEE: done: generated tests = 3{{$}} + +#include <klee/klee.h> + +int main(int argc, char** args){ + + int x; + int p; + int i; + + klee_make_symbolic(&x, sizeof(x), "x"); + x = x % 20; + + klee_open_merge(); + for (i = 0; i < x; ++i){ + if (x % 3 == 0){ + klee_close_merge(); + if (x > 10){ + return 1; + } else { + return 2; + } + } + } + klee_close_merge(); + + klee_open_merge(); + if (x > 10){ + p = 1; + } else { + p = 2; + } + klee_close_merge(); + return p; + +} diff --git a/test/Merging/easy_merge.c b/test/Merging/easy_merge.c new file mode 100644 index 00000000..b9c634dc --- /dev/null +++ b/test/Merging/easy_merge.c @@ -0,0 +1,44 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 2{{$}} +#include <klee/klee.h> + +int main(int argc, char** args){ + + int x; + int a; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&a, sizeof(a), "a"); + + if (a == 0){ + klee_open_merge(); + + if (x == 1) { + foo = 5; + } else if (x == 2) { + foo = 6; + } else { + foo = 7; + } + + klee_close_merge(); + } + + return foo; +} diff --git a/test/Merging/indirect_value.c b/test/Merging/indirect_value.c new file mode 100644 index 00000000..ffea14ec --- /dev/null +++ b/test/Merging/indirect_value.c @@ -0,0 +1,32 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s + +// CHECK: generated tests = 2{{$}} +#include <stdlib.h> +#include <stdio.h> + +#include <klee/klee.h> + +int main(int argc, char** argv) { + + int sym = klee_int("sym"); + int* heap_int = calloc(1, sizeof(*heap_int)); + + klee_open_merge(); + + if(sym != 0) { + *heap_int = 1; + } + + klee_close_merge(); + + klee_print_expr("*heap_int: ", *heap_int); + if(*heap_int != 0) { + printf("true\n"); + } else { + printf("false\n"); + } + + return 0; +} diff --git a/test/Merging/loop_merge.c b/test/Merging/loop_merge.c new file mode 100644 index 00000000..4a38d98f --- /dev/null +++ b/test/Merging/loop_merge.c @@ -0,0 +1,38 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// There will be 20 'close merge' statements. Only checking a few, the generated +// test count will confirm that the merge was closed correctly +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 2{{$}} + +#include <klee/klee.h> + +int main(int argc, char** args){ + + int x; + int i; + + klee_make_symbolic(&x, sizeof(x), "x"); + x = x % 20; + + klee_open_merge(); + for (i = 0; i < x; ++i){ + if (x % 3 == 0){ + klee_close_merge(); + return 1; + } + } + klee_close_merge(); + + return 0; +} diff --git a/test/Merging/merge_fail.c b/test/Merging/merge_fail.c new file mode 100644 index 00000000..5cd9f782 --- /dev/null +++ b/test/Merging/merge_fail.c @@ -0,0 +1,36 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// CHECK: generated tests = 2{{$}} + +// This test will not merge because we cannot merge states when they allocated memory. + +#include <klee/klee.h> + +int main(int argc, char **args) { + + int* arr = 0; + int a = 0; + + klee_make_symbolic(&a, sizeof(a), "a"); + + klee_open_merge(); + if (a == 0) { + arr = (int*) malloc(7 * sizeof(int)); + arr[0] = 7; + } else { + arr = (int*) malloc(8 * sizeof(int)); + arr[0] = 8; + } + klee_close_merge(); + a = arr[0]; + free(arr); + + return a; +} diff --git a/test/Merging/nested_merge.c b/test/Merging/nested_merge.c new file mode 100644 index 00000000..027c72d3 --- /dev/null +++ b/test/Merging/nested_merge.c @@ -0,0 +1,48 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// 5 close merges +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 1{{$}} + +#include <klee/klee.h> + +int main(int argc, char **args) { + + int x; + int a; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&a, sizeof(a), "a"); + + klee_open_merge(); + if (a == 0) { + klee_open_merge(); + + if (x == 1) { + foo = 5; + } else if (x == 2) { + foo = 6; + } else { + foo = 7; + } + + klee_close_merge(); + } + klee_close_merge(); + + return foo; +} diff --git a/test/Merging/split_merge.c b/test/Merging/split_merge.c new file mode 100644 index 00000000..bca8a5a2 --- /dev/null +++ b/test/Merging/split_merge.c @@ -0,0 +1,41 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + + +// CHECK: open merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 2{{$}} + +#include <klee/klee.h> + +int main(int argc, char** args){ + + int x; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + + klee_open_merge(); + + if (x == 1){ + foo = 5; + } else if (x == 2){ + klee_close_merge(); + return 6; + } else { + foo = 7; + } + + klee_close_merge(); + + return foo; +} diff --git a/test/Merging/unexpected_close.c b/test/Merging/unexpected_close.c new file mode 100644 index 00000000..b4994de1 --- /dev/null +++ b/test/Merging/unexpected_close.c @@ -0,0 +1,35 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --search=nurs:covnew --max-time=2 %t.bc + +// CHECK: ran into a close at +// CHECK: generated tests = 2{{$}} + +#include <klee/klee.h> + +int main(int argc, char **args) { + + int x; + int a; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&a, sizeof(a), "a"); + + if (a == 0) { + klee_open_merge(); + + if (x == 1) { + foo = 5; + } else if (x == 2) { + foo = 6; + } else { + foo = 7; + } + + klee_close_merge(); + } + klee_close_merge(); + + return foo; +} diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index f1def38c..2b2fe3eb 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -718,6 +718,8 @@ static const char *modelledExternals[] = { "klee_is_symbolic", "klee_make_symbolic", "klee_mark_global", + "klee_open_merge", + "klee_close_merge", "klee_prefer_cex", "klee_posix_prefer_cex", "klee_print_expr", |