本文为看雪论坛优秀文章
看雪论坛作者ID：bigeast
2.1 KLEE的用法
llvm-gcc --emit-llvm -c tr.c -o tr.bcklee --max-time 2 --sym-args 1 10 10--sym-files 2 2000 --max-fail 1 tr.bc
--sym-args 1 10 10：表示使用0至3个命令行参数，第一个参数是一字符长，剩下两个是10字符长。
--sym-files 2 2000：表示使用标准输入和一个文件，每个数据包含2000字节的符号数据。
--max-fail 1：选项表示每个程序路径最多一个系统调用失败。
示例程序1 : void expand(char *arg, unsigned char *buffer) { 82 : int i, ac; 93 : while (*arg) { 10*4 : if (*arg == ’\’) { 11*5 : arg++;6 : i = ac = 0;7 : if (*arg >= ’0’ && *arg <= ’7’) {8 : do {9 : ac = (ac << 3) + *arg++ − ’0’;10: i++;11: } while (i<4 && *arg>=’0’ && *arg<=’7’);12: *buffer++ = ac;13: } else if (*arg != ’’)14: *buffer++ = *arg++;15: } else if (*arg == ’[’) { 12*16: arg++; 1317: i = *arg++; 1418: if (*arg++ != ’-’) { 15!19: *buffer++ = ’[’;20: arg −= 2;21: continue;22: }23: ac = *arg++;24: while (i <= ac) *buffer++ = i++;25: arg++; /* Skip ’]’ */26: } else27: *buffer++ = *arg++;28: }29: }30: . . .31: int main(int argc, char* argv[ ]) { 132: int index = 1; 233: if (argc > 1 && argv[index][0] == ’-’) { 3*34: . . . 435: } 536: . . . 637: expand(argv[index++], index); 738: . . .39: }
2.2 KLEE符号执行的具体过程
klee --max-time 2 --sym-args 1 10 10--sym-files 2 2000 --max-fail 1 tr.bc
[ "" ""3.The KLEE Architecture
3.1 Basic architecture
%dst = add i32 %src0, %src1%src1)到%dst寄存器。为了提高效率，构建表达式的代码会检查是否所有给定的操作数都是具体的（即常数），如果是，则在直接执行该操作，并返回一个常量表达式。即如果操作数是1和2则返回3给%dst寄存器。
条件分支采用一个布尔表达式（分支条件），并根据该条件是为真还是false来更改该状态的指令指针。KLEE会去调用约束求解器去求解这个表达式，以确定分支条件在当前路径上是可满足的还是不可满足的；如果有一条路径是不可满足的，则指令指针将更新到适当的位置。否则，如果这两个分支都是可能的：KLEE克隆状态，以便它可以探索这两条路径，并且更新每个路径上的指令指针和路径条件。
存在潜在危险的操作指令会隐式地生成分支去检查是否存在可能导致错误的输入值。例如，一个除法指令生成一个检查零除数的分支。这些分支与正常分支相同。当检查成功，即检测出错误的时候，会继续执行条件为假的路径，也就是添加相反的约束，比如使得除数不为0的约束。此外，还会为错误生成测试样例，并且终止检测出错误的状态。
与其他危险操作一样，加载和存储指令也会生成检查：在这种情况下，要检查地址是否在有效内存对象的范围内。然而，加载和存储操作还存在额外的复杂性。所选代码所使用的内存的最直接的表示方式将是一个平面字节数组。在这种情况下，加载和存储会简单的映射成数组读表达式和写表达式。
许多操作比如边界检查，对象级的copy-on-write）需要对象特定的信息。如果一个指针指向很多对象，这些操作就很难实现。为了简化实现，KLEE用以下方式回避了这个问题。当一个解引用的指针p指向N个对象时，KLEE复制当前状态N次。在每个状态，KLEE限制指针p在其对象的边界内，然后实现读或写操作。虽然这个方法对于有很大points-to 集合的指针的开销很大，但实际情况中，大部分的符号指针只指向1个对象，所以这个优化还是可以的。（没太看懂，为什么一个指针会被指向很多个对象？）
3.2 Compact state representation（紧凑状态表示）
由于KLEE保存所有内存对象，因此它可以在对象级别（而不是页面粒度）上实现对写的复制，从而大大减少了每个状态的内存需求。通过将堆实现为不可变映射，堆结构的一些部分也可以在多个状态之间共享(类似于fork()的共享部分页表)。此外，这个堆结构可以在恒定的时间内被复制，考虑到这个操作的频率，这很重要。
3.3 Query optimization（查询优化）
x+0改成x,x*2^n改成x<<n2*x-x改成x
x<10x=5隐式的值具体化：例如当一个约束
x+1=10约束的独立性（名字取自EXE）：根据约束集所引用的符号变量，将约束集划分为不相交的独立子集。通过显式地跟踪这些子集，KLEE可以在向约束求解器发送查询之前消除不相关的约束。例如，给定约束集。
Counter-example Cache：冗余查询非常频繁，而一个简单的缓存可以有效地减少大量的冗余查询由于约束集的特定结构，需要构建一个更复杂的缓存。Counter-example Cache将约束集映射counter-examples（即变量分配），以及在一组约束没有解决方案时使用的特殊哨兵。这个cache存储在一个自定义数据结构中——该结构来自Hoffmann和Hoehler[28]提出的UBTree结构，它能有效地搜索约束集的子集和超集的缓存条目。通过以这种方式存储缓存，counter-examples有三种方式减少查询。
例如，我们假设 counter-example cashe有下面两个条目：
{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的解约束集{i<10，j=8，i！=3}的解还是i→5，j→8。实验结果：
3.4 state scheduling
3.41 Random Path Selection
这个方法偏爱在分支中的较高的state。因为这些states对其符号输入的约束较少，因此有更大的自由来获取未覆盖的代码。第二，可以避免饥饿（当程序进入包含符号约束的循环时，会有路径fork爆炸）。
3.42 Coverage-Optimized Search
4 Environment Modeling环境建模
在虚拟机Ubuntu20.04中安装KLEE
安装一些必备工具
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 doxygensudo apt-get install python3 python3-pip gcc-multilib g++-multilibbigeast@ubuntu:~$ locate pip3/usr/local/lib/python3.6/dist-packages/bin/pip3/usr/local/lib/python3.6/dist-packages/bin/pip3.6/usr/share/man/man1/pip3.1.gz
sudo ln -s /usr/local/lib/python3.6/dist-packages/bin/pip3.6 /usr/local/bin/pip3pip3 install lit tabulate wllvmsudo apt-get install clang-9 llvm-9 llvm-9-dev llvm-9-tools安装Z3约束求解器
git clone https://github.com/Z3Prover/z3.gitcd z3/python scripts/mk_make.pysudo make install
（可选）构建 uClibc 和 POSIX 环境模型（macOS 不支持）
bigeast@ubuntu:~$ git clone https://github.com/klee/klee-uclibc.gitbigeast@ubuntu:~$ cd klee-uclibcbigeast@ubuntu:~/klee-uclibc$ ./configure --make-llvm-libINFO:Disabling assertionsINFO:Configuring for Debug buildINFO:Configuring for LLVM bitcode archiveINFO:Using llvm-config at...NoneERROR:llvm-config cannot be found
./configure --make-llvm-lib --with-llvm-config /usr/bin/llvm-config-9（可选）获取 Google 测试源：
curl -OL https://github.com/google/googletest/archive/release-1.7.0.zipunzip release-1.7.0.zip
安装gcc9
sudo add-apt-repository ppa:ubuntu-toolchain-r/testsudo apt-get updatesudo apt-get install gcc-9 g++-9
bigeast@ubuntu:~/klee-2.1$ sudo LLVM_VERSION=9 SANITIZER_BUILD= BASE=/usr/include/c++/9 REQUIRES_RTTI=1 DISABLE_ASSERTIONS=1 ENABLE_DEBUG=0 ENABLE_OPTIMIZED=1 ./scripts/build/build.sh libcxxDetected OS: linuxOS=linuxDetected distribution: ubuntuDISTRIBUTION=ubuntuDetected version: 18.04DISTRIBUTION_VER=18.04Component sanitizer not found.Component sanitizer not found.Already installed llvm/usr/bin/llvm-config-9Already installed clangCMake Error at /usr/share/cmake-3.10/Modules/CMakeDetermineCCompiler.cmake:48 (message):Could not find compiler set in environment variable CC:wllvm.Call Stack (most recent call first):CMakeLists.txt:49 (project)CMake Error: CMAKE_C_COMPILER not set, after EnableLanguageCMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguageCMake Error: CMAKE_ASM_COMPILER not set, after EnableLanguage-- Configuring incomplete, errors occurred!See also "/usr/include/c++/9/libc++-build-9/CMakeFiles/CMakeOutput.log".make: *** No rule to make target 'cxx'. Stop.
bigeast@ubuntu:~/klee-2.1$ sudo -H python3 -m pip install wllvmbigeast@ubuntu:~/klee-2.1$ sudo LLVM_VERSION=9 SANITIZER_BUILD= BASE=/usr/include/c++/9 REQUIRES_RTTI=1 DISABLE_ASSERTIONS=1 ENABLE_DEBUG=0 ENABLE_OPTIMIZED=1 ./scripts/build/build.sh libcxxmkdir buildcd buildcmake-DENABLE_POSIX_RUNTIME=ON-DENABLE_KLEE_UCLIBC=ON-DENABLE_KLEE_LIBCXX=ON-DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/-DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/-DENABLE_KLEE_EH_CXX=ON-DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/-DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/-DENABLE_UNIT_TESTS=ON-DENABLE_SYSTEM_TESTS=ON-DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/-DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9-DLLVMCC=/usr/bin/clang-9-DLLVMCXX=/usr/bin/clang++-9-DCMAKE_C_COMPILER=clang-DCMAKE_CXX_COMPILER=clang++..
bigeast@ubuntu:~/klee-2.1/build$ cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/ -DENABLE_UNIT_TESTS=ON -DENABLE_SYSTEM_TESTS=ON -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/ -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 -DLLVMCC=/usr/bin/clang-9 -DLLVMCXX=/usr/bin/clang++-9 -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ ..-- The CXX compiler identification is unknown-- The C compiler identification is unknownCMake Error at CMakeLists.txt:43 (project):The CMAKE_CXX_COMPILER:clang++is not a full path and was not found in the PATH.Tell CMake where to find the compiler by setting either the environmentvariable "CXX" or the CMake cache entry CMAKE_CXX_COMPILER to the full pathto the compiler, or to the compiler name if it is in the PATH.CMake Error at cmake/cxx_flags_override.cmake:24 (message):Overrides not set for compilerCall Stack (most recent call first):/usr/share/cmake-3.10/Modules/CMakeCXXInformation.cmake:89 (include)CMakeLists.txt:43 (project)CMake Error at CMakeLists.txt:43 (project):The CMAKE_C_COMPILER:clangis not a full path and was not found in the PATH.Tell CMake where to find the compiler by setting either the environmentvariable "CC" or the CMake cache entry CMAKE_C_COMPILER to the full path tothe compiler, or to the compiler name if it is in the PATH.-- Configuring incomplete, errors occurred!See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeOutput.log".See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeError.log".
bigeast@ubuntu:~/klee-2.1/build$ cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/ -DENABLE_UNIT_TESTS=ON -DENABLE_SYSTEM_TESTS=ON -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/ -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 -DLLVMCC=/usr/bin/clang-9 -DLLVMCXX=/usr/bin/clang++-9 -DCMAKE_C_COMPILER=clang-9 -DCMAKE_CXX_COMPILER=clang++-9 ..-- The CXX compiler identification is Clang 9.0.0-- The C compiler identification is Clang 9.0.0-- Check for working CXX compiler: /usr/bin/clang++-9-- Check for working CXX compiler: /usr/bin/clang++-9 -- works-- Detecting CXX compiler ABI info-- Detecting CXX compiler ABI info - done-- Detecting CXX compile features-- Detecting CXX compile features - done-- Check for working C compiler: /usr/bin/clang-9-- Check for working C compiler: /usr/bin/clang-9 -- works-- Detecting C compiler ABI info-- Detecting C compiler ABI info - done-- Detecting C compile features-- Detecting C compile features - done-- KLEE version 2.1-- CMake generator: Unix Makefiles-- CMAKE_BUILD_TYPE is not set. Setting default-- The available build types are: Debug;Release;RelWithDebInfo;MinSizeRel-- Build type: RelWithDebInfo-- KLEE assertions enabled-- LLVM_CONFIG_BINARY: /usr/bin/llvm-config-9-- LLVM_PACKAGE_VERSION: "9.0.0"-- LLVM_VERSION_MAJOR: "9"-- LLVM_VERSION_MINOR: "0"-- LLVM_VERSION_PATCH: "0"-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"-- LLVM_ENABLE_ASSERTIONS: "ON"-- LLVM_ENABLE_EH: "OFF"-- LLVM_ENABLE_RTTI: "ON"-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"-- Looking for bitcode compilers-- Found /usr/bin/clang-9-- Found /usr/bin/clang++-9-- Testing bitcode compiler /usr/bin/clang-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang-9" is compatible-- Testing bitcode compiler /usr/bin/clang++-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang++-9" is compatible-- LLVMCC: /usr/bin/clang-9-- LLVMCXX: /usr/bin/clang++-9-- Performing Test HAS__Wall_CXX-- Performing Test HAS__Wall_CXX - Success-- C++ compiler supports -Wall-- Performing Test HAS__Wextra_CXX-- Performing Test HAS__Wextra_CXX - Success-- C++ compiler supports -Wextra-- Performing Test HAS__Wno_unused_parameter_CXX-- Performing Test HAS__Wno_unused_parameter_CXX - Success-- C++ compiler supports -Wno-unused-parameter-- Performing Test HAS__Wall_C-- Performing Test HAS__Wall_C - Success-- C compiler supports -Wall-- Performing Test HAS__Wextra_C-- Performing Test HAS__Wextra_C - Success-- C compiler supports -Wextra-- Performing Test HAS__Wno_unused_parameter_C-- Performing Test HAS__Wno_unused_parameter_C - Success-- C compiler supports -Wno-unused-parameter-- Not treating compiler warnings as errors-- Could NOT find STP (missing: STP_DIR)-- STP solver support disabled-- Found Z3 libraries: "/usr/lib/libz3.so"-- Found Z3 include path: "/usr/include"-- Found Z3: /usr/include-- Z3 solver support enabled-- Found Z3-- Checking prototype Z3_get_error_msg for HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT - True-- Z3_get_error_msg requires context-- metaSMT solver support disabled-- Performing Test HAS__fno_exceptions-- Performing Test HAS__fno_exceptions - Success-- C++ compiler supports -fno-exceptions-- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.so (found version "1.2.11")-- Zlib support enabled-- TCMalloc support enabled-- Looking for C++ include gperftools/malloc_extension.h-- Looking for C++ include gperftools/malloc_extension.h - not foundCMake Error at CMakeLists.txt:419 (message):Can't find "gperftools/malloc_extension.h"-- Configuring incomplete, errors occurred!See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeOutput.log".See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeError.log".
sudo apt-get install libtcmalloc-minimal4 libgoogle-perftools-devbigeast@ubuntu:~/klee-2.1/build$ cmake> -DENABLE_POSIX_RUNTIME=ON> -DENABLE_KLEE_UCLIBC=ON> -DENABLE_KLEE_LIBCXX=ON> -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/> -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/> -DENABLE_KLEE_EH_CXX=ON> -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/> -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/> -DENABLE_UNIT_TESTS=ON> -DENABLE_SYSTEM_TESTS=ON> -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/> -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9> -DLLVMCC=/usr/bin/clang-9> -DLLVMCXX=/usr/bin/clang++-9> -DCMAKE_C_COMPILER=clang-9> -DCMAKE_CXX_COMPILER=clang++-9> ..-- KLEE version 2.1-- CMake generator: Unix Makefiles-- Build type: RelWithDebInfo-- KLEE assertions enabled-- LLVM_CONFIG_BINARY: /usr/bin/llvm-config-9-- LLVM_PACKAGE_VERSION: "9.0.0"-- LLVM_VERSION_MAJOR: "9"-- LLVM_VERSION_MINOR: "0"-- LLVM_VERSION_PATCH: "0"-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"-- LLVM_ENABLE_ASSERTIONS: "ON"-- LLVM_ENABLE_EH: "OFF"-- LLVM_ENABLE_RTTI: "ON"-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"-- Looking for bitcode compilers-- Found /usr/bin/clang-9-- Found /usr/bin/clang++-9-- Testing bitcode compiler /usr/bin/clang-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang-9" is compatible-- Testing bitcode compiler /usr/bin/clang++-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang++-9" is compatible-- LLVMCC: /usr/bin/clang-9-- LLVMCXX: /usr/bin/clang++-9-- C++ compiler supports -Wall-- C++ compiler supports -Wextra-- C++ compiler supports -Wno-unused-parameter-- C compiler supports -Wall-- C compiler supports -Wextra-- C compiler supports -Wno-unused-parameter-- Not treating compiler warnings as errors-- Could NOT find STP (missing: STP_DIR)-- STP solver support disabled-- Found Z3 libraries: "/usr/lib/libz3.so"-- Found Z3 include path: "/usr/include"-- Z3 solver support enabled-- Found Z3-- Z3_get_error_msg requires context-- metaSMT solver support disabled-- C++ compiler supports -fno-exceptions-- Zlib support enabled-- TCMalloc support disabled-- Could NOT find SQLITE3 (missing: SQLITE3_LIBRARY SQLITE3_INCLUDE_DIR)CMake Error at CMakeLists.txt:434 (message):SQLite3 not found, please install-- Configuring incomplete, errors occurred!See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeOutput.log".See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeError.log".
sudo apt-get install sqlite3 libsqlite3-devcmake-DENABLE_POSIX_RUNTIME=ON-DENABLE_KLEE_UCLIBC=ON-DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-9/-DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-9/include/c++/v1/-DENABLE_KLEE_EH_CXX=ON-DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/libc++-9/libcxxabi/-DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/-DENABLE_UNIT_TESTS=ON-DENABLE_SYSTEM_TESTS=ON-DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/-DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9-DLLVMCC=/usr/bin/clang-9-DLLVMCXX=/usr/bin/clang++-9-DCMAKE_C_COMPILER=clang-9-DCMAKE_CXX_COMPILER=clang++-9..
-- KLEE version 2.1-- CMake generator: Unix Makefiles-- Build type: RelWithDebInfo-- KLEE assertions enabled-- LLVM_CONFIG_BINARY: /usr/bin/llvm-config-9-- LLVM_PACKAGE_VERSION: "9.0.0"-- LLVM_VERSION_MAJOR: "9"-- LLVM_VERSION_MINOR: "0"-- LLVM_VERSION_PATCH: "0"-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"-- LLVM_ENABLE_ASSERTIONS: "ON"-- LLVM_ENABLE_EH: "OFF"-- LLVM_ENABLE_RTTI: "ON"-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"-- Looking for bitcode compilers-- Found /usr/bin/clang-9-- Found /usr/bin/clang++-9-- Testing bitcode compiler /usr/bin/clang-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang-9" is compatible-- Testing bitcode compiler /usr/bin/clang++-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang++-9" is compatible-- LLVMCC: /usr/bin/clang-9-- LLVMCXX: /usr/bin/clang++-9-- C++ compiler supports -Wall-- C++ compiler supports -Wextra-- C++ compiler supports -Wno-unused-parameter-- C compiler supports -Wall-- C compiler supports -Wextra-- C compiler supports -Wno-unused-parameter-- Not treating compiler warnings as errors-- Could NOT find STP (missing: STP_DIR)-- STP solver support disabled-- Found Z3 libraries: "/usr/lib/libz3.so"-- Found Z3 include path: "/usr/include"-- Z3 solver support enabled-- Found Z3-- Z3_get_error_msg requires context-- metaSMT solver support disabled-- C++ compiler supports -fno-exceptions-- Zlib support enabled-- TCMalloc support disabled-- SELinux support disabled-- Workaround for LLVM PR39177 (affecting LLVM 3.9 - 7.0.0) disabled-- KLEE_RUNTIME_BUILD_TYPE: Debug+Asserts-- POSIX runtime enabled-- klee-uclibc support enabled-- Found klee-uclibc library: "/home/bigeast/klee-uclibc/lib/libc.a"-- klee-libcxx support enabled-- Use libc++ include path: "/usr/include/c++/9/libc++-install-9/include/c++/v1/"-- Found libc++ library: "/usr/include/c++/9/libc++-install-9/lib/libc++.bca"-- CMAKE_CXX_FLAGS: -Wall -Wextra -Wno-unused-parameter-- KLEE_COMPONENT_EXTRA_INCLUDE_DIRS: '/usr/lib/llvm-9/include;/usr/include;/usr/include'-- KLEE_COMPONENT_CXX_DEFINES: '-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS;-DKLEE_UCLIBC_BCA_NAME="klee-uclibc.bca";-DKLEE_LIBCXX_BC_NAME="libc++.bca"'-- KLEE_COMPONENT_CXX_FLAGS: '-fno-exceptions'-- KLEE_COMPONENT_EXTRA_LIBRARIES: '/usr/lib/x86_64-linux-gnu/libz.so'-- KLEE_SOLVER_LIBRARIES: '/usr/lib/libz3.so'-- Testing is enabled-- Using lit: /home/bigeast/.local/bin/lit-- Unit tests enabled-- Google Test: Building from source.-- GTEST_SRC_DIR: /home/bigeast/googletest-release-1.7.0/-- Found PythonInterp: /usr/bin/python (found version "2.7.17")-- Looking for pthread.h-- Looking for pthread.h - found-- Looking for pthread_create-- Looking for pthread_create - not found-- Looking for pthread_create in pthreads-- Looking for pthread_create in pthreads - not found-- Looking for pthread_create in pthread-- Looking for pthread_create in pthread - found-- Found Threads: TRUE-- GTEST_INCLUDE_DIR: /home/bigeast/googletest-release-1.7.0/include-- System tests enabledCMake Deprecation Warning at test/CMakeLists.txt:133 (cmake_policy):The OLD behavior for policy CMP0026 will be removed from a future versionof CMake.The cmake-policies(7) manual explains that the OLD behaviors of allpolicies are deprecated and that a policy should be set to OLD only underspecific short-term circumstances. Projects should be ported to the NEWbehavior and not rely on setting a policy to OLD.-- Could NOT find Doxygen (missing: DOXYGEN_EXECUTABLE)CMake Warning at docs/CMakeLists.txt:46 (message):Doxygen not found. Can't build Doxygen documentation-- Configuring done-- Generating doneCMake Warning:Manually-specified variables were not used by the project:KLEE_LIBCXXABI_SRC_DIR-- Build files have been written to: /home/bigeast/klee-2.1/build
makesudo make install
-I ../../include-emit-llvm -c-g-O0 -Xclang -disable-O0-optnoneget_sign.c
/** First KLEE tutorial: testing a small function*/int get_sign(int x) {if (x == 0)return 0;if (x < 0)return -1;elsereturn 1;}int main() {int a;klee_make_symbolic(&a, sizeof(a), "a");return get_sign(a);}
bigeast@ubuntu:~/klee-2.1/examples/get_sign$ klee get_sign.bcKLEE: output directory is "/home/bigeast/klee-2.1/examples/get_sign/klee-out-0"KLEE: Using Z3 solver backendKLEE: done: total instructions = 33KLEE: done: completed paths = 3KLEE: done: generated tests = 3
bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ls klee-lastassembly.ll messages.txt run.stats test000002.ktest warnings.txtinfo run.istats test000001.ktest test000003.ktest
bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ktest-tool klee-last/test000001.ktestktest file : 'klee-last/test000001.ktest'args : ['get_sign.bc']num objects: 1object 0: name: 'a'object 0: size: 4object 0: data: b'x00x00x00x00'object 0: hex : 0x00000000object 0: int : 0object 0: uint: 0object 0: text: ....bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ktest-tool klee-last/test000002.ktestktest file : 'klee-last/test000002.ktest'args : ['get_sign.bc']num objects: 1object 0: name: 'a'object 0: size: 4object 0: data: b'xffx00x00x00'object 0: hex : 0xff000000object 0: int : 255object 0: uint: 255object 0: text: ....bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ktest-tool klee-last/test000003.ktestktest file : 'klee-last/test000003.ktest'args : ['get_sign.bc']num objects: 1object 0: name: 'a'object 0: size: 4object 0: data: b'x00x00x00x80'object 0: hex : 0x00000080object 0: int : -2147483648object 0: uint: 2147483648object 0: text: ....
https://b33t1e.github.io/2018/01/30/klee%E6%BA%90%E7%A0%81%E5%88%86%E6%9E%90/
https://www.anquanke.com/post/id/240038
https://github.com/klee/klee
https://jywhy6.zone/2020/12/11/klee-notes/
https://klee.github.io/build-llvm9/
看雪ID：bigeast
https://bbs.pediy.com/user-home-859945.htm
# 往期推荐
2.人人都可以拯救正版硬件受害者(Jlink提示Clone)
球分享
球点赞
球在看
点击“阅读原文”，了解更多！
- 左青龙
- 微信扫一扫
-
- 右白虎
- 微信扫一扫
-
评论