diff --git a/examples/panic1.rs b/examples/panic1.rs new file mode 100644 index 0000000000000000000000000000000000000000..e578971297abb283ce684ff44d95f3ff83a08358 --- /dev/null +++ b/examples/panic1.rs @@ -0,0 +1,112 @@ +//! 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. diff --git a/examples/panic2.rs b/examples/panic2.rs new file mode 100644 index 0000000000000000000000000000000000000000..47fc06aa35a1780e04e2536621dccecc1d5e3527 --- /dev/null +++ b/examples/panic2.rs @@ -0,0 +1,125 @@ +//! 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. diff --git a/examples/panic3.rs b/examples/panic3.rs new file mode 100644 index 0000000000000000000000000000000000000000..da3ac12448fef95a84e6387a1db2f3a455f71474 --- /dev/null +++ b/examples/panic3.rs @@ -0,0 +1,120 @@ +//! 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. diff --git a/examples/panic4.rs b/examples/panic4.rs new file mode 100644 index 0000000000000000000000000000000000000000..a6e1a7bc326181b2e20fd1d7cfcedb2076ee9ece --- /dev/null +++ b/examples/panic4.rs @@ -0,0 +1,97 @@ +//! 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?