From cf45768f69527f2f0111e0242cc98b05736c0d9e Mon Sep 17 00:00:00 2001 From: Per <Per Lindgren> Date: Sun, 25 Nov 2018 15:41:10 +0100 Subject: [PATCH] README --- README.md | 80 +++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 60 insertions(+), 20 deletions(-) diff --git a/README.md b/README.md index 42b1230..3f7c9da 100644 --- a/README.md +++ b/README.md @@ -1,13 +1,27 @@ -# 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 (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 + +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/lib.rs:24: 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/lang_items.rs:6: 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/lib.rs -Line: 24 -assembly.ll line: 76 -Stack: - #000000076 in _ZN4core9panicking9panic_fmt17hc7d7358b749037fdE () at /home/pln/klee/klee-rust/klee/src/lib.rs:24 - #100000070 in _ZN4core9panicking5panic17h4680eb5ae9b0e3d0E () at HOME/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/src/libcore/pani -cking.rs:51 - #200000044 in main (=1, =94362321163792) at PWD/klee-examples/examples/foo.rs:22 +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/lang_items.rs +Line: 6 +assembly.ll line: 49 +Stack: + #000000049 in _ZN4core9panicking9panic_fmt17h8e7152a45a601b4bE () at /home/pln/rust/klee/src/lang_items.rs:6 + #100000055 in _ZN4core9panicking5panic17h9a94013c5e0723bbE () at /rustc/edaac35d67bed09260dc0c318acc5212fb66246e/src/libcore/panicking.rs:52 + #200000023 in main () at /home/pln/rust/klee/klee-examples/examples/foo.rs:24 ``` -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 -- GitLab