From 93073bdc45c32628a38069bc694334af370136bd Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Thu, 9 Jan 2020 02:23:30 +0100
Subject: [PATCH] This is the way!
---
Cargo.toml | 10 ++---
examples/assume_assert.rs | 1 +
examples/cortex_m_rt_test.rs | 2 +
examples/cortex_m_rt_test2.rs | 2 +
examples/cortex_m_rt_test3.rs | 5 +++
examples/cortex_m_test1.rs | 1 +
examples/cortex_m_test_nightly.rs | 2 +-
examples/f401_minimal.rs | 1 +
examples/klee_hybrid_test.rs | 64 +++++++++++++++++--------------
examples/klee_init_expand.rs | 54 --------------------------
examples/klee_rtfm_expand.rs | 29 --------------
examples/klee_rtfm_init_test.rs | 26 -------------
examples/klee_test copy 2.rs | 33 ----------------
examples/paths.rs | 2 +-
examples/register_test.rs | 2 +
examples/struct.rs | 59 ++++++++++++++++++++++++----
examples/vcell_test.rs | 6 +++
17 files changed, 115 insertions(+), 184 deletions(-)
delete mode 100644 examples/klee_init_expand.rs
delete mode 100644 examples/klee_rtfm_expand.rs
delete mode 100644 examples/klee_rtfm_init_test.rs
delete mode 100644 examples/klee_test copy 2.rs
diff --git a/Cargo.toml b/Cargo.toml
index f6ebd3e..1d0a236 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 8ad40eb..bf3c8e8 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 266bec4..5d4726e 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 d8309ef..2d6e2fd 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 e608e78..40d17d4 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 02dcb7d..b32155c 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 00dae90..499a803 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 1d1a734..ca716ee 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 7c22c43..4cf7e10 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 15f596f..0000000
--- 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 97951b2..0000000
--- 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 488f793..0000000
--- 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 2dc2836..0000000
--- 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 5ecad1b..df641d0 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 8b30504..637bea8 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 3d90506..8889b74 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 b0b637e..babc274 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!
--
GitLab