mostly comments and README.md

README.md

 # klee-examples
 
-This repo contains a set of usage examples for `klee-sys` low-level KLEE bindings.
+This repo contains a set of usage examples for `klee-sys` low-level KLEE bindings. For more information on internal design behind see the [klee-sys](https://gitlab.henriktjader.com/pln/klee-sys) repo.
 
-## paths.rs
+See section `Cargo.toml` for detaled information on features introduced.
 
-This example showcase the different path termintaiton conditions possible and their effect to KLEE test case generation.
+### General dependencies
 
-## assume_assert.rs
+- llvm toolchain tested with (9.0.1)
+- rustup tested with 1.40.0 (73528e339 2019-12-16)
+- klee tested with KLEE 2.1-pre (https://klee.github.io)
 
-This example showcase contract based verification, and the possibilies to extract proofs.
+- cargo-klee (installed from git)
 
-## struct.rs
+---
 
-This example show the case of partially symbolic structures.
+## Basic test examples
 
-## vcell_test.rs
+- `paths.rs`
 
-Simple test to showcase low-level `vcell` access.
+    This example showcase the different path termintaiton conditions possible and their effect to KLEE test case generation.
 
-## register_test.rs
+- `assume_assert.rs`
 
-Simple test to showcase the use of the `volatile-register` abstraction.
+    This example showcase contract based verification, and the possibilies to extract proofs.
 
-## f401_minimal.rs
+- `struct.rs`
 
-This example showcase the execution of code on the stm32f401 (and similar targets from the f4).
+    This example show the case of partially symbolic structures.
+
+---
+
+## Hardware oriented test examples
+
+- `vcell_test.rs`
+
+    Simple test to showcase low-level [vcell](https://github.com/perlindgren/vcell) access. `vcell` underlies all machine generated hardware accesses in the Rust embedded ecosystem.
+
+    The `klee-analysis` feature replaces `read` operations to memory by symbolic values (using `klee-sys`). `write` operations are suppressed as for analysis we are not interested in the side effects.
+
+- `register_test.rs`
+
+    Simple test to showcase the use of the `volatile-register` abstraction. `volitile-register` builds on `vcell` and is used by both hand written and machine generated hardware accesses in the Rust embedded ecosystem. 
+
+- `cortex-m-test1.rs`
+
+   Simple test to showcase the [cortex-m](https://github.com/perlindgren/vcell) abstraction of ARM-core peripherals ARM thumb assembly instructions and ARM thumb CPU registers. `cortex-m` uses the `volatile-register` abstraction for ARM-core peripherals. The `klee-analysis` feature replaces read operations on CPU registers by symbolic data and suppresses write operations as for analysis we are not interested in the side effects.
 
-### dependencies
+   Moreover the example showcase the discrepancies between Rust source code paths and paths in the generated (semantically equivalent) LLVM-IR.  
 
-- stm32401 nucleo board or similiar with recent stlink firmware
-- (recent) openocd (tested with version 0.10.0)
-- arm-none-eabi-gdb (tested with version 0.8.3)
-- llvm target thumbv7em-none-eabi (`rustup target add thumbv7em-none-eabi`)
+   TODO: perhaps the latter part should be moved to Basic test examples as it is not `cortex-m` specific.
+
+- `cortex-m-test-nightly.rs`
+
+    This example showcase how compiler "intrinsics" can be safely adopted by proving the absence of errors.
+
+    TODO: perhaps this part should also be moved to Basic test examples as it is not `cortex-m` specific.
+
+---
+
+## Testing on hardware
+
+### Additional Dependencies:
+
+- `stm32401` Nucleo64 board or similar with recent `stlink` firmware (tested with latest firmware as of 2020-01-10).
+- `openocd` (tested with version 0.10.0)
+- `arm-none-eabi-gdb` (tested with version 0.8.3)
+- llvm target `thumbv7em-none-eabihf` 
+  - `> rustup show`, to show current Rust tool-chain and installed targets.
+  - `> rustup target add <target>`, to add target, e.g., `thumbv7em-none-eab¡hf`.
+  
+### Examples
+
+- `f401_minimal.rs`
+
+This example showcase the execution of code on the stm32f401 (and similar targets from the f4).
 
+--
 
 ## Licencse
 
 Copyright Per Lindgren.
 
-All rights reserved, use restricted for non-commercial purpose.
\ No newline at end of file
+All rights reserved, use restricted for non-commercial purpose.

examples/assume_assert.rs

@@ -23,7 +23,7 @@ fn f1(a: u32) -> u32 {
 
 // This example showcase how contracts can be encoded
 //
-// Let us start with the functian f1 (above).
+// Let us start with the function f1 (above).
 // Intuitively `f1(a) > a` right?
 //
 // Well let's check that....
@@ -59,23 +59,56 @@ fn f1(a: u32) -> u32 {
 //
 // > cargo klee --example assume_assert
 //
-// We can now finalize the contract, by uncommenting line 20 (with the post condition).
+// We can now finalize the contract, by un-commenting line 20 (with the post condition).
 //
 // So our pre-condition is that a < u32.MAX and the post condition is that r > a.
 //
 // Can assumptions go wrong?
 // Well they can? And we will spot it!
 //
-// Try uncommenting line 18, re-run `cargo klee`
+// Try un-commenting line 18, re-run `cargo klee`
 //
 // You should get...
 // KLEE: ERROR: /home/pln/.cargo/git/checkouts/klee-sys-7ee2aa8a1a6bbc46/c8275a3/src/lib.rs:19: invalid klee_assume call (provably false)
 //
 // So KLEE tracks the "path condition", i.e., at line 18 it knows (assumes) that that
-// a < u32::MAX, and finds that the assumtion a == u32::MAX cannot be satisfied.
+// a < u32::MAX, and finds that the assumption a == u32::MAX cannot be satisfied.
 //
-// This is exeteremely powerful as KLEE tracks all known "constraints" and all their raliaitons
+// This is extremely powerful as KLEE tracks all known "constraints" and all their raliaitons
 // and mathematically checks for the satisfiability of each "assume" and "assert".
-//
 // So what we get here is not a mere test, but an actual proof!!!!
 // This is the way!
+//
+// In the future we could provide some additional syntactic support for
+// contracts. It could look something like:
+//
+//#[contract: {
+// pre: a < u32::MAX,
+// post: f1(a) > a,
+// } ]
+//fn f1(a: u32) -> u32 {
+//     a + 1
+//}
+//
+// The corresponding generated code could look something like:
+// fn f1(a: u32) -> u32 {
+//     klee_assume(a < u32::MAX); // pre
+//     let r = f1_body(a);
+//     klee_assert!(r > a); // post
+//     r
+// }
+// #[inline(always)]
+// fn f1_body(a: u32) -> u32 {
+//     a + 1
+// }
+//
+// It might even be possible to derive post condtitions from pre conditions,
+// and report them to the user. Problem is that the conditions are
+// represented as "first order logic" (FOL) constraints, which need to be
+// converted into readable form (preferably Rust expressions.)
+//
+// Another potential extension is the extend contracts, assumptions and assertions
+// to support FOL natively, this would give us logic quantifiers:
+// `forall` and `exists`. Using FOL we can reason on programs in a more
+// general way, however the system will be significantly more difficult
+// to understand and use, so it remains to be seen/evaluated.

examples/cortex_m_test1.rs

@@ -45,7 +45,7 @@ fn main() {
 //
 // This is due to that the `dwt.read` has rendered `a` as a symbolic value.
 //
-// Now let's comment out line 18 and uncamment line 19.
+// Now let's comment out line 18 and un-comment line 19.
 //
 // > cargo klee --example cortex_m_test1
 // ...
@@ -76,7 +76,7 @@ fn main() {
 // So what we see here, is that the if statement is nowhere to be found
 // and we call @obort(), and the code below is unreachable (as abort() -> !)
 //
-// This is semantically equivallent to:
+// This is semantically equivalent to:
 // if a == unsafe { S } {
 //     // panic!();
 //     klee_abort!(); // (A)
@@ -104,6 +104,6 @@ fn main() {
 // Our test provides "complete" coverage regarding the semantics of the source code
 // (as we have not missed any potential error).
 //
-// This example is of course contrieved, but showcase that "classical" measures/
+// This example is of course contrived, but showcase that "classical" measures/
 // quality goals restated and certification procedures updated accordingly!
 // This is the way!

examples/cortex_m_test_nightly.rs

@@ -2,7 +2,7 @@
 #![no_std]
 #![no_main]
 
-use klee_sys::klee_abort;
+use klee_sys::*;
 extern crate cortex_m;
 extern crate panic_klee;
 
@@ -13,18 +13,25 @@ use core::{intrinsics::unchecked_div, num::Wrapping, ptr::read_volatile};
 #[no_mangle]
 fn main() {
     let peripherals = Peripherals::take().unwrap();
-    // let peripherals = Peripherals::take().unwrap();
+
     let mut dwt = peripherals.DWT;
     dwt.enable_cycle_counter();
     let a = dwt.cyccnt.read();
     let b = dwt.cyccnt.read();
     let c = dwt.cyccnt.read();
+    // let d = (Wrapping(c) - (Wrapping(b) - Wrapping(100))).0;
+    // klee_assume(d != 0);
     unsafe {
         let some_time_quota = unchecked_div(a, (Wrapping(c) - (Wrapping(b) - Wrapping(100))).0);
         read_volatile(&some_time_quota); // prevent optimization in release mode
     }
 }
 
+// Notice this example currently requires the nightly build of Rust.
+// > rustup override set nightly
+// When you are done with this example, you may return to stable Rust.
+// > rust override unset
+//
 // > cargo klee --example cortex_m_test_nightly -r -k -g -v
 // ...
 // KLEE: WARNING: undefined reference to function: rust_eh_personality
@@ -133,5 +140,13 @@ fn main() {
 // We can fearlessly apply optimisations (including intrinsic/primitive operations)
 // and let the tool prove that the code is free of potential errors.
 //
-// Thus we get BOTH improved performance and improved reliability/correctness at the same time.
+// Try uncommenting lines 22 and 23. This introduces a sufficient assumption
+// for KLEE to prove the absence of errors. (Beware that this guarantee
+// holds only for the exact source code given. If you change anything
+// the analysis needs to be re-done.)
+//
+// In conclusion, programs proven free of errors offer both
+// - improved performance (allow safe use of intrinsics), and
+// - improved reliability/correctness
+// at the same time.
 // This is the way!

examples/paths.rs

@@ -11,7 +11,7 @@ fn main() {
     let mut a: i32 = 0;
     klee_make_symbolic!(&mut a, "a");
     // Rust panic on a == 200 (div by zero), or a - 200 (causing an arithmetic overflow).
-    let _ = 100 / (a - 200); // let _ = 100 / a.wrapping_sub(200);
+    let _ = 100 / a.wrapping_sub(200);
 
     let _ = match a {
         0 => klee_abort!(),
@@ -23,7 +23,7 @@ fn main() {
         6 => klee_assert_eq!(false, true),
         _ => (),
     };
-    panic!("at end"); // just one instane of panic! will be spotted
+    panic!("at end"); // just one instance of panic! will be spotted
 }
 
 // KLEE will generate one test per explicit error: