From 27cfe79c1867ece6edf0c4a4bfcbdecf01020774 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Tue, 21 Dec 2021 13:59:30 +0000 Subject: introduce BranchTypes --- lib/Core/Executor.cpp | 50 +++++++++++++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 23 deletions(-) (limited to 'lib/Core/Executor.cpp') 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 > &conditions, - std::vector &result) { +void Executor::branch(ExecutionState &state, + const std::vector> &conditions, + std::vector &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 Executor::maxStaticPctChecks(ExecutionState ¤t, return condition; } -Executor::StatePair -Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { +Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, + bool isInternal, BranchType reason) { Solver::Validity res; std::map< ExecutionState*, std::vector >::iterator it = seedMap.find(¤t); @@ -1164,7 +1165,7 @@ Executor::fork(ExecutionState ¤t, ref 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 branches; - branch(state, conditions, branches); + branch(state, conditions, branches, BranchType::GetVal); std::vector::iterator bit = branches.begin(); for (std::set< ref >::iterator vit = values.begin(), @@ -2196,7 +2197,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref 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 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 branches; - branch(state, conditions, branches); + branch(state, conditions, branches, BranchType::Switch); std::vector::iterator bit = branches.begin(); for (std::vector::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 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 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 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 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 -- cgit 1.4.1