Skip to content

Various refactorings (round #4) #110

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
vitalych merged 6 commits into from
Jan 4, 2026
Merged

Various refactorings (round #4) #110

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cdf5cbe
klee,s2e: use ExecutionStatePtr in terminateState
vitalych Jan 2, 2026
e558c72
klee,s2e: moved fork implementation to s2e executor
vitalych Jan 3, 2026
852bb08
s2e: removed unused m_forkProcTerminateCurrentState
vitalych Jan 3, 2026
774a33c
klee: removed default param value from fork()
vitalych Jan 3, 2026
63641e5
klee,s2e: removed duplicated fork logic
vitalych Jan 3, 2026
2a951ec
libs2ecore: support unconditional fork in notifyFork
vitalych Jan 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 6 additions & 12 deletions klee/include/klee/Executor.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,12 +125,6 @@ class Executor {
void executeMemoryOperation(ExecutionState &state, bool isWrite, ref<Expr> address,
ref<Expr> value /* undef if read */, KInstruction *target /* undef if write */);

/// When the fork is complete and state properly updated,
/// notify the S2EExecutor, so that it can generate an onFork event.
/// Sending notification after the fork completed
/// allows plugins to kill states and exit to the CPU loop safely.
virtual void notifyFork(ExecutionState &originalState, ref<Expr> &condition, Executor::StatePair &targets) = 0;

const Cell &eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const;

typedef void (*FunctionHandler)(Executor *executor, ExecutionState *state, KInstruction *target,
Expand All @@ -150,17 +144,17 @@ class Executor {
// keepConditionTrueInCurrentState makes sure original state will have condition equal true.
// This is useful when forking one state with several different values.
// NOTE: In concolic mode it will recompute initial values for current state, do not use it for seed state.
virtual StatePair fork(ExecutionState &current, const ref<Expr> &condition,
bool keepConditionTrueInCurrentState = false);

// Unconditional fork
virtual StatePair fork(ExecutionState &current);
virtual StatePair fork(ExecutionState &current, const ref<Expr> &condition, bool keepConditionTrueInCurrentState,
std::function<void(ExecutionStatePtr, const StatePair &)> onBeforeNotify) = 0;

// remove state from queue and delete
virtual void terminateState(ExecutionState &state);
virtual void terminateState(ExecutionStatePtr state);

virtual const llvm::Module *setModule(llvm::Module *module);

static void reexecuteCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp);
static void skipCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp);

/*** State accessor methods ***/
size_t getStatesCount() const {
return m_states.size();
Expand Down
187 changes: 26 additions & 161 deletions klee/lib/Core/Executor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,124 +290,6 @@ void Executor::initializeGlobals(ExecutionState &state) {
}
}

Executor::StatePair Executor::fork(ExecutionState &current, const ref<Expr> &condition_,
bool keepConditionTrueInCurrentState) {
auto condition = current.simplifyExpr(condition_);

// If we are passed a constant, no need to do anything
if (auto ce = dyn_cast<ConstantExpr>(condition)) {
if (ce->isTrue()) {
return StatePair(&current, nullptr);
} else {
return StatePair(nullptr, &current);
}
}

// Evaluate the expression using the current variable assignment
ref<Expr> evalResult = current.concolics()->evaluate(condition);
ConstantExpr *ce = dyn_cast<ConstantExpr>(evalResult);
check(ce, "Could not evaluate the expression to a constant.");
bool conditionIsTrue = ce->isTrue();

if (current.forkDisabled) {
if (conditionIsTrue) {
if (!current.addConstraint(condition)) {
abort();
}
return StatePair(&current, nullptr);
} else {
if (!current.addConstraint(Expr::createIsZero(condition))) {
abort();
}
return StatePair(nullptr, &current);
}
}

if (keepConditionTrueInCurrentState && !conditionIsTrue) {
// Recompute concrete values to keep condition true in current state

// Build constraints where condition must be true
ConstraintManager tmpConstraints = current.constraints();
tmpConstraints.addConstraint(condition);

if (!current.solve(tmpConstraints, *(current.concolics()))) {
// Condition is always false in the current state
return StatePair(nullptr, &current);
}

conditionIsTrue = true;
}

// Build constraints for branched state
ConstraintManager tmpConstraints = current.constraints();
if (conditionIsTrue) {
tmpConstraints.addConstraint(Expr::createIsZero(condition));
} else {
tmpConstraints.addConstraint(condition);
}

AssignmentPtr concolics = Assignment::create(true);
if (!current.solve(tmpConstraints, *concolics)) {
if (conditionIsTrue) {
return StatePair(&current, nullptr);
} else {
return StatePair(nullptr, &current);
}
}

// Branch
auto branchedState = current.clone();
m_addedStates.insert(branchedState);

*klee::stats::forks += 1;

// Update concrete values for the branched state
branchedState->setConcolics(concolics);

// Add constraint to both states
if (conditionIsTrue) {
if (!current.addConstraint(condition)) {
abort();
}
if (!branchedState->addConstraint(Expr::createIsZero(condition))) {
abort();
}
} else {
if (!current.addConstraint(Expr::createIsZero(condition))) {
abort();
}
if (!branchedState->addConstraint(condition)) {
abort();
}
}

// Classify states
ExecutionStatePtr trueState, falseState;
if (conditionIsTrue) {
trueState = &current;
falseState = branchedState;
} else {
falseState = &current;
trueState = branchedState;
}

return StatePair(trueState, falseState);
}

Executor::StatePair Executor::fork(ExecutionState &current) {
if (current.forkDisabled) {
return StatePair(&current, nullptr);
}

auto clonedState = current.clone();
m_addedStates.insert(clonedState);

// Deep copy concolics().
clonedState->setConcolics(Assignment::create(current.concolics()));

return StatePair(&current, clonedState);
}

const Cell &Executor::eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const {
assert(index < ki->inst->getNumOperands());
int vnumber = ki->operands[index];
Expand Down Expand Up @@ -702,6 +584,17 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
}
}

void Executor::reexecuteCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp) {
assert(sp.first == state);
if (sp.second) {
sp.second->llvm.pc = sp.second->llvm.prevPC;
}
}

void Executor::skipCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp) {
// This is a noop for llvm.
}

void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
*klee::stats::instructions += 1;
auto &llvmState = state.llvm;
Expand Down Expand Up @@ -771,16 +664,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
// FIXME: Find a way that we don't have this hidden dependency.
assert(bi->getCondition() == bi->getOperand(0) && "Wrong operand index!");
ref<Expr> cond = eval(ki, 0, llvmState).value;
Executor::StatePair branches = fork(state, cond);

if (branches.first) {
branches.first->llvm.transferToBasicBlock(bi->getSuccessor(0), bi->getParent());
}
if (branches.second) {
branches.second->llvm.transferToBasicBlock(bi->getSuccessor(1), bi->getParent());
}

notifyFork(state, cond, branches);
fork(state, cond, false, [&](ExecutionStatePtr state, const StatePair &sp) {
if (sp.first) {
sp.first->llvm.transferToBasicBlock(bi->getSuccessor(0), bi->getParent());
}
if (sp.second) {
sp.second->llvm.transferToBasicBlock(bi->getSuccessor(1), bi->getParent());
}
});
}
break;
}
Expand All @@ -792,12 +683,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {

klee::ref<klee::Expr> concreteCond = state.concolics()->evaluate(cond);
klee::ref<klee::Expr> condition = EqExpr::create(concreteCond, cond);
StatePair sp = fork(state, condition);
assert(sp.first == &state);
if (sp.second) {
sp.second->llvm.pc = sp.second->llvm.prevPC;
}
notifyFork(state, condition, sp);
StatePair sp = fork(state, condition, false, reexecuteCurrentInstructionInForkedState);

cond = concreteCond;

if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
Expand Down Expand Up @@ -1557,15 +1444,15 @@ void Executor::updateStates(ExecutionStatePtr current) {
m_removedStates.clear();
}

void Executor::terminateState(ExecutionState &state) {
void Executor::terminateState(ExecutionStatePtr state) {
*klee::stats::completedPaths += 1;

StateSet::iterator it = m_addedStates.find(&state);
StateSet::iterator it = m_addedStates.find(state);
if (it == m_addedStates.end()) {
// XXX: the following line makes delayed state termination impossible
// llvmState.pc = llvmState.prevPC;

m_removedStates.insert(&state);
m_removedStates.insert(state);
} else {
// never reached searcher, just delete immediately
m_addedStates.erase(it);
Expand Down Expand Up @@ -1600,21 +1487,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,

klee::ref<klee::Expr> condition = EqExpr::create(concreteArg, arg);

StatePair sp = fork(state, condition);

assert(sp.first == &state);

if (sp.second) {
sp.second->llvm.pc = sp.second->llvm.prevPC;
}

KInstIterator savedPc = sp.first->llvm.pc;
sp.first->llvm.pc = sp.first->llvm.prevPC;

// This might throw an exception
notifyFork(state, condition, sp);

sp.first->llvm.pc = savedPc;
fork(state, condition, false, reexecuteCurrentInstructionInForkedState);

cas.push_back(concreteArg->getZExtValue());
}
Expand Down Expand Up @@ -1749,15 +1622,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, bool isWrite, ref<E

assert(state.concolics()->evaluate(condition)->isTrue());

StatePair branches = fork(state, condition);

assert(branches.first == &state);
if (branches.second) {
// The forked state will have to re-execute the memory op
branches.second->llvm.pc = branches.second->llvm.prevPC;
}

notifyFork(state, condition, branches);
fork(state, condition, false, reexecuteCurrentInstructionInForkedState);

if (isa<ConstantExpr>(address)) {
auto ce = dyn_cast<ConstantExpr>(address)->getZExtValue();
Expand Down
2 changes: 1 addition & 1 deletion libs2ecore/include/s2e/S2E.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -295,7 +295,7 @@ template <class PluginClass> PluginClass *S2E::getPlugin() const {
<< ": " << message << "\n"; \
print_stacktrace(s2e_warning_print, "state assertion failed"); \
assert(currentState != nullptr && "state assertion failed, no current state to terminate"); \
g_s2e->getExecutor()->terminateState(*currentState, "state assertion failed"); \
g_s2e->getExecutor()->terminateState(currentState, "state assertion failed"); \
assert(false && "Unreachable code - current state must be terminated"); \
} \
} while (0)
Expand Down
23 changes: 15 additions & 8 deletions libs2ecore/include/s2e/S2EExecutor.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,6 @@ class S2EExecutor : public klee::Executor {

bool m_executeAlwaysKlee;

bool m_forkProcTerminateCurrentState;

bool m_inLoadBalancing;

struct CPUTimer *m_stateSwitchTimer;
Expand All @@ -76,7 +74,8 @@ class S2EExecutor : public klee::Executor {

/** Called on fork, used to trace forks */
StatePair fork(klee::ExecutionState &current, const klee::ref<klee::Expr> &condition,
bool keepConditionTrueInCurrentState = false);
bool keepConditionTrueInCurrentState,
std::function<void(klee::ExecutionStatePtr, const StatePair &)> onBeforeNotify);

// A special version of fork() which does not take any symbolic condition,
// so internally it will just work like the regular fork method
Expand Down Expand Up @@ -169,16 +168,13 @@ class S2EExecutor : public klee::Executor {
}

/** Kills the specified state and raises an exception to exit the cpu loop */
virtual void terminateState(klee::ExecutionState &state);
virtual void terminateState(klee::ExecutionStatePtr state);

/** Kills the specified state and raises an exception to exit the cpu loop */
virtual void terminateState(klee::ExecutionState &state, const std::string &message);
virtual void terminateState(klee::ExecutionStatePtr state, const std::string &message);

void resetStateSwitchTimer();

// Should be public because of manual forks in plugins
void notifyFork(klee::ExecutionState &originalState, klee::ref<klee::Expr> &condition, StatePair &targets);

/**
* To be called by plugin code
*/
Expand Down Expand Up @@ -216,6 +212,17 @@ class S2EExecutor : public klee::Executor {
// If `condition` is a nullptr, then no path constraints will be added.
StatePair doFork(klee::ExecutionState &current, const klee::ref<klee::Expr> &condition,
bool keepConditionTrueInCurrentState);

StatePair unconditionalFork(klee::ExecutionState &current);

StatePair conditionalFork(klee::ExecutionState &current, const klee::ref<klee::Expr> &condition_,
bool keepConditionTrueInCurrentState);

/// When the fork is complete and state properly updated,
/// notify the S2EExecutor, so that it can generate an onFork event.
/// Sending notification after the fork completed
/// allows plugins to kill states and exit to the CPU loop safely.
void notifyFork(klee::ExecutionState &originalState, const klee::ref<klee::Expr> &condition, StatePair &targets);
};

} // namespace s2e
Expand Down
17 changes: 2 additions & 15 deletions libs2ecore/src/FunctionHandlers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,23 +98,10 @@ void handleForkAndConcretize(Executor *executor, ExecutionState *state, klee::KI
}

// XXX: may create deep paths!
Executor::StatePair sp = s2eExecutor->fork(*state, condition);

// The condition is always true in the current state
//(i.e., expr == concreteAddress holds).
assert(sp.first == state);

// It may happen that the simplifier figures out that
// the condition is always true, in which case, no fork is needed.
// TODO: find a test case for that
if (sp.second) {
// Will have to reexecute handleForkAndConcretize in the speculative state
sp.second->llvm.pc = sp.second->llvm.prevPC;
}
Executor::StatePair sp =
s2eExecutor->fork(*state, condition, false, S2EExecutor::reexecuteCurrentInstructionInForkedState);

state->llvm.bindLocal(target, concreteAddress);

s2eExecutor->notifyFork(*state, condition, sp);
}

static void handleGetValue(klee::Executor *executor, klee::ExecutionState *state, klee::KInstruction *target,
Expand Down
Loading