KLEE源码解析之klee_make_symbolic跟踪
使用klee时，一般要利用klee_make_symbolic函数，将要跟踪的变量标记为symbolic，但是klee是如何找到这个函数，并且对应标记的呢。。。。。
把klee_make_symbolic使用的分为两个过程，1。绑定 2.调用
1.绑定
在main.cpp中
line：1303
Interpreter *interpreter =
theInterpreter = Interpreter::create(IOpts, handler);//////////调用static函数创建了interpretor
handler->setInterpreter(interpreter); ////////////设置了interpreter输出文件的路径？？
line：1313
const Module *finalModule =
interpreter->setModule(mainModule, Opts);.////////////////////////////在setModule函数中，完成了klee_make_symbolic函数到SpecialFunctionHandler::handleMakeSymbolic的绑定
Executor.cpp
跟踪Executor::setModule(Executor作为Interpreter的子类，实现了setModule虚函数)
line:348行
specialFunctionHandler = new SpecialFunctionHandler(*this);/////实现了Executor::specialFuntionHandler变量与包含它的类变量的相互绑定
line：352
specialFunctionHandler->bind();///////////////////////////////继续绑定过程
SpecialFunctionHandler.cpp
line:149
Function *f = executor.kmodule->module->getFunction(hi.name);/////////利用llvm提供的功能函数，查找到对应的hi.name（这里为klee_make_symbolic）的Function指针
line:151
if (f && (!hi.doNotOverride || f->isDeclaration()))//代码中存在klee_make_symbolic函数
handlers[f] = std::make_pair(hi.handler, hi.hasReturnValue);/////////////////////// 建立klee_make_symbolic函数返回指针和hi的对应关系,对应klee::SpecialFunctionHandler::handleMakeSymbolic()
handlers_ty handlers; typedef std::map<const llvm::Function*,
std::pair<Handler,bool> > handlers_ty;
至此绑定结束
2.运行klee_make_symbolicd对应的handleMakeSymbolic函数
main.cpp
if (!ReplayOutDir.empty() || !ReplayOutFile.empty())///////////感觉一直都为真吧？？？
{
line1365
interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
}
Executor.cpp
进入runFunctionAsMain函数
line3257
run(*state);//////////// ExecutionState *state = new ExecutionState(kmodule->functionMap[f]);生成state，并完成一系列的初始工作
进入run函数
line2402
while (!seedMap.empty())对应论文里面提到的state没有运行完，则程序继续运行
{
line2415
executeInstruction(state, ki);
}
进入 executeInstruction(state, ki)函数
line1547
case Instruction::Call: ///////指令作用为函数调用，顾名思义。。。
{
line：1604
executeCall(state, ki, f, arguments);
}
进入 executeCall(state, ki, f, arguments);
函数头：：
void Executor::executeCall(ExecutionState &state,
KInstruction *ki,
Function *f,
std::vector< ref<Expr> > &arguments) {
line1125
callExternalFunction(state, ki, f, arguments);
进入callExternalFunction(state, ki, f, arguments);
函数头：
void Executor::callExternalFunction(ExecutionState &state,
KInstruction *target,
Function *function,
std::vector< ref<Expr> > &arguments) {
line2665
if (specialFunctionHandler->handle(state, function, target, arguments))/////注意这里的Executor::specialFunctionHandler为Executore::setModule生成的
进入SpecialFunctionHandler::handle函数
SpecialFuntionHandler.cpp
line161-163
handlers_ty::iterator it = handlers.find(f);
if (it != handlers.end()) {
Handler h = it->second.first;/////////////找到对应的Handler
line170
(this->*h)(state, target, arguments);调用klee_make_symbolic对应的处理函数handleMakeSymbolic(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> > &arguments) 成功
下面，让我们看一下handleMakeSymbolic函数是如何实现symbolic的添加
void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> > &arguments) {
追踪下参数的来源
handleMakeSymbolic第三个参数：：
Executor.cpp
executeInstruction()函数
line1559中
std::vector< ref<Expr> > arguments;
line1563中
arguments.push_back(eval(ki, j+1, state).value);
这是handleMakeSymbolic第三个参数的来源
第二个参数
Executor.cpp
run()函数中
2412行
KInstruction *ki = state.pc;////////当前状态，当前指令的位置
第一个参数
state也是在run()函数中选择出来的////论文里是两种方式interleave！！！有待考察！！！
SpecialFuntionHandler.cpp
line：683行
if (res) {
executor.executeMakeSymbolic(*s, mo, name);
}
跟踪进入executeMakeSymbolic
Executor.cpp
line:3103
const Array *array = new Array(uniqueName, mo->size);
bindObjectInState(state, mo, false, array);
state.addSymbolic(mo, array);
完成了符号symbolic的添加
