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

1

先在网上下载了LLVM2.8的代码，然后解压到

 

 

 

 

 

 

llvm-2.8文件夹

 

 

 

 

 

 

 

 

$ curl -O http://llvm.org/releases/2.8/llvm-2.8.tgz 
$ tar zxvf llvm-2.8.tgz 
$ cd llvm-2.8 
$ ./configure --enable-optimized --enable-assertions

 

 

 

 

 

 

 

后半句的作用就是使用代码优化

$ make

   make install

 

 

2

安装LLVM-gcc

在网上下载LLVM 2.8 release of llvm-gcc 源码

解压到llvm-gcc文件夹

然后在与llvm-gcc等同的目录下创建obj，install文件夹

进入obj文件夹下

执行配置命令

../llvm-gcc4.2-x.y.source/configure --prefix=`pwd`/../install --program-prefix=llvm --enable-llvm=$LLVMOBJDIR --enable-languages=c,c++$EXTRALANGS $TARGETOPTIONS --target=i686-pc-linux-gnu --with-tune=generic --with-arch=pentium4

说明：

 

 

 

 

 

 

 

--prefix=`pwd`/../install安装在了等级的install文件（刚刚创建的）

 

 

 

 

 

 

 

 

生成make $BUILDOPTIONS

 

然后make install

 

 

 

 

 

 

 

make是用来编译的，它从Makefile中读取指令，然后编译。
make install是用来安装的，它也从Makefile中读取指令，安装到指定的位置。

添加路径到  vim ~/.bash_profile

source ~/.bash_profile使路径立即生效

 

 

 

 

 

 

 

重新make了llvm，使用了configure -h 查看帮助

除了上面两个选项外，又重新增加了指定llvmgcc，llvmg++的绝对路径（不然make check的时候会有问题，而且编译uClibc的时候要改变$LLVMGCC到llvmgcc的绝对路径）

 

 

3.安装KLEE

3.1先安装uClibc

 

$ tar zxvf klee-uclibc-0.01.tgz 

 

 

 

 

 

 

 

$ ./configure --with-llvm=path/to/llvm 
$ make

这时候出现了问题，说什么找不到，主要是自动生成的Makefile的问题，这时候修改Rules.mak中tool的路径（在llvm下面，Realease+Assert/bin）

 

在make

3.2安装KLEE

 

下载

配置

 

 

 

 

 

./configure --with-llvm=path/to/llvm --with-uclibc=path/to/klee-uclibc --enable-posix-runtime

 

make

 

 

 

 

 

这时候的make check就可以通过了

 

小技巧：find /fse/ | xargs grep  “llvm”

查找/fse/文件夹下面的文件，谁的内容有llvm