Hello Namrata,
I worked a lot on the current C++ support in KLEE (the recent C++
support PRs to KLEE were by me), so I hope I can help. I think the
main problem is that llvm 6.0 is quite old, and your example should
pretty much work as-is if you switch to a recent llvm version (the
most recent being 10, which should work). I tried your example locally
with llvm (and libc++) 10 and it produced the expected output ("12").
You can also run KLEE's testsuite to see if your build works (or
whether some tests already fail); To do so, go to the directory you
built KLEE in and run "make check". This will run KLEE's unit- and
integrationtests, which also test the C++ support. If this issue is
simply due to llvm 6.0 being too old, I would expect some tests to
fail (unless the tests relevant to your case aren't executed for older
llvm versions).
As building the bitcode file with the right flags can also be
non-trivial, here are the flags I use to build (up to large) C++
projects for execution with KLEE (I've been wondering about a good way
to share them anyway, so I guess they might also be helpful in
general).
Let's go over your flags first:
clang++ -emit-llvm -c experiment.cpp -o experiment.bc
What this will do: Use your system clang++ (unless you have another
clang++ in your PATH before that) and use that to compile your program
and output bitcode. clang++ will by default (at least on Linux) use
your g++'s C++ standard library implementation for compiling and
linking. As <vector> and <iostream> are both header only (at least for
the functionality in your example), your example doesn't require
linking against a bitcode-version of libcxx to run in KLEE.
Using the command you give to build the bitcode file (but using llvm
10's clang++), I was able to run your program using `klee --libcxx
--libc=uclibc main.bc` as well as just `klee --libc=uclibc main.bc`,
so without explicitly linking libcxx.
For many programs, especially small examples, this is often the case.
However, as soon as your program makes use of functionality that
requires actually linking against a libcxx (so running KLEE with
`--libcxx`), this might cause weird things to happen, or simply not
work at all, as you are now mixing g++'s (through `#include`s) and
llvm's (through `--libcxx`) standard library implementations.
Therefore, my general recommendation would be to always build against
the libcxx version you also give to KLEE's CMake invocation (the
-DKLEE_LIBCXX_DIR parameter).
clang++-6.0 -emit-llvm -c -std=c++11
-I"/home/namrata/libc++-install-60/include/c++/v1/" -nostdinc++
experiment.cpp
This should properly cause your example to include <vector> and
<iostream> from your libcxx version (at least for recent llvm/clang++
version, i.e., 9 or 10). Running KLEE with `--libcxx` should then also
link the corresponding libcxx-library version into your program.
However, compiling your programs to a working binary this way might be
a problem, or might still mix up llvm and g++ versions of the standard
library (as I'm not sure what this uses for linking, or whether it
reports an error). This might especially be the case when you build
larger real-word projects using wllvm++.
Here are the flags I generally use to build C++ programs for running
with KLEE:
LIBCXX_LIB_DIR="/<path-to-llvm-libcxx-build-directory>/lib"
LIBCXXABI_LIB_DIR="/<path-to-llvm-libcxxabi-build-directory>/lib"
MY_CXX_FLAGS="-nostdinc++ -stdlib=libc++ -lc++ -lc++abi \
-I/<path-to-llvm-directory>/libcxx/include \
-I/<path-to-llvm-directory>/libcxxabi/include \
-Wl,-L$LIBCXX_LIB_DIR -Wl,-L$LIBCXXABI_LIB_DIR \
-Wl,-rpath=$LIBCXX_LIB_DIR -Wl,-rpath=$LIBCXXABI_LIB_DIR"
And then build a file main.cpp using:
clang++ $MY_CXX_FLAGS -emit-llvm -c main.cpp
Or, when building a project that uses cmake (plus setup for
clang++/wllvm++):
cmake -DCMAKE_CXX_FLAGS="$MY_CXX_FLAGS" <path-to-project>
Depending on how you build libcxx and libcxxabi (I build them without
checking out the rest of llvm's source, which I think leads to a
slightly different setup), you might need only some of these. E.g., if
your build process outputs a `libc++.bca` that already contains a
linked version of `libc++abi`, the linker directives (those beginning
with -Wl) for libcxxabi should not be needed (but those for libcxx are
still required).
Additionally, I usually use a version of KLEE that supports C++
exceptions (exactly this PR: https://github.com/klee/klee/pull/966),
which is why the libcxxabi/libc++abi setup is required, but you might
be able to avoid specifying those if you use one of the released KLEE
versions or KLEE's current master.
Some more explanations: `-nostdinc++` makes the compiler not set
default paths for including standard library headers, which you also
used in your example. `-stdlib=libc++` makes clang++ use llvm's libc++
implementation instead of g++'s. I sometimes get warnings that this
flag is ignored by the compiler, which I think is due to the fact that
the next flags, `-lc++` and `-lc++abi`, already cause linking against
libc++ and libc++abi. The two `-I` directives then set up
include-paths for standard library includes done by the program
(pretty much what your example also did).
I then tell the linker, using the `-Wl,-L` flags, to also check the
given paths for required libraries, which leads to my versions of
libc++ and libc++abi being used. The `-Wl,-rpath=` flags make sure
that these same directories are also in the runtime path of the
program, which can be required if the program (additionally) loads
some parts of the standard library at runtime. I think this happens
when the standard library (or some part of it) is linked dynamically
(and not statically).
Maybe these flags can help as a starting point for determining the
flags you need in your use-case/setup. I think especially the
libcxxabi/libc++abi parts might no be required for you (yet), or might
need adjusting so you don't link libc++abi twice (once as part of
libc++ and once as libc++abi).
For running KLEE, `--libcxx` should always be accompanied by
`--libc=uclibc` (which you also did), as libcxx relies on a libc for
certain parts of its functionality (such as printing).
Sorry for this lengthy trace, if unnecessary or if this is a trivial
issue.
I found the steps and output you gave really helpful to see what
exactly is going on.
To sum up, try running KLEE's tests, and try building with a more
recent version of llvm (I'd suggest 10) and see if that fixes the
issue. Also, when building larger programs, you might need to adjust
your compiler/linker flags to make sure things work correctly.
I'd be happy to hear if this fixed the issue, and in general how your
experience with KLEE's C++ support goes, and the kinds of
issues/questions that come up.
Best,
Felix
________________________________________
From: [email protected]
<[email protected]> on behalf of Namrata Jain
<[email protected]>
Sent: Sunday, May 24, 2020 5:47 PM
To: [email protected]
Subject: [klee-dev] Error while using C++ STL, libcxx
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
