Klee installation error

Question

I am trying to install klee (http://klee.github.io/build-llvm34/) in Ubuntu 16.04 LTS. I am having clang-3.9. After executing below command in klee_build_dir, I have bin directory with klee-stats and ktest-tool, but no klee. Please help

cmake -DENABLE_SOLVER_Z3=ON -DENABLE_SOLVER_STP=OFF -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_UNIT_TESTS=OFF -DENABLE_SYSTEM_TESTS=OFF -DKLEE_UCLIBC_PATH=/home/balaji/Downloads/klee-uclibc /home/balaji/Downloads/klee-- The CXX compiler identification is GNU 5.4.0
-- The C compiler identification is GNU 5.4.0
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- 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/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- KLEE version 1.4.0.0
-- 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
-- LLVM_PACKAGE_VERSION: "3.8.0"
-- LLVM_VERSION_MAJOR: "3"
-- LLVM_VERSION_MINOR: "8"
-- LLVM_VERSION_PATCH: "0"
-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"
-- LLVM_ENABLE_ASSERTIONS: "OFF"
-- LLVM_ENABLE_EH: "OFF"
-- LLVM_ENABLE_RTTI: "ON"
-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-3.8/include"
-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-3.8/lib"
-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-3.8/bin"
-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "ON"
-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"
CMake Warning at CMakeLists.txt:237 (message):
  LLVM was built without assertions but KLEE will be built with them.

  This might lead to unexpected behaviour.

Answer 1

You are welcome to use my GitHub repository which uses 6 easy scripts to install KLEE on UBUNTU 14.04.5 LTS. The reason I prefer UBUNTU 14.04 over UBUNTU 16.04 is the default GCC version which ships with them. Note that the 6th script uses an absolute path which you need to change (from /home/oren/GIT/ to /home/YourUserName/Some/Dirname). I've also included a 7th script which invokes KLEE and checks the installation with some simple input.c file. Good luck!

Answer 2

If anyone still trying to install KLEE on Ubuntu 14, you can use my virtual machine at the following link:

Github link: https://github.com/balajibalasubramaniam/dig

Most important feature of this virtual machine is that it comes pre-installed with SAGE (free open-source mathematics software system), Z3 (theorem prover from Microsoft Research), KLEE(symbolic virtual machine built on top of the LLVM compiler infrastructure), Java, JPF(system to verify executable Java bytecode programs) and Junit. Most importantly, it includes DIG or SymInfer - a state of the art tool for generating numerical invariants using symbolic states extracted from a symbolic execution tool for both C and Java programs (please visit https://bitbucket.org/nguyenthanhvuh/symtraces/wiki/Home to know more).

Answer 3

In the KLEE installation guide(http://klee.github.io/build-llvm34/), they point out that you need to use llvm-3.4. That means that you need to install llvm-3.4 and then use clang-3.4/clang++-3.4 as your compilers.

To install llvm-3.4, you can run:

sudo apt-get update
sudo apt-get install clang-3.4 llvm-3.4 llvm-3.4-dev llvm-3.4-tools

For me to compile klee, I used the following commands.

1. use cmake for configuration. You need to know where your llvm-3.4 binaries are.

   cmake -DENABLE_SOLVER_STP=ON   -DENABLE_POSIX_RUNTIME=ON\
         -DENABLE_KLEE_UCLIBC=ON   -DKLEE_UCLIBC_PATH=[klee-uclibc-repository] \ 
         -DGTEST_SRC_DIR=/[google-release-repository] \ 
         -DENABLE_SYSTEM_TESTS=ON   -DENABLE_UNIT_TESTS=ON \ 
         -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-3.4 -DLLVMCC=/usr/bin/clang-3.4 \ 
         -DLLVMCXX=/usr/bin/clang++-3.4 [your-klee-repository]
   

2. Actually make Klee by run make.

3. Run Klee test cases to make sure your install is successful.