一.klee介绍

1.1.简单介绍

Klee是一个LLVM IR符号执行工具（OSDI 08 Paper地址），能够自动生成测试，实现对各种复杂且环境密集型程序的高覆盖率

klee有2个目标：

命中目标程序中的每一行代码
检测到每一个危险操作（dereference, assertion等等，如果任何的输入能够触发此危险操作）

当klee检测到错误或路径到达 exit 调用时，klee求解当前路径的约束来生成一个测试用例，当在同样的程序上重新运行时，该测试用例将执行相同的路径。

klee的核心是1个循环，每轮循环中klee会从state列表中选出1个state并执行处于该state上下文中的1个指令（参考ExecutionState.h，klee在每个状态都会记录将要执行的指令和已经执行的指令），这个循环会持续到列表中不再有state或者用户设定的时间上限达到了。循环大致伪代码如下：

initalState = create();
stateList.add(initialState);while (!stateList.empty() && !haltExecution){state = selectState(stateList); // 根据策略从列表选择状态executeState(state); // 符号执行，可能会fork新的stateupdateStateList(stateList); // 更新状态列表
}

当状态列表不为空或者终止条件（超时、内存超出等）没达到时循环继续。
selectState 的实现根据不同的搜索策略（DFS、BFS、RSS等）有不同的实现方式。

与普通进程不同，状态（寄存器、堆栈和堆对象）的存储位置引用表达式（树）而不是原始数据值。

大部分指令的符号执行是简洁明了的，比如 %dst = add i32 %src0, %src1，klee从寄存器 %src0 和 %src1 中获取加数并将 Add(%src0, %src1 写入寄存器 %dst。为了提高效率，构建表达式的代码检查所有给定操作数是否都是具体的（即常量，符号变量越少效率越高），如果是，则以本机方式执行操作，返回常量表达式。

条件分支是1个布尔表达式（分支条件），并根据条件是true 还是 false 更改状态的指令指针。

1.2.klee架构

1.2.1.基础架构

KLEE查询约束解算器以确定分支条件沿当前路径是可证明为真还是可证明为假；如果是，指令指针将更新到适当的位置。否则，两个分支都是可能的：KLEE克隆（fork）state，以便它可以探索两条路径，适当更新每条路径上的指令指针和路径条件。

潜在危险的操作隐式生成分支，检查是否存在可能导致错误的输入值。例如，除法指令生成检查零除数的分支。这些分支的工作原理与普通分支相同。因此，即使检查成功（即检测到错误），也会在错误路径上继续执行，这会将检查的否定添加为约束（例如，使除数不为零）。如果检测到错误，KLEE会生成一个测试用例来触发错误并终止状态。

与其他危险操作一样，load 和 store 指令生成check：检查被测地址是否在有效内存对象的边界内。然而，load 和 store 操作带来了额外的复杂性。被测代码使用的内存最直接的表示形式是一个平面字节数组。在这种情况下，load 和 store 将分别映射到数组读取和写入表达式。不幸的是，约束解算器STP几乎永远无法求解结果约束（我们所知道的其他约束解算程序也无法解算）。KLEE将被测代码中的每个内存对象映射到不同的STP数组（从某种意义上说，将平面地址空间映射到分段地址空间）。这种表示法极大地提高了性能，因为它允许STP忽略给定表达式未引用的所有数组。

许多操作（如bound checks或object-level copy-on-write）需要特定于对象的信息。如果一个指针可以引用许多对象，那么这些操作就很难执行。为了简单起见，KLEE回避了这个问题，如下所示。当dereferenced pointer p 可以引用 N 个对象时，KLEE会将当前状态克隆 N 次。在每个状态下，它将 p 限制在其各自对象的边界内，然后执行适当的读或写操作。虽然这种方法对于具有大points-to集合的指针来说代价高昂，但我们测试的大多数程序只使用指向单个对象的符号指针，并且KLEE针对这种情况进行了很好的优化。

1.2.2.Query优化

给定复杂的路径约束，在调用求解器（STP, Z3等）之前，klee会对约束进行一些简化，加快约束求解的过程，主要的优化包括：

表达式简化：最基本的优化反映了编译器中的优化：例如，简单的算术简化（x+0=0）、强度减少（x * pow(2, n)=x<<n）、线性简化（2*x-x=x）。
约束集简化: 符号执行通常涉及向路径条件添加大量约束。程序的自然结构意味着对相同变量的约束会变得更加具体。比如前一个有 x < 10，后面添加了等于约束 x = 5 ，那么 x 的值会具体化为5，约束 x < 10 会被删除。
隐含值具体化：当诸如 x + 1 = 10 这样的等于约束添加到路径约束中，x 的值被具体化（这里为9）并将具体值写入内存。
约束独立性：许多约束在引用的内存方面没有重叠。约束独立性（取自EXE）根据约束集引用的符号变量将其划分为不相交的独立子集。通过显式跟踪这些子集，KLEE可以在向约束解算器发送查询之前经常消除不相关的约束。比如 {i < j, j < 20, k > 0} 中，遇到查询 i < 20，只会需要求解前2个约束。
示例缓存：冗余查询非常频繁，简单的缓存可以有效地消除大量冗余查询。然而，由于约束集的特殊结构，可以构建更复杂的缓存。示例缓存将约束集映射到示例（即变量赋值），并在一组约束没有解决方案时使用一个特殊的哨兵。假设缓存目前含有约束 {i < 10, i = 10}（无解）和 {i < 10, j = 8}（有解 i = 5, j = 8）。
- 当约束集的子集没有解时，原始约束集也没有解。向不可满足的约束集添加约束不能使其满足。在上述缓存优化下，路径约束 {i < 10, i = 10, j = 12} 很快被确定为无解。
- 当约束集的超集有解时，该解也满足原始约束集。从约束集中删除约束不会使该集合的解决方案无效。赋值 i → 5, j → 8 能满足约束 i < 10 和 j = 8。
- 当约束集的子集有解时，这很可能也是该约束集的解。这是因为额外的约束通常不会使子集的解决方案无效。由于检查潜在解决方案的成本很低，KLEE尝试用所有解决方案替换约束集的子集，如果找到，则返回满意的解决方案。i = 5, j = 8 依旧是 {i < 10, j = 8, i != 3} 的一个解。

作者在coreutils上运行了5分钟，独立性优化能减少45%的运行时间，示例缓存能够减少40%的STP查询以及运行时间。当这2项优化开启后，STP查询的数量减小为原来的5%，平均运行时间减少了一个数量级以上。

在原始情况下，STP求解能占据92%的运行时间，开启2项优化后降低为41%。

1.2.3.状态调度

paper发出时klee采用下面2种状态选择策略：

Random Path Selection：该策略维护一个二叉树，记录所有活动状态所遵循的程序路径，即树的叶子是当前状态，内部节点是执行分叉的地方。该策略从root结点随机选择方向遍历到叶子结点。
覆盖率优化的策略：尽可能选择能覆盖到新代码的状态，根据与未覆盖指令的最小距离、状态的调用栈深度、该状态是否最近覆盖新指令计算权重，然后根据权重随机选择状态。

执行一个指令所花费的时间可能与多个因素有关（指令本身、是否fork状态、是否调用约束求解器），为了不让一个耗时的state影响klee工作，klee运行每一个状态在1个time slice以内。

1.3.环境建模

当代码从其环境中读取值（命令行参数、环境变量、文件数据和元数据、网络数据包等）时，klee从概念上想返回读取可以合法生成的所有值，而不仅仅是单个具体值。当它写入其环境时，这些更改的影响应反映在后续读取中。

原理上，klee通过将访问环境的库调用重定向到环境模型来处理环境，这些模型能够很好地理解所需操作的语义，从而生成所需的约束。重要的是，这些模型是用普通的C代码编写的，用户可以轻松地定制、扩展甚至替换，而无需了解KLEE的内部原理。klee有大约2500行代码来定义大约40个系统调用的简单模型。(e.g., open, read, write, stat, lseek, ftruncate, ioctl).

对于文件读写，如果文件名是具体值，klee会调用OS提供的对应API进行读写，对于符号文件，读取时klee会从保存数据的符号缓冲区种中读取数据传给用户数组。

二.安装

官方给的安装教程（LLVM 11 + klee-2.3）

首先装klee前，系统得配置好其它的包（包括LLVM等）

官方首先给了命令 sudo apt-get install build-essential cmake curl file g++-multilib gcc-multilib git libcap-dev libgoogle-perftools-dev libncurses5-dev libsqlite3-dev libtcmalloc-minimal4 python3-pip unzip graphviz doxygen ，很明显这么一大长串有包的系统已经装好了，因此可以从命令中移除，对我来说 libgoogle-perftools-dev 和 libsqlite3-dev 包是还没装好的，因此我只装了这2个包，python环境我用的是anaconda的。
python包 lit, wllvm, tabulate
- lit是用来测试用的，wllvm是方便将程序编译成bytecode，直接使用 pip install lit wllvm==1.0.17 安装。
- tabulate包：官方给的命令是 sudo apt-get install python3-tabulate，我是使用 pip install tabulate 安装，这个包是在klee符号执行完毕后，使用klee-stats查看run.stats文件时使用的。
LLVM-11，官方给的安装命令是 sudo apt-get install clang-11 llvm-11 llvm-11-dev llvm-11-tools，但是我这边ubuntu直接找不到 llvm-11，因此只能尝试其它安装方法
- 最简单的方法就是从github上下载release(找到clang+llvm-11.0.0-x86_64-linux-gnu-ubuntu-20.04.tar.xz，我系统是ubuntu的) ，但是下载release版的有个小问题，就是LLVM_DIR/bin目录下少了ELF文件 FileCheck 和 not，当然这并不影响LLVM的使用，但是编译klee的时候会报错。（这2个文件源码在目录llvm-project/llvm/utils目录下，分别有个FileCheck和not目录）
- 因此我只能尝试重新编译安装LLVM 11（花费2个小时，为了2个ELF文件这么干真的耗时，但奈何不知道如何只编译这2个文件），下载完LLVM 11源码后，命令行切到源码根目录下，cmake的时候添加 -DLLVM_BUILD_UTILS=ON 参数，编译完成之后可以在build/bin目录下找到FileCheck和not，但是这2个ELF在 make install 的时候不会自动复制到LLVM的安装目录下，需要手动从build目录下复制到安装目录下.
- 完整的编译命令如下：mkdir build && cd build，cmake -G "Unix Makefiles" -DLLVM_ENABLE_PROJECTS='clang;clang-tools-extra;libcxx;libcxxabi;libunwind;lldb;compiler-rt;lld;polly' -DCMAKE_INSTALL_PREFIX=<LLVM_DIR> -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_ASSERTIONS=On -DLLVM_BUILD_UTILS=On ../llvm，cmake --build . -j 4，cmake --build . --target install。
从github上下载klee-ulibc的源码并编译，直接按github上的教程编译就行，不用设置额外参数。
编译klee
- mkdir build && cd build
- cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=<KLEE_UCLIBC_DIR> -DCMAKE_INSTALL_PREFIX=<KLEE_DIR> ..（<KLEE_DIR> 是klee安装目录，该目录下只有 bin, lib, include 3个文件夹，比 build 目录简单。<KLEE_UCLIBC_DIR> 是 klee-uclibc 的源码目录，klee-uclibc 只需编译后就行不用install）
- make -j4
- make install

最终环境

工具	版本
LLVM	11.0.0
klee	2.3
wllvm	1.0.17

三.klee使用

参考官方示例

3.1.Testing a Small Function

get_sign.c

#include<klee/klee.h>int get_sign(int x) {if (x == 0)return 0;if (x < 0)return -1;else return 1;
} int main() {int a;klee_make_symbolic(&a, sizeof(a), "a");return get_sign(a);
}

用下面命令编译代码 clang -I $KLEE_DIR/include -emit-llvm -c get_sign.c（不要用clang优化）生成bc文件，用 klee get_sign.bc 测试，测试结束后会在当前目录生成klee-out-0文件夹，klee-out-0中包含若干文件：assembly.II（实际执行的LLVM代码），testxxxxx.ktest，info，run.stats，message.txt等

执行的LLVM IR（assembly.II）为：

; ModuleID = 'sample.bc'
source_filename = "sample.c"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @get_sign(i32 %x) #0 {entry:%retval = alloca i32, align 4%x.addr = alloca i32, align 4store i32 %x, i32* %x.addr, align 4%0 = load i32, i32* %x.addr, align 4%cmp = icmp eq i32 %0, 0br i1 %cmp, label %if.then, label %if.endif.then:                                          ; preds = %entrystore i32 0, i32* %retval, align 4br label %returnif.end:                                           ; preds = %entry%1 = load i32, i32* %x.addr, align 4%cmp1 = icmp slt i32 %1, 0br i1 %cmp1, label %if.then2, label %if.elseif.then2:                                         ; preds = %if.endstore i32 -1, i32* %retval, align 4br label %returnif.else:                                          ; preds = %if.endstore i32 1, i32* %retval, align 4br label %returnreturn:                                           ; preds = %if.else, %if.then2, %if.then%2 = load i32, i32* %retval, align 4ret i32 %2
}; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 {entry:%retval = alloca i32, align 4%a = alloca i32, align 4store i32 0, i32* %retval, align 4%0 = bitcast i32* %a to i8*call void @klee_make_symbolic(i8* %0, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))%1 = load i32, i32* %a, align 4%call = call i32 @get_sign(i32 %1)ret i32 %call
}declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }!llvm.module.flags = !{!0}
!llvm.ident = !{!1}!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 11.0.0"}

在这个示例中，klee生成了3个ktest文件：test000001.ktest, test000002.ktest, test000003.ktest表示生成了3个测试用例，分别对应程序3个分支（x < 0, x = 0, x > 0）

使用 ktest-tool klee-out-0/test000001.ktest 查看其内容：

ktest file : 'klee-last/test000001.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x00'
object 0: hex : 0x00000000
object 0: int : 0
object 0: uint: 0
object 0: text: ....

num objects 表示符号变量数量，size为变量大小（计量单位byte），data为对应的数据

run.stats包含了一些统计信息，使用 klee-stats klee-out-0（不要加文件名，定位到目录就行）查看

Path	Instrs	Time(s)	ICov(%)	BCov(%)	ICount	TSolver(%)
klee-out-0	31	0.09	100.00	100.00	25	97.82

ICov表示LLVM指令的覆盖率
BCov表示分支覆盖率
ICount表示指令数量

run.istats包含了一些状态信息，可用kcachegrind工具查看 (kcachegrind xxx.istats)

version: 1
creator: klee
pid: 13664
cmd: sample.bcpositions: instr line
event: Icov : CoveredInstructions
event: Forks : Forks
event: Ireal : InstructionRealTimes
event: Itime : InstructionTimes
event: I : Instructions
event: UCdist : MinDistToUncovered
event: Rtime : ResolveTime
event: States : States
event: Iuncov : UncoveredInstructions
event: Q : Queries
event: Qiv : QueriesInvalid
event: Qv : QueriesValid
event: Qtime : QueryTime
events: Icov Forks Ireal Itime I UCdist Rtime States Iuncov Q Qiv Qv Qtime
ob=assembly.ll
fn=get_sign
11 0 1 0 0 0 1 0 0 0 0 0 0 0 0
12 0 1 0 0 0 1 0 0 0 0 0 0 0 0
13 0 1 0 0 0 1 0 0 0 0 0 0 0 0
14 0 1 0 0 0 1 0 0 0 0 0 0 0 0
15 0 1 0 0 0 1 0 0 0 0 0 0 0 0
16 0 1 1 0 0 1 0 0 0 0 2 2 0 73279
19 0 1 0 0 0 1 0 0 0 0 0 0 0 0
20 0 1 0 0 0 1 0 0 0 0 0 0 0 0
23 0 1 0 0 0 1 0 0 0 0 0 0 0 0
24 0 1 0 0 0 1 0 0 0 0 0 0 0 0
25 0 1 1 0 0 1 0 0 0 0 1 1 0 18761
28 0 1 0 0 0 1 0 0 0 0 0 0 0 0
29 0 1 0 0 0 1 0 0 0 0 0 0 0 0
32 0 1 0 0 0 1 0 0 0 0 0 0 0 0
33 0 1 0 0 0 1 0 0 0 0 0 0 0 0
36 0 1 0 0 0 3 0 0 0 0 0 0 0 0
37 0 1 0 0 0 3 0 0 0 0 0 0 0 0
fn=main
43 0 1 0 0 0 1 0 0 0 0 0 0 0 0
44 0 1 0 0 0 1 0 0 0 0 0 0 0 0
45 0 1 0 0 0 1 0 0 0 0 0 0 0 0
46 0 1 0 0 0 1 0 0 0 0 0 0 0 0
47 0 1 0 0 0 1 0 0 0 0 0 0 0 0
48 0 1 0 0 0 1 0 0 0 0 0 0 0 0
49 0 1 0 0 0 1 0 0 0 0 0 0 0 0
cfn=get_sign
calls=1 8 0
49 0 17 2 0 0 21 0 0 0 0 3 3 0 92040
50 0 1 0 0 0 3 0 0 0 0 0 0 0 0

每个状态对应一个int列表

第1列为指令在assenmbly.II中的行号
第2列为指令对应的源代码中的行号，需要在clang编译源码时添加参数 -g 保存debug信息，不然全是0
第3列表示该状态覆盖的指令数
第4列表示该状态Fork的数量
第5，6列表示指令时间
最后一个是求解时间

3.2.Using Symbolic Environment

3.2.1.sym-arg

-sym-arg <N> 能够提供1个长度为N 的命令行参数
-sym-args <MIN> <MAX> <N> 提供最少 MIN 个，最多 MAX 个长度最长为 N 的命令行参数

#include <stdio.h>int check_password(char *buf) {if (buf[0] == 'h' && buf[1] == 'e' &&buf[2] == 'l' && buf[3] == 'l' &&buf[4] == 'o')return 1;return 0;
}int main(int argc, char **argv) {if (argc < 2)return 1;if (check_password(argv[1])) {printf("Password found!\n");return 0;}return 1;
}

3.2.2.sym-files

-sym-files <NUM> <N> 参数创建 <NUM> 个，第一个命令为 A，第二个命名 B，依此类推，每个文件大小 N byte，子选项 -sym-stdin 和 -sym-stdout 会使得标准输入和输出符号化

以类似的代码为例

#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <stdio.h>
#include <unistd.h>int check_password(int fd) {char buf[5];if (read(fd, buf, 5) != -1) {if (buf[0] == 'h' && buf[1] == 'e' &&buf[2] == 'l' && buf[3] == 'l' &&buf[4] == 'o')return 1;}return 0;
}int main(int argc, char **argv) {int fd;if (argc >= 2) {if ((fd = open(argv[1], O_RDONLY)) != -1) {if (check_password(fd)) {printf("Password found in %s\n", argv[1]);close(fd);return 0;}close(fd);return 1;}}if (check_password(0)) {printf("Password found in standard input\n");return 0;}return 1;
}

编译之后用 klee -posix-runtime password.bc A -sym-files 1 10 跑，生成6个testcase，用ktest-tool查看其中一个，结果为

ktest file : 'klee-last/test000006.ktest'
args       : ['password.bc', 'A', '-sym-files', '1', '10']
num objects: 3
object 0: name: 'A-data'
object 0: size: 10
object 0: data: b'hellohhhhh'
object 0: hex : 0x68656c6c6f6868686868
object 0: text: hellohhhhh
object 1: name: 'A-data-stat'
object 1: size: 144
object 1: data: b'\x01\x08\x00\x00\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x01\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\x00\x10\x00\x00\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\xed\xa7Bc\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\xaa\xa8Bc\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\xaa\xa8Bc\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01'
object 1: hex : 0x010800000000000001010101010101010100000000000000a4810000e8030000e8030000010101010000000000000000010101010101010100100000000000000101010101010101eda74263000000000101010101010101aaa84263000000000101010101010101aaa84263000000000101010101010101010101010101010101010101010101010101010101010101
object 1: text: ..........................................................................Bc..............Bc..............Bc....................................
object 2: name: 'model_version'
object 2: size: 4
object 2: data: b'\x01\x00\x00\x00'
object 2: hex : 0x01000000
object 2: int : 1
object 2: uint: 1
object 2: text: ....

只关注第一个object，名称为 A-data，text为 hellohhhhh，可以通过测试程序的密码检测。

四.源码简单分析

klee的 main 函数在tools/klee/main.cpp中，main 函数前面一大堆的代码是解析环境、参数啥的，在main.cpp中的1384行，程序新建了一个Interpreter，而之后，程序会调用Interpreter::runFunctionAsMain方法进行符号执行，这个方法是个虚方法。在实际执行中，程序调用的 Interpreter 子类是Executor类，因此符号执行的入口代码在Executor::runFunctionAsMain中（这里我删除了部分解析环境的代码）

void Executor::runFunctionAsMain(Function *f,int argc,char **argv,char **envp) {std::vector<ref<Expr> > arguments;ExecutionState *state = new ExecutionState(kmodule->functionMap[f]);initializeGlobals(*state);processTree = std::make_unique<PTree>(state);run(*state);processTree = nullptr;
}

PTree在Random Path Search中用到了，其它搜索策略均没用到。
ExecutionState *state = new ExecutionState(kmodule->functionMap[f]); 和 initializeGlobals(*state); 完成了初始状态的初始化。
run方法则以是符号执行的主要代码（下面是精简过的代码）

void Executor::run(ExecutionState &initialState) {states.insert(&initialState);searcher = constructUserSearcher(*this);std::vector<ExecutionState *> newStates(states.begin(), states.end());searcher->update(0, newStates, std::vector<ExecutionState *>());// main interpreter loopwhile (!states.empty() && !haltExecution) {ExecutionState &state = searcher->selectState();KInstruction *ki = state.pc;stepInstruction(state);executeInstruction(state, ki);updateStates(&state);}delete searcher;searcher = nullptr;doDumpStates();
}

states.insert(&initialState); 将初始状态添加到状态列表中。需要注意的是 states 是 Executor 维护的状态集合（成员变量），每个Searcher类都会有一个自己的状态列表，但是二者是同步的。
searcher = constructUserSearcher(*this); 根据命令行参数选择状态选择策略，构造状态选择器Searcher。
!states.empty() && !haltExecution 表示当状态列表不为空或者没有到终止条件（超市等）时循环继续。
ExecutionState &state = searcher->selectState(); 从状态列表中取出1个状态。
executeInstruction(state, ki); 在状态state下执行相关指令 ki（参考Executor::executeInstruction），执行指令的时候是可能产生终止状态的（调用Executor::terminateStateOnExit）以及生成新状态（调用Execute::fork），之后我会详细分析这个函数。
updateStates(&state); 更新状态列表，Executor 和 Searcher 的都会更新。

updateStates 的部分代码如下（精简过）：

void Executor::updateStates(ExecutionState *current) {if (searcher) {searcher->update(current, addedStates, removedStates);}states.insert(addedStates.begin(), addedStates.end());addedStates.clear();for (std::vector<ExecutionState *>::iterator it = removedStates.begin(), ie = removedStates.end(); it != ie; ++it) {ExecutionState *es = *it;std::set<ExecutionState*>::iterator it2 = states.find(es);assert(it2!=states.end());states.erase(it2);delete es;}removedStates.clear();
}

大概意思就是在 Searcher 和 Executor 的状态列表中删除 removedStates 中的state，添加 addStates 中的state。

addStates 是 Executor 的成员变量，在fork的时候会添加状态（参考Executor::branch和Executor::fork）
removedStates 也是 Executor 的成员变量，在（参考Executor::terminateState），只有终止状态会被添加到 removedStates 中。

五.对于符号执行流程的简单探索

在 Executor::run 下插入代码（只有 if (state.constraints.size() < 4) 是插入的代码）：

// main interpreter loopwhile (!states.empty() && !haltExecution) {ExecutionState &state = searcher->selectState();KInstruction *ki = state.pc;// klee_message("next instruction %s \n", ki->inst->getName().data());if (state.constraints.size() < 4) {ki->inst->dump();klee_message("constraint num %lu \n", state.constraints.size());for (ConstraintSet::const_iterator iter = state.constraints.begin();iter != state.constraints.end(); ++iter)iter->get()->dump();klee_message("============================= \n");}stepInstruction(state);executeInstruction(state, ki);timers.invoke();if (::dumpStates) dumpStates();if (::dumpPTree) dumpPTree();updateStates(&state);if (!checkMemoryUsage()) {// update searchers when states were terminated early due to memory pressureupdateStates(nullptr);}}

大概就是每次取出1个状态时打印将要执行的指令以及打印当前状态的约束集合。

测试以下代码

5.1.示例1

主要探索循环语句的影响，源码如下：

#include<klee/klee.h>int main() {int a;klee_make_symbolic(&a, sizeof(a), "a");int i = a;while (i < 5){i++;}
}

LLVM IR：

; ModuleID = 'sample.c'
source_filename = "sample.c"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 {entry:%retval = alloca i32, align 4%a = alloca i32, align 4%i = alloca i32, align 4store i32 0, i32* %retval, align 4%0 = bitcast i32* %a to i8*call void @klee_make_symbolic(i8* %0, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))%1 = load i32, i32* %a, align 4store i32 %1, i32* %i, align 4br label %while.condwhile.cond:                                       ; preds = %while.body, %entry%2 = load i32, i32* %i, align 4%cmp = icmp slt i32 %2, 5br i1 %cmp, label %while.body, label %while.endwhile.body:                                       ; preds = %while.cond%3 = load i32, i32* %i, align 4%inc = add nsw i32 %3, 1store i32 %inc, i32* %i, align 4br label %while.condwhile.end:                                        ; preds = %while.cond%4 = load i32, i32* %retval, align 4ret i32 %4
}declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }!llvm.module.flags = !{!0}
!llvm.ident = !{!1}!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 11.0.0"}

在klee执行的过程中可以发现：

当第1次执行完 br i1 %cmp, label %while.body, label %while.end 后，状态的约束集合添加了1个。
- 如果下一个执行是 %4 = load i32, i32* %retval, align 4，也就是在false branch，添加的约束为 (Eq false (Slt (ReadLSB w32 0 a) 5))，表示 ~(a < 5)（这里 a 是符号值）。
- 如果是 while.body: 中的指令，添加的约束为 (Slt (ReadLSB w32 0 a) 5)，表示 a < 5。
第2次执行完 br i1 %cmp, label %while.body, label %while.end，状态的约束集合又添加了1个。
- 对于false branch（%4 = load i32, i32* %retval, align 4），2个约束分别为 Slt (ReadLSB w32 0 a) 5, (Eq false (Slt (Add w32 1 (ReadLSB w32 0 a)) 5))。分别表示 a < 5, ~((a + 1) < 5)。
- 对于true branch（while.body: 中的），则为 Slt (ReadLSB w32 0 a) 5, (Slt (Add w32 1 (ReadLSB w32 0 a)) 5) 。分别表示 a < 5, (a + 1) < 5。
符号执行会不断进行下去，循环不会停止，除非外部中断。

5.2.示例2

主要探索函数调用的影响，源码如下：

#include <klee/klee.h>int f(int x)
{if (x % 2 == 0)return x / 2;elsereturn 3 * x + 1;
}int main(void)
{int x;klee_make_symbolic(&x, sizeof(x), "x");int a = 0;if (x < 5)a += f(x);elsea += f(x);return 0;
}

LLVM IR

; ModuleID = 'sample.c'
source_filename = "sample.c"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"@.str = private unnamed_addr constant [2 x i8] c"x\00", align 1; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @f(i32 %x) #0 {entry:%retval = alloca i32, align 4%x.addr = alloca i32, align 4store i32 %x, i32* %x.addr, align 4%0 = load i32, i32* %x.addr, align 4%rem = srem i32 %0, 2%cmp = icmp eq i32 %rem, 0br i1 %cmp, label %if.then, label %if.elseif.then:                                          ; preds = %entry%1 = load i32, i32* %x.addr, align 4%div = sdiv i32 %1, 2store i32 %div, i32* %retval, align 4br label %returnif.else:                                          ; preds = %entry%2 = load i32, i32* %x.addr, align 4%mul = mul nsw i32 3, %2%add = add nsw i32 %mul, 1store i32 %add, i32* %retval, align 4br label %returnreturn:                                           ; preds = %if.else, %if.then%3 = load i32, i32* %retval, align 4ret i32 %3
}; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 {entry:%retval = alloca i32, align 4%x = alloca i32, align 4%a = alloca i32, align 4store i32 0, i32* %retval, align 4%0 = bitcast i32* %x to i8*call void @klee_make_symbolic(i8* %0, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))store i32 0, i32* %a, align 4%1 = load i32, i32* %x, align 4%cmp = icmp slt i32 %1, 5br i1 %cmp, label %if.then, label %if.elseif.then:                                          ; preds = %entry%2 = load i32, i32* %x, align 4%call = call i32 @f(i32 %2)%3 = load i32, i32* %a, align 4%add = add nsw i32 %3, %callstore i32 %add, i32* %a, align 4br label %if.endif.else:                                          ; preds = %entry%4 = load i32, i32* %x, align 4%call1 = call i32 @f(i32 %4)%5 = load i32, i32* %a, align 4%add2 = add nsw i32 %5, %call1store i32 %add2, i32* %a, align 4br label %if.endif.end:                                           ; preds = %if.else, %if.thenret i32 0
}declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }!llvm.module.flags = !{!0}
!llvm.ident = !{!1}!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 11.0.0"}

这个示例klee探索了4条路径，其中主程序中fork了1次，2次调用f各fork了1次。

接下来换示例3

5.3.示例3

#include <klee/klee.h>int f(int x){if (x % 2 == 0)return x / 2;elsereturn 3 * x + 1;
}int main(void){int x;klee_make_symbolic(&x, sizeof(x), "x");int a = f(x);if (x < 5)a++;elsea--;return 0;
}

IR就不放了，这次运行klee依旧产生了4个path，首先在 f 调用返回时已经fork成2个状态了，在 f fork的2个状态返回主程序之后又分别在 if (x < 5) 又fork了一次，就这样最后fork成了4个状态，对应4个path。

程序分析-klee工具分析相关推荐

【.NET程序性能分析】使用VS自带的工具分析.NET程序的性能
这篇博文给大家分享的是,如何使用VS自带的性能分析工具来分析我们编写的.NET程序,一边找出程序性能的瓶颈,改善代码的质量.在实际开发中,性能真的很重要,往往决定一个产品的生死~良好的用户体验的基础之 ...
Java程序内存分析：使用mat工具分析内存占用
1. 用jmap生成堆信息 2. 将堆信息导入到mat中分析 3. 生成分析报告 Histogram Dominator Tree Top consumers Leak Suspects MAT 不是 ...
python程序分析,用Python编写分析Python程序性能的工具的教程
用Python编写分析Python程序性能的工具的教程来源:中文源码网浏览: 次日期:2018年9月2日 [下载文档: 用Python编写分析Python程序性能的工具的教程.tx ...
Python 开发工具集：关于文档、测试、调试、程序的优化和分析
Python 开发工具集:关于文档.测试.调试.程序的优化和分析原文 http://segmentfault.com/a/1190000000410521 Python已经演化出了一个广泛的生 ...
小程序积分营销工具| 拆解分析3种裂变营销玩法
裂变营销其实就是小程序积分营销工具.运营流程中的非常常见一环.用白话文来说,其实就是MGM模式,即老用户带新用户,简称"老带新". 在微信裂变营销风靡的几年中,裂变营销的玩法确实是 ...
Linux性能分析命令工具汇总
转自:http://rdc.hundsun.com/portal/article/731.html?ref=myread 出于对Linux操作系统的兴趣,以及对底层知识的强烈欲望,因此整理了这篇文章. ...
200 个工具分析机器学习十年：开源是大势，工程师是核心
[编者按]人工智能和机器学习经过十年多的发展,在过去的几年间,各类工具数量迎来了持续的爆发式的增长,机器学习也正式由科研走进工业生产阶段.本文作者 -- 来自硅谷一家初创公司的计算机科学家 Chip ...
使用MAT(Memory Analyzer Tool)工具分析dump文件--转
原文地址:http://gao-xianglong.iteye.com/blog/2173140?utm_source=tuicool&utm_medium=referral 前言生产环境中 ...
python3 爬虫 requests安装_BOSS直聘招聘信息获取之爬虫工具分析
点击蓝色"不太灵光的程序员"关注我哟加个"星标",每天上午 09:30,干货推送! 文中使用的组件库仅限于Python语言,由于最近收到一些同学的留言说,按照 ...

程序分析-klee工具分析