Basic Architecture
In the "3.1 Basic Architecture" of KLEE Paper, the author states the basic function of KLEE, which is the symbolic execution engine they implemented.
However, because of the concise nature of the papers, there won't be lots of source code in the paper. In this blog, I am going to state the core source code.
Select and Execute
According to the source code of KLEE, the interpreter loop is implemented in the Executor::run in the file lib\Core\Executor.cpp. This function takes a reference to the ExecutionState as a parameter and iterates over the states until they are exhausted or the time expires.
// in the /lib/Core/Executor.cpp of the KLEE source
// main interpreter loop
while (!states.empty() && !haltExecution) {
ExecutionState &state = searcher->selectState();
KInstruction *ki = state.pc;
stepInstruction(state);
executeInstruction(state, ki);
timers.invoke();
if (::dumpStates) dumpStates();
if (::dumpPTree) dumpPTree();
updateStates(&state);
if (!checkMemoryUsage()) {
// update searchers when states were terminated early due to memory pressure
updateStates(nullptr);
}
}
By the way, there is a "usingSeeds" keyword in the "Executor::run" function, whose meaning is that it is a boolean variable that indicates whether the symbolic execution engine is running in the seeding mode or not. Seeding mode is the feature of KLEE that allows it to use concrete value inputs as seeds to guide the exploration of the state space. (similar to the concept "concolic" of DART). Seeding mode can improve the coverage and efficiency of symbolic execution, especially for programs that have complex or unknown input formats.
/// in the lib/Core/Executor.cpp of the KLEE source.
class Executor : public Interpreter {
...
public:
...
private:
...
/// When non-null a list of "seed" inputs which will be used to
/// drive execution.
const std::vector<struct KTest *> *usingSeeds
...
The state of symbolic execution is represented by the class ExecutionState is defined in the source file lib/Core/ExecutionState.h.
class ExecutionState {
...
public:
using stack_ty = std::vector<StackFrame>;
/// @brief Pointer to instruction to be executed after the current
/// instruction
KInstIterator pc;
/// @brief Pointer to instruction which is currently executed
KInstIterator prevPC;
/// @brief Stack representing the current instruction stream
stack_ty stack;
/// @brief Remember from which Basic Block control flow arrived
/// (i.e. to select the right phi values)
std::uint32_t incomingBBIndex;
// Overall state of the state - Data specific
/// @brief Exploration depth, i.e., number of times KLEE branched for this state
std::uint32_t depth = 0;
/// @brief Address space used by this state (e.g. Global and Heap)
AddressSpace addressSpace;
/// @brief Stack allocator (used with deterministic allocation)
kdalloc::StackAllocator stackAllocator;
/// @brief Heap allocator (used with deterministic allocation)
kdalloc::Allocator heapAllocator;
/// @brief Constraints collected so far
ConstraintSet constraints;
/// Statistics and information
... ....
}
Check whether concrete
Symbolic execution of the majority of instructions is straightforward. For example, to symbolically execute an LLVM add instruction:
%dst = add i32 %src0, %src1
KLEE retrieves the addends from the %src0 and %src1 registers and writes a new expression Add(%src0, %src1) to the %dst register. For efficiency, the code that builds expressions checks if all given operands are concrete (i.e., constants) and if so, operates natively, returning a constant expression.
The method AddExpr::create is invoked to check for concrete operands and return either a constant expression or a non-constant expression accordingly. For example, the add expression kind is defined as follows:
ref<Expr> AddExpr::createActual(ref<Expr> l, ref<Expr> r) {
Expr::Width type = l->getWidth();
assert(l->getWidth() == r->getWidth() && "type mismatch");
if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) {
if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r))
return cl->Add(cr);
else if (cl->isZero())
return r;
} else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {
if (cr->isZero())
return l;
}
return AddExpr::alloc(l, r);
}
As you can see, this method checks if both operands are constant expressions (ConstantExpr) and, if so, performs the addition natively using the Add the method of the ConstantExpr class. Otherwise, it checks if either operand is zero and returns the other operand as a shortcut. Finally, if none of these cases apply, it allocates a new AddExpr object using the alloc method of the AddExpr class. Similar checks are performed for other expression kinds, such as Sub, Mul, Div, etc.
Fork Branch
void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
Instruction *i = ki->inst;
switch (i->getOpcode()) {
...
case Instruction::Br: {
BranchInst *bi = cast<BranchInst>(i);
if (bi->isUnconditional()) {
transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
} else {
// 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, state).value;
cond = optimizer.optimizeExpr(cond, false);
Executor::StatePair branches = fork(state, cond, false, BranchType::Conditional);
// NOTE: There is a hidden dependency here, markBranchVisited
// requires that we still be in the context of the branch
// instruction (it reuses its statistic id). Should be cleaned
// up with convenient instruction specific data.
if (statsTracker && state.stack.back().kf->trackCoverage)
statsTracker->markBranchVisited(branches.first, branches.second);
if (branches.first)
transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), *branches.first);
if (branches.second)
transferToBasicBlock(bi->getSuccessor(1), bi->getParent(), *branches.second);
}
break;
}
...
}
...
}
As you can see, this method checks if the branch instruction is unconditional or conditional. If it is unconditional, it simply transfers the execution state to the successor basic block using the transferToBasicBlock method. If it is conditional, it evaluates the branch condition using the eval method and then fork the execution state into two possible branches using the fork method returning a pair of execution states, one for a true branch and one for a false branch.
The method then transfers each execution state to the corresponding successor basic block using the transferToBasicBlock method. This way, the instruction pointer of each state is altered based on the branch condition.
void Executor::executeGetValue(ExecutionState &state,
ref<Expr> e,
KInstruction *target) {
e = ConstraintManager::simplifyExpr(state.constraints, e);
std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
seedMap.find(&state);
if (it == seedMap.end() || isa<ConstantExpr>(e)) {
ref<ConstantExpr> value;
e = optimizer.optimizeExpr(e, true);
bool success =
solver->getValue(state.constraints, e, value, state.queryMetaData);
assert(success && "FIXME: Unhandled solver failure");
(void) success;
bindLocal(target, state, value);
} else {
std::set< ref<Expr> > values;
for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
siie = it->second.end(); siit != siie; ++siit) {
ref<Expr> cond = siit->assignment.evaluate(e);
cond = optimizer.optimizeExpr(cond, true);
ref<ConstantExpr> value;
bool success =
solver->getValue(state.constraints, cond, value, state.queryMetaData);
assert(success && "FIXME: Unhandled solver failure");
(void) success;
values.insert(value);
}
std::vector< ref<Expr> > conditions;
for (std::set< ref<Expr> >::iterator vit = values.begin(),
vie = values.end(); vit != vie; ++vit)
conditions.push_back(EqExpr::create(e, *vit));
std::vector<ExecutionState*> branches;
branch(state, conditions, branches, BranchType::GetVal);
std::vector<ExecutionState*>::iterator bit = branches.begin();
for (std::set< ref<Expr> >::iterator vit = values.begin(),
vie = values.end(); vit != vie; ++vit) {
ExecutionState *es = *bit;
if (es)
bindLocal(target, *es, *vit);
++bit;
}
}
}
As you can see, the Executor::executeGetValue in the lib\Core\Executor.cpp first checks if the current state is seed or the expression being executed is concrete, if so, invoke the solver to get the final value and bind it locally. Otherwise, deal with the seed condition and the branch condition.
Deal with Dangerous Operation
The part of the code that implements the function of mapping every memory object in the checked code to a distinct STP array is the Executor::getInitialArray method in the file lib/Core/Executor.cpp1. This method takes two parameters: a reference to the execution state and a pointer to the memory object. The method performs the following steps:
It checks if the memory object has already been mapped to an STP array, and if so, it returns the existing array.
It creates a new STP array with a unique name based on the memory object’s address and size. The name is prefixed with either “arr” or “reg” depending on whether the memory object is allocated on the heap or on the stack2.
It inserts the new STP array into a map that associates memory objects with STP arrays, using the memory object as the key.
It returns the new STP array.
Query optimization
In the KLEE paper, the author describes lots of optimizations of queries such as expression rewriting, constraint set simplification and so on. The KLEE implements the function in lib/Solver/Solver.cpp.
Random Path Selection and Coverage-Optimized Search
The KLEE source code contains two different search heuristics for selecting the next state to explore: Random Path Selection and Coverage-Optimized Search.
// lib\Core\Searcher.cpp
// RP Selection
ExecutionState &RandomSearcher::selectState() {
return *states[theRNG.getInt32() % states.size()];
}
// CO Selection
ExecutionState &WeightedRandomSearcher::selectState() {
return *states->choose(theRNG.getDoubleL());
}
REFERENCE
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
