[klee-dev] Error while using C++ STL, libcxx
Namrata Jain
Namrata.Jain.mcs18 at cse.iitd.ac.in
Sun May 24 16:47:27 BST 2020
Hello all,
I always run into 'Terminator found in the middle of basic block' when I
try running C++ program with STL. I could not figure out if this error
is due to some error in program, how I run KLEE, libcxx or due to some
mistake while building KLEE.
An example program:
#include <vector>
#include <iostream>
int main()
{
std::vector<int> x;
x.push_back(1);
x.push_back(2);
std::cout << x[0] << x[1];
return 0;
}
To generate bitcode:
clang++ -emit-llvm -c experiment.cpp -o experiment.bc
(I also tried: clang++-6.0 -emit-llvm -c -std=c++11 -I
"/home/namrata/libc++-install-60/include/c++/v1/" -nostdinc++
experiment.cpp)
command I used to run klee:
klee -libc=uclibc -libcxx -posix-runtime
/home/namrata/Desktop/project/verifTool/experiment.bc
Output:
KLEE: NOTE: Using POSIX model:
/home/namrata/build/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: NOTE: Using libcxx :
/home/namrata/build/Debug+Asserts/lib/libc++.bca
KLEE: NOTE: Using klee-uclibc :
/home/namrata/build/Debug+Asserts/lib/klee-uclibc.bca
KLEE: output directory is
"/home/namrata/Desktop/project/verifTool/klee-out-19"
KLEE: Using STP solver backend
WARNING: this target does not support the llvm.stacksave intrinsic.
Terminator found in the middle of a basic block!
label %1
LLVM ERROR: Broken function found, compilation aborted!
KLEE source directory: /home/namrata/klee
KLEE build directory: /home/namrata/build
I followed the instructions on while building:
https://klee.github.io/build-llvm60/
KLEE Build command:
cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON
-DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/namrata/klee-uclibc/
-DLLVM_CONFIG_BINARY=/usr/lib/llvm-6.0/bin/llvm-config
-DENABLE_KLEE_LIBCXX=ON -DENABLE_UNIT_TESTS=OFF
-DLLVMCC=/usr/lib/llvm-6.0/bin/clang
-DLLVMCXX=/usr/lib/llvm-6.0/bin/clang++
-DKLEE_LIBCXX_DIR=/home/namrata/libc++-install-60/
-DKLEE_LIBCXX_INCLUDE_DIR=/home/namrata/libc++-install-60/include/c++/v1/
/home/namrata/klee
Output:
-- The CXX compiler identification is GNU 7.5.0
-- The C compiler identification is GNU 7.5.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 2.1-pre
-- 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/lib/llvm-6.0/bin/llvm-config
-- LLVM_PACKAGE_VERSION: "6.0.0"
-- LLVM_VERSION_MAJOR: "6"
-- 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: "OFF"
-- LLVM_ENABLE_EH: "OFF"
-- LLVM_ENABLE_RTTI: "ON"
-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-6.0/include"
-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-6.0/lib"
-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-6.0/bin"
-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "ON"
-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"
CMake Warning at CMakeLists.txt:248 (message):
LLVM was built without assertions but KLEE will be built with them.
This might lead to unexpected behaviour.
-- Looking for bitcode compilers
-- Found /usr/lib/llvm-6.0/bin/clang
-- Found /usr/lib/llvm-6.0/bin/clang++
-- Testing bitcode compiler /usr/lib/llvm-6.0/bin/clang
-- Compile success
-- Checking compatibility with LLVM 6.0.0
-- "/usr/lib/llvm-6.0/bin/clang" is compatible
-- Testing bitcode compiler /usr/lib/llvm-6.0/bin/clang++
-- Compile success
-- Checking compatibility with LLVM 6.0.0
-- "/usr/lib/llvm-6.0/bin/clang++" is compatible
-- LLVMCC: /usr/lib/llvm-6.0/bin/clang
-- LLVMCXX: /usr/lib/llvm-6.0/bin/clang++
-- 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
-- STP solver support enabled
-- Found STP version 2.1.2
-- Using STP static library
-- STP_DIR: /usr/local/lib/cmake/STP
-- Could not find Z3 libraries
-- Could not find Z3 include path
-- Could NOT find Z3 (missing: Z3_INCLUDE_DIRS Z3_LIBRARIES)
-- Z3 solver support disabled
-- 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 - found
-- Performing Test HAS__fno_builtin_malloc
-- Performing Test HAS__fno_builtin_malloc - Success
-- C++ compiler supports -fno-builtin-malloc
-- Performing Test HAS__fno_builtin_calloc
-- Performing Test HAS__fno_builtin_calloc - Success
-- C++ compiler supports -fno-builtin-calloc
-- Performing Test HAS__fno_builtin_realloc
-- Performing Test HAS__fno_builtin_realloc - Success
-- C++ compiler supports -fno-builtin-realloc
-- Performing Test HAS__fno_builtin_free
-- Performing Test HAS__fno_builtin_free - Success
-- C++ compiler supports -fno-builtin-free
-- Found SQLITE3: /usr/lib/x86_64-linux-gnu/libsqlite3.so
-- Looking for sys/capability.h
-- Looking for sys/capability.h - found
-- Looking for pty.h
-- Looking for pty.h - found
-- Looking for util.h
-- Looking for util.h - not found
-- Looking for libutil.h
-- Looking for libutil.h - not found
-- Looking for openpty
-- Looking for openpty - not found
-- Looking for openpty in util
-- Looking for openpty in util - found
-- Looking for __ctype_b_loc
-- Looking for __ctype_b_loc - found
-- Looking for mallinfo
-- Looking for mallinfo - found
-- Looking for malloc_zone_statistics
-- Looking for malloc_zone_statistics - not found
-- Looking for sys/statfs.h
-- Looking for sys/statfs.h - found
-- Looking for selinux/selinux.h
-- Looking for selinux/selinux.h - not found
-- Looking for sys/acl.h
-- Looking for sys/acl.h - not found
-- SELinux support disabled
-- Performing Test LLVM_PR39177_FIXED
-- Performing Test LLVM_PR39177_FIXED - Failed
-- Workaround for LLVM PR39177 (affecting LLVM 3.9 - 7.0.0) enabled
-- KLEE_RUNTIME_BUILD_TYPE is not set. Setting default
-- The available runtime build types are:
Release;Release+Debug;Release+Asserts;Release+Debug+Asserts;Debug;Debug+Asserts
-- KLEE_RUNTIME_BUILD_TYPE: Debug+Asserts
-- POSIX runtime enabled
-- klee-uclibc support enabled
-- Found klee-uclibc library: "/home/namrata/klee-uclibc/lib/libc.a"
-- klee-libcxx support enabled
-- Use libc++ include path:
"/home/namrata/libc++-install-60/include/c++/v1/"
-- Found libc++ library:
"/home/namrata/libc++-install-60/lib/libc++.bca"
-- -Wall -Wextra -Wno-unused-parameter
-- KLEE_GIT_SHA1HASH: 615c7054223544a5b1b31e00279cde45064d810f
-- KLEE_COMPONENT_EXTRA_INCLUDE_DIRS:
'/usr/lib/llvm-6.0/include;/usr/local/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:
'-fvisibility-inlines-hidden;-fno-exceptions;-fno-builtin-malloc;-fno-builtin-calloc;-fno-builtin-realloc;-fno-builtin-free'
-- KLEE_COMPONENT_EXTRA_LIBRARIES:
'/usr/lib/x86_64-linux-gnu/libz.so;/usr/lib/x86_64-linux-gnu/libtcmalloc.so'
-- KLEE_SOLVER_LIBRARIES: 'libstp'
-- Testing is enabled
-- Using lit: /home/namrata/.local/bin/lit
-- Unit tests disabled
-- System tests enabled
CMake Deprecation Warning at test/CMakeLists.txt:118 (cmake_policy):
The OLD behavior for policy CMP0026 will be removed from a future
version
of CMake.
The cmake-policies(7) manual explains that the OLD behaviors of all
policies are deprecated and that a policy should be set to OLD only
under
specific short-term circumstances. Projects should be ported to the
NEW
behavior 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 done
-- Build files have been written to: /home/namrata/build
Did I do something wrong while giving paths or anything else?
Sorry for this lengthy trace, if unnecessary or if this is a trivial
issue.
Thankyou.
--
Namrata Jain
--
namrata.jain
More information about the klee-dev
mailing list