ArnaudCharlet
commented
2 years ago The undefined references are indeed found in libgnat, so you need to feed libgnat.bc to KLEE somehow. I'm not familiar with KLEE, so can't give more details unfortunately, let us know what you find, this might be useful for others!
Hi,
I have a simple hello world Ada program:
with ADA.TEXT_IO;
procedure hello_world is
begin
end hello_world;
After generating the bytecode with llvm-gcc -c -emit-llvm I try to run it with klee (simply to test) I have the following error:
KLEE: output directory is "/mnt/d/wls/debian/klee_test/klee-out-6" KLEE: Using STP solver backend KLEE: WARNING: undefined reference to function: adatext_io__put_line2 *klee: /mnt/d/wls/debian/klee/lib/Expr/Expr.cpp:356: void klee::ConstantExpr::toMemory(void): Assertion `0 && "invalid type"' failed.**
0 0x0000000002066d61 PrintStackTraceSignalHandler(void*) Signals.cpp:0:0
1 0x000000000206461e SignalHandler(int) Signals.cpp:0:0
2 0x00007f96774be140 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x14140)
3 0x00007f9676b80ce1 raise (/lib/x86_64-linux-gnu/libc.so.6+0x3bce1)
4 0x00007f9676b6a537 abort (/lib/x86_64-linux-gnu/libc.so.6+0x25537)
5 0x00007f9676b6a40f (/lib/x86_64-linux-gnu/libc.so.6+0x2540f)
6 0x00007f9676b79662 (/lib/x86_64-linux-gnu/libc.so.6+0x34662)
7 0x0000000001f082d2 llvm::APInt::getZExtValue() const /mnt/d/wls/debian/klee/lib/Expr/Expr.cpp:356:12
8 0x0000000001f082d2 klee::ConstantExpr::getZExtValue(unsigned int) const /mnt/d/wls/debian/klee/include/klee/Expr/Expr.h:1032:30
9 0x0000000001f082d2 klee::ConstantExpr::toMemory(void*) /mnt/d/wls/debian/klee/lib/Expr/Expr.cpp:357:58
10 0x000000000049ed71 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction, llvm::Function, std::vector<klee::ref, std::allocator<klee::ref > >&) /mnt/d/wls/debian/klee/lib/Core/Executor.cpp:3830:35
11 0x00000000004aa478 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction, llvm::Function, std::vector<klee::ref, std::allocator<klee::ref > >&) /mnt/d/wls/debian/klee/lib/Core/Executor.cpp:1667:7
12 0x00000000004b0c0a klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) /mnt/d/wls/debian/klee/lib/Core/Executor.cpp:2487:3
13 0x00000000004b24f0 klee::Executor::run(klee::ExecutionState&) /mnt/d/wls/debian/klee/lib/Core/Executor.cpp:3525:18
14 0x00000000004b30a7 std::__uniq_ptr_impl<klee::PTree, std::default_delete >::reset(klee::PTree*) /usr/local/include/c++/11.3.0/bits/unique_ptr.h:179:16
15 0x00000000004b30a7 std::unique_ptr<klee::PTree, std::default_delete >::reset(klee::PTree*) /usr/local/include/c++/11.3.0/bits/unique_ptr.h:456:12
16 0x00000000004b30a7 std::unique_ptr<klee::PTree, std::default_delete >::operator=(std::nullptr_t) /usr/local/include/c++/11.3.0/bits/unique_ptr.h:397:7
17 0x00000000004b30a7 klee::Executor::runFunctionAsMain(llvm::Function*, int, char, char) /mnt/d/wls/debian/klee/lib/Core/Executor.cpp:4437:17
18 0x0000000000426fde main /mnt/d/wls/debian/klee/tools/klee/main.cpp:1518:5
19 0x00007f9676b6bd0a __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x26d0a)
20 0x000000000048a4ba _start (/usr/local/bin/klee+0x48a4ba)
Aborted
The same happens with other Ada functions, like interfaces.c.strings.new_string, which is needed to make variables symbolics.
The way I run klee is: klee --entry-point=_ada_hello_world hello_world.bc
Linkink with the bytecode libgnat.bc gives the same error.
I don't know if I'm using wrongly klee or there are some known issue about using gnat-llvm with klee.
Regards.