LLVM-11 support

[alastairreid]

The experimental support for LLVM-11 does not fully work.

• Verifying a program (i.e., that defines 'main') seems to work (but has not been tested extensively)
• Verifying a function annotated with #[test] does not work: KLEE crashes during its preprocessing phase.
• Almost all of the regression tests rely on #[test] and do not work.

The error seen with #[test] is as follows. (This is obtained by using cargo verify -vvvvvv then cutting and pasting the command used to invoke KLEE.)

[Long list of errors that look like the next three lines]
Instruction does not dominate all uses!
  %.i3348 = phi i64 [ <badref>, <badref> ], [ %.i3682, %2236 ], [ %.i3344, %2227 ]
  %2378 = insertelement <4 x i64> %.upto24216, i64 %.i3348, i32 3

PHI nodes not grouped at top of basic block!
  %.i0345 = phi i64 [ <badref>, <badref> ], [ %.i0679, %2236 ], [ %.i0341, %2227 ]
label %2370
in function _ZN4test9run_tests17h3c40b1ee8455d4dbE

LLVM ERROR: Broken function found, compilation aborted!
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1f)[0x7fae470b242f]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7fae470b0762]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0xaa6905)[0x7fae470b2905]
/lib/x86_64-linux-gnu/libc.so.6(+0x46210)[0x7fae4612d210]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xcb)[0x7fae4612d18b]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x12b)[0x7fae4610c859]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0x9f9c28)[0x7fae47005c28]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0x9f9a48)[0x7fae47005a48]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0xc2295f)[0x7fae4722e95f]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm13FPPassManager13runOnFunctionERNS_8FunctionE+0x3b9)[0x7fae471c1579]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm13FPPassManager11runOnModuleERNS_6ModuleE+0x33)[0x7fae471c6b23]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x3e0)[0x7fae471c1b90]
klee(+0xa34bf)[0x564c44ede4bf]
klee(+0x49e4c)[0x564c44e84e4c]
klee(+0x2cc9c)[0x564c44e67c9c]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7fae4610e0b3]
klee(+0x3c16e)[0x564c44e7716e]
Aborted

It is not obvious what is going wrong here.

[alastairreid]

Note: @fshaked pointed out that, instead of using -vvvvvv and then grovelling through the output produced, it is better to use the flag '--script commands.sh' to generate a file containing exactly the shell commands used by cargo-verify. You can then execute the commands in commands.sh one by one, modify the commands, etc. to try to debug.

[alastairreid]

Note that rustc is now based on LLVM12 and that KLEE has a LLVM12 pull request: 1389

[thierrymarianne]

Fyi, I've tried integrating LLVM12 by cherry-picking the changes that you've applied to inkwell in this fork on top of the latest commit from inkwell master branch...

The docker images building process terminates well, including rvt-patch-llvm compilation but so far I can only see stack traces (like the one below) when running klee against generated bitcodes.

By checking out the aforementioned branch supporting LLVM12, I'll get more promising results hopefully.

Edit With demo/simple/klee, I get the following stacktrace for instance after including the work from klee/klee#1389

$ klee --libc=klee --silent-klee-assume --warnings-only-to-file ./try_klee.out
KLEE: output directory is "/home/rust-verification-tools/demos/simple/klee/./klee-out-0"
KLEE: Using STP solver backend
klee: /home/rvt/klee/lib/Core/Executor.cpp:1262: const klee::Cell& klee::Executor::eval(klee::KInstruction*, unsigned int, klee::ExecutionState&) const: Assertion `vnumber != -1 && "Invalid operand to eval(), not a value or constant!"' failed.
 #0 0x00007f9221a0be53 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/usr/lib/llvm-12/lib/libLLVM-12.so.1+0xbd8e53)
 #1 0x00007f9221a0a142 llvm::sys::RunSignalHandlers() (/usr/lib/llvm-12/lib/libLLVM-12.so.1+0xbd7142)
 #2 0x00007f9221a0c4bf (/usr/lib/llvm-12/lib/libLLVM-12.so.1+0xbd94bf)
 #3 0x00007f9220954210 (/lib/x86_64-linux-gnu/libc.so.6+0x46210)
 #4 0x00007f922095418b raise (/lib/x86_64-linux-gnu/libc.so.6+0x4618b)
 #5 0x00007f9220933859 abort (/lib/x86_64-linux-gnu/libc.so.6+0x25859)
 #6 0x00007f9220933729 (/lib/x86_64-linux-gnu/libc.so.6+0x25729)
 #7 0x00007f9220944f36 (/lib/x86_64-linux-gnu/libc.so.6+0x36f36)
 #8 0x00005620a4faa7a0 klee::Executor::eval(klee::KInstruction*, unsigned int, klee::ExecutionState&) const /home/rvt/klee/lib/Core/Executor.cpp:1259:3
 #9 0x00005620a4fc89fd std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >::push_back(klee::ref<klee::Expr> const&) /usr/include/c++/9/bits/stl_vector.h:1186:20
#10 0x00005620a4fc89fd klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) /home/rvt/klee/lib/Core/Executor.cpp:2473:26
#11 0x00005620a4fca68a klee::Executor::run(klee::ExecutionState&) /home/rvt/klee/lib/Core/Executor.cpp:3613:18
#12 0x00005620a4fcb24d _ZSt4swapIPN4klee5PTreeEENSt9enable_ifIXsrSt6__and_IJSt6__not_ISt15__is_tuple_likeIT_EESt21is_move_constructibleIS7_ESt18is_move_assignableIS7_EEE5valueEvE4typeERS7_SH_ /usr/include/c++/9/bits/move.h:193:11
#13 0x00005620a4fcb24d std::unique_ptr<klee::PTree, std::default_delete<klee::PTree> >::reset(klee::PTree*) /usr/include/c++/9/bits/unique_ptr.h:400:6
#14 0x00005620a4fcb24d std::unique_ptr<klee::PTree, std::default_delete<klee::PTree> >::operator=(std::nullptr_t) /usr/include/c++/9/bits/unique_ptr.h:336:2
#15 0x00005620a4fcb24d klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) /home/rvt/klee/lib/Core/Executor.cpp:4489:17
#16 0x00005620a4f94967 main /home/rvt/klee/tools/klee/main.cpp:1525:35
#17 0x00007f92209350b3 __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x270b3)
#18 0x00005620a4fa133e _start (/usr/bin/klee+0x3c33e)
Aborted (core dumped)

whereas after switching to uclibc, someting slightly better comes out of it but with the external call failing, it doesn't appear to be very helpful.

$ klee --version
KLEE 2.3-pre (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: ON)
  Build revision: 2ea638415501008f6b7a078bae98b8393949dfff

LLVM (http://llvm.org/):
  LLVM version 12.0.0

  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake

$ klee --libc=uclibc --silent-klee-assume --warnings-only-to-file ./try_klee.out
KLEE: NOTE: Using klee-uclibc : /usr/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca
KLEE: output directory is "/home/rust-verification-tools/demos/simple/klee/./klee-out-1"
KLEE: Using STP solver backend
KLEE: ERROR: libc/signal/sigaction.c:58: failed external call: __syscall_rt_sigaction
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 14103
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1