# Cargo subcommand `cargo klee` to compile Rust crates for KLEE analysis
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.
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. KLEE infers further checks for common program errors, e.g., out of bounds indexing and division by zero.
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. In the general case of adopting unchecked operations safety can be
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, a Rust program passing KLEE analysis is thus ensured to be panic free at run-time, and thus 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. 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. under a `klee-analysis` feature) the assertions (and their implied overhead) will be omitted in a production build.
## Requirements
...
...
@@ -10,10 +12,10 @@ ensured by adding assertions to the source. If those assertions are condititonal
- LLVM KLEE installed from recent package
- LLVM llc and clang for building replay binaries
- GNU gdb for executing replay binaries
- nightly toolchain (edition-2018)
- nightly toolchain (edition-2018), tested with nightly-2019-01-25-x86_64-unknown-linux-gnu
The `klee` tool needs to installed and accissible in path. The tool has been tested on a
the master branch of KLEE (https://github.com/klee/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 (https://aur.archlinux.org/packages/klee/), altered to refer `source` to the KLEE master branch.
The `klee` tool needs to installed and accissible in path. The tool has been tested on the master branch of KLEE (https://github.com/klee/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 (https://aur.archlinux.org/packages/klee/), altered to refer `source` to the KLEE master branch.
## TODO
...
...
@@ -26,97 +28,47 @@ If the code under analysis is targeting another architecture (e.g., with other b
## usage
``` console
$systemctl start docker.service # if not already started/enabled, docker is optional
$cargo install--path cargo-klee # add -f, if already installed
$cd klee-examples
$cargo klee --example foo --release
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: NOTE: now ignoring this error at this location
fnf2(u:u8)->u8{
100/u// <- Rust div 0 panic!
}
KLEE: done: total instructions = 10
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
```
The application is compiled for `#[no_std]` (thus isolating the application to dependencies of the environment). `extern crate klee` gives us access to the `klee` bindings. `ksymbol` marks the variable `u` as symbolic (unknown). `read_volatile(&T)` ensures that `T` is computed (and thus prevents the corresesponding code from being optimized out by the compiler).
## Examples
Further examples is found in the `klee-examples` directory.
-`foo`, shows the above example.
-`foo2`, shows further use of `ksymbol!(&mut T, &str)` for making declared variables symbolic.
\ No newline at end of file
You may analyse code using either `--bin` and `--examples`. See `src/foo.rs` for a complete example for analysis and replay functionality.
