KLEE--constraint与state的关系
在 executor.cpp中，有run函数，一切程序的运行的驱动都是从这里开始的
line:2460
while (!states.empty() && !haltExecution)
{
line2465:
executeInstruction(state, ki);
.....................
....................
....................
updateStates(&state);
}
executeInstruction顾名思义就是执行当前的Ki指令，当前选择的状态是state
updateState就是当这条指令执行结束的时候，更行状态集合
Executor::executeInstruction
{
让我们直接来看
line1452:Instruction:Br
Executor::StatePair branches = fork(state, cond, false) //////////////cond是这个分支对应的条件
}
在Executor::fork()
{
line：712
bool success = solver->evaluate(current, condition, res);//////////////////////通过这个，计算出当前情况下res的值，然后判断
line：807
if (res==Solver::True)
{
}
else if (res==Solver::False)
{
}
else
{
falseState = trueState->branch(); /////通过ExecutionState::branch()，复制了一份相同的falseState
addedStates.insert(falseState); ////////////////将falseState添加到addStates中，addedStates将在updateState中使用
}
addConstraint(*trueState, condition);///////////////////////////////ExecutionState:: state.addConstraint(condition);
///////////////////将condtion添加到 ConstraintManager constraints;里面去
addConstraint(*falseState, Expr::createIsZero(condition));
}/////end of Executor::fork
我们看到在fork中，程序完成了state的复制和相应的condition的添加
现在让我们进入
Executor::updateStates()
{
line:2301
states.insert(addedStates.begin(), addedStates.end());//完成了新加状态的添加
/////////////////sates就是run中while循环终结的语句 while (!states.empty() && !haltExecution)
}
Executor---------- std::set<ExecutionState*> states;
ExecutionState--------- ConstraintManager constraints;
在run中，Executor的states不断的更新，与之对应的是ExecutionState中的constraint也不断的更新
当系统遇到返回或者终结时，会根据入参state，solve出对应的constraint的解答
评论 (0)
