diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 50 |
1 files changed, 27 insertions, 23 deletions
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 |