List of LLVM-based verifiers that we know of (edit this issue to add new ones)

• KLEE
• KLEE-Native
• SeaHorn
• SMACK
• Crux-LLVM

Some typical steps involved (edit this issue if new ones are found)

• Figure out how to invoke verifier directly on bitcode file (e.g., see docs/using-klee.md)
• Handle unimplemented LLVM intrinsics
  • Try to compile/optimize so that intrinsic disappears (-optlevel 1, dead code elimination, restrict CPU version, etc.)
  • For symbolic execution, ensure that symbolic execution fails only if the current path executes an unimplemented intrinsic (e.g., see klee/klee#1295)
  • Implement missing intrinsics by converting them to simpler intrinsics
  • Implement missing intrinsics by converting them to SMT (e.g., see klee/klee#1278)
• Make sure that weak symbols are supported (e.g., see klee/klee#1271 ?) (This affects 'atexit' support)
• Handle libc/etc dependencies in libcore/libstd including
  • memory allocator
  • syscalls
  • pthread functions
• Create FFI binding for verification annotation API
• Add support to scripts/cargo-verify
  • New/different flags for compiling Rust code
  • Invoke verifier
    • Filter stdout/stderr to discover verification result
    • Filter stdout/stderr to decide what tool output to produce at each verbosity level
  • If counterexamples are generated by tool, add "replay" support to display cex using Rust print functions

This project should have some CI checking.

There’s two steps to this

1. Setup a standard CI flow that does any check - this mostly needs github familiarity
2. Start populating it with more useful checks

Some checks we might want include

• rustfmt was applied
• all backends run all #tests ok
• documentation examples are ok

For a symbolic execution tool like KLEE, the major cause of problems is path splits that lead to path explosion: KLEE basically enumerates all viable paths and most programs have an exponential growth in number of paths as data sizes, etc. increase.
For a model checker, the problem is state-space explosion caused by path splits and path joins.

Inspired by Bornholt's Finding Code That Explodes under Symbolic Evaluation, and by Cristian Cadar's
blog post about measuring coverage, is it possible to identify verification hotspots that are causing verification efficiency problems?

e.g., in KLEE, we could consider using KLEE's profiling support to identify hotspots or common sequences in execution traces.

Questions:

• Do we want to find the code that explodes or inputs that trigger the explosion?
• Does seeing where a hotspot occurs help us come up with a mitigation? (see also #33 and #66)
• Are there particular Rust crates, idioms, language features, etc. that cause problems?
• Do hotspots and their mitigation for one tool work for other verification tools and/or fuzzers?

(The starting point is probably a literature search and/or twitter query to find what others have done.)

README.md refers to ./scripts/cargo-verify that seems deprecated (I see old-cargo-verify)

Could you update README.md ?

Why do you require sudo to build docker images?

I would love to test Klee but requireemnt to run docker build with sudo makes me suspicious.

The right way to support #[test] in a formal verification tool is almost certainly to implement it as part of rustc because that is how it is supported for testing.
Instead, we jump through a number of hoops to

• make a list of all the tests
• find the mangled names of tests
• invoke each test individually
• find whether a test #[should_panic]
• run N copies of the verifier in parallel

This allows us to write tests that work for both dynamic verification (testing / fuzzing) and static verification (symbolic execution, model checking, ...) but the result is that scripts/cargo-verify is a collection of hacks to do the above.

The current approach makes it possible to experiment with the interface and understand the issues - but, in the long run, some changes to rustc will probably be required.

Rationale: pointless incompatibility with SMACK that we should eliminate

link

todo:

• possibly enforce with precommit hooks
• check that this is consistent with Google commit message guidelines

When I visit https://project-oak.github.io/rust-verification-tools/, there's a "subscribe via RSS" link that points to https://project-oak.github.io/rust-verification-tools/feed.xml (which according to View Source is actually a <link type="application/atom+xml", not RSS). However, RSS or Atom, this link is broken and points to a 404.

Is it possible to fix the link to enable subscribing in a RSS reader?

Galois has just announced Crux, an open-source symbolic execution engine that operates on Rust MIR directly instead of LLVM IR. It might be worthwhile to use it instead of KLEE.

At present, traits are handled by testing with specific instances of the trait (see compatibility-test/src/dynamic.rs).
This seems like the only option when fuzzing but, for tools that support modular verification, we would ideally be using a contract for the methods in the trait so that the verification is valid for all possible implementations of the trait, not just the ones that we test with.

The current abstract_value implementation is not safe for types that are not contiguous in memory or where some values are not legal (eg enumerations).

See smack.rs but, for consistency with existing design, omit verifer_ prefix

Fine if first solution doesn’t support all backends.
We can improve later.

Now that Galois has released Crux-MIR and Crux-LLVM, we should switch to using their releases either using their tarballs or their docker images.

downloads
docker for crux-llvm
docker for crux-mir

It is a good idea to implement the same interface as other verification tools.
In particular, the SMACK interface (see smack.rs).
The main functions provided by SMACK are

• verifier_assert, verifier_assert_eq, verifier_assert_ne
• verifier_assume
• verifier_nondet, trait VerifierNonDet #30
• use 'verifier_' prefix instead of 'verifier::' prefix. #34

(See also the Rust Benchmarks verifier/src/lib.rs

While trying to verify the oak-runtime crate, the llvm-link step produced this error message.
The error seems to involve the ring crate.

It may not be relevant, but this was using a modified version of cargo-verify that leaves x86 vector instructions disabled (see #112)

STDERR: llvm-link: /usr/local/google/home/adreid/rust/oak/oak_runtime/target/x86_64-unknown-linux-gnu/debug/build/ring-de761000f43e0b68/out/aesni-gcm-x86_64-elf.o:1:1: error: expected top-level entity
STDERR: �ELF>@@ÄÁzoS H�êÅÙïäÅzoy�ÅqüÒÅ)üÚÅ!üâÅüêÅüòÄAqïÏÅú�d$ë f.�f��Ã�ÔÄÁzoYàÅ�üÊÄA)ï×ÄA!ïßÄÁzÄãADëÄAïçÅøQ�ÄãADóM1äM9÷Äb1ÜÊÅúoD$8ÄAïïÄãADËÄb)ÜÒÄA ï÷A�ÄÄãADûÄb!ÜÚÄÁzoYðI÷ÜÄbÜâÅÉïõÄãyDëÅ9ïÄÄbÜêÅñïåI�äÅxy ÄãyDËÄb ÜòÄãyDÓO�4&ÄB1ÜÏÅ9ïD$ÄãyDÛÅúoD$HÄB)Ü×M8ðnXÄB!ÜßM8ðfPÄBÜçL�l$(ÄBÜïL�d$0ÄÁzoiÄB Ü÷Åxy°ÅÉïñÄãyDÍÄB1ÜÏÅÉïòÄãyDÕÄB)Ü×ÅÁïûÄãyDÝÄB!ÜßÄãyDíÅúoD$XÄBÜçÄBÜïÅÙïáÄÁzoI ÄB Ü÷ÅxyÀÅÉïòÄãyDÑÄB1ÜÏÅÉïóÄãyDÙÄB)Ü×M8ðnHÅÁïýÄãyDéÄB!ÜßM8ðf@ÄãyDÉÅúoD$hÄBÜçL�l$8ÄBÜïL�d$@ÅÙïâÄÁzoQ@ÄB Ü÷ÅxyÐÅÉïóÄãyDÚÄB1ÜÏÅÉïõÄãyDêÄB)Ü×M8ðn8ÅÁïùÄãyDÊÅ9ïD$xÄB!ÜßM8ðf0ÄãyDÒÄBÜçL�l$HÄBÜïL�d$PÅÙïãÄÁzoYPÄB Ü÷ÅxyàÅÉïõÄã9DëÄB1ÜÏÅÉïñÄã9DËÄB)Ü×M8ðn(ÅÁïúÄã9DÓÄB!ÜßM8ðf Äc9DÃÄBÜçL�l$XÄBÜïL�d$ÅÉïõÄB Ü÷ÅÉïñÅxyðÅÑsÅÙïâÄÁzo[ÄB1ÜÏÄÁAïøÄB)Ü×ÅÙïåM8ðnÄB!ÜßM8ðfÄãYÄãYDãL�l$hÄBÜçL�d$pÄBÜïÅø ÄB Ü÷Äb1ÜÉÅxyÄb)ÜÑÅÉsÄb!ÜÙÅÁïþÄbÜáÅÙïàM8ðÄbÜéM8ð&Äb ÜñÅøI �ý �ÄB1ÜÏÄB)Ü×ÄB!ÜßÄBÜçÄBÜïÄB Ü÷Äb1ÜÉÄb)ÜÑÄb!ÜÙÄbÜáÄbÜéÅxy0Äb ÜñÅøI@ÄB1ÜÏÄB)Ü×ÄB!ÜßÄBÜçÄBÜïÄB Ü÷Äb1ÜÉÄb)ÜÑÄb!ÜÙÄbÜáÄbÜéÅxyPÄb ÜñÅøIësf.�f�ÄÁzoÄâqðÄÁzok0ÄAIþS@ÅIþÝÄÁzoYàÅ)þåÄb)ÐÅ!þíÄb!ØÄA)ï×ÅþõÄbàÄA!ïßÅ�þÍÄbèÄb ðÄâqÈéãûÿÿÄB1ÜÏÅú�|$ÄcYÄB)Ü×ÄãYDãÅñïÄB!ÜßÅñïGÄBÜçÅñïo ÄBÜïÅñïw0ÄB Ü÷Åñï�@Åñï_PÄÁzÄb1ÝÊÄÁzoS Äb)ÝÐÅñüÂL�l$xH��Äb!ÝÝÅùüêL�¤$�H�vÅzoy�ÄbÝæÅÑüòÄbÝïÅÉüúÄb ÝóÅÁüÚI�ÂH�êrBÅxN ÄAqïÏÅxV°ÅyoÐÅx^ÀÅyoÝÅxfÐÅyoæÅxnàÅyoïÅxvðÅyoóÅúo|$(éÐúÿÿÅ9ïD$Å9ïÄóÃ@M1ÒH�ú�H�$SUATAUAVAWÅøwÄÁzH�Ä�A�X
L�ÎL�q�IÇÇ�ÄAzoH�ä�ÄÁzoH���M�I@�ipÄb9ÀM!þI!çM)÷r
I�ÿsL)üÅúo�PL�7Åúog@L�¼@ÿÿÿÅúoo0HÁêM1ÒÅúow ÄâAøÅúoWÄâYàÅúoÄâQèÅú�d$0ÄâIðÅú�l$@ÄâiÐÅú�t$PÄâaØÅú�T$Åú�\$pè�ùÿÿÅxN ÅxV°Åx^ÀÅxfÐÅxnàÅxvðÄB9ÄAz�AÀÅøwL�xÐL�pØL�hàL�èH�hðH�XøH� L�ÐóÃf.�DÅúoa�ÄÁzoS L�mÿÅxy�L�a ÅqïÌ�Ã�øÅqüÒÅ)üÚÅ)ïÔÅ!üâÅ!ïÜÅüêÅïäÅüòÅïìÅ�üÊÅ ïôë
STDERR: llvm-link: error: loading file '/usr/local/google/home/adreid/rust/oak/oak_runtime/target/x86_64-unknown-linux-gnu/debug/build/ring-de761000f43e0b68/out/aesni-gcm-x86_64-elf.o'

By default, rustc compiles code to use any processor specific intrinsics supported by the target processor.

Some of these can be turned off.
cargo-verify uses the flags '-Ctarget-feature=-mmx,-sse,-sse2,-sse3,-ssse3,-sse4.1,-sse4.2,-3dnow,-3dnowa,-avx,-avx2'

But this does not completely prevent generation of processor specific intrinsics.

It may be necessary to rebuild libstd/libcore with these flags?
It may be necessary to add other flags?

It is not very useful to be able to specify the symbol name when propverify creates a symbolic value.
But, for more conventional uses of the verifier API, this can be very useful so an Option[str] argument might be a good idea to make the library more useful?

(We should be careful though: do all verifiers that we want to support have the ability to do something with names for symbolic values?)

Things to fix

1. cargo-verify does not expect command line arguments and does not pass to KLEE during verification
2. argc/argv are just arguments to 'main' in C but in Rust they are special global variables so we need to know their name. And their name is different on OSX from Linux (see the source)
3. For KLEE, I think we need to pass the --posix-runtime argument (which is not supported on OSX) (This is not true)

Docker version 20.10.6, build 370c289 macOS 11.4 aarch64 on commit e58c6a5.

=> ERROR importing cache manifest from rvt_base:latest

I had to delete this line from docker/mkimage:

--cache-from="${DOCKER_IMAGE_NAME}:${DOCKER_VERSION}" \

This cache doesn't exist on the first build?

At the moment, crates that include code written in C are not supported.
You will see linking errors (if you use the -v verbosity flag enough times) and verification will not be able to explore any paths that use C code.

For tools that are based on LLVM, it may be possible to fix this by using LTO more aggressively.

It is not clear whether this can be fixed for tools that use MIR.

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

Please see the attached image. The reproduce steps:

1. docker/build
2. docker/run
3. cd compatibility-test
4. cargo-verify --tests

I noticed a couple of broken links when browsing around your repo, so I ran it through a link-checker while I was waiting for docker/build to run.

$ npx markdown-link-check README.md 
npx: installed 65 in 4.194s

FILE: README.md
[✓] https://github.com/AltSysrq/proptest
[✓] http://klee.github.io/
[✖] docs/README.md
[✖] docs/install-rust.md
[✖] docs/install-klee.md
[✖] docs/using-propverify.md
[✓] https://altsysrq.github.io/proptest-book/intro.html
[✓] compatibility-test/src
[✖] docs/installation.md
[✓] LICENSE-APACHE
[✓] http://www.apache.org/licenses/LICENSE-2.0
[✓] LICENSE-MIT
[✓] http://opensource.org/licenses/MIT
[✓] https://github.com/burntsushi/quickcheck
[✓] https://hypothesis.works/
[✓] CONTRIBUTING.md

16 links checked.

After this patch, npx markdown-link-check README.md is clean.

If you would prefer for me to link to the rendered versions on https://project-oak.github.io then I can do.

Proptest has a great interface that provides a lot of control over the values that you fuzz with.
But (as far as I can tell), it is a blackbox fuzzer that cannot learn/use any knowledge of the code being fuzzed.
It would be good if a graybox fuzzing backend like AFL or libfuzzer could be used with the proptest API.

Arguably, this should be an enhancement request on the proptest project but I am putting it here because the whole idea of being able to easily switch between fuzzing and using formal verification is broken if, in practice, people are forced to use a different fuzzer because they need the added power of graybox fuzzing.

List of MIR-based verifiers that we know of (edit this issue to add new ones)

• crux-mir
• MIRAI

Implement propverify on top of verification-annotations support.
Without #[test] support, all tests will have to be written as main()

Getting this error on cmake for KLEE:

-- Looking for bitcode compilers
CMake Error at cmake/find_bitcode_compiler.cmake:27 (message):
  Failed to find C bitcode compiler
Call Stack (most recent call first):
  CMakeLists.txt:292 (include)
# attempts to match "clang-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang" "llvm-gcc"

So KLEE needs clang as a dependency? Should the rust build also pull the corresponding clang to build?

Update. Seems Rust hosts a fork of llvm-project that includes clang: https://github.com/rust-lang/llvm-project

This is thought to be benign but it would be nice to fix it.

The problem is that KLEE links some libraries with the bitcode it is verifying.
Those libraries are currently compiled with the standard version of clang.
To fix the mismatch, we need KLEE to use a version of clang built using the same LLVM that Rustc uses.

Rustc does not need clang so, even though it includes clang as a submodule, it does not build it.
It is not clear (I tried!) how to get the rustc build process to build a copy of clang.

Thread support will probably have to be implemented separately for every verifier we support.
Some verifiers that we plan to use do not support threads or only have very limited support.

Hi!

Despite of patching like mentioned in #137 (i.e. paths in Cargo.toml files and +nightly for cargo calls) , still does not compile:

cd demos/simple/klee
bash verify.sh

output:

Compiling verification-annotations v0.1.0 (/home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations)
error: /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/verifier/klee.rs:91:14: in function _ZN24verification_annotations8verifier4klee82_$LT$impl$u20$verification_annotations..traits..VerifierNonDet$u20$for$u20$f32$GT$15verifier_nondet17h03b474201f344241E float (float): SSE register return with SSE disabled


error: aborting due to previous error

error: could not compile `verification-annotations`

To learn more, run the command again with --verbose.

cargo +nightly build --features=verifier-klee --verbose
Compiling verification-annotations v0.1.0 (/home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations)
Running rustc --crate-name verification_annotations --edition=2018 /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="verifier-klee"' -C metadata=bbfe5df2a5b9d5c6 -C extra-filename=-bbfe5df2a5b9d5c6 --out-dir /home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -C incremental=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/incremental -L dependency=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -Ctarget-feature=-mmx,-sse,-sse2,-sse3,-ssse3,-sse4.1,-sse4.2,-3dnow,-3dnowa,-avx,-avx2 -Cno-vectorize-loops -Cno-vectorize-slp -Copt-level=1 -Zpanic_abort_tests -Cpanic=abort -Warithmetic-overflow -Coverflow-checks=yes --cfg=verify -Clto -Cembed-bitcode=yes --emit=llvm-bc
error: /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/verifier/klee.rs:91:14: in function ZN24verification_annotations8verifier4klee82$LT$impl$u20$verification_annotations..traits..VerifierNonDet$u20$for$u20$f32$GT$15verifier_nondet17h03b474201f344241E float (float): SSE register return with SSE disabled

error: aborting due to previous error

error: could not compile verification-annotations

Caused by:
process didn't exit successfully: rustc --crate-name verification_annotations --edition=2018 /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="verifier-klee"' -C metadata=bbfe5df2a5b9d5c6 -C extra-filename=-bbfe5df2a5b9d5c6 --out-dir /home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -C incremental=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/incremental -L dependency=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -Ctarget-feature=-mmx,-sse,-sse2,-sse3,-ssse3,-sse4.1,-sse4.2,-3dnow,-3dnowa,-avx,-avx2 -Cno-vectorize-loops -Cno-vectorize-slp -Copt-level=1 -Zpanic_abort_tests -Cpanic=abort -Warithmetic-overflow -Coverflow-checks=yes --cfg=verify -Clto -Cembed-bitcode=yes --emit=llvm-bc (exit status: 1)

Switching back and forth between 'cargo-verify --tests' and 'cargo-verify ' causes compilation error problems.
The problem is that it is hard to predict the exact name of the bitcode file generated on different systems under different compilation commands so 'cargo-verify' uses an overly liberal glob to find the file.

For now, the workaround is to run cargo clean to remove old files.
The right fix is probably to get cargo to report the actual filename that we need.

The bitcode files we generate do not work with 'klee --posix-runtime'.
Which makes it impossible to use --sym-arg, etc. to run a program in a symbolic environment.

Typical stack dump - apparently something to do with thread local storage.

Error: invalid function pointer
Stack:
#000030261 in _ZN3std6thread5local4fast12Key$LT$T$GT$14try_initialize17he85fa310dd78a6ceE.llvm.10040754990062079632 (=94662824143424)
#100030822 in _ZN3std10sys_common11thread_info11THREAD_INFO7__getit17ha8ce496b12c79945E ()
#200030692 in _ZN3std6thread5local17LocalKey$LT$T$GT$4with17h1164a555be013fdaE (=94662823622704)
#300002949 in _ZN3std10sys_common11thread_info3set17h0e2f32e25a4ddd50E (=94662825314400, =94662825439936)
#400002529 in _ZN3std2rt19lang_start_internal17h44f9e5387d49d91bE (=94662825126040, =94662824680192, =2, =94662825319264)
#500002495 in _ZN3std2rt10lang_start17hbd19511f3b57d3aeE (main=94662794447624, argc=2, argv=94662825319264) at /home/adreid/rust/src/libstd/rt.rs:67
#600002447 in __klee_posix_wrapped_main (=2, =94662825319264)
#700002388 in main (=2, =94662797389984, =94662797390008) at runtime/POSIX/klee_init_env.c:245

If Cargo.toml has

name = "foo"
...
[[bin]]
name = "bar"
path = "src/main.rs"

then we check for "main" in target/$tgt/debug/deps/foo*.bc
but we should be checking for it in target/$tgt/debug/deps/bar*.bc.

Since we are checking the wrong file, we get an error like

(Discovered in coreutils)

Each verifier has its own way of reporting overflow, for example. This makes the should_panic annotation non-portable.

We could add some mapping in cargo-verify from the strings in the annotation to how each verifier reports them.

If we don't fix this, maybe we should add the verifier name to the annotation?

Status of proptest feature support. Edit to add to this as gaps are spotted

• container type support (all? Except hash based)
• ValueTree (currently replaced by Value)
• Strategy trait
• weighting / control over probability distribution
• deriving procedural macro
• proptest macro (but only simplest form supported)
• prop_compose macro
• Arbitrary trait
• string regex support (this may be quite hard to support?)
• prop_assume! macro

cargo-verify currently exploits parallelism between verification targets but not within each individual verification.
To exploit parallelism. we need some way of doing a case split on input values (which hopefully makes values more concrete).
It is not clear whether this needs to be under user control (allowing the user to indicate case splits that may make sense) or whether it can be automatic.

Some places to get ideas from

• Proptest-derive modifiers
  (see also recursive strategies).
  Weights are used to modify the probability of generating particular random values.
  In a verification context, do they also indicate something about useful case splits or the number of parallel verification processes to assign to a particular case or the order in which to explore case splits in a sequential verification effort?

• DeepState: Symbolic Unit Testing for C and C++ - sections II, III and IV describe various optimizations

Challenges:

• Is there an effective way to apply sharding?
• If we add hints to aid verification:
  • do they work for all verification tools?
  • do different tools need conflicting annotations?
  • can fuzz-testers use the annotations as well?

Hello, I want to use klee to analyse some rust program and I set up my environment in a ubuntu18.04 docker following your docs. However, when I want to analyse the compiled file using klee --output-dir=kleeout --warnings-only-to-file target/debug/deps/try_klee*.bc, some error occured.The full error information is attached. I wonder how to fix it. Thanks a lot.

Output is only suitable for human consumption at the moment.
It would be nice to be able to connect it to other tools so that we can do things like:

• aggregate the result of verifying multiple programs/libraries
• collect data about the trajectory of passing checks through time

(A likely side-effect is that using 'cargo-verify -j' could probably produce output in a less disorganized manner?)

I think that the code that cargo-test uses is here.

While trying to verify some code in uutils/coreutils, I got the following error

Compiling uucore_procs v0.0.5 (/home/rust-verification-tools/expt/coreutils/src/uucore_procs)
error: cannot prefer dynamic linking when performing LTO
note: only 'staticlib', 'bin', and 'cdylib' outputs are supported with LTO
error: aborting due to previous error
error: could not compile uucore_procs
To learn more, run the command again with --verbose.

It's not obvious how we can use the current LTO trick with dynamically linked libraries so this may be tricky to overcome?

I'm getting some errors running the build script; the 'klee' container fails, complaining about a missing header:

make[2]: *** [runtime/POSIX/fd_init32_Release+Debug+Asserts.bc] Error 1
In file included from /root/klee/klee/runtime/klee-libc/strncpy.c:37:                                                                                                                                             
/usr/include/stdlib.h:25:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                               
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
In file included from /root/klee/klee/runtime/klee-libc/putchar.c:10:                                                                                                                                             
/usr/include/stdio.h:27:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                                
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
In file included from /root/klee/klee/runtime/klee-libc/strcoll.c:10:                                                                                                                                             
/usr/include/string.h:26:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                               
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
In file included from /root/klee/klee/runtime/klee-libc/strtol.c:34:                                                                                                                                              
In file included from /usr/lib/llvm-10/lib/clang/10.0.0/include/limits.h:21:                                                                                                                                      
/usr/include/limits.h:26:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                               
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
1 error generated.                                                                                                                                                                                                
1 error generated.   

It looks like the scripts are just pulling from the master branch directly; do you have a SHA that's verified to work for klee?

It looks as if SSE is not disabled while compiling libcore - and this can cause compatibility issues because we disable SSE when compiling for verification.

An (overly complex) example that shows this is the following

curl --location https://github.com/protocolbuffers/protobuf/releases/download/v3.13.0/protoc-3.13.0-linux-x86_64.zip > /tmp/protobuf.zip
unzip /tmp/protobuf.zip -d /tmp/protobuf
export PATH=$PATH:/tmp/protobuf/bin

git clone https://github.com/stepancheg/rust-protobuf.git
cd rust-protobuf
cargo build
cd protobuf-examples
cargo verify -vv

Fails with many errors of the form

ld.lld: error: /home/adreid/rust/src/libcore/num/dec2flt/algorithm.rs:375:16: in function _ZN8protobuf11text_format5lexer5float20parse_protobuf_float17h0fd5e56663b316c7E void (%"core::result::Result<f64, text_format::lexer::float::ProtobufFloatParseError>", [0 x i8], i64): SSE register return with SSE disabled

It would be good to have a smaller example!

This is the first step in supporting Galois' mir-verifier.
May require changes to verification-annotations/src/tests.rs unless #[test] is supported.

Example :

diff --git a/compatibility-test/Cargo.toml b/compatibility-test/Cargo.toml
index 7a18f73..2b31ff5 100644
--- a/compatibility-test/Cargo.toml
+++ b/compatibility-test/Cargo.toml
@@ -11,7 +11,7 @@ description = "Tests for both the propverify and the proptest crates - to check
 [dependencies]
 
 [target.'cfg(verify)'.dependencies]
-propverify = { path="/home/rust-verification-tools/propverify" }
+propverify = { path="../propverify" }
 
 [target.'cfg(not(verify))'.dependencies]
 proptest = { version = "*" }
diff --git a/demos/simple/klee/Cargo.toml b/demos/simple/klee/Cargo.toml
index 11fe766..fa1e6f4 100644
--- a/demos/simple/klee/Cargo.toml
+++ b/demos/simple/klee/Cargo.toml
@@ -5,7 +5,8 @@ authors = [""]
 edition = "2018"
 
 [dependencies]
-verification-annotations = { path="/home/rust-verification-tools/verification-annotations" }
+#verification-annotations = { path="/home/rust-verification-tools/verification-annotations" }
+verification-annotations = { path="../../../verification-annotations" }
 

btw. also maybe consider +nightly in scripts as it seems that some nightly features are required, example:

 cargo clean
-cargo build --features=verifier-klee
+cargo  +nightly build --features=verifier-klee

This issue is to keep track of the status of Rust language/feature support.
It is limited to LLVM-based verifiers because MIR-based verifiers will probably have completely different issues.
Add new problems as they are discovered with links to more detailed issues if they exist

• #[should_panic] support
• #[test] support
• Hybrid crates that include Rust + C code #6
• Crates that rely on C library calls #45
• std.env.args #21
• Thread support when only one thread is actually used #5
• Thread support when multiple threads are used #5
• Floating point support (see #154 about KLEE)
• Dynamically linked Rust libraries #111
• Embedded assembly language (see KLEE PR)
• Processor specific SIMD intrinsics #44
• Processor specific non-SIMD intrinsics

The following minimal example is verified by Seahorn, even though it should obviously fail:

#[test]
fn t00() {
    for _ in 0..1 {
        verifier::VerifierNonDet::verifier_nondet(i32::default());
    }
    if prop_is_replay() { // prop_is_replay is always false for Seahorn
        verifier::VerifierNonDet::verifier_nondet(0);
    }
    verifier::assert!(false);
}

Crates that perform FFI calls to C libraries (i.e., libraries that are built separately from the cargo build system) are a problem because

1. The library is (probably) not being built as a bitcode file.

2. Even if we had bitcode files for those libraries, it is not clear how to link them with the Rust code.

The second part of the problem is the most tractable and would let us take a small number of really important libraries and futz with their build process to generate bitcode files. This would probably be quite painful so may not scale well.

The most general approach to the first problem might be to define a new target that treats LLVM bitcode files as the native representation. If that existed, than any reasonably portable package would "just work". But this is probably not the simplest approach (unless somebody has already done this).

See also #6.

Lazy construction will work better with concolic execution because it defers path splitting to the point where a value is accessed.

This cannot be done for types like Option
But it can possibly be done for abstract Types like BTreeMap - possibly depending mutability?