使用#

klee因为其复杂性，依赖比较多。除了llvm,cmake之类的通用依赖之外，还需要为其编译SAT求解器minisat和SMT求解器stp。因此为了简洁使用，可以通过官方提供的docker来使用，通过以下命令即可使用。

docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee:3.0

docker start -aiklee_container

shell

KLEE 在 LLVM 位码上运行。要使用 KLEE 运行程序，首先使用将其编译为 LLVM 位码clang -emit-llvm。

clang -I ../klee_build/include -emit-llvm -g -O0 -Xclang -disable-O0-optnone -c test.c -o test.bc

运行 KLEE#

要在位码文件上运行 KLEE，只需执行：

$ klee get_sign.bc

bash

应该看到类似以下输出：

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

bash

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

KLEE 生成的测试用例#

KLEE 生成的测试用例被写入名为.ktest扩展的文件中。这些是二进制文件，可以使用_ktest-tool_实用程序读取。ktest -tool_输出同一对象的不同表示形式，例如 Python 字节字符串（数据）、整数（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: ....

执行测试用例#

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

$ export LD_LIBRARY_PATH=path-to-klee-build-dir/lib/:$LD_LIBRARY_PATH
$ gcc -I ../../include -L path-to-klee-build-dir/lib/ get_sign.c -lkleeRuntest
$ KTEST_FILE=klee-last/test000001.ktest ./a.out
$ echo $?
0
$ KTEST_FILE=klee-last/test000002.ktest ./a.out
$ echo $?
1
$ KTEST_FILE=klee-last/test000003.ktest ./a.out
$ echo $?
255

KLEE 的符号执行引擎确实支持浮点数（如 float 和 double 类型），但是其处理能力是有限的。KLEE 原生并不完全支持浮点数的符号执行，尤其是在精确度和操作的复杂度上，可能会遇到一些困难。这是因为符号执行主要设计时主要针对整数类型的符号执行进行了优化，而浮点数涉及的数值范围、舍入误差等问题，使得其符号执行变得更加复杂。

KLEE 对浮点数的处理

符号执行支持： KLEE 确实能够进行浮点数的符号执行，但在浮点数计算时，其对某些操作（如浮点比较、算术运算等）可能没有与整数运算一样的精确支持。这意味着 KLEE 在遇到浮点数时可能无法像处理整数那样精确地模拟计算过程，特别是在符号约束（symbolic constraints）和符号路径（symbolic path）上。
浮点数具体化（Concretization）：如果 KLEE 遇到无法精确符号执行的浮点数表达式，它通常会将浮点数的值“具体化”为一个常数（如 0）。例如，如果代码中涉及到浮点数的算术运算或比较，KLEE 可能会将浮点数的值设置为一个默认的数值（通常是 0），以避免符号执行失败。
浮点数操作的精度问题：浮点数计算涉及舍入误差和精度问题，这对于符号执行来说是一个挑战。KLEE 在浮点数计算时可能无法精确模拟这些操作，尤其是对于复杂的浮点数函数（如三角函数、对数等）来说，符号执行的表现可能不如整数。
浮点数的优化和支持： KLEE 团队已经进行了一些优化，尤其是在浮点数符号执行方面。具体来说，KLEE 使用了一个叫 SymFPU 的浮点数支持库，来改进对浮点数操作的处理。SymFPU 是一个专门用于浮点数符号执行的模块，它能够处理浮点数的符号执行，尤其是在有限的操作和函数支持上有所改进。

KLEE 使用

使用#

运行 KLEE#

KLEE 生成的测试用例#

执行测试用例#