This is the way!

Cargo.toml

@@ -66,13 +66,13 @@ f4 = ["stm32f4/stm32f401", "stm32f4/rt", "cortex-m-semihosting", "cortex-m-rt"]
 
 [profile.dev]
 panic = "abort"
-# incremental = false # used to be required due to bug in rust toolchain
+incremental = false # needed due to bug in rust toolchain
 lto = true
 # codegen-units = 1 # used to be required due to bug in rust toolchain
 
 [profile.release]
-debug = true
 panic = "abort"
-incremental = false
-lto = true
-codegen-units = 1
+debug = true        # better debugging
+incremental = false # better optimization
+lto = true          # better optimization
+codegen-units = 1   # better optimization

examples/assume_assert.rs

@@ -78,3 +78,4 @@ fn f1(a: u32) -> u32 {
 // 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!

examples/cortex_m_rt_test.rs

@@ -32,3 +32,5 @@ unsafe fn main() -> ! {
 
 #[pre_init]
 unsafe fn pre_init() {}
+
+// This is the way.

examples/cortex_m_rt_test2.rs

@@ -26,3 +26,5 @@ unsafe fn main() -> ! {
 
 #[pre_init]
 unsafe fn pre_init() {}
+
+// This is the way!

examples/cortex_m_rt_test3.rs

@@ -99,3 +99,8 @@ fn PendSV() {
 fn SysTick() {
     //klee_abort!();
 }
+
+// Test all bindings to the cortex core.
+// Todo: handle weak bindings
+// Todo: handle arbitrary interrupt bindings
+// This is the way!

examples/cortex_m_test1.rs

@@ -106,3 +106,4 @@ fn main() {
 //
 // This example is of course contrieved, but showcase that "classical" measures/
 // quality goals restated and certification procedures updated accordingly!
+// This is the way!

examples/cortex_m_test_nightly.rs

@@ -134,4 +134,4 @@ fn main() {
 // 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.
-// This is the Way!
+// This is the way!

examples/f401_minimal.rs

@@ -29,3 +29,4 @@ fn main() -> ! {
 // openocd -f openocd.cfg
 //
 // cargo run --example f401_minimal --features f4 --target thumbv7em-none-eabihf
+// This is the way!

examples/klee_hybrid_test.rs

@@ -5,36 +5,44 @@
 #![no_main]
 
 #[cfg(feature = "klee-analysis")]
+mod klee_analysis {
+    use klee_sys::*;
     use panic_klee as _;
 
-#[cfg(not(feature = "klee-analysis"))]
-use panic_halt as _;
-
-#[cfg(not(feature = "klee-analysis"))]
+    // we could use `cortex-m-rt` and entry here as well but it introduces some noise.
+    // so in principle main could be exactly the same, for analysis and run
     #[no_mangle]
     fn main() {
-    let mut a = 0;
-    panic!();
+        let mut v = 0;
+        klee_make_symbolic!(&mut v, "v");
+        let r = super::f(v);
+    }
 }
 
-#[cfg(feature = "klee-analysis")]
-use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-#[cfg(feature = "klee-analysis")]
-#[no_mangle]
-fn main() {
-    let mut a = 0;
-    klee_make_symbolic!(&mut a, "a");
-    // Rust panic on a == 200;
-    let _ = 100 / (a - 200);
-    match a {
-        0 => klee_abort!(),
-        1 => klee_abort!(),
-        2 => klee_abort!(),
-        3 => panic!("3"), // just one instance of panic! will be spotted
-        4 => klee_assert!(false),
-        5 => klee_assert_eq!(false, true),
-        6 => klee_assert_eq!(false, true),
-        _ => (),
-    };
-    panic!("at end"); // just one instane of panic! will be spotted
+#[cfg(not(feature = "klee-analysis"))]
+mod bare_metal {
+    extern crate panic_halt;
+    use cortex_m_rt::entry;
+    use cortex_m_semihosting::hprintln;
+    use stm32f4::stm32f401 as stm32;
+
+    #[entry]
+    fn main() -> ! {
+        let r = super::f(72); // 72 happened to be the value but it could be u32::MAX, who knows?
+        hprintln!("Hello, world! {}", r).unwrap();
+
+        loop {}
+    }
 }
+// some potentially dangerous function
+fn f(v: u32) -> u32 {
+    v + 1
+}
+
+// For KLEE analysis:
+// cargo klee --example klee_hybrid_test
+//
+// For bare metal execution
+// cargo run --example klee_hybrid_test --features f4 --target thumbv7em-none-eabihf
+//
+// This is the way!

examples/klee_init_expand.rs

-#![feature(core_intrinsics)]
-#![feature(rustc_private)]
-#![feature(core_panic)]
-#![feature(prelude_import)]
-//! examples/init.rs
-
-// #![deny(unsafe_code)]
-// #![deny(warnings)]
-#![no_main]
-#![no_std]
-
-#[cfg(feature = "klee-analysis")]
-use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-
-#[no_mangle]
-fn main() -> ! {
-    fn_to_test();
-    loop {}
-}
-
-// Safe access to local `static mut` variable
-
-#[cfg(feature = "klee-analysis")]
-fn fn_to_test() {
-    let mut a = 0; // just one instance of panic! will be spotted
-                   // just one instane of panic! will be spotted
-
-    ::klee_sys::klee_make_symbolic(unsafe { &mut a }, unsafe {
-        ::klee_sys::CStr::from_bytes_with_nul_unchecked("a\u{0}".as_bytes())
-    });
-    match a {
-        0 => unsafe { ::klee_sys::ll::abort() },
-        1 => unsafe { ::klee_sys::ll::abort() },
-        2 => ::core::panicking::panic("explicit panic", ::core::intrinsics::caller_location()),
-        3 => ::core::panicking::panic("3", ::core::intrinsics::caller_location()),
-        4 => {
-            if !false {
-                unsafe { ::klee_sys::ll::abort() };
-            }
-        }
-        5 => {
-            if !(false == true) {
-                unsafe { ::klee_sys::ll::abort() };
-            }
-        }
-        6 => {
-            if !(false == true) {
-                unsafe { ::klee_sys::ll::abort() };
-            }
-        }
-        _ => (),
-    };
-    ::core::panicking::panic("at end", ::core::intrinsics::caller_location());
-}

examples/klee_rtfm_expand.rs

-// klee-analysis
-#![feature(prelude_import)]
-#![feature(rustc_private)]
-//! examples/init.rs
-
-// #![deny(unsafe_code)]
-// #![deny(warnings)]
-#![no_main]
-#![no_std]
-#[prelude_import]
-use core::prelude::v1::*;
-#[macro_use]
-extern crate core;
-#[macro_use]
-extern crate compiler_builtins;
-
-// use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-use panic_klee as _;
-// use rtfm;
-
-#[no_mangle]
-fn main() -> ! {
-    loop {}
-}
-//static mut X: u32 = 0;
-
-// Safe access to local `static mut` variable
-// let _x: &'static mut u32 = X;
-//    fn_to_test();

examples/klee_rtfm_init_test.rs

-//! examples/init.rs
-
-// #![deny(unsafe_code)]
-// #![deny(warnings)]
-#![no_main]
-#![no_std]
-
-// use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-use panic_klee as _;
-// use rtfm;
-// use cortex_m_rt as _;
-// use lm3s6965 as _;
-// extern crate cortex_m_rt;
-// extern crate lm3s6965;
-
-#[rtfm::app(device = lm3s6965)]
-const APP: () = {
-    #[init]
-    fn init(_cx: init::Context) {
-        //static mut X: u32 = 0;
-
-        // Safe access to local `static mut` variable
-        // let _x: &'static mut u32 = X;
-        //    fn_to_test();
-    }
-};

examples/klee_test copy 2.rs

-#![no_std]
-#![no_main]
-
-#[cfg(feature = "klee-analysis")]
-use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-
-#[cfg(not(feature = "klee-analysis"))]
-use panic_halt as _;
-
-#[cfg(not(feature = "klee-analysis"))]
-#[no_mangle]
-fn main() {
-    let mut a = 0;
-    panic!();
-}
-
-#[cfg(feature = "klee-analysis")]
-#[no_mangle]
-fn main() {
-    let mut a = 0;
-    klee_make_symbolic!(&mut a, "a");
-    match a {
-        0 => klee_abort!(),
-        1 => klee_abort!(),
-        2 => panic!(),
-        3 => panic!("3"), // just one instance of panic! will be spotted
-        4 => klee_assert!(false),
-        5 => klee_assert_eq!(false, true),
-        6 => klee_assert_eq!(false, true),
-        _ => (),
-    };
-    panic!("at end"); // just one instane of panic! will be spotted
-}

examples/paths.rs

@@ -110,4 +110,4 @@ fn main() {
 //
 // In this case we see that the panic was triggered by the division by zero.
 //
-//
+// This is the way!

examples/register_test.rs

@@ -144,3 +144,5 @@ fn main() {
 //
 // If this does not work its a gdb problem
 // try lldb the LLVM debugger (debug info may not be completely compatible)
+//
+// This is the way!

examples/struct.rs

+// showcase partially symbolic structures
+
 #![no_std]
 #![no_main]
 
-#[macro_use]
-extern crate klee_sys;
-
-#[cfg(not(feature = "klee-analysis"))]
-extern crate panic_halt;
+use klee_sys::*;
+use panic_klee as _;
 
 struct A {
     a: u8,
@@ -15,13 +14,12 @@ struct A {
 #[no_mangle]
 fn main() {
     let mut a = 0;
-    // ksymbol!(&mut a, "a");
+    klee_make_symbolic!(&mut a, "a");
     let mut u = A { a: a, b: 0 };
     u.b = 7;
     let _ = f2(f1(u.a));
 }
 
-// add 1 wrapping instead of panic
 fn f1(u: u8) -> u8 {
     u.wrapping_add(1)
 }
@@ -29,3 +27,50 @@ fn f1(u: u8) -> u8 {
 fn f2(u: u8) -> u8 {
     100 / u
 }
+
+// Often we may have structures with partially unknown data.
+//
+// Let us find out what valu of `u` that may cause a ponic by replay in gdb.
+//
+// > cargo klee --example struct -k -g -r
+//
+// 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 = 175
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 2
+// ...
+// Reading symbols from struct.replay...
+// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
+// (gdb) run
+// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/struct.replay
+// [Inferior 1 (process 114832) exited with code 0144]
+// (gdb) set env KTEST_FILE=klee-last/test000002.ktest
+// (gdb) run
+// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/struct.replay
+
+// Program received signal SIGABRT, Aborted.
+// 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// (gdb) bt
+// #0  0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// #1  0x00007ffff7dbd897 in abort () from /usr/lib/libc.so.6
+// #2  0x000055555555533b in rust_begin_unwind (_info=0x7fffffffd308) at /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8
+// #3  0x000055555555529d in core::panicking::panic_fmt () at src/libcore/panicking.rs:139
+// #4  0x0000555555555309 in core::panicking::panic () at src/libcore/panicking.rs:70
+// #5  0x000055555555526d in struct::f2 (u=0) at examples/struct.rs:28
+// #6  0x000055555555520f in main () at examples/struct.rs:20
+//
+// So it's f2(u=0) that crashes.
+// Let us take a look at frame 6, calling f2(f1(u.a)).
+//
+// (gdb) f 6
+// #6  0x000055555555520f in main () at examples/struct.rs:20
+// 20          let _ = f2(f1(u.a));
+// (gdb) i locals
+// u = struct::A {a: 255, b: 7}
+// a = 255
+//
+// So in this cose u.a = 255, causes a wraparound, and that in turn causes the crash.
+// Not obvious to the naked eye.
+// This is the way!

examples/vcell_test.rs

@@ -14,3 +14,9 @@ fn main() {
         _ => (),
     };
 }
+
+// cargo klee --example vcell_test
+//
+// We get three paths, as the vc is made symbolic.
+//
+// This is the way!