Commit cf45768f authored by Per's avatar Per


parent fea54c47
# 1 minute introduction
# KLEE bindings for Rust
## requirements
- docker
- nightly toolchain (nightly-2018-01-10)
KLEE is a symbolic execution engine, based on the LLVM compiler infrastructure. KLEE generetes test cases aiming to cover (all) reachable paths of the input program. The KLEE run-time infers further checks for common program errors, e.g., out of bounds indexing and division by zero. Rust as being designed for safety, catches such errors and panics in precence of such faults. For analysis, a Rust `panic` implies an `abort`, which is detected as an error by KLEE, thus our `klee` tool spots potential panicing behavior of the application at hand.
In effect, the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code), without jeopordizing memory safety and robustnes for programs. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficent to re-run KLEE if the source program is changed. To in the general case of adopting unchecked operations safety can be
ensured by adding assertions to the source. If those assertions are condititonally compiled, e.g. by a `klee` feature, the assertions (and their implied overhead) will be omitted in a production build.
## Requirements
- docker (optional)
- KLEE (optional)
- nightly toolchain (edition-2018)
The `klee` tool needs either access to a docker image providing KLEE, or KLEE being natively installed and accissible in path. The tool has been tested on a
the master branch of KLEE ( as of Sun Nov 25 14:57:29 CET 2018, built under arch linux with the system LLVM (v7) using a modified aur recepie (, altered to refer `source` to the klee master branch.
Currently only native KLEE is supported, we need to build a new docker with recent KLEE first in order to re-enable docker usage.
## usage
``` console
$ systemctl start docker.service # if not already started/enabled
$ systemctl start docker.service # if not already started/enabled, docker is optional
$ cargo install --path cargo-klee # add -f, if already installed
......@@ -15,29 +29,55 @@ $ cd klee-examples
$ cargo klee --example foo --release
KLEE: output directory is "/mnt/target/release/examples/klee-out-0"
KLEE: Using STP solver backend
KLEE: ERROR: /home/pln/klee/klee-rust/klee/src/ abort failure
KLEE: output directory is "/home/pln/rust/klee/klee-examples/target/release/examples/klee-out-0"
KLEE: Using Z3 solver backend
warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-pc-linux-gnu' whereas 'target/release/examples/foo-cda2f387c054965f.ll' is 'x86_64-unknown-linux-gnu'
KLEE: ERROR: /home/pln/rust/klee/src/ abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 20
KLEE: done: total instructions = 22
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
$ more target/release/examples/klee-out-0/test000001.abort.err
Error: abort failure
File: /home/pln/klee/klee-rust/klee/src/
Line: 24
assembly.ll line: 76
#000000076 in _ZN4core9panicking9panic_fmt17hc7d7358b749037fdE () at /home/pln/klee/klee-rust/klee/src/
#100000070 in _ZN4core9panicking5panic17h4680eb5ae9b0e3d0E () at HOME/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/src/libcore/pani
#200000044 in main (=1, =94362321163792) at PWD/klee-examples/examples/
KLEE generates two test cases, we can view them by:
``` sh
$ ktest-tool target/release/examples/klee-last/test000001.ktest
ktest file : 'target/release/examples/klee-last/test000001.ktest'
args : ['target/release/examples/foo-cda2f387c054965f.ll']
num objects: 1
object 0: name: b'u'
object 0: size: 1
object 0: data: b'\xff'
$ ktest-tool target/release/examples/klee-last/test000002.ktest
ktest file : 'target/release/examples/klee-last/test000002.ktest'
args : ['target/release/examples/foo-cda2f387c054965f.ll']
num objects: 1
object 0: name: b'u'
object 0: size: 1
object 0: data: b'\x00'
The first test triggers an error, we can view details by:
``` sh
$ more target/release/examples/klee-last/test000001.abort.err
Error: abort failure
File: /home/pln/rust/klee/src/
Line: 6
assembly.ll line: 49
#000000049 in _ZN4core9panicking9panic_fmt17h8e7152a45a601b4bE () at /home/pln/rust/klee/src/
#100000055 in _ZN4core9panicking5panic17h9a94013c5e0723bbE () at /rustc/edaac35d67bed09260dc0c318acc5212fb66246e/src/libcore/
#200000023 in main () at /home/pln/rust/klee/klee-examples/examples/
The error found is at line 22.
In this case it is the Rust built in division by zero detection that causes a `panic!`.
The error found is at line 24.
``` rust
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment