aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp50
-rw-r--r--lib/Core/Executor.h19
-rw-r--r--lib/Core/PTree.cpp3
-rw-r--r--lib/Core/PTree.h3
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp15
5 files changed, 48 insertions, 42 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 &current,
return condition;
}
-Executor::StatePair
-Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
+Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
+ bool isInternal, BranchType reason) {
Solver::Validity res;
std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
seedMap.find(&current);
@@ -1164,7 +1165,7 @@ Executor::fork(ExecutionState &current, 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 &current, 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 &current, 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);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-22 22:27:39 +0000