今天博士检查了我的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的崩溃！！