Klee examples does not build

[gww-parity]

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)

[alastairreid]

The SSE register return issue was due to us thinking that it was possible to disable SSE2 when compiling Rust - as a way of ensuring that there are no x86-specific vector intrinsic calls in the generated bitcode file. (See this post for why we thought that was a good idea.)

But, we recently found that this did not always work. In particular, it breaks use of floating point which relies on SSE2 as well.
The current main branch fixes this (See this newer post about what we do now.)

It would be great if you could try again and let us know how it goes. We want to eliminate obstacles like this that prevent you from even trying to use KLEE with Rust programs.

btw Our own usage of RVT looks something like this:

docker/build
// wait 15-20 minutes
docker/run scripts/regression-tests

or, alternatively, we run docker interactively like this

docker/build
// wait 15-20 minutes
docker/run

// we are now inside docker
scripts/regression-tests

or, if we want to run KLEE on some existing applications such as uu/coreutils

cd rust-verification-tools
docker/build
cd ../coreutils
../rust-verification-tools/docker run

cd src/uu/arch
echo >> Cargo.toml << EOF
[features]
verifier-klee = ["propverify/verifier-klee"]
verifier-crux = ["propverify/verifier-crux"]
verifier-seahorn = ["propverify/verifier-seahorn"]
EOF
cargo verify -o arch.bc
klee --libc=klee --posix-runtime -disable-verify arch.bc --sym-args 0 3 10 --sym-files 2 8

[gww-parity]

As I have problems with your Dockerfile build file ( as we discuss #139 ),
I tried to just run it on my machine , but does not build.

I don't know what's weird about your setup, I may have time to dig into this in few weeks , not now,
but maybe if Dockefile is not enough, you may want to make Vagrantfile that would build VM maybe with architecture tweaks you need? (also , as Vagrantfile builds VM e.g. using Virtualbox backend, you can run inside it e.g. Dockerfile with root access -> although it's super far from ideal solution ;), sometimes I am testing that way some of my Dockerfiles, to see how they perform on other systems )