安装依赖

for ubuntu

1

sudo apt-get install build-essential curl libcap-dev git cmake libncurses5-dev python-minimal python-pip unzip libtcmalloc-minimal4 libgoogle-perftools-dev libsqlite3-dev doxygen

for ubuntu >= 18.04

1

sudo apt-get install python3 python3-pip gcc-multilib g++-multilib

查看ubuntu版本

1

cat /etc/lsb-release

安装lit以启用测试，tabulate支持klee-stats和wllvm中的其他功能，以便更容易将程序编译到LLVM位码

1

pip3 install lit tabulate wllvm

安装 llvm9

1

sudo apt-get install clang-9 llvm-9 llvm-9-dev llvm-9-tools

安装约束求解器

任选其一

  • STP(recommend)
  • Z3
  • metaSTM

STP

外部依赖

1

sudo apt-get install cmake bison flex libboost-all-dev python perl zlib1g-dev minisat

安装STP

1
2
3
4
5
6
7
8

git clone https://github.com/stp/stp.git
cd stp
git checkout tags/2.3.3
c
cd build
cmake ..
make -j
sudo make install

在对更大的基准运行带有STP的KLEE之前，必须将堆栈的大小设置为非常大的值

可以写到 .bashrc 持久化

1

ulimit -s unlimited

获取KLEE

1

git clone https://github.com/klee/klee.git

配置KLEE

1
2

mkdir build
cd build

配置选项

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

cmake \
  -DENABLE_SOLVER_STP=ON \
  -DENABLE_POSIX_RUNTIME=ON \
  -DENABLE_KLEE_UCLIBC=ON \
  -DKLEE_UCLIBC_PATH=<KLEE_UCLIBC_SOURCE_DIR> \
  -DENABLE_UNIT_TESTS=ON \
  -DGTEST_SRC_DIR=<GTEST_SOURCE_DIR> \
  -DLLVM_CONFIG_BINARY=<PATH_TO_llvm-config-9> \
  -DLLVMCC=<PATH_TO_clang-9> \
  -DLLVMCXX=<PATH_TO_clang++-9> \
  <KLEE_SRC_DIRECTORY>

1
2
3
4
5
6
7
8

cmake \
  -DENABLE_SOLVER_STP=ON \
  -DENABLE_POSIX_RUNTIME=ON \
  -DENABLE_KLEE_UCLIBC=ON \
  -DKLEE_UCLIBC_PATH=/home/eveneko/Workspace/klee-uclibc \
  -DENABLE_UNIT_TESTS=OFF \
  -DENABLE_SYSTEM_TESTS=OFF \
  /home/eveneko/Workspace/klee

默认选项，这些选项不包括对uClibC和POSIX运行时的支持

1

cmake ..

Build KLEE

1

make -j

Example

get_sign

1
2
3

# examples/get_sign

clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c
  • clang -emit-llvm 将其编译为LLVM位码
  • -I 参数是为了让编译器可以找到klee/klee.h
  • -g 构建以向位码文件添加调试信息非常有用，我们使用位码文件生成源线级统计信息。
  • -O0 -Xclang -disable-O0-optnone 传递给KLEE的位码不应该优化，因为我们手工为KLEE挑选了正确的优化。在较新的LLVM版本（>5.0）中，为KLEE编译时不应使用-O0零标志，因为它阻止KLEE进行自己的优化。

运行KLEE

1

klee get_sign.bc

KLEE生成的测试用例

1

ktest-tool klee-last/test000001.ktest

regexp

1

clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone Regexp.c
  • -c 是因为我们希望将代码编译到对象文件（而不是本机可执行文件）

llvm-nm来验证此步骤是否有效

1

llvm-nm Regexp.bc

通常，在运行此程序之前，我们需要链接它才能创建本机可执行文件。然而，KLEE直接在LLVM位码文件上运行。

由于此程序只有一个文件，因此无需链接。

对于具有多个输入的“真实”程序，可以使用llvm链接工具代替常规链接步骤，将多个LLVM位码文件合并到一个模块中，该模块可以由KLEE执行。

使用KLEE执行代码

1

klee --only-output-states-covering-new Regexp.bc
  • --only-output-states-covering-new 将测试生成限制在实际覆盖新代码的状态。
  • --emit-all-errors 为所有路径生成测试用例。

默认情况下，KLEE将运行到用户按下Control-C 停止。

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

Coreutils

使用gcov构建coreutils

1
2
3
4
5
6
7

coreutils-6.11$ mkdir obj-gcov
coreutils-6.11$ cd obj-gcov
obj-gcov$ ../configure --disable-nls CFLAGS="-g -fprofile-arcs -ftest-coverage"
... verify that configure worked ...
obj-gcov$ make
obj-gcov$ make -C src arch hostname
... verify that make worked ...
  • --disable-nls 因为这在C库中添加了许多我们不感兴趣的额外初始化
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

obj-gcov$ cd src
src$ ls -l ls echo cat
-rwxrwxr-x 1 klee klee 150632 Nov 21 21:58 cat
-rwxrwxr-x 1 klee klee 135984 Nov 21 21:58 echo
-rwxrwxr-x 1 klee klee 390552 Nov 21 21:58 ls
src$ ./cat --version
cat (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.

在gcov支持下构建

我们可以使用gcov工具本身生成人类可读的覆盖信息形式

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

src$ rm -f *.gcda # Get rid of any stale gcov files
src$ ./echo**

src$ ls -l echo.gcda
-rw-rw-r-- 1 klee klee 896 Nov 21 22:00 echo.gcda
src$ gcov echo
File '../../src/echo.c'
Lines executed:24.27% of 103
Creating 'echo.c.gcov'

File '../../src/system.h'
Lines executed:0.00% of 3
Creating 'system.h.gcov'

安装WLLVM

1

pip install --upgrade wllvm

要成功执行WLLVM，必须将环境变量LLVM_COMPILER设置为底层LLVM编译器（dragonegg或clang）

1

export LLVM_COMPILER=clang

使用LLVM构建Coreutils

1
2
3
4
5
6
7

coreutils-6.11$ mkdir obj-llvm
coreutils-6.11$ cd obj-llvm
obj-llvm$ CC=wllvm ../configure --disable-nls CFLAGS="-g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES  -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__"
... verify that configure worked ...
obj-llvm$ make
obj-llvm$ make -C src arch hostname
... verify that make worked ...

coreutils 可执行文件

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

obj-llvm$ cd src
src$ ls -l ls echo cat
-rwxrwxr-x 1 klee klee 105448 Nov 21 12:03 cat
-rwxrwxr-x 1 klee klee  95424 Nov 21 12:03 echo
-rwxrwxr-x 1 klee klee 289624 Nov 21 12:03 ls
src$ ./cat --version
cat (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.

我们获得的不是LLVM位码文件，而是可执行文件。

要获取所有Coreutils的LLVM位码版本，我们可以在所有可执行文件上调用extract-bc：

1
2
3

src$ find . -executable -type f | xargs -I '{}' extract-bc '{}'
src$ ls -l ls.bc
-rw-rw-r-- 1 klee klee 543052ls Nov 21 12:03 ls.bc

使用KLEE作为解释器

1

klee --libc=uclibc --posix-runtime  ./cat.bc --version

向应用程序介绍符号数据

1

klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3

获得KLEE内部统计数据的简短摘要

1

klee-stats klee-last

运行LLVM优化传递

1

klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3

重播KLEE生成的测试用例

1

klee-replay ./echo ../../obj-llvm/src/klee-last/test000001.ktest

Reference