klee2.3 教程1-2

1. klee2.3 安装

system：unbuntu 20.04

note: llvm-13+klee2.3+z3-4.10

1.1 install dependencies

KLEE 需要 LLVM 的所有依赖项（请参阅此处），以及更多。特别是，您应该安装下面列出的程序和库。graphviz/doxygen是可选的，只需要生成源代码文档。

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

您还应该安装lit以启用测试，tabulate以支持 LLVM 中的其他功能klee-stats并wllvm使其更容易将程序编译为 LLVM 位码：

sudo pip3 install lit wllvm
sudo apt-get install python3-tabulate

1.2 install llvm 13

下载源码安装包https://github.com/llvm/llvm-project/tree/release/13.x，解压。

cd /home/aaa
unzip llvm-project-release-13.x.zip
mv llvm-project-release-13.x llvm-11
cd llvm-13

编译安装。

mkdir build
mkdir install
cd bulid
cmake -G "Unix Makefiles" \
	-DLLVM_ENABLE_PROJECTS="clang" \
	-DLLVM_TARGETS_TO_BUILD=X86 \
	-DCMAKE_BUILD_TYPE="Release" \
	-DCMAKE_INSTALL_PREFIX="/home/aaa/llvm-13/install" \
	../llvm

make -j2
make install
#or
#cmake --build .
#cmake --build . --target install

…/llvm是cmakelist.txt文件的路径。
注释：为什么不直接 make，而是使用 cmake --build 形式的命令，主要是为了跨平台，使用这种形式后，不管你是使用的什么生成器，CMake 都能正确构建，否则如果使用的是 Ninja 或者其他生成器，那 make 就不生效了

1.3 install z3

下载链接：https://github.com/z3prover/z3/tree/z3-4.10.2

unzip z3-z3-4.10.2.zip
mv z3-z3-4.10.2 z3-4.10
cd z3-4.10
mkdir build
mkdir install
cd build 
cmake -G "Unix Makefiles" \
-DCMAKE_INSTALL_PREFIX=/home/aaa/z3-4.10/install \
-DCMAKE_BUILD_TYPE=Release ../

make -j2
sudo make install

1.4 install klee-uclib

下载链接：https://github.com/klee/klee-uclibc

unzip klee-uclibc-klee_0_9_29.zip
mv klee-uclibc-klee_0_9_29.zip klee-ulibc
cd klee-uclibc  
./configure --make-llvm-lib   
make -j2

1.5 陪环境变量

# 打开环境变量文本
sudo gedit ~/.bashrc
# 文本末行加入
export LLVM_DIR=/home/aaa/llvm-13/build
export Z3_DIR=/home/aaa/z3-4.10/
export LLVM_BIN=/home/aaa/llvm-13/install/bin
export Z3_BIN=/home/aaa/z3-4.10/install/bin
export KLEE=/home/aaa/install/bin
export PATH=$PATH:$Z3_BIN:$LLVM_BIN:$Z3_DIR:$LLVM_DIR:$KLEE
# 更新环境变量
source ~/.bashrc

1.6 install klee-2.3

下载原码资源包https://github.com/klee/klee/tree/2.3.x，解压。

unzip klee-2.3.x.zip
mv klee-2.3.x/ klee-2.3
cd kell-2.3

**构建 libc++：**为了能够运行 C++ 代码，您还需要启用对 C++ 标准库的支持。确保它clang++-13在您的路径中。然后，从主 KLEE 源目录运行：

LLVM_VERSION=13 BASE=/home/aaa/llvm-13/libcxx ./scripts/build/build.sh libcxx

CmakeLists add by yx

set(Z3_DIR /home/aaa/z3-4.10/install)
set(Z3_INCLUDE_DIRS /home/aaa/z3-4.10/install/include)
set(Z3_LIBRARIES /home/aaa/z3-4.10/install/lib/libz3.so)

mkdir build
cd build
cmake -DENABLE_SOLVER_Z3=ON  \
       -DENABLE_SOLVER_STP=OFF \
       -DENABLE_POSIX_RUNTIME=ON \
       -DENABLE_UNIT_TESTS=OFF \
       -DCMAKE_BUILD_TYPE=Release \
       -DCMAKE_INSTALL_PREFIX=/home/aaa/klee-2.3/install \
       -DLLVM_CONFIG_BINARY=/home/aaa/llvm-13/install/bin/llvm-config \
       -DENABLE_KLEE_UCLIBC=ON \
       -DKLEE_UCLIBC_PATH=/home/aaa/klee-uclibc \
       -DENABLE_KLEE_LIBCXX=ON \
       -DKLEE_LIBCXX_DIR=/home/aaa/llvm-13/libcxx/libc++-install-130 \
       -DKLEE_LIBCXX_INCLUDE_DIR=/home/aaa/llvm-13/libcxx/libc++-install-130/include/c++/v1 \
       -DENABLE_KLEE_EH_CXX=ON \
       -DKLEE_LIBCXXABI_SRC_DIR=/home/aaa/llvm-13/libcxxabi \
         ..

CmakeLists中有些错误，install/bin里面缺点东西，我们需要copy过去

sudo cp /home/aaa/llvm-13/build/bin/FileCheck FileCheck
sudo cp /home/aaa/llvm-13/build/bin/not not

make编译时，代码报错，可以找到后直接注释掉

在这里插入图片描述

make -j2
make install

1.7 运行回归测试套件

如果 KLEE 配置为启用系统测试，那么您可以像这样运行它们：

$ make systemtests

如果你想lit手动调用使用：

$ lit test/

这样您就可以运行单独的测试或套件的子集：

$ lit test/regression

1.8 构建并运行单元测试

如果 KLEE 配置为启用了单元测试，那么您可以构建并运行单元测试：

$ make unittests

2. 教程一

本教程将引导您完成使用 KLEE 测试简单功能所需的主要步骤。这是我们的简单功能：

int get_sign(int x) {
  if (x == 0)
    return 0;

  if (x < 0)
    return -1;
  else
    return 1;
}

您可以在下的源代码树中找到此示例的完整代码examples/get_sign。也可以在此处访问源代码的一个版本。

2.1 将输入标记为符号

为了用 KLEE 测试这个函数，我们需要在符号输入上运行它。要将变量标记为符号变量，我们使用klee_make_symbolic()函数（在中定义klee/klee.h），该函数接受三个参数：我们要将其视为符号变量的地址（内存位置）、它的大小和名称（可以是任何名称） . 这是一个简单的main()函数，它将变量标记a为符号变量并使用它来调用get_sign()：

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}

2.2 编译为 LLVM 位码

KLEE 在 LLVM 位码上运行。要使用 KLEE 运行程序，首先使用clang -emit-llvm.

从examples/get_sign目录中：

$ clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c

这应该会创建一个get_sign。LLVM位码格式。使用-I参数，编译器可以找到klee/klee.h，其中包含用于与klee虚拟机交互的内在函数的定义，例如klee_make_symbolic。使用-g构建将调试信息添加到位码文件中是很有用的，我们使用该文件生成源行级统计信息。

传递给KLEE的位码不应该被优化，因为我们为KLEE精心挑选了正确的优化，这可以通过KLEE的优化命令行选项启用。然而，在较新的LLVM版本(> 5.0)中，在为KLEE编译时不应该使用-O0零标志，因为它会阻止KLEE进行自己的优化。应该使用-O0 -Xclang -disable-O0-optnone来代替，详情请参阅此问题。

如果你不希望像后面描述的那样重放测试用例，也不关心调试信息和优化，你可以删除klee/klee.h include，然后编译get_sign.c:

$ clang -emit-llvm -c get_sign.c

但是，我们建议使用上面更长的命令。

2.3 运行 KLEE

要在bitcode文件上运行KLEE，只需执行:

$ klee get_sign.bc

您应该看到以下输出:

KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3

这个简单函数有三条路径，一条a为0，一条a小于0，一条a大于0。正如预期的那样，KLEE告诉我们它在程序中探索了三条路径，并为每一条路径生成了一个测试用例。对于较大的程序，由于时间或内存限制，KLEE可能无法探索每条路径直到其结束。在这种情况下，它还告诉我们中断(部分完成)路径的数量。KLEE执行的输出是一个目录(在我们的例子中是KLEE -out-0)，其中包含由KLEE生成的测试用例。KLEE将输出目录命名为KLEE -out-N，其中N是可用的最小值(因此如果我们再次运行KLEE，它将创建一个名为KLEE -out-1的目录)，并为方便起见，还生成了一个名为KLEE -last的符号链接到该目录:

$ ls klee-last/
assembly.ll      run.istats       test000002.ktest
info             run.stats        test000003.ktest
messages.txt     test000001.ktest warnings.txt

如果您想了解KLEE生成的文件的概述，请单击这里。在本教程中，我们只关注由KLEE生成的实际测试文件。

2.4 klee 生成test案例

由KLEE生成的测试用例被写入扩展名为.ktest的文件。这些是二进制文件，可以用ktest-tool实用程序读取。ktest-tool为同一个对象输出不同的表示形式，例如Python字节字符串(data)、整数(int)或ascii文本(text)。让我们来看看每个文件:

$ ktest-tool klee-last/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: ....

$ ktest-tool klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x01\x01\x01\x01'
object 0: hex : 0x01010101
object 0: int : 16843009
object 0: uint: 16843009
object 0: text: ....

$ ktest-tool klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

在每个测试文件中，KLEE报告调用程序时使用的参数(在我们的例子中，除了程序名称本身没有参数)，该路径上符号对象的编号(在我们的例子中只有一个)，符号对象的名称(‘a’)及其大小(4)。实际测试本身由输入值表示:第一个测试为0，第二个测试为16843009，最后一个测试为-2147483648。正如预期的那样，KLEE生成了值0、一个正值(16843009)和一个负值(-2147483648)。现在，我们可以在程序的本机版本上运行这些值，以遍历代码中的所有路径!

2.5 重复一个测试案例

虽然我们可以在程序上手动运行KLEE生成的测试用例(或借助现有测试基础设施)，但KLEE提供了一个方便的重放库，它只是将对klee_make_symbolic的调用替换为对一个函数的调用，该函数将存储在.ktest文件中的值赋给我们的输入。要使用它，只需将程序与libkleeRuntest库链接起来，并设置KTEST_FILE环境变量以指向所需测试用例的名称:

3. 教程二

3.1 测试一个简单的正则表达式库

这是一个使用 KLEE 来测试一个简单的正则表达式匹配函数的例子。您可以在下的源代码树中找到基本示例examples/regexp。

Regexp.c包含一个简单的正则表达式匹配函数，以及main()使用 KLEE 探索此代码所需的基本测试工具（在中）。您可以在此处查看源代码的一个版本。

此示例说明如何使用 KLEE 构建和运行示例，以及如何解释输出，以及在手动编写测试驱动程序时可以使用的一些额外的 KLEE 功能。

我们将首先展示如何构建和运行示例，然后更详细地解释测试工具的工作原理。

3.2 构建示例

第一步是使用可以生成 LLVM 位码格式的目标文件的编译器编译源代码。

从examples/regexp目录中执行：

$ clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone Regexp.c

它应该以 LLVM 位码格式创建一个 Regexp.bc 文件。使用该-I参数以便编译器可以找到 klee/klee.h，其中包含用于与 KLEE 虚拟机交互的内部函数的定义。-c之所以使用，是因为我们只想将代码编译成目标文件（而不是本机可执行文件），并最终-g将额外的调试信息存储在目标文件中，KLEE 将使用这些信息来确定源代码行号信息。-O0 -Xclang -disable-O0-optnone用于在不进行任何优化的情况下进行编译，但不会阻止 KLEE 执行其自身的优化，这与 will 一起编译-O0。

如果您在路径中安装了 LLVM 工具，则可以通过在生成的文件上运行 llvm-nm 来验证此步骤是否有效：

$ llvm-nm Regexp.bc
                 U klee_make_symbolic
---------------- T main
---------------- T match
---------------- t matchhere
---------------- t matchstar

通常，在运行这个程序之前，我们需要链接它来创建一个本地可执行文件。但是，KLEE 直接在 LLVM 位码文件上运行。由于此程序只有一个文件，因此无需链接。对于具有多个输入的“真实”程序，可以使用llvm-link工具代替常规链接步骤，将多个 LLVM 位码文件合并到一个可以由 KLEE 执行的模块中。

3.3 使用 KLEE 执行代码

下一步是使用 KLEE 执行代码（指令数量因 LLVM 版本和优化级别而异）：

$ klee --only-output-states-covering-new Regexp.bc
KLEE: output directory = "klee-out-0"
KLEE: ERROR: Regexp.c:23: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: Regexp.c:25: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 4848112
KLEE: done: completed paths = 6675
KLEE: done: partially completed paths = 763
KLEE: done: generated tests = 16

在启动时，KLEE 打印用于存储输出的目录（在本例中为klee-out-0）。默认情况下，KLEE 将使用第一个空闲klee-out-N目录并创建一个klee-last指向最近创建的目录的符号链接。-output-dir=path您可以使用命令行参数指定用于输出的目录。

当 KLEE 运行时，它会打印“重要”事件的状态消息，例如当它在程序中发现错误时。在这种情况下，KLEE 在我们的测试程序的第 23 行和第 25 行检测到两次无效的内存访问。我们稍后会仔细研究。

最后，当 KLEE 完成执行时，它会打印出一些关于运行的统计信息。在这里我们看到 KLEE 总共执行了约 480 万条指令，探索了 7,438 条路径，并生成了 16 个测试用例。KLEE 仅生成 16 个测试用例，因为我们将测试生成限制为实际覆盖新代码的状态--only-output-states-covering-new。如果我们省略这个标志，KLEE 将创建 6,677 个测试用例！尽管如此，KLEE 并未为每条路径创建测试用例。每当它发现错误时，它都会为到达错误的第一个状态创建一个测试用例。在同一位置到达错误的所有其他路径都将静默终止并报告为部分完成的路径。如果您不介意错误案例的重复，请使用--emit-all-errors为所有 7,438 个路径生成测试案例。

请注意，许多现实程序都有无限（或极大）数量的路径通过它们，并且 KLEE 不会终止是很常见的。默认情况下，KLEE 将一直运行，直到用户按下 Control-C（即 klee 得到一个SIGINT），但还有其他选项可以限制 KLEE 的运行时间和内存使用：

-max-time=<time span>: 在给定的时间后停止执行，例如10min或1h5s。
-max-forks=N：在符号分支后停止分叉N，并运行剩余的路径到终止。
-max-memory=N：尝试将内存消耗限制在N兆字节以内。

3.4 KLEE 错误报告

当 KLEE 在正在执行的程序中检测到错误时，它将生成一个显示错误的测试用例，并将有关错误的一些附加信息写入文件testN.TYPE.err，其中N是测试用例编号，并TYPE标识错误的类型。KLEE 检测到的一些错误类型包括：

ptr：存储或加载无效的内存位置。
free：双倍或无效free()。
中止：调用的程序abort()。
assert：断言失败。
div：检测到除以零的除法或模数。
用户：输入有问题（无效的 klee 内部调用）或 KLEE 的使用方式。
exec : 有一个问题阻止了 KLEE 执行程序；例如未知指令、对无效函数指针的调用或内联汇编。
模型：KLEE 无法保持完全精确，只能探索部分程序状态。例如，目前不支持 malloc 的符号大小，在这种情况下，KLEE 将具体化参数。

KLEE检测到错误时会向控制台打印一条消息，在上面的测试运行中我们可以看到KLEE检测到两个内存错误。.err对于所有程序错误，KLEE 将在文件中写入一个简单的回溯。这是上面的错误之一：

Error: memory error: out of bound pointer
File: .../klee/examples/regexp/Regexp.c
Line: 23
Stack:
  #0 00000146 in matchhere (re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:23
  #1 00000074 in matchstar (c, re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #2 00000172 in matchhere (re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #3 00000074 in matchstar (c, re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #4 00000172 in matchhere (re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #5 00000074 in matchstar (c, re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #6 00000172 in matchhere (re=14816465, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #7 00000231 in matchhere (re=14816464, text=14815300) at .../klee/examples/regexp/Regexp.c:30
  #8 00000280 in match (re=14816464, text=14815296) at .../klee/examples/regexp/Regexp.c:38
  #9 00000327 in main () at .../klee/examples/regexp/Regexp.c:59
Info:
  address: 14816471
  next: object at 14816624 of size 4
  prev: object at 14816464 of size 7

回溯的每一行都列出了帧号、指令行（这是assembly.ll与运行输出一起找到的文件中的行号）、函数和参数（包括具体参数的值）以及源信息。

特定的错误报告还可能包含其他信息。对于内存错误，KLEE 将显示无效地址，以及该地址前后堆上的对象。在这种情况下，我们可以看到地址恰好是前一个对象末尾后的一个字节。

3.5 更换测试线束

KLEE 在此程序中发现内存错误的原因不是因为正则表达式函数有错误，而是表明我们的测试驱动程序存在问题。问题是我们正在使输入正则表达式缓冲区完全符号化，但匹配函数期望它是一个以空字符结尾的字符串。让我们看看解决这个问题的两种方法。

解决此问题的最简单方法是在将其符号化后将“\0”存储在缓冲区的末尾。这使我们的驱动程序看起来像这样：

int main() {
  // The input regular expression.
  char re[SIZE];

  // Make the input symbolic.
  klee_make_symbolic(re, sizeof re, "re");
  re[SIZE - 1] = '\0';

  // Try to match against a constant string "hello".
  match(re, "hello");

  return 0;
}

使缓冲区符号化只是初始化内容以引用符号变量，我们仍然可以随意修改内存。如果你在这个测试程序上重新编译并运行 klee，内存错误现在应该消失了。

实现相同效果的另一种方法是使用klee_assume内在函数。klee_assume接受一个参数（一个无符号整数），通常应该是某种条件表达式，并“假设”该表达式在当前路径上为真（如果这永远不会发生，即表达式可证明为假，KLEE 将报告一个错误）。

我们可以使用klee_assume这样的驱动程序来使 KLEE 仅探索字符串为 null 终止的状态：

int main() {
  // The input regular expression.
  char re[SIZE];

  // Make the input symbolic.
  klee_make_symbolic(re, sizeof re, "re");
  klee_assume(re[SIZE - 1] == '\0');

  // Try to match against a constant string "hello".
  match(re, "hello");

  return 0;
}

在此特定示例中，两种解决方案都可以正常工作，但通常klee_assume更灵活：

通过显式声明约束，这将强制测试用例包含'\0'其中。在第一个示例中，我们显式地写入终止空值，符号输入的最后一个字节是什么并不重要，KLEE 可以自由生成任何值。在某些您想手动检查测试用例的情况下，测试用例显示所有重要的值会更方便。
klee_assume可用于编码更复杂的约束。例如，我们可以使用klee_assume(re[0] != '^')让 KLEE 只探索第一个字节不是的状态'^'。

注意klee_assume：在多个条件下使用时有一个重要警告。请记住，布尔条件语句如'&&'and'||'可能会被编译成在计算表达式结果之前分支的代码。在这种情况下，KLEE 会在调用之前对流程进行分支klee_assume，这可能会导致探索不必要的额外状态。出于这个原因，最好使用尽可能简单的表达式klee_assume（例如将单个调用拆分为多个），并使用'&'and'|'运算符而不是短路运算符。