diff options
| -rw-r--r-- | include/klee/Core/BranchTypes.h | 58 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 50 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 19 | ||||
| -rw-r--r-- | lib/Core/PTree.cpp | 3 | ||||
| -rw-r--r-- | lib/Core/PTree.h | 3 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 15 | ||||
| -rw-r--r-- | unittests/Searcher/SearcherTest.cpp | 10 |
7 files changed, 111 insertions, 47 deletions
diff --git a/include/klee/Core/BranchTypes.h b/include/klee/Core/BranchTypes.h new file mode 100644 index 00000000..5c3e5f32 --- /dev/null +++ b/include/klee/Core/BranchTypes.h @@ -0,0 +1,58 @@ +//===-- BranchTypes.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_BRANCHTYPES_H +#define KLEE_BRANCHTYPES_H + +#include <cstdint> + +/// \cond DO_NOT_DOCUMENT +#define BRANCH_TYPES \ + BTYPE(NONE, 0U) \ + BTYPE(ConditionalBranch, 1U) \ + BTYPE(IndirectBranch, 2U) \ + BTYPE(Switch, 3U) \ + BTYPE(Call, 4U) \ + BTYPE(MemOp, 5U) \ + BTYPE(ResolvePointer, 6U) \ + BTYPE(Alloc, 7U) \ + BTYPE(Realloc, 8U) \ + BTYPE(Free, 9U) \ + BTYPE(GetVal, 10U) \ + MARK(END, 10U) +/// \endcond + +/** @enum BranchType + * @brief Reason an ExecutionState forked + * + * | Value | Description | + * |---------------------------------|----------------------------------------------------------------------------------------------------| + * | `BranchType::NONE` | default value (no branch) | + * | `BranchType::ConditionalBranch` | branch caused by `br` instruction with symbolic condition | + * | `BranchType::IndirectBranch` | branch caused by `indirectbr` instruction with symbolic address | + * | `BranchType::Switch` | branch caused by `switch` instruction with symbolic value | + * | `BranchType::Call` | branch caused by `call` with symbolic function pointer | + * | `BranchType::MemOp` | branch caused by memory operation with symbolic address (e.g. multiple resolutions, out-of-bounds) | + * | `BranchType::ResolvePointer` | branch caused by symbolic pointer | + * | `BranchType::Alloc` | branch caused by symbolic `alloc`ation size | + * | `BranchType::Realloc` | branch caused by symbolic `realloc`ation size | + * | `BranchType::Free` | branch caused by `free`ing symbolic pointer | + * | `BranchType::GetVal` | branch caused by user-invoked concretization while seeding | + */ +enum class BranchType : std::uint8_t { +/// \cond DO_NOT_DOCUMENT +#define BTYPE(N,I) N = (I), +#define MARK(N,I) N = (I), + BRANCH_TYPES +#undef BTYPE +#undef MARK +/// \endcond +}; + +#endif \ No newline at end of file diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fdb8e3b8..c50e4520 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -868,9 +868,10 @@ bool Executor::branchingPermitted(const ExecutionState &state) const { return true; } -void Executor::branch(ExecutionState &state, - const std::vector< ref<Expr> > &conditions, - std::vector<ExecutionState*> &result) { +void Executor::branch(ExecutionState &state, + const std::vector<ref<Expr>> &conditions, + std::vector<ExecutionState *> &result, + BranchType reason) { TimerStatIncrementer timer(stats::forkTime); unsigned N = conditions.size(); assert(N); @@ -894,7 +895,7 @@ void Executor::branch(ExecutionState &state, ExecutionState *ns = es->branch(); addedStates.push_back(ns); result.push_back(ns); - processTree->attach(es->ptreeNode, ns, es); + processTree->attach(es->ptreeNode, ns, es, reason); } } @@ -1006,8 +1007,8 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState ¤t, return condition; } -Executor::StatePair -Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { +Executor::StatePair Executor::fork(ExecutionState ¤t, ref<Expr> condition, + bool isInternal, BranchType reason) { Solver::Validity res; std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = seedMap.find(¤t); @@ -1164,7 +1165,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { } } - processTree->attach(current.ptreeNode, falseState, trueState); + processTree->attach(current.ptreeNode, falseState, trueState, reason); if (pathWriter) { // Need to update the pathOS.id field of falseState, otherwise the same id @@ -1351,7 +1352,7 @@ void Executor::executeGetValue(ExecutionState &state, conditions.push_back(EqExpr::create(e, *vit)); std::vector<ExecutionState*> branches; - branch(state, conditions, branches); + branch(state, conditions, branches, BranchType::GetVal); std::vector<ExecutionState*>::iterator bit = branches.begin(); for (std::set< ref<Expr> >::iterator vit = values.begin(), @@ -2196,7 +2197,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<Expr> cond = eval(ki, 0, state).value; cond = optimizer.optimizeExpr(cond, false); - Executor::StatePair branches = fork(state, cond, false); + Executor::StatePair branches = fork(state, cond, false, BranchType::ConditionalBranch); // NOTE: There is a hidden dependency here, markBranchVisited // requires that we still be in the context of the branch @@ -2269,7 +2270,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // fork states std::vector<ExecutionState *> branches; - branch(state, expressions, branches); + branch(state, expressions, branches, BranchType::IndirectBranch); // terminate error state if (result) { @@ -2395,7 +2396,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { conditions.push_back(branchTargets[*it]); } std::vector<ExecutionState*> branches; - branch(state, conditions, branches); + branch(state, conditions, branches, BranchType::Switch); std::vector<ExecutionState*>::iterator bit = branches.begin(); for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(), @@ -2503,7 +2504,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { solver->getValue(free->constraints, v, value, free->queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; - StatePair res = fork(*free, EqExpr::create(v, value), true); + StatePair res = fork(*free, EqExpr::create(v, value), true, BranchType::Call); if (res.first) { uint64_t addr = value->getZExtValue(); auto it = legalFunctions.find(addr); @@ -4077,8 +4078,9 @@ void Executor::executeAlloc(ExecutionState &state, example = tmp; } - StatePair fixedSize = fork(state, EqExpr::create(example, size), true); - + StatePair fixedSize = + fork(state, EqExpr::create(example, size), true, BranchType::Alloc); + if (fixedSize.second) { // Check for exactly two values ref<ConstantExpr> tmp; @@ -4098,10 +4100,10 @@ void Executor::executeAlloc(ExecutionState &state, } else { // See if a *really* big value is possible. If so assume // malloc will fail for it, so lets fork and return 0. - StatePair hugeSize = - fork(*fixedSize.second, - UltExpr::create(ConstantExpr::alloc(1U<<31, W), size), - true); + StatePair hugeSize = + fork(*fixedSize.second, + UltExpr::create(ConstantExpr::alloc(1U << 31, W), size), true, + BranchType::Alloc); if (hugeSize.first) { klee_message("NOTE: found huge malloc, returning 0"); bindLocal(target, *hugeSize.first, @@ -4131,7 +4133,8 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address, KInstruction *target) { address = optimizer.optimizeExpr(address, true); - StatePair zeroPointer = fork(state, Expr::createIsZero(address), true); + StatePair zeroPointer = + fork(state, Expr::createIsZero(address), true, BranchType::Free); if (zeroPointer.first) { if (target) bindLocal(target, *zeroPointer.first, Expr::createPointer(0)); @@ -4173,9 +4176,10 @@ void Executor::resolveExact(ExecutionState &state, for (ResolutionList::iterator it = rl.begin(), ie = rl.end(); it != ie; ++it) { ref<Expr> inBounds = EqExpr::create(p, it->first->getBaseExpr()); - - StatePair branches = fork(*unbound, inBounds, true); - + + StatePair branches = + fork(*unbound, inBounds, true, BranchType::ResolvePointer); + if (branches.first) results.push_back(std::make_pair(*it, branches.first)); @@ -4281,7 +4285,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, const ObjectState *os = i->second; ref<Expr> inBounds = mo->getBoundsCheckPointer(address, bytes); - StatePair branches = fork(*unbound, inBounds, true); + StatePair branches = fork(*unbound, inBounds, true, BranchType::MemOp); ExecutionState *bound = branches.first; // bound can be 0 on failure or overlapped diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index e9763547..7da4f63c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -19,6 +19,7 @@ #include "UserSearcher.h" #include "klee/ADT/RNG.h" +#include "klee/Core/BranchTypes.h" #include "klee/Core/Interpreter.h" #include "klee/Core/TerminationTypes.h" #include "klee/Expr/ArrayCache.h" @@ -324,16 +325,16 @@ private: /// Create a new state where each input condition has been added as /// a constraint and return the results. The input state is included - /// as one of the results. Note that the output vector may included + /// as one of the results. Note that the output vector may include /// NULL pointers for states which were unable to be created. - void branch(ExecutionState &state, - const std::vector< ref<Expr> > &conditions, - std::vector<ExecutionState*> &result); - - // Fork current and return states in which condition holds / does - // not hold, respectively. One of the states is necessarily the - // current state, and one of the states may be null. - StatePair fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal); + void branch(ExecutionState &state, const std::vector<ref<Expr>> &conditions, + std::vector<ExecutionState *> &result, BranchType reason); + + /// Fork current and return states in which condition holds / does + /// not hold, respectively. One of the states is necessarily the + /// current state, and one of the states may be null. + StatePair fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal, + BranchType reason); // If the MaxStatic*Pct limits have been reached, concretize the condition and // return it. Otherwise, return the unmodified condition. diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index af5dbc36..6c17e296 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -36,7 +36,8 @@ PTree::PTree(ExecutionState *initialState) initialState->ptreeNode = root.getPointer(); } -void PTree::attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState) { +void PTree::attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) { assert(node && !node->left.getPointer() && !node->right.getPointer()); assert(node == rightState->ptreeNode && "Attach assumes the right state is the current state"); diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 3d87611d..dbee70dd 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -10,6 +10,7 @@ #ifndef KLEE_PTREE_H #define KLEE_PTREE_H +#include "klee/Core/BranchTypes.h" #include "klee/Expr/Expr.h" #include "klee/Support/ErrorHandling.h" #include "llvm/ADT/PointerIntPair.h" @@ -48,7 +49,7 @@ namespace klee { ~PTree() = default; void attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState); + ExecutionState *rightState, BranchType reason); void remove(PTreeNode *node); void dump(llvm::raw_ostream &os); std::uint8_t getNextId() { diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index ab2f07b1..e2ff9cb2 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -715,18 +715,17 @@ void SpecialFunctionHandler::handleRealloc(ExecutionState &state, ref<Expr> address = arguments[0]; ref<Expr> size = arguments[1]; - Executor::StatePair zeroSize = executor.fork(state, - Expr::createIsZero(size), - true); - + Executor::StatePair zeroSize = + executor.fork(state, Expr::createIsZero(size), true, BranchType::Realloc); + if (zeroSize.first) { // size == 0 executor.executeFree(*zeroSize.first, address, target); } if (zeroSize.second) { // size != 0 - Executor::StatePair zeroPointer = executor.fork(*zeroSize.second, - Expr::createIsZero(address), - true); - + Executor::StatePair zeroPointer = + executor.fork(*zeroSize.second, Expr::createIsZero(address), true, + BranchType::Realloc); + if (zeroPointer.first) { // address == 0 executor.executeAlloc(*zeroPointer.first, size, false, target); } diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp index eff5a8af..0a7c8797 100644 --- a/unittests/Searcher/SearcherTest.cpp +++ b/unittests/Searcher/SearcherTest.cpp @@ -37,7 +37,7 @@ TEST(SearcherTest, RandomPath) { // Two states ExecutionState es1(es); - processTree.attach(es.ptreeNode, &es1, &es); + processTree.attach(es.ptreeNode, &es1, &es, BranchType::NONE); rp.update(&es, {&es1}, {}); // Random path seed dependant @@ -68,7 +68,7 @@ TEST(SearcherTest, TwoRandomPath) { root.ptreeNode = processTree.root.getPointer(); ExecutionState es(root); - processTree.attach(root.ptreeNode, &es, &root); + processTree.attach(root.ptreeNode, &es, &root, BranchType::NONE); RNG rng, rng1; RandomPathSearcher rp(processTree, rng); @@ -83,7 +83,7 @@ TEST(SearcherTest, TwoRandomPath) { // Two states ExecutionState es1(es); - processTree.attach(es.ptreeNode, &es1, &es); + processTree.attach(es.ptreeNode, &es1, &es, BranchType::NONE); rp.update(&es, {}, {}); rp1.update(nullptr, {&es1}, {}); @@ -127,7 +127,7 @@ TEST(SearcherTest, TwoRandomPathDot) { rootPNode = root.ptreeNode; ExecutionState es(root); - processTree.attach(root.ptreeNode, &es, &root); + processTree.attach(root.ptreeNode, &es, &root, BranchType::NONE); rightLeafPNode = root.ptreeNode; esParentPNode = es.ptreeNode; @@ -138,7 +138,7 @@ TEST(SearcherTest, TwoRandomPathDot) { rp.update(nullptr, {&es}, {}); ExecutionState es1(es); - processTree.attach(es.ptreeNode, &es1, &es); + processTree.attach(es.ptreeNode, &es1, &es, BranchType::NONE); esLeafPNode = es.ptreeNode; es1LeafPNode = es1.ptreeNode; |