docker/build script fails to build klee

[alsuren]

Full output lives here: docker-build-output.txt and I have included a hopefully-relevant snippet below.

I don't have any experience with klee, so I haven't tried digging into this too deeply.

I did notice that we have UCLIBC_VERSION defined as klee_uclibc_v1.2 in docker/mkimage but it's not used anywhere. There are about 6 commits between https://github.com/klee/klee-uclibc.git HEAD and klee_uclibc_v1.2, so my current theory is that it might be one of those.

I had also removed the sudo around the docker calls, because my user already has permission to use docker (on macos). I'm currently doing a full-rebuild with sudo enabled and git checkout UCLIBC_VERSION in docker/klee/build_klee. I will tell you how it goes.

I do wonder whether it would be worthwhile publishing the relevant docker images somewhere. This would also help with #2 , and it's a workflow that people will be used to if they have used cross before.

 > [9/9] RUN sh build_klee:                                                                                                        
#14 0.331 Cloning into 'klee-uclibc'...                                                                                            
#14 4.260 INFO:Forcing C compiler to be.../usr/bin/clang-10
#14 4.260 INFO:Absolute path to compiler.../usr/bin/clang-10
#14 4.260 INFO:Disabling assertions
#14 4.260 INFO:Configuring for Debug build
#14 4.260 INFO:Configuring for LLVM bitcode archive
...
#14 161.5 [ 93%] Built target RuntimeFortify
#14 161.5 [ 93%] Built target BuildKLEERuntimes
#14 161.6 [ 94%] Built target kleeModule
#14 161.6 [ 97%] Built target kleeCore
#14 161.7 [ 97%] Built target klee
#14 161.7 Scanning dependencies of target systemtests
#14 161.7 [ 97%] Running system tests
#14 161.8 -- Testing: 346 tests, 4 workers --
#14 161.8 Testing:  0.. 10.. 20.. 30.. 40.. 50.. 60..
#14 185.0 FAIL: KLEE :: Runtime/POSIX/FD_Fail.c (241 of 346)
#14 185.0 ******************** TEST 'KLEE :: Runtime/POSIX/FD_Fail.c' FAILED ********************
#14 185.0 Script:
#14 185.0 --
#14 185.0 : 'RUN: at line 1';   /usr/bin/clang-10 -I/home/david/klee/include /home/david/klee/test/Runtime/POSIX/FD_Fail.c -emit-llvm -O0 -Xclang -disable-O0-optnone -c -o /home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc
#14 185.0 : 'RUN: at line 2';   rm -rf /home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out
#14 185.0 : 'RUN: at line 3';   /home/david/klee/build/bin/klee --output-dir=/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out --libc=uclibc --posix-runtime /home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc --max-fail 1 | FileCheck /home/david/klee/test/Runtime/POSIX/FD_Fail.c
#14 185.0 --
#14 185.0 Exit Code: 2
#14 185.0 
#14 185.0 Command Output (stdout):
#14 185.0 --
#14 185.0 $ ":" "RUN: at line 1"
#14 185.0 $ "/usr/bin/clang-10" "-I/home/david/klee/include" "/home/david/klee/test/Runtime/POSIX/FD_Fail.c" "-emit-llvm" "-O0" "-Xclang" "-disable-O0-optnone" "-c" "-o" "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc"
#14 185.0 $ ":" "RUN: at line 2"
#14 185.0 $ "rm" "-rf" "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out"
#14 185.0 $ ":" "RUN: at line 3"
#14 185.0 $ "/home/david/klee/build/bin/klee" "--output-dir=/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out" "--libc=uclibc" "--posix-runtime" "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc" "--max-fail" "1"
#14 185.0 # command stderr:
#14 185.0 KLEE: NOTE: Using POSIX model: /home/david/klee/build/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
#14 185.0 KLEE: NOTE: Using klee-uclibc : /home/david/klee/build/runtime/lib/klee-uclibc.bca
#14 185.0 KLEE: output directory is "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out"
#14 185.0 KLEE: Using STP solver backend
#14 185.0 KLEE: WARNING: executable has module level assembly (ignoring)
#14 185.0 KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 94153668978176) at runtime/POSIX/fd.c:1007 10
#14 185.0 KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
#14 185.0 KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
#14 185.0 KLEE: ERROR: (location information missing) ASSERTION FAIL: f
#14 185.0 KLEE: NOTE: now ignoring this error at this location
#14 185.0 
#14 185.0 KLEE: done: total instructions = 30080
#14 185.0 KLEE: done: completed paths = 2
#14 185.0 KLEE: done: generated tests = 1
#14 185.0 
#14 185.0 $ "FileCheck" "/home/david/klee/test/Runtime/POSIX/FD_Fail.c"
#14 185.0 # command stderr:
#14 185.0 FileCheck error: '-' is empty.
#14 185.0 FileCheck command line:  FileCheck /home/david/klee/test/Runtime/POSIX/FD_Fail.c
#14 185.0 
#14 185.0 error: command failed with exit status: 2
#14 185.0 
#14 185.0 --
#14 185.0 
#14 185.0 ********************
#14 185.0 Testing:  0.. 10.. 20.. 30.. 40.. 50.. 60.. 70.. 80.. 90.. 
#14 222.8 ********************
#14 222.8 Failed Tests (1):
#14 222.8   KLEE :: Runtime/POSIX/FD_Fail.c
#14 222.8 
#14 222.8 
#14 222.8 Testing Time: 60.97s
#14 222.8   Unsupported      :  28
#14 222.8   Passed           : 315
#14 222.8   Expectedly Failed:   2
#14 222.8   Failed           :   1
#14 222.8 make[3]: *** [test/CMakeFiles/systemtests.dir/build.make:63: test/CMakeFiles/systemtests] Error 1
#14 222.8 make[2]: *** [CMakeFiles/Makefile2:1752: test/CMakeFiles/systemtests.dir/all] Error 2
#14 222.8 make[1]: *** [CMakeFiles/Makefile2:854: CMakeFiles/check.dir/rule] Error 2
#14 222.8 make: *** [Makefile:164: check] Error 2

[alastairreid]

Thanks for this report (and the accompanying fixes).

TL;DR: I'm confused about this problem and will need to try to reproduce it before I can fix it. The following is just me thinking aloud about what could be going on here.

I haven't tried to use docker on the Mac since around the time that we switched to using docker - so I haven't seen this before.

This is a slightly confusing error report from KLEE's test harness. At first glance, the failing "assert(f)" is the problem.
Looking at the failing test, the relevant lines (klee/test/Runtime/POSIX/FD_Fail.c) are

int main(int argc, char** argv) {
  ...
  FILE* f = fopen("/etc/mtab", "r");
  assert(f);
  ...
}

So the obvious possibility is that /etc/mtab cannot be opened read-only - which could conceivably be caused by not running with sudo.
But it is perfectly possible to build and test KLEE on a variety of systems without using sudo - so this explanation doesn't completely make sense.
(It seems that my macbook does not have /etc/mtab - but that is irrelevant because the test is run within docker using the Ubuntu filesystem, not directly on the mac)

The other important line in this test is line 3 that includes the flag --max-fail 1.
This flag allows some/all POSIX commands to report a failure so that you can test whether your program can handle those failures.
From the test, it looks as though the calls to fread and fclose are expected to be affected by this.
But if fopen was also affected by this command line flag, it could maybe result in the error being reported ??
But, an initial look at the code implementing this (klee/runtime/POSIX/fd.c) suggests that fopen is not supposed to be affected by the max-fail flag.

Since I don't see anything obviously wrong just by eyeballing the code, I'll need to take a closer look to see if it is a docker-on-Mac thing or whether the KLEE, uclibc, etc. versions that I am looking at (which, for convenience is just my LLVM11 branch) don't have a problem that show up on the main branch?

[alastairreid]

PR #135 cleaned up a bunch of the docker build process. The main change was to decrease build time from several hours to about 15 minutes but I think it also 'fixed' this by the simple trick of not running the tests for KLEE so that the build would go through successfully on a Mac.

[alsuren]

After your excellent work on the docker build process, I thought I'd give it another shot. Your main branch seems to build images fine now, so this issue can probably be closed.

I will keep an eye on this project, and try again once your LLVM 11 branch lands, because I'm getting ERROR - FAILED: 'llvm-link-10' terminated with exit code 1. when do the following inside docker/run (if it still happens after your llvm 11 branch lands, I will open a separate issue)

david@docker-desktop:/Users/david/src/rust-verification-tools$ (cd  compatibility-test/ && cargo clean && cargo-verify --backend=klee --verbose )
Checking compatibility_test
  Building compatibility_test for verification
STDERR:    Compiling verification-annotations v0.1.0 (/home/rust-verification-tools/verification-annotations)
STDERR:    Compiling propverify v0.1.0 (/home/rust-verification-tools/propverify)
STDERR:    Compiling compatibility-test v0.1.0 (/Users/david/src/rust-verification-tools/compatibility-test)
STDERR:     Finished dev [unoptimized + debuginfo] target(s) in 7.86s
ERROR - FAILED: 'llvm-link-10' terminated with exit code 1.

[NEUZhangy]

After your excellent work on the docker build process, I thought I'd give it another shot. Your main branch seems to build images fine now, so this issue can probably be closed.

I will keep an eye on this project, and try again once your LLVM 11 branch lands, because I'm getting ERROR - FAILED: 'llvm-link-10' terminated with exit code 1. when do the following inside docker/run (if it still happens after your llvm 11 branch lands, I will open a separate issue)

david@docker-desktop:/Users/david/src/rust-verification-tools$ (cd  compatibility-test/ && cargo clean && cargo-verify --backend=klee --verbose )
Checking compatibility_test
  Building compatibility_test for verification
STDERR:    Compiling verification-annotations v0.1.0 (/home/rust-verification-tools/verification-annotations)
STDERR:    Compiling propverify v0.1.0 (/home/rust-verification-tools/propverify)
STDERR:    Compiling compatibility-test v0.1.0 (/Users/david/src/rust-verification-tools/compatibility-test)
STDERR:     Finished dev [unoptimized + debuginfo] target(s) in 7.86s
ERROR - FAILED: 'llvm-link-10' terminated with exit code 1.

Hi @alsuren , may I know how did you resolve this issue? I encountered the same issue. Thanks!

[alastairreid]

Hi @NEUZhangy ,

So this is a problem trying to use LLVM11?
I added partial LLVM11 support to RVT because I wanted to look at the Rust for Linux codebase which depends on a nightly from around February 2021.
After I got it working enough for that narrow purpose, I have been focused on the Rust for Linux code and have not had the time to make the LLVM11 support better. Sorry about that.

I think? that the state of LLVM11 at the moment is:

• If you want to run a "main" function that uses verification-annotations directly, it works.
• If you want to run a test function (i.e., using the #[test] annotation), it does not work.
• If you want to run a "main" function that uses the propverify crate, I'm not sure but I think that it works.

I think that the cause of this as that our #[test] support is a complete hack that takes advantage of the way that cargo test compiles and links code. My assumption is that more recent versions of cargo test have changed either the way that test functions are compiled or, perhaps, the test library that they are linked with.
(Although that seems to be contradicted by your error message mentioning llvm-link-10 which should obviously be llvm-link-11.)

[NEUZhangy]

Hi @alastairreid, thanks for your kind reply, I resolved the issue and find the solution:
cd runtime; make
cd ../simd_emulation; make
make runtime and make simd_emulation seems should be done after first-time docker/run.