diff --git a/Cargo.toml b/Cargo.toml
index f6ebd3e9e500a1c52d1c5017a368759fbecf43c3..1d0a2361b95351b32cb1ab1705d0e551ddf35f82 100644
--- a/Cargo.toml
+++ b/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
diff --git a/examples/assume_assert.rs b/examples/assume_assert.rs
index 8ad40ebe1a40e8ad1ddb4c24dbb9a3c8eb06884c..bf3c8e83f65082a553f17e7f0f807ae0414297ac 100644
--- a/examples/assume_assert.rs
+++ b/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!
diff --git a/examples/cortex_m_rt_test.rs b/examples/cortex_m_rt_test.rs
index 266bec4b8e6d22cfd10b661a60edde03ef5926d7..5d4726e31a6e2c78f5a932576bf4c52692d2b0f8 100644
--- a/examples/cortex_m_rt_test.rs
+++ b/examples/cortex_m_rt_test.rs
@@ -32,3 +32,5 @@ unsafe fn main() -> ! {
#[pre_init]
unsafe fn pre_init() {}
+
+// This is the way.
diff --git a/examples/cortex_m_rt_test2.rs b/examples/cortex_m_rt_test2.rs
index d8309ef8cf1541b879d04de02fa804560a0ac1a5..2d6e2fd0abc76146d5eaa0864fced09c8c4ad007 100644
--- a/examples/cortex_m_rt_test2.rs
+++ b/examples/cortex_m_rt_test2.rs
@@ -26,3 +26,5 @@ unsafe fn main() -> ! {
#[pre_init]
unsafe fn pre_init() {}
+
+// This is the way!
diff --git a/examples/cortex_m_rt_test3.rs b/examples/cortex_m_rt_test3.rs
index e608e7812b3fa2ff5e185ab7278d0f6007e66f12..40d17d4d2e0a351720ccc661a1f6ef41e87fefaf 100644
--- a/examples/cortex_m_rt_test3.rs
+++ b/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!
diff --git a/examples/cortex_m_test1.rs b/examples/cortex_m_test1.rs
index 02dcb7d6062bb7c70ca736f190e098b76b85bfdd..b32155c045ee4c39d22353f7793dd62e602740d8 100644
--- a/examples/cortex_m_test1.rs
+++ b/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!
diff --git a/examples/cortex_m_test_nightly.rs b/examples/cortex_m_test_nightly.rs
index 00dae900c63ae422c53b8f32d5ad2c2a4960c597..499a8034c66f7c0a24e68391152335f30ac2ffab 100644
--- a/examples/cortex_m_test_nightly.rs
+++ b/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!
diff --git a/examples/f401_minimal.rs b/examples/f401_minimal.rs
index 1d1a7347304f6e946ea0a1242c7aaa61d1f8a4ea..ca716eee56850b60fd9fab0d8a1263ebd148ef49 100644
--- a/examples/f401_minimal.rs
+++ b/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!
diff --git a/examples/klee_hybrid_test.rs b/examples/klee_hybrid_test.rs
index 7c22c43dfd3658ac6f57e3f7958fdc7259c63dcb..4cf7e10343fdd4af0e042616affa07d097f9a847 100644
--- a/examples/klee_hybrid_test.rs
+++ b/examples/klee_hybrid_test.rs
@@ -5,36 +5,44 @@
#![no_main]
#[cfg(feature = "klee-analysis")]
-use panic_klee as _;
+mod klee_analysis {
+ use klee_sys::*;
+ use panic_klee as _;
-#[cfg(not(feature = "klee-analysis"))]
-use panic_halt as _;
+ // 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 v = 0;
+ klee_make_symbolic!(&mut v, "v");
+ let r = super::f(v);
+ }
+}
#[cfg(not(feature = "klee-analysis"))]
-#[no_mangle]
-fn main() {
- let mut a = 0;
- panic!();
-}
+mod bare_metal {
+ extern crate panic_halt;
+ use cortex_m_rt::entry;
+ use cortex_m_semihosting::hprintln;
+ use stm32f4::stm32f401 as stm32;
-#[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
+ #[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!
diff --git a/examples/klee_init_expand.rs b/examples/klee_init_expand.rs
deleted file mode 100644
index 15f596f3805d3f625a199ccd372fd56dd2038575..0000000000000000000000000000000000000000
--- a/examples/klee_init_expand.rs
+++ /dev/null
@@ -1,54 +0,0 @@
-#![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());
-}
diff --git a/examples/klee_rtfm_expand.rs b/examples/klee_rtfm_expand.rs
deleted file mode 100644
index 97951b28842f095c291e90254050f5c3f45f9c35..0000000000000000000000000000000000000000
--- a/examples/klee_rtfm_expand.rs
+++ /dev/null
@@ -1,29 +0,0 @@
-// 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();
diff --git a/examples/klee_rtfm_init_test.rs b/examples/klee_rtfm_init_test.rs
deleted file mode 100644
index 488f793857124a123db1479fd98d71341b9fefbe..0000000000000000000000000000000000000000
--- a/examples/klee_rtfm_init_test.rs
+++ /dev/null
@@ -1,26 +0,0 @@
-//! 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();
- }
-};
diff --git a/examples/klee_test copy 2.rs b/examples/klee_test copy 2.rs
deleted file mode 100644
index 2dc2836ca0c6f519ba1bf369f67cf5ea0f91b57b..0000000000000000000000000000000000000000
--- a/examples/klee_test copy 2.rs
+++ /dev/null
@@ -1,33 +0,0 @@
-#![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
-}
diff --git a/examples/paths.rs b/examples/paths.rs
index 5ecad1b7f22c79ae63f39df3965e6f1b74acdb44..df641d0b2e1415743a083bbd7886b24b0f26b985 100644
--- a/examples/paths.rs
+++ b/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!
diff --git a/examples/register_test.rs b/examples/register_test.rs
index 8b30504619bf6ba90e8ecb9e95b65598312c745f..637bea821ed662b9216c7019c8e781c43b91d511 100644
--- a/examples/register_test.rs
+++ b/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!
diff --git a/examples/struct.rs b/examples/struct.rs
index 3d90506b8011e3e2041ff16e0a54a24b31a7513d..8889b7494fb706f23e2285d8d52d9f92d7415f9b 100644
--- a/examples/struct.rs
+++ b/examples/struct.rs
@@ -1,11 +1,10 @@
+// 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!
diff --git a/examples/vcell_test.rs b/examples/vcell_test.rs
index b0b637e924a20ba17a1723ca1caea21661021d45..babc274f6ef213439fe59840923f737f7bb0b233 100644
--- a/examples/vcell_test.rs
+++ b/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!