Closed inengch closed 6 years ago
It seems the LLVM version you got was built without RTTI but IKOS needs it. There have been a similar issue on Klee with LLVM 3.4 there.
Maybe building a new LLVM 4.0.1 on Debian 8 using the same configuration and the flag LLVM_ENABLE_RTTI
turned ON
(It is OFF
by default) would work?
When I use the -DLLVM_ENABLE_RTTI=true
flag, the error still exists.
cmake .. -DLLVM_CONFIG_EXECUTABLE=/root/clang+llvm-4.0.1-x86_64-linux-gnu-debian8/bin/llvm-config -DLLVM_ENABLE_RTTI=true
Scanning dependencies of target ikos-pp-lib
Scanning dependencies of target arbos-api
[ 4%] Building CXX object abs-repr/CMakeFiles/arbos-api.dir/src/arbos/api/ar.cpp.o
[ 8%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/lower_cst_expr.cpp.o
[ 12%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/lower_select.cpp.o
[ 16%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/name_values.cpp.o
[ 20%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/non_det_init.cpp.o
[ 25%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/mark_internal_inline.cpp.o
[ 29%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/remove_unreachable_blocks.cpp.o
[ 33%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/remove_printf_calls.cpp.o
[ 37%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp-lib.dir/src/passes/mark_no_return_functions.cpp.o
[ 41%] Building CXX object abs-repr/CMakeFiles/arbos-api.dir/src/arbos/api/ar_factory.cpp.o
Linking CXX static library libikos-pp-lib.a
[ 41%] Built target ikos-pp-lib
Scanning dependencies of target llvm-to-ar
[ 45%] Building CXX object frontends/llvm/CMakeFiles/llvm-to-ar.dir/src/passes/llvm_to_ar.cpp.o
[ 50%] Building CXX object abs-repr/CMakeFiles/arbos-api.dir/src/arbos/api/ar_visitor.cpp.o
Linking CXX shared library libarbos-api.so
[ 50%] Built target arbos-api
Scanning dependencies of target python_module
[ 54%] Generating python/ikos/settings/__init__.py, [force-rebuild]
[ 58%] Generating python/build/lib/ikos/__init__.py
[ 58%] Built target python_module
Scanning dependencies of target unify-exit-nodes
[ 62%] Building CXX object analyzer/CMakeFiles/unify-exit-nodes.dir/src/ar-passes/unify_exit_nodes.cpp.o
Linking CXX shared module ../../lib/llvm-to-ar.so
[ 62%] Built target llvm-to-ar
Scanning dependencies of target arbos
[ 66%] Building CXX object abs-repr/CMakeFiles/arbos.dir/src/arbos/arbos.cpp.o
Linking CXX shared library libunify-exit-nodes.so
[ 66%] Built target unify-exit-nodes
Scanning dependencies of target print
[ 70%] Building CXX object abs-repr/CMakeFiles/print.dir/src/passes/dumps/print.cpp.o
Linking CXX executable arbos
[ 70%] Built target arbos
Scanning dependencies of target ikos-pp
[ 75%] Building CXX object frontends/llvm/CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o
Linking CXX shared library libprint.so
[ 75%] Built target print
Scanning dependencies of target add-loop-counters
[ 79%] Building CXX object analyzer/CMakeFiles/add-loop-counters.dir/src/ar-passes/add_loop_counters.cpp.o
Linking CXX executable ikos-pp
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl15OptionValueCopyISsEE[_ZTIN4llvm2cl15OptionValueCopyISsEE]+0x10): undefined reference to `typeinfo for llvm::cl::GenericOptionValue'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl4listISsbNS0_6parserISsEEEE[_ZTIN4llvm2cl4listISsbNS0_6parserISsEEEE]+0x18): undefined reference to `typeinfo for llvm::cl::Option'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl3optI7PPLevelLb0ENS0_6parserIS2_EEEE[_ZTIN4llvm2cl3optI7PPLevelLb0ENS0_6parserIS2_EEEE]+0x18): undefined reference to `typeinfo for llvm::cl::Option'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl6parserI7PPLevelEE[_ZTIN4llvm2cl6parserI7PPLevelEE]+0x10): undefined reference to `typeinfo for llvm::cl::generic_parser_base'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl15OptionValueCopyI7PPLevelEE[_ZTIN4llvm2cl15OptionValueCopyI7PPLevelEE]+0x10): undefined reference to `typeinfo for llvm::cl::GenericOptionValue'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl15OptionValueCopyIbEE[_ZTIN4llvm2cl15OptionValueCopyIbEE]+0x10): undefined reference to `typeinfo for llvm::cl::GenericOptionValue'
libikos-pp-lib.a(lower_cst_expr.cpp.o):(.data.rel.ro._ZTIN7ikos_pp16LowerCstExprPassE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(lower_select.cpp.o):(.data.rel.ro._ZTIN7ikos_pp11LowerSelectE+0x10): undefined reference to `typeinfo for llvm::FunctionPass'
libikos-pp-lib.a(name_values.cpp.o):(.data.rel.ro._ZTIN7ikos_pp10NameValuesE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(mark_internal_inline.cpp.o):(.data.rel.ro._ZTIN7ikos_pp18MarkInternalInlineE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(remove_printf_calls.cpp.o):(.data.rel.ro._ZTIN7ikos_pp17RemovePrintfCallsE+0x10): undefined reference to `typeinfo for llvm::FunctionPass'
libikos-pp-lib.a(mark_no_return_functions.cpp.o):(.data.rel.ro._ZTIN7ikos_pp21MarkNoReturnFunctionsE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(remove_unreachable_blocks.cpp.o):(.data.rel.ro._ZTIN7ikos_pp23RemoveUnreachableBlocksE+0x10): undefined reference to `typeinfo for llvm::FunctionPass'
clang-4.0: error: linker command failed with exit code 1 (use -v to see invocation)
frontends/llvm/CMakeFiles/ikos-pp.dir/build.make:120: recipe for target 'frontends/llvm/ikos-pp' failed
make[2]: *** [frontends/llvm/ikos-pp] Error 1
CMakeFiles/Makefile2:2581: recipe for target 'frontends/llvm/CMakeFiles/ikos-pp.dir/all' failed
make[1]: *** [frontends/llvm/CMakeFiles/ikos-pp.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
Linking CXX shared library libadd-loop-counters.so
[ 79%] Built target add-loop-counters
Makefile:127: recipe for target 'all' failed
make: *** [all] Error 2
It's the same as above.
cmake .. -DLLVM_CONFIG_EXECUTABLE=/root/clang+llvm-4.0.1-x86_64-linux-gnu-debian8/bin/llvm-config -DLLVM_ENABLE_RTTI=True
Follow the official document instructions and the problem is solved. Cheers.
sudo apt update && sudo apt upgrade -y
echo "deb http://apt.llvm.org/jessie/ llvm-toolchain-jessie-4.0 main" | sudo tee -a /etc/apt/sources.list
wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
sudo apt update
sudo apt install cmake libgmp-dev libsqlite3-dev libz-dev libedit-dev libboost-dev libboost-program-options-dev libboost-filesystem-dev gcc g++ llvm-4.0 clang-4.0 -y
PATH="/usr/lib/llvm-4.0/bin:$PATH"
wget https://github.com/NASA-SW-VnV/ikos/archive/v1.3.tar.gz && tar xvf v1.3.tar.gz && rm v1.3.tar.gz
cd ikos-1.3 && mkdir build && cd build
cmake ..
make -j2
Thanks anyway.
The -DLLVM_ENABLE_RTTI=ON
is not on the IKOS cmake, it is when building LLVM from sources.
Development Environment
Error Message
Thanks in advance.