该实例是用KLEE测试Gun CoreUtils，之前一直有问题，这段时间想在grep的编译生成上，忘记改什么了，反正可以用了。
该实例的应用假定你已经在编译KLEE时正确引用了uclibc和posix运行支持。实际上我也不知道当时怎么搞得。
步骤1：利用gcov构造CoreUtils
首先下载 coreutils，本例用的是版本6.11。gcov（GCC Coveage）是一个测试代码覆盖率的工具，配合Gcc共同实现对C/C++文件的语句覆盖和分支覆盖进行测试。其使用就是在通过参数”-fprofile-arcs -ftest-coverage“告诉编译器生成gcov需要的额外信息，并在目标文件中插入gcov需要的extra profiling information。因此，该命令在生成可执行文件test的同时生成.gcno文件(gcov note文件)。之后可以用命令解读该文件，或者直接查看该文件。编译为支持gcov的目的是在后面可以和KLEE产生的覆盖统计相对比，具体的编译生成命令如下：
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 ...成功完成后可以进入src目录运行编译生成的代码，如下：
obj-gcov$ cd src src$ ls -l ls echo cat -rwxr-xr-x 1 ddunbar ddunbar 164841 2009-07-25 20:58 cat -rwxr-xr-x 1 ddunbar ddunbar 151051 2009-07-25 20:59 echo -rwxr-xr-x 1 ddunbar ddunbar 439712 2009-07-25 20: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.在运行中会生成.gcda文件，包含对程序运行情况的统计。也可以用gcov工具生成可阅读的格式。例如
src$ rm -f *.gcda # Get rid of any stale gcov files src$ ./echo** src$ ls -l echo.gcda -rw-r--r-- 1 ddunbar ddunbar 1832 2009-08-04 21:14 echo.gcda src$ gcov echo File '../../src/system.h' Lines executed:0.00% of 47 ../../src/system.h:creating 'system.h.gcov' .......步骤2：利用LLVM构造 Coreutils
这里使用klee-gcc进行编译。命令如下：
coreutils-6.11$ mkdir obj-llvm coreutils-6.11$ cd obj-llvm obj-llvm$ ../configure --disable-nls CFLAGS="-g" ... verify that configure worked ... obj-llvm$ make CC=/full/path/to/klee/scripts/klee-gcc obj-llvm$ make -C src arch hostname CC=/full/path/to/klee/scripts/klee-gcc ... verify that make worked ...成功后，可以在src文件夹下面看到每一个命令会有三个文件，例如cat会有cat、cat.bc、cat.o。其中cat.bc是llvm格式的二进制代码，没有通过连接生成可执行文件，不过可以利用KLEE命令解释执行。
下面运行一个cat程序：
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. LLVM ERROR: JIT does not support inline asm!cat文件并不是真正连接生成的可执行文件，而是一个sh文件，cat打开就可以看到，他实际是利用lli解释执行，如下例：
src$ cat ls #!/bin/sh lli=${LLVMINTERP-lli} exec $lli \ -load=/usr/lib/librt.so \ ls.bc ${1+"$@"} src$ ls -l ls.bc -rwxr-xr-x 1 ddunbar ddunbar 643640 2009-07-25 23:38 ls.bc步骤3：利用KLEE解释执行
除了可以利用上述方式直接执行（实际上也是利用llvm解释执行），还可以利用klee执行。使用命令如下：
src$ klee --libc=uclibc --posix-runtime ./cat.bc --version KLEE: NOTE: Using model: /home/ddunbar/public/klee/Release/lib/libkleeRuntimePOSIX.bca KLEE: output directory = "klee-out-3" KLEE: WARNING: undefined reference to function: __signbitl KLEE: WARNING: executable has module level assembly (ignoring) KLEE: WARNING: calling external: syscall(54, 0, 21505, 177325672) KLEE: WARNING: calling __user_main with extra arguments. KLEE: WARNING: calling external: getpagesize() KLEE: WARNING: calling external: vprintf(177640072, 183340048) cat (GNU coreutils) 6.11 ...... KLEE: done: total instructions = 259357 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1基本格式是：klee klee的参数 要运行的程序 程序参数。运行正常的程序链接的是C库，在这里的例子中是直接运行LLVM bitcode，为了提高效率，需要为程序制定外部调用所用的函数，这里利用 --libc=uclibc指定所要使用的库； --posix-runtime则是指定posix runtime为运行的操作系统基础。
运行过程中出现一些警告信息，意味着相关函数找不到，影响不大。具体参考原文。
步骤4：引入符号数据进行程序运行
从上面步骤可以看到，KLEE能够解释执行一个程序，但是KLEE的真正目的是为了能够让部分输入符号化，从而可以更加全面和精准的穷举程序运行。下面以echo应用为例说明这一过程。
在使用UClibc和Posix作为运行时库的支持时，KLEE替换程序的main()函数为一个特定的函数klee_init_env()，该函数能够提供一些运行库的支持。该函数对正常命令输入进行了一定的修改，特别是构造符号参数的支持。例如为echo提供--help参数，运行如下：
src$ klee --libc=uclibc --posix-runtime ./echo.bc --help ... usage: (klee_init_env) [options] [program arguments] -sym-arg - 符号化参数长度为N -sym-args - 替换最少Min个参数，最多Max个，每个参数最大长度为N -sym-files - 让stdin最大可以为NUM个符号文件，每个文件最大N. -sym-stdout - 设置输出符号化. -max-fail - 设定允许的植入失败个数 -fd-fail - 快捷方式指向设定'-max-fail 1' ...从这个运行可以看出，他返回的结果不是echo --help的运行结果（真实结果是回显--help），而是新替换的函数的help。告诉你如何使用，设置echo的符号化允许参数。
应用例：设置--sym-args 3，也就是设置参数符号化的最大字符个数为3（As an example, lets run echo with a symbolic argument of 3 characters）
src$ klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3 KLEE: NOTE: Using model: /home/ddunbar/public/klee/Release/lib/libkleeRuntimePOSIX.bca KLEE: output directory = "klee-out-16" KLEE: WARNING: undefined reference to function: __signbitl KLEE: WARNING: executable has module level assembly (ignoring) ... ... Copyright (C) 2008 Free Software Foundation, Inc. KLEE: done: total instructions = 300193 KLEE: done: completed paths = 25 KLEE: done: generated tests = 25显示结果表明KLEE探测了25条路径，各条路径输出混合在一起，但是从中可以看出除了回显各种随机符号外，也输出了一些文本块。例如--v输出版本，--h输出帮助等等。
利用klee-stats可以看到KLEE的一个运行情况总结，具体命令和结果如下，当然这里列出的结果有可能和你的运行有些区别。
src$ klee-stats klee-last ------------------------------------------------------------------------- | Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | Solver(%) | ------------------------------------------------------------------------- | klee-last | 300673 | 1.47 | 28.18 | 17.37 | 28635 | 5.65 | -------------------------------------------------------------------------其中ICov表示LLVM指令覆盖情况，BCov表示分支的覆盖情况。这个值的分母包括所调用库中的相关代码，所以看起来覆盖率很低，当然也可以在KLEE中设置--optimize参数改善这一情况，KLEE会去掉一些Dead code。设置了--optimize后运行结果如下：
src$ klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3 ... KLEE: done: total instructions = 123251 KLEE: done: completed paths = 25 KLEE: done: generated tests = 25 src$ klee-stats klee-last ------------------------------------------------------------------------- | Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | Solver(%) | ------------------------------------------------------------------------- | klee-last | 123251 | 0.32 | 38.02 | 25.43 | 9531 | 29.66 | -------------------------------------------------------------------------步骤5：利用kcachegrind查看结果（图形化的一款工具）
略
步骤6： 利用klee-replay好kest******数据重现某次执行
略
