[klee-dev] Error while using C++ STL, libcxx

[Namrata Jain]

Hello Felix,

Thankyou for the reply.
As suggested, I ran "make check" from klee-build-directory and found 
that 47 unexpected tests were failing.
So, I installed llvm-10, but while installing libcxx from 
klee-source-directory using the command:
	LLVM_VERSION=10 SANITIZER_BUILD= BASE=<absolute-path> 
./scripts/build/build.sh libcxx

it generated output:

Detected OS: linux
OS=linux
Detected distribution: ubuntu
DISTRIBUTION=ubuntu
Detected version: 18.04
DISTRIBUTION_VER=18.04
Component sanitizer not found.
Component sanitizer not found.
ENABLE_OPTIMIZED Required but unset

What this error is about? I also found this as an open issue on klee 
github page.

As you mentioned that libcxx support was not required for the example I 
stated, I built klee (version 2.1) without enabling libcxx and was able 
to see the output "12" with no errors.

(using the command: klee --libc=uclibc <absolute-path>/experiment.bc)

Warnings that were generated:

KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: llvm.dbg.label
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING: undefined reference to function: kill (UNSAFE)!
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 94590150907232) at 
libc/termios/tcgetattr.c:43 12
KLEE: WARNING ONCE: calling __user_main with extra arguments.

Are these due to not linking libcxx?

I also want to know about klee version-2.1-pre, is it the same as 
version 2.0? This is because I have made some changes in my klee source 
(2.1-pre) for a project and now I will be using version-2.1.

Thankyou.

--
Namrata Jain


On 25.05.2020 17:21, Felix Rath wrote:
> 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: klee-dev-bounces at imperial.ac.uk
> <klee-dev-bounces at imperial.ac.uk> on behalf of Namrata Jain
> <Namrata.Jain.mcs18 at cse.iitd.ac.in>
> Sent: Sunday, May 24, 2020 5:47 PM
> To: klee-dev at imperial.ac.uk
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-- 
namrata.jain