KLEE - kain's Blog

今天博士检查了我的PPT，各种不合格，需要努力的地方还有很多

现在针对PPT中没有给出的两个重要问题做下解释：

1.KLEE的工作流程

2 KLEE为什么是单线程的

1.KLEE的工作流程

我们从最普通的命令行说起

klee -libc=uclibc -posix-runtime *.bc

启动klee程序，读入参数

在LinkModule的时候，判断link哪个库，这里我们link的是uclibc和posix-runtime，注意link的先后顺序

然后初始化变量

进入runFuncitonAsMain进行运行

主要的环节在

while(state)//////判断sate是否全部终结

{

从Executor中的一堆state中根据规则select出来一个state

executeInstruction(state.instruciton, state);

update（state）

}

在executeInstruction中根据不同的指令，执行不同的动作（相当于KLEE解释.bc文件）

如果遇到函数调用，则判断函数是外部函数还是内部函数，如果是外部函数，则调用外部库函数或者handler一下

如果是内部函数，则Frame入栈，state.pc更改，随着下一次state的选择执行调用函数的指令

当遇到返回指令的时候，如果state.stack为空，则solve 出constraint

若state.stack不为空，则相当于内部函数返回，pop Frame，更改state.pc

如果遇到分支指令，则根据condition，看是否必要在fork中生成新的falsestate，update（state）时添加新的状态

2KLEE的单线程

KLEE执行函数调用的方法是保留栈stack，popFrame和pushFrame

并没有为函数调用开启新的state或者其他特殊方法

当遇到pthread_create函数的时候，系统没有在uclibc和posix-runtime的库中链接到相应的函数于是直接调用了

系统函数pthread_create导致了KLEE的崩溃！！

关于函数的调用在klee使用中的体现

klee -libc=uclibc -posix-runtime *.bc

在executeInstrucion()中

通过判断instruction的类型，区分了call,和invoke

然后通过判断是不是直接的函数调用（是否为函数指针？？）

如果是直接的函数调用，则调用函数executeCall（）,如果是非直接，则做进一步处理，待考证

executeCall()

{

if(f->isDeclaration())//////////如果函数仅仅有函数头, 即函数是外部函数，则调用

callExternFunction();

{

在这里面判断是否为定义的特殊函数例如klee_make_symbolic是，间接调用相应的函数

否，则使用系统调用相应的函数

}

else

{

函数的定义包含在module中，注意，这里的定义包含其实分为两种情况

1.函数为自己定义的函数，这样刚开始的时候函数即在里面

2.函数是外部函数，例如puts之类，但是因为我们使用klee的时候，加上了参数uclibc,和runPosixTime，所以在原module和

库函数链接的时候，就把定义链接了进去(经过实验，不知道为嘛printf没有被链接进去？？？)

注意klee::main.cpp中链接的顺序，先是链接uclibc，将fopen之类的函数展开，在这里是展开为open

然后链接PosixRuntime库，在runTime/Fd_32.c中有open的定义，调用了

fd.c中的__fd_open函数，在这里面就判断了文件名参数path是否为symbolic

是，则使用klee定义的symbolic 模块

否，则调用真正的系统调用

}

这样大概解释了pthread_create的调用过程

因为uclibc中的libc库没有pthread_create的定义，而且specialHanlder也没有，就直接进入了symtem调用最直接的 pthread_create

在 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的解答

使用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的添加

kain's Blog

KLEE小解

KLEE-之函数调用

KLEE--constraint与state的关系

KLEE源码解析之klee_make_symbolic跟踪

kain

分类

最新评论

最新留言

链接

功能