From ccf21da99f8ddbb0742fac22b795cf944f9e449f Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Fri, 10 Jan 2020 16:09:19 +0100
Subject: [PATCH] mostly comments and README.md
---
README.md | 81 +++++++++++++++++++++++--------
examples/assume_assert.rs | 45 ++++++++++++++---
examples/cortex_m_test1.rs | 6 +--
examples/cortex_m_test_nightly.rs | 21 ++++++--
examples/paths.rs | 4 +-
5 files changed, 124 insertions(+), 33 deletions(-)
diff --git a/README.md b/README.md
index dc1a2d1..4712f56 100644
--- a/README.md
+++ b/README.md
@@ -1,41 +1,84 @@
# 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.
diff --git a/examples/assume_assert.rs b/examples/assume_assert.rs
index bf3c8e8..788ae13 100644
--- a/examples/assume_assert.rs
+++ b/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.
diff --git a/examples/cortex_m_test1.rs b/examples/cortex_m_test1.rs
index b32155c..08ac0ea 100644
--- a/examples/cortex_m_test1.rs
+++ b/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!
diff --git a/examples/cortex_m_test_nightly.rs b/examples/cortex_m_test_nightly.rs
index 499a803..7151685 100644
--- a/examples/cortex_m_test_nightly.rs
+++ b/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!
diff --git a/examples/paths.rs b/examples/paths.rs
index df641d0..71a096c 100644
--- a/examples/paths.rs
+++ b/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:
--
GitLab