Hey, > As suggested, I ran "make check" from klee-build-directory and found > that 47 unexpected tests were failing.
That definitely sounds like something might have been broken there. > What this error is about? I also found this as an open issue on klee > github page. I sadly cannot help with this, as I don't use KLEE's build scripts, and am not really familiar with how they work at all. So I don't know what the correct options, usage, etc. for building KLEE with libcxx support are. > 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. Nice :) Then I would assume that LLVM 9 or 10 should definitely help with running with `--libcxx`. > Are these due to not linking libcxx? > 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 I think these are from not linking libcxxabi, which can be part of libcxx depending on how you build it. > 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)! Some of these actually are provided by --posix-runtime (like `open`, `ioctl` and maybe more), so that might help here. Others might not be modeled for KLEE (yet), but they don't seem to be from libcxx, as libcxx usually contains C++-mangled names (but they might appear in the program because you #include'd <vector> and <iostream>). > 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. Can't really help with this, not really familiar with KLEE's release process. Best, Felix ________________________________________ From: Namrata Jain <namrata.jain.mc...@cse.iitd.ac.in> Sent: Tuesday, May 26, 2020 2:32 PM To: Felix Rath Cc: klee-dev@imperial.ac.uk Subject: Re: [klee-dev] Error while using C++ STL, libcxx 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-boun...@imperial.ac.uk > <klee-dev-boun...@imperial.ac.uk> on behalf of Namrata Jain > <namrata.jain.mc...@cse.iitd.ac.in> > Sent: Sunday, May 24, 2020 5:47 PM > To: klee-dev@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@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev -- namrata.jain _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev