diff --git a/README.md b/README.md
index d392dab12f564df32de5b8cb02822096c3898ca6..56fdc5bbdb57c5ebc4db29f2684487adb0b9d833 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,10 @@
# 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: ERROR: /home/pln/rust/klee/src/lang_items.rs:6: abort failure
-KLEE: NOTE: now ignoring this error at this location
+$ cargo klee --help
+cargo-klee 0.2.0
+Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>
+KLEE analysis of Rust application
-KLEE: done: total instructions = 22
-KLEE: done: completed paths = 2
-KLEE: done: generated tests = 2
-```
+USAGE:
+ cargo-klee [FLAGS] [OPTIONS] --bin <NAME> --example <NAME>
-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'
-```
+FLAGS:
+ --all-features Activate all available features
+ -g, --gdb Run the generated replay binary in `gdb`. The environment variable `GDB_CWD` determines the
+ `gdb` working directory, if unset `gdb` will execute in the current working directory
+ -h, --help Prints help information
+ -k, --klee Run KLEE test generatation [default enabled unless --replay]
+ --release Build artifacts in release mode, with optimizations
+ -r, --replay Generate replay binary in target directory
+ -V, --version Prints version information
+ -v, --verbose Use verbose output
-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
-```
+OPTIONS:
+ --bin <NAME> Build only the specified binary
+ --example <NAME> Build only the specified example
+ --features <FEATURES> Space-separated list of features to activate
-In this case it is the Rust built in division by zero detection that causes a `panic!`.
-The error found is at line 24.
+$ cargo klee --bin foo --release
-``` rust
-#![no_std]
-#![no_main]
+....
-#[macro_use]
-extern crate klee;
-
-use core::ptr;
-
-#[no_mangle]
-fn main() {
- let u = ksymbol!("u");
-
- unsafe {
- ptr::read_volatile(&f2(f1(u)));
- }
-}
-
-// add 1 wrapping
-fn f1(u: u8) -> u8 {
- u.wrapping_add(1)
-}
+KLEE: output directory is "/home/pln/rust/cargo-klee/klee-examples/target/release/deps/klee-out-5"
+KLEE: Using Z3 solver backend
+KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31: abort failure
+KLEE: NOTE: now ignoring this error at this location
-fn f2(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.
\ No newline at end of file