Merge branch 'klee' of gitlab.henriktjader.com:KLEE/cortex-m-rtfm-klee into klee

examples/panic1.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::k_assert;
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+        },
+    },
+}
+
+fn exti1() {
+    let mut j = 0;
+    for _ in 0..100 {
+        j += 1;
+    }
+    k_assert(j == 100);
+    k_assert(j == 101);
+}
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// LLVM KLEE is a tool for symbolic execution operating on LLVM bit code (`*.bc` files)
+//
+// You can generate a LLVM BC from a Rust RTFM application by
+//
+// 1> rustup override set nightly-2018-01-10
+//
+// 2> xargo build --example panic1 --features klee_mode --target x86_64-unknown-linux-gnu
+//
+// 1) We need a slightly older version of Rust with a LLVM 4 backend to run KLEE
+//    `rustup override` will stick the direcory to a set tool-chain (run once)
+//
+// 2) As LLVM runs on our host we generate the `.bc` with x86 as target
+//
+// Start a docker with pre-installed KLEE tools
+//
+// 3>  docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+//
+// 3) This will start the docker with the right previliges and mount the directory
+//    where the example `.bc` file(s) are stored (shared/overlayed with the host file system).
+//
+// You can now let KLEE run on the `.bc` file.
+//
+// 4> klee panic1*.bc
+// ...
+// KLEE: WARNING: undefined reference to function: WWDG
+// KLEE: WARNING: executable has module level assembly (ignoring)
+// KLEE: ERROR: /home/pln/klee/cortex-m-rtfm/klee/src/lib.rs:48: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+//
+// KLEE: done: total instructions = 66549
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 2
+//
+// Here the loop is executed by the virtual machine and the `k_assert`s checked.
+// As a expected the second `k_assert` will fail (as j is 100 not 101).
+//
+// The latest experiment is linked under the `klee-last` directory.
+//
+// 5> ls klee-last
+// ...
+// test000002.abort.err
+// ...
+// 6> cat klee-last/test000002.abort.err
+// ...
+// #100000921 in EXTI1 () at /home/pln/klee/cortex-m-rtfm/examples/panic1.rs:19
+// ...
+// 6) the file gives you a stack trace leading up to the error,
+//    we are just concerned with the line number in the `panic1.rs` file.
+//
+// So the lesson learned here is just that KLEE can execute our code
+// and we can get stack traces for failing assertions, nothing more.
+//
+// Show to the lab assistant that you can replicate the above, and explain
+// the process and result.

examples/panic2.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+        },
+    },
+}
+
+fn exti1() {
+    let mut j: u8 = 0; // unsigned 8 bit integer
+    k_symbol!(&mut j, "j");
+    if j > 10 {
+        k_abort();
+    } else {
+        k_assert(1 == 0);
+    }
+}
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// The real power of KLEE is the ability to symbolic execution.
+// We mark the mutable variable `j` as being symbolic (unknown).
+//
+// > xargo build --example panic2 --features klee_mode --target x86_64-unknown-linux-gnu
+//
+// You can now let KLEE run on the `.bc` file.
+//
+// > klee panic1*.bc
+// ...
+// KLEE: ERROR: /home/pln/klee/cortex-m-rtfm/klee/src/lib.rs:48: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: /home/pln/klee/cortex-m-rtfm/klee/src/lib.rs:48: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+
+// KLEE: done: total instructions = 193
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+//
+// > ls klee-last/*err
+// klee-last/test000002.abort.err  klee-last/test000003.abort.err
+//
+// > cat klee-last/test000002.abort.err
+//  ... /home/pln/klee/cortex-m-rtfm/examples/panic2.rs:35
+//
+// > cat klee-last/test000003.abort.err
+//  ... /home/pln/klee/cortex-m-rtfm/examples/panic2.rs:37
+//
+// (logically a failing `k_assert` amounts to a `k_abort`)
+//
+// KLEE also provides us with "counter examples" for the failing assertions.
+//
+// We can use the `ktest-tool` (python script) to inspect those.
+//
+// > ktest-tool klee-last/test000002.ktest
+// ktest file : 'klee-last/test000002.ktest'
+// args       : ['panic2-46c7df2ab3607698.bc']
+// num objects: 2
+// object    0: name: b'task'
+// object    0: size: 4
+// object    0: data: b'\x00\x00\x00\x00'
+// object    1: name: b'j'
+// object    1: size: 1
+// object    1: data: b'\xff'
+//
+// task here amounts to the task we are inspecting (in this case only one...)
+// 'j' has the value 0xff (255 as integer), triggering the `then` branch
+//
+// and
+// > ktest-tool klee-last/test000003.ktest
+// ...
+// object    1: name: b'j'
+// object    1: size: 1
+// object    1: data: b'\x00'
+//
+// here 'j' has the value 0x00 (0 as integer), triggering the `else` branch
+//
+// How, can KLEE figure out concrete values for the symbolic variable `j`?
+// Well, it tracks the data dependencies and condititonals along feasible execution paths
+// of the program (task EXTI1 in our case). And when encountering a `k_abort`
+// it passes the collected (path) condition to an SMT solver.
+// The solver returns with a concrete assigmnent for a `k_abort` if possible.
+// This can be seen as a reachabilty proof or (equivalently) as a counter example
+// to an `k_assert`.
+//
+// Show to the lab assistant that you can replicate the above, and explain
+// the process and result.

examples/panic3.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u64 = 0;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X],
+        },
+        EXTI2: {
+            path: exti2,
+            priority: 1,
+            resources: [X],
+        },
+    },
+}
+
+fn exti1(t: &mut Threshold, r: EXTI1::Resources) {
+    k_assert(*r.X > 0);
+}
+
+fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
+    // k_assume(*r.X > 0 && *r.X < 8); // our pre-condition
+    // let y = *r.X + 1;
+    // *r.X = y;
+    // k_assert(*r.X > 0 && *r.X < 8); // our post-condition
+}
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust RTFM is a framework for concurrent programming, ensuring race free
+// access to shared resources. In this example we have a single resource X
+// with a non atomic data type (u64), amounting to sequential reads
+// (which are 32 bit on the ARM Cortex M).
+//
+// However the framework analysis is clever enought to realize that the tasks
+// `EXTI1` and `EXTI2` can never preempt each other, hence we can
+// can access the data without "claiming" the resouce.
+//
+// Access is done by "dereferencing" `*r.X`, and we can now assert the
+// the value to be `*r.X`. However, as tasks operetate concurrently,
+// (without knowlegde on other tasks in the system), our analysis here
+// marks `X` as a (implicitly) symbolic.
+//
+// Compile and run the example in KLEE.
+// Find the failing assertion, and the concrete assignment of X that
+// triggers the fail.
+//
+// You might find that the task identifier is no longer 0.
+// On the host side you find the list of tasks by.
+//
+// > more klee/tasks.txt
+// autogenerated file
+// ["EXTI1", "EXTI2"]
+//
+// In this case EXTI => task 0, EXTI2 = task 1, but they might be swapped
+// due to the underlyind data structure being an (unordered) hash-map.
+//
+// Now uncomment the code in `exiti2` and comment out the assertion in `exti1`.
+//
+// Run the KLEE tool and find the failing assertion.
+//
+// What value of X was assigned by KLEE for the assertion to fail.
+// ** your answer here **
+//
+// The designers intent was a saturating add (with a max value of 7)
+//
+// Fix the error by an if statement.
+//
+// Run KLEE and see that the analysis passes without errors.
+//
+// Show the lab assistant your solution.
+//
+// Comment out your solution.
+//
+// Now fix the error using the Rust `min` function (on u64).
+//
+// Run KLEE and see that the analysis passes without errors.
+//
+// Show the lab assistant your solution.

examples/panic4.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u64 = 1;
+        static A:[u64; 11] = [0; 11];
+        static I:u64 = 0;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X],
+        },
+        EXTI2: {
+            path: exti2,
+            priority: 1,
+            resources: [X, A, I],
+        },
+    },
+}
+
+fn exti1(t: &mut Threshold, mut r: EXTI1::Resources) {
+    // k_assume(*r.X > _ && *r.X < _); // pre-condition on X
+    let u = 11 / (*r.X);
+    *r.X = u;
+    // k_assert(*r.X > _ && *r.X < _); // post-condition on X
+}
+
+fn exti2(t: &mut Threshold, r: EXTI2::Resources) {
+    // k_assume(*r.X > _ && *r.X < _); // pre-contition on X
+    let b = r.A[*r.X as usize];
+    *r.I = b;
+    // as we don't change X post-condtiton is trivially true
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-condtitons
+// at the same time.
+//
+// If not, why is that not possible?