when use klee

[StevenJiang1110]

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.

[StevenJiang1110]

when I install klee using git merge nowack/handle_global_variables reid/lazy_intrinsic_rejection in your doc, something seems incorrect. I wonder if this is about the error.

[StevenJiang1110]

I put my scripts and dockerfile on thie link, it should replay the error above. I hope I can get some idea to fix it. https://github.com/StevenJiang1110/work_env/tree/master/docker.

[alastairreid]

Hi Steven,

Thanks for reporting these issues - we really appreciate it.

The biggest barrier to using these tools is that it is so hard to install them.
It would be great if you could send us a pull request for your dockerfile when you have something working.
I have barely used Docker myself so it would be great to get some help with this.

The stack dump is a direct result of the git merge failure.
The git merge failure was caused by the reid/lazy_intrinisic_rejection pull request being merged into the KLEE master branch.
I have fixed the instructions (waiting for review) to replace the merge instructions with

git remote add nowack https://github.com/MartinNowack/klee.git
git fetch --all
git merge nowack/handle_global_variables

I am told that the KLEE warnings about linking modules with different target tuples is probably benign.
I have opened a separate issue #37 for this.
(TL;DR: ideally, building rustc would also build a matching copy of clang. But it may not matter.)

[StevenJiang1110]

Thanks a lot for your reply. I follow your new instructions and the core dump problem is now fixed.
However, there seems to be some new problems when I follow your try-klee example. When I ran klee --output-dir=kleeout --warnings-only-to-file target/debug/deps/try_klee*.bc, the result is as follows.

And When I look into the klee result follow your doc, the analyse seems not to generate correct results. When I ran ktest-tool kleeout/test000001.ktest, there seems no proper answers.

When I ran KTEST_FILE=kleeout/test000001.ktest cargo run --features=verifier-klee, there seems some link error.

I hope I can get some advice from you about how to fix these problems. Thanks a lot.

I will send a PR tomorrow for my dockerfile after I add some necessary instructions. This dockerfile can be built properly but leads to the problem I mentioned above.

[alastairreid]

I am seeing this same error on Linux (but not on OSX).

The problem can be solved by

1. Adding --libc=klee (which works on Linux but cannot be used on OSX)
2. Adding --silent-klee-assume (which suppresses another problem)

$ rm -rf kleeout/; klee --libc=klee --silent-klee-assume --output-dir=kleeout --warnings-only-to-file target/debug/deps/try_klee*.bc
...
KLEE: done: total instructions = 10153
KLEE: done: completed paths = 3
KLEE: done: generated tests = 1

I'll update the documentation to fix this.

[StevenJiang1110]

Thanks a lot. This really helps and now I can get the same result, and ktest-tool kleeout/test000001.ktest will output the correct answer.
However, when I follow your Replaying the input values example, there seems one link error. When I execute KTEST_FILE=kleeout/test000001.ktest cargo run --features=verifier-klee, the result is

I have sent a pull request for my dockerfile. And the final image will replay the problem.

[alastairreid]

I think this is all resolved

• the instructions were fixed
• Steven provided docker support (that flushed out more problems in the instructions)
• we have now switched to using docker and have updated the instructions