Skip to content
Snippets Groups Projects
Commit 62864935 authored by Per's avatar Per
Browse files

cortex_m_rt_test

parent 7fa81f96
Branches
No related tags found
No related merge requests found
...@@ -9,6 +9,7 @@ panic-halt = "0.2.0" ...@@ -9,6 +9,7 @@ panic-halt = "0.2.0"
vcell = "0.1.2" vcell = "0.1.2"
volatile-register = "0.2.0" volatile-register = "0.2.0"
cortex-m-rt = "0.6.11"
[dependencies.lm3s6965] [dependencies.lm3s6965]
version = "0.1.3" version = "0.1.3"
...@@ -37,12 +38,12 @@ optional = true ...@@ -37,12 +38,12 @@ optional = true
[patch.crates-io] [patch.crates-io]
vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" } vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
# volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" } cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" }
[features] [features]
klee-analysis = [ "vcell/klee-analysis", "cortex-m/klee-analysis" ] klee-analysis = [ "vcell/klee-analysis", "cortex-m/klee-analysis", "cortex-m-rt/klee-analysis" ]
rtpro = [ "cortex-m-rtfm/klee-analysis", "lm3s6965" ]
[profile.dev] [profile.dev]
panic = "abort" panic = "abort"
......
#![no_std]
#![no_main]
// extern crate cortex_m;
use cortex_m_rt::{entry, pre_init};
use panic_klee as _;
use klee_sys::klee_abort;
use cortex_m::peripheral::Peripherals;
// #[entry]
// unsafe 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();
// if a == 100 {
// klee_abort!();
// }
// klee_abort!();
// }
#[pre_init]
unsafe fn pre_init() {}
// > cargo klee --example klee_cortex_m_test -r -k -g -v --release
// ...
// KLEE: done: total instructions = 33
// KLEE: done: completed paths = 1
// KLEE: done: generated tests = 1
//
// The example, has just one path, leading up to an abort.
// The reason is that the progam unconditionally will panic, as
// taking the peripheral is only only allowed once (for soundness).
// (Internally this in tracked by a state variable.)
//
// This is very good news, that KLEE will detect the error at compile time.
//
// Let's remove the error to see if the example code is correct.
// (comment out the second `take`)
//
// > cargo klee --example klee_cortex_m_test -r -k -g -v
// ...
// KLEE: ERROR: examples/klee_cortex_m_test.rs:120: divide by zero
// KLEE: NOTE: now ignoring this error at this location
// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
// KLEE: NOTE: now ignoring this error at this location
//
// KLEE: done: total instructions = 1454
// KLEE: done: completed paths = 6
// KLEE: done: generated tests = 4
// ..
//(gdb) shell ls klee-last
// assembly.ll info messages.txt run.istats run.stats test000001.div.err test000001.kquery test000001.ktest test000002.ktest warnings.txt
//
// So we see that test000001.ktest was causing a division error,
// the other test case passed
//
// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
// (gdb) run
// Starting program: /home/pln/rust/grepit/klee-examples/target/debug/examples/klee_cortex_m_test.replay
// Program received signal SIGFPE, Arithmetic exception.
// 0x0000555555555528 in main () at examples/klee_cortex_m_test.rs:133
// 133 let some_time_quota = unchecked_div(a, c - (b - 100));
//
// Let's look at the actual test
// (gdb) shell ktest-tool klee-last/test000001.ktest
// ktest file : 'klee-last/test000001.ktest'
// args : ['/home/pln/rust/grepit/klee-examples/target/debug/examples/klee_cortex_m_test-d9038188a1e4d0b0.ll']
// num objects: 5
// object 0: name: 'PRIMASK'
// object 0: size: 4
// object 0: data: b'\x01\x01\x01\x01'
// object 0: hex : 0x01010101
// object 0: int : 16843009
// object 0: uint: 16843009
// object 0: text: ....
// object 1: name: 'vcell'
// object 1: size: 4
// object 1: data: b'\x00\x00\x00\x00'
// object 1: hex : 0x00000000
// object 1: int : 0
// object 1: uint: 0
// object 1: text: ....
// object 2: name: 'vcell'
// object 2: size: 4
// object 2: data: b'\x00\x00\x00\x00'
// object 2: hex : 0x00000000
// object 2: int : 0
// object 2: uint: 0
// object 2: text: ....
// object 3: name: 'vcell'
// object 3: size: 4
// object 3: data: b'd\x00\x00\x00'
// object 3: hex : 0x64000000
// object 3: int : 100
// object 3: uint: 100
// object 3: text: d...
// object 4: name: 'vcell'
// object 4: size: 4
// object 4: data: b'\x00\x00\x00\x00'
// object 4: hex : 0x00000000
// object 4: int : 0
// object 4: uint: 0
// object 4: text: ....
//
// (gdb) backtrace
// #0 0x0000555555555528 in main () at examples/klee_cortex_m_test.rs:133
// (gdb) print a
// $1 = 0
// (gdb) print b
// $2 = 100
// (gdb) print c
// $3 = 0
//
// In order to analyze hardware dependent code, hardware access are treated
// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
// might in the future change to giving the address to the register instead.
//
// A breakdown of the example:
// Behind the scenes the PRIMASK register is accessed, and given concrete value.
// (Under the hood, `Peripherals.take` executes in a global critical section.)
//
// This access is along the "happy path" towards the error, so any value would
// suffice (in this case 0x00000000 was selected by KLEE).
//
// The first `vcell` access: was done when enabling the cycle counter.
// The rest of accesses stem from reading `a`, `b`, and `c`.
// Critical here is that KLEE spots that `(c - (b - 100)) = 0`, leading up to a division
// by zero error (satisfied by `c == 0` and `b == 100`)
//
// Notice here, that this error is spotted EVEN while we are telling
// Rust to use the primitive (intrinsic) division for "unchecked_div" performance.
//
#![feature(core_intrinsics)] // we use intrinsic division
#![no_std]
#![no_main]
// extern crate klee_sys;
extern crate cortex_m;
extern crate panic_klee;
use cortex_m::peripheral::Peripherals;
use core::{intrinsics::unchecked_div, 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();
unsafe {
let some_time_quota = unchecked_div(a, c - (b - 100));
read_volatile(&some_time_quota); // prevent optimization
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment