[klee-dev] C++ support and uclibc Dwarf issue
Vikram Narayan (vnarayan)
vnarayan at micron.com
Wed Nov 24 16:52:09 GMT 2021
Dear KLEE Team,
Requesting help on two topics: 1. C++ support, and 2. uclibc Dwarf issue.
Best Regards,
Vikram
------------------------------------------------------------
Steps followed and the outcome so far:
(a) Followed the installation instructions: https://klee.github.io/build-llvm9/ upto step 9
(b) Used "make check" in he build dir, and have the following observations:
1. All the C++ examples failed
Testing Time: 166.68s
Unsupported : 9
Passed : 296
Expectedly Failed: 2
Failed : 50
2. Example C++ Failure message:
********************
FAIL: KLEE :: CXX/symex/libc++/vector.cpp (59 of 357)
******************** TEST 'KLEE :: CXX/symex/libc++/vector.cpp' FAILED ********************
Script:
--
: 'RUN: at line 5'; /usr/bin/clang++-9 -I/home/vikram/klee/include /home/vikram/klee/test/CXX/symex/libc++/vector.cpp -emit-llvm -O0 -Xclang -disable-O0-optnone -c -std=c++11 -I "/home/vikram/build_libcxx/libc++-install-90/include/c++/v1" -g -nostdinc++ -o /home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp1.bc
: 'RUN: at line 6'; rm -rf /home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp.klee-out
: 'RUN: at line 7'; /home/vikram/klee/build/bin/klee --output-dir=/home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp.klee-out --exit-on-error --libc=uclibc --libcxx /home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp1.bc 2>&1 | FileCheck /home/vikram/klee/test/CXX/symex/libc++/vector.cpp
--
Exit Code: 1
Command Output (stdout):
--
$ ":" "RUN: at line 5"
$ "/usr/bin/clang++-9" "-I/home/vikram/klee/include" "/home/vikram/klee/test/CXX/symex/libc++/vector.cpp" "-emit-llvm" "-O0" "-Xclang" "-disable-O0-optnone" "-c" "-std=c++11" "-I" "/home/vikram/build_libcxx/libc++-install-90/include/c++/v1" "-g" "-nostdinc++" "-o" "/home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp1.bc"
$ ":" "RUN: at line 6"
$ "rm" "-rf" "/home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp.klee-out"
$ ":" "RUN: at line 7"
$ "/home/vikram/klee/build/bin/klee" "--output-dir=/home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp.klee-out" "--exit-on-error" "--libc=uclibc" "--libcxx" "/home/vikram/klee/build/test/CXX/symex/libc++/Output/vector.cpp.tmp1.bc"
note: command had no output on stdout or stderr
error: command failed with exit status: 1
$ "FileCheck" "/home/vikram/klee/test/CXX/symex/libc++/vector.cpp"
# command stderr:
/home/vikram/klee/test/CXX/symex/libc++/vector.cpp:17:11: error: CHECK: expected string not found in input
// CHECK: KLEE: done: completed paths = 1
^
<stdin>:1:1: note: scanning from here
KLEE: NOTE: Using libc++ : /home/vikram/klee/build/runtime/lib/libc++.bca
^
<stdin>:2:1: note: possible intended match here
KLEE: NOTE: Enabled runtime support for C++ exceptions
^
error: command failed with exit status: 1
(c) Example C failure:
********************
FAIL: KLEE :: Runtime/POSIX/CanonicalizeFileName.c (246 of 357)
******************** TEST 'KLEE :: Runtime/POSIX/CanonicalizeFileName.c' FAILED ********************
Script:
--
: 'RUN: at line 2'; /usr/bin/clang-9 -I/home/vikram/klee/include /home/vikram/klee/test/Runtime/POSIX/CanonicalizeFileName.c -Wall -emit-llvm -g -O0 -Xclang -disable-O0-optnone -c -o /home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.bc
: 'RUN: at line 3'; rm -rf /home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.klee-out
: 'RUN: at line 4'; /home/vikram/klee/build/bin/klee --output-dir=/home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.klee-out --libc=uclibc --posix-runtime --exit-on-error /home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.bc
--
Exit Code: 1
Command Output (stdout):
--
$ ":" "RUN: at line 2"
$ "/usr/bin/clang-9" "-I/home/vikram/klee/include" "/home/vikram/klee/test/Runtime/POSIX/CanonicalizeFileName.c" "-Wall" "-emit-llvm" "-g" "-O0" "-Xclang" "-disable-O0-optnone" "-c" "-o" "/home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.bc"
$ ":" "RUN: at line 3"
$ "rm" "-rf" "/home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.klee-out"
$ ":" "RUN: at line 4"
$ "/home/vikram/klee/build/bin/klee" "--output-dir=/home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.klee-out" "--libc=uclibc" "--posix-runtime" "--exit-on-error" "/home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.bc"
# command stderr:
KLEE: NOTE: Using POSIX model: /home/vikram/klee/build/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc : /home/vikram/klee/build/runtime/lib/klee-uclibc.bca
KLEE: output directory is "/home/vikram/klee/build/test/Runtime/POSIX/Output/CanonicalizeFileName.c.tmp.klee-out"
KLEE: Using STP solver backend
warning: Linking two modules of different data layouts: 'fd64_Debug+Asserts.bc' is 'e-m:e-i64:64-f80:128-n8:16:32:64-S128' whereas '__uClibc_main.os' is 'e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128'
error: linking module flags 'Dwarf Version': IDs have conflicting behaviors in 'fd64_Debug+Asserts.bc' and '__uClibc_main.os'
error: command failed with exit status: 1
The CMAKE results are pasted below:
> -DENABLE_SOLVER_STP=ON \
> -DENABLE_POSIX_RUNTIME=ON \
> -DENABLE_KLEE_UCLIBC=ON \
> -DKLEE_UCLIBC_PATH=/home/vikram/klee-uclibc \
> -DENABLE_UNIT_TESTS=ON \
> -DGTEST_SRC_DIR=/home/vikram/googletest-release-1.7.0 \
> -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 \
> -DLLVMCC=/usr/bin/clang-9 \
> -DLLVMCXX=/usr/bin/clang++-9 \
> -DENABLE_POSIX_RUNTIME=ON \
> -DENABLE_KLEE_LIBCXX=ON \
> -DKLEE_LIBCXX_INCLUDE_DIR=/home/vikram/build_libcxx/libc++-install-90/include/c++/v1 \
> -DKLEE_LIBCXX_DIR=/home/vikram/build_libcxx/libc++-install-90 \
> -DENABLE_KLEE_EH_CXX=ON\
> -DKLEE_LIBCXXABI_SRC_DIR=/home/vikram/build_libcxx/llvm-90/libcxxabi \
> /home/vikram/klee
-- The CXX compiler identification is GNU 9.3.0
-- The C compiler identification is GNU 9.3.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.3-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/bin/llvm-config-9
-- LLVM_PACKAGE_VERSION: "9.0.1"
-- LLVM_VERSION_MAJOR: "9"
-- LLVM_VERSION_MINOR: "0"
-- LLVM_VERSION_PATCH: "1"
-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"
-- LLVM_ENABLE_ASSERTIONS: "ON"
-- LLVM_ENABLE_EH: "OFF"
-- LLVM_ENABLE_RTTI: "ON"
-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"
-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"
-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"
-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"
-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"
-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"
-- Looking for bitcode compilers
-- Found /usr/bin/clang-9
-- Found /usr/bin/clang++-9
-- Testing bitcode compiler /usr/bin/clang-9
-- Compile success
-- Checking compatibility with LLVM 9.0.1
-- "/usr/bin/clang-9" is compatible
-- Testing bitcode compiler /usr/bin/clang++-9
-- Compile success
-- Checking compatibility with LLVM 9.0.1
-- "/usr/bin/clang++-9" is compatible
-- LLVMCC: /usr/bin/clang-9
-- LLVMCXX: /usr/bin/clang++-9
-- 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.3.3
-- Using STP shared library
-- STP_DIR: /usr/local/lib/cmake/STP
-- Found Z3 libraries: "/usr/lib/x86_64-linux-gnu/libz3.so"
-- Found Z3 include path: "/usr/include"
-- Found Z3: /usr/include
-- Z3 solver support enabled
-- Found Z3
-- Performing Test HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT
-- Performing Test HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT - Success
-- Z3_get_error_msg requires context
-- 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
-- Workaround for LLVM PR39177 (affecting LLVM 3.9 - 7.0.0) disabled
-- 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
-- Performing Test M32_SUPPORTED
-- Performing Test M32_SUPPORTED - Success
-- 32bit platform supported: 1
-- POSIX runtime enabled
-- klee-uclibc support enabled
-- Found klee-uclibc library: "/home/vikram/klee-uclibc/lib/libc.a"
-- klee-libc++ support enabled
-- Use libc++ include path: "/home/vikram/build_libcxx/libc++-install-90/include/c++/v1"
-- Found libc++ library: "/home/vikram/build_libcxx/libc++-install-90/lib/libc++.bca"
-- Use libc++abi source path: "/home/vikram/build_libcxx/llvm-90/libcxxabi"
-- Support for C++ Exceptions enabled
-- CMAKE_CXX_FLAGS: -Wall -Wextra -Wno-unused-parameter
-- KLEE_GIT_SHA1HASH: 0379144709c2bc47b6fc4bc42c5fe00a24d01a0d
-- KLEE_COMPONENT_EXTRA_INCLUDE_DIRS: '/usr/lib/llvm-9/include;/usr/local/include;/usr/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: '-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: 'stp;/usr/lib/x86_64-linux-gnu/libz3.so'
-- LIB_BC_SUFFIX: 64_Release;64_Release+Debug;64_Release+Asserts;64_Release+Debug+Asserts;64_Debug;64_Debug+Asserts;32_Release;32_Release+Debug;32_Release+Asserts;32_Release+Debug+Asserts;32_Debug;32_Debug+Asserts
-- KLEE_RUNTIME_DIRECTORY: /home/vikram/klee/build/runtime/lib
-- Testing is enabled
-- Using lit: /home/vikram/anaconda3/bin/lit
-- Unit tests enabled
-- Google Test: Building from source.
-- GTEST_SRC_DIR: /home/vikram/googletest-release-1.7.0
-- Found PythonInterp: /home/vikram/anaconda3/bin/python (found version "3.8.8")
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Failed
-- Looking for pthread_create in pthreads
-- Looking for pthread_create in pthreads - not found
-- Looking for pthread_create in pthread
-- Looking for pthread_create in pthread - found
-- Found Threads: TRUE
-- GTEST_INCLUDE_DIR: /home/vikram/googletest-release-1.7.0/include
-- System tests enabled
-- Found Doxygen: /usr/bin/doxygen (found version "1.8.17") found components: doxygen dot
-- Doxygen found
-- Configuring done
-- Generating done
-- Build files have been written to: /home/vikram/klee/build
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list