diff --git a/Cargo.1.lock b/Cargo.1.lock
new file mode 100644
index 0000000000000000000000000000000000000000..7cdd108925ce60d9ec30b8ed257990d9951ac7ef
--- /dev/null
+++ b/Cargo.1.lock
@@ -0,0 +1,355 @@
+[[package]]
+name = "aligned"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "backtrace"
+version = "0.3.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "backtrace-sys 0.1.16 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cfg-if 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libc 0.2.36 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rustc-demangle 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "winapi 0.3.4 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "backtrace-sys"
+version = "0.1.16"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cc 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libc 0.2.36 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "bare-metal"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "cc"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "cfg-if"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "chrono"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "num 0.1.42 (registry+https://github.com/rust-lang/crates.io-index)",
+ "time 0.1.39 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "aligned 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bare-metal 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "aligned 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bare-metal 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "untagged-option 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rt"
+version = "0.3.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "chrono 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.3.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rustc_version 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rtfm"
+version = "0.3.1"
+dependencies = [
+ "cortex-m 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rt 0.3.13 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rtfm-macros 0.3.0",
+ "klee 0.1.0",
+ "rtfm-core 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "stm32f413 0.2.0 (git+https://gitlab.henriktjader.com/pln/stm32f413.git)",
+ "untagged-option 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rtfm-macros"
+version = "0.3.0"
+dependencies = [
+ "error-chain 0.10.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "klee 0.1.0",
+ "quote 0.3.15 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rtfm-syntax 0.2.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 0.11.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cstr_core"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "memchr 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cty"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "error-chain"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "backtrace 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "klee"
+version = "0.1.0"
+dependencies = [
+ "cstr_core 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "libc"
+version = "0.2.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "memchr"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "num"
+version = "0.1.42"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "num-integer 0.1.36 (registry+https://github.com/rust-lang/crates.io-index)",
+ "num-iter 0.1.35 (registry+https://github.com/rust-lang/crates.io-index)",
+ "num-traits 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "num-integer"
+version = "0.1.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "num-traits 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "num-iter"
+version = "0.1.35"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "num-integer 0.1.36 (registry+https://github.com/rust-lang/crates.io-index)",
+ "num-traits 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "num-traits"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "quote"
+version = "0.3.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "r0"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "redox_syscall"
+version = "0.1.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rtfm-core"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rtfm-syntax"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "error-chain 0.10.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 0.3.15 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 0.11.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "rustc-demangle"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rustc_version"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver-parser"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "stm32f413"
+version = "0.2.0"
+source = "git+https://gitlab.henriktjader.com/pln/stm32f413.git#b54e84d86efdaa584f8be7ed52242d716b0c799f"
+dependencies = [
+ "bare-metal 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rt 0.3.13 (registry+https://github.com/rust-lang/crates.io-index)",
+ "vcell 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "syn"
+version = "0.11.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "quote 0.3.15 (registry+https://github.com/rust-lang/crates.io-index)",
+ "synom 0.11.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "unicode-xid 0.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "synom"
+version = "0.11.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "unicode-xid 0.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "time"
+version = "0.1.39"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "libc 0.2.36 (registry+https://github.com/rust-lang/crates.io-index)",
+ "redox_syscall 0.1.37 (registry+https://github.com/rust-lang/crates.io-index)",
+ "winapi 0.3.4 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "unicode-xid"
+version = "0.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "untagged-option"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "vcell"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "volatile-register"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "vcell 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "winapi"
+version = "0.3.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "winapi-i686-pc-windows-gnu 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "winapi-x86_64-pc-windows-gnu 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[metadata]
+"checksum aligned 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "d1a92995cea48691c7c93e12597cca4d692bb3130d0a291c7141b9793c7829e7"
+"checksum backtrace 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "ebbbf59b1c43eefa8c3ede390fcc36820b4999f7914104015be25025e0d62af2"
+"checksum backtrace-sys 0.1.16 (registry+https://github.com/rust-lang/crates.io-index)" = "44585761d6161b0f57afc49482ab6bd067e4edef48c12a152c237eb0203f7661"
+"checksum bare-metal 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "aacbba24771a81cfe18f5aedd5bf3208ca8324ecdd9344ddb61f8d2a051a4574"
+"checksum cc 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)" = "deaf9ec656256bb25b404c51ef50097207b9cbb29c933d31f92cae5a8a0ffee0"
+"checksum cfg-if 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "d4c819a1287eb618df47cc647173c5c4c66ba19d888a6e50d605672aed3140de"
+"checksum chrono 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "7c20ebe0b2b08b0aeddba49c609fe7957ba2e33449882cb186a180bc60682fa9"
+"checksum cortex-m 0.3.1 (registry+https://github.com/rust-lang/crates.io-index)" = "4d553ca1f23403c81e6d3d28a64ef6e8eadd7f395195aacda65cbc0dc987738e"
+"checksum cortex-m 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)" = "2864dd1e83344abe7a6192befbeb8cd88bf763cfc560e28680d5b06a8ce9b7f7"
+"checksum cortex-m-rt 0.3.13 (registry+https://github.com/rust-lang/crates.io-index)" = "53c69efde430b7033dff0257ab2d899be0c66d1d60091aa6ff1eea8db0f74e44"
+"checksum cstr_core 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "7829882406e7b36cff95319f674b72fc51dd3b0e6968f33db8f6a26903c1e128"
+"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
+"checksum error-chain 0.10.0 (registry+https://github.com/rust-lang/crates.io-index)" = "d9435d864e017c3c6afeac1654189b06cdb491cf2ff73dbf0d73b0f292f42ff8"
+"checksum libc 0.2.36 (registry+https://github.com/rust-lang/crates.io-index)" = "1e5d97d6708edaa407429faa671b942dc0f2727222fb6b6539bf1db936e4b121"
+"checksum memchr 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "148fab2e51b4f1cfc66da2a7c32981d1d3c083a803978268bb11fe4b86925e7a"
+"checksum num 0.1.42 (registry+https://github.com/rust-lang/crates.io-index)" = "4703ad64153382334aa8db57c637364c322d3372e097840c72000dabdcf6156e"
+"checksum num-integer 0.1.36 (registry+https://github.com/rust-lang/crates.io-index)" = "f8d26da319fb45674985c78f1d1caf99aa4941f785d384a2ae36d0740bc3e2fe"
+"checksum num-iter 0.1.35 (registry+https://github.com/rust-lang/crates.io-index)" = "4b226df12c5a59b63569dd57fafb926d91b385dfce33d8074a412411b689d593"
+"checksum num-traits 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "e7de20f146db9d920c45ee8ed8f71681fd9ade71909b48c3acbd766aa504cf10"
+"checksum quote 0.3.15 (registry+https://github.com/rust-lang/crates.io-index)" = "7a6e920b65c65f10b2ae65c831a81a073a89edd28c7cce89475bff467ab4167a"
+"checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
+"checksum redox_syscall 0.1.37 (registry+https://github.com/rust-lang/crates.io-index)" = "0d92eecebad22b767915e4d529f89f28ee96dbbf5a4810d2b844373f136417fd"
+"checksum rtfm-core 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "11ba440da895db782b3e459c39316133e36ee13c60a836bb99f7df4940beb441"
+"checksum rtfm-syntax 0.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "c87b30451349244ed3d59115a9b57a3723ae7f512c906223fd0a32e37719d699"
+"checksum rustc-demangle 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)" = "f312457f8a4fa31d3581a6f423a70d6c33a10b95291985df55f1ff670ec10ce8"
+"checksum rustc_version 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a54aa04a10c68c1c4eacb4337fd883b435997ede17a9385784b990777686b09a"
+"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
+"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
+"checksum stm32f413 0.2.0 (git+https://gitlab.henriktjader.com/pln/stm32f413.git)" = "<none>"
+"checksum syn 0.11.11 (registry+https://github.com/rust-lang/crates.io-index)" = "d3b891b9015c88c576343b9b3e41c2c11a51c219ef067b264bd9c8aa9b441dad"
+"checksum synom 0.11.3 (registry+https://github.com/rust-lang/crates.io-index)" = "a393066ed9010ebaed60b9eafa373d4b1baac186dd7e008555b0f702b51945b6"
+"checksum time 0.1.39 (registry+https://github.com/rust-lang/crates.io-index)" = "a15375f1df02096fb3317256ce2cee6a1f42fc84ea5ad5fc8c421cfe40c73098"
+"checksum unicode-xid 0.0.4 (registry+https://github.com/rust-lang/crates.io-index)" = "8c1f860d7d29cf02cb2f3f359fd35991af3d30bac52c57d265a3c461074cb4dc"
+"checksum untagged-option 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "89553f60895e868761e18120e72077da22920614562d2f4fe98fa707fbb12fe6"
+"checksum vcell 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "45c297f0afb6928cd08ab1ff9d95e99392595ea25ae1b5ecf822ff8764e57a0d"
+"checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
+"checksum winapi 0.3.4 (registry+https://github.com/rust-lang/crates.io-index)" = "04e3bd221fcbe8a271359c04f21a76db7d0c6028862d1bb5512d85e1e2eb5bb3"
+"checksum winapi-i686-pc-windows-gnu 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+"checksum winapi-x86_64-pc-windows-gnu 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
diff --git a/examples/resource.rs b/examples/resource.rs
index fda75f6fe8fe183f6c47060e1da7424b6c78f08d..f82b222f8be90ab9cd740af7b0345f3db706dd32 100644
--- a/examples/resource.rs
+++ b/examples/resource.rs
@@ -75,8 +75,8 @@ fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
r.X.claim_mut(t, |x, _| {
*x += 1;
});
- cortex_m::asm::bkpt();
- cortex_m::asm::bkpt()
+ // cortex_m::asm::bkpt();
+ // cortex_m::asm::bkpt()
}
#[inline(never)]
diff --git a/expand_wcet_bkpt.rs b/expand_wcet_bkpt.rs
new file mode 100644
index 0000000000000000000000000000000000000000..3e23cde2a55d34acb35594e96a0d834df4beb641
--- /dev/null
+++ b/expand_wcet_bkpt.rs
@@ -0,0 +1,899 @@
+#![feature(prelude_import)]
+#![no_std]
+//! Example using shared resources
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+#![feature(asm)]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core as core;
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::*;
+use rtfm::{bkpt_1, bkpt_2, bkpt_3};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+// this is the path to the device crate
+
+#[allow(non_camel_case_types)]
+#[allow(non_snake_case)]
+pub struct _initResources<'a> {
+ pub Y: &'a mut u32,
+ pub X: &'a mut u32,
+}
+#[allow(unsafe_code)]
+mod init {
+ pub struct Peripherals {
+ pub core: ::stm32f413::CorePeripherals,
+ pub device: ::stm32f413::Peripherals,
+ }
+ pub use _initResources as Resources;
+ #[allow(unsafe_code)]
+ impl<'a> Resources<'a> {
+ pub unsafe fn new() -> Self {
+ Resources {
+ Y: &mut ::_Y,
+ X: &mut ::_X,
+ }
+ }
+ }
+}
+#[allow(private_no_mangle_statics)]
+#[no_mangle]
+static mut _Y: u32 = 0;
+#[allow(private_no_mangle_statics)]
+#[no_mangle]
+static mut _X: u32 = 0;
+pub unsafe fn read_resources() {
+ let _ = k_read(&_Y);
+ let _ = k_read(&_X);
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI2::Y {
+ type Data = u32;
+ fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+ // cortex_m::asm::bkpt();
+ // cortex_m::asm::bkpt()
+
+ // Static code analysis
+ // In this lab we will study how a Rust RTFM application can be
+ // statically analysed.
+ //
+ // The application has three tasks EXTI1, EXTI2 and EXTI3,
+ // with associated priorites 1 (lowest), 3 (highest), and 2 (mid).
+ //
+ // Assignment 1.
+ // Build the application for KLEE analysis.
+ // > xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu
+ //
+ // Start the KLEE docker
+ // > 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
+ //
+ // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
+ // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+ //
+ // Now run KLEE in the docker.
+ // > klee resource-*.bc
+ // KLEE: WARNING: executable has module level assembly (ignoring)
+ // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
+ // KLEE: NOTE: now ignoring this error at this location
+
+ // KLEE: done: total instructions = 11575
+ // KLEE: done: completed paths = 25
+ // KLEE: done: generated tests = 16
+ //
+ // When compiled with the --features klee_mode, resources are treated as symbolic.
+ // Investigate the output files (in `klee-last`). Use `ktest-tool` to examine the tests.
+ // The file `klee/tasks.txt` gives the order of tasks, it may vary for each run.
+ // ```
+ // // autogenerated file
+ // ["EXTI1", "EXTI2", "EXTI3"]
+ // ```
+ //
+ // How many tests were generated for task EXIT1?
+ // ** your answer here **
+ // Why that many, (look at the code and the generted tests).
+ // ** your answer here **
+ //
+ // How many tests were generated for task EXIT2?
+ // ** your answer here **
+ // Why that many, (look at the code and the generted tests).
+ // ** your answer here **
+ //
+ // How many tests were generated for task EXIT3?
+ // ** your answer here **
+ // Why that many, (look at the code and the generted tests).
+ // ** your answer here **
+ //
+ // (There will be one additional "dymmy" test for testing "no task".)
+ //
+ // Now identify the cause of generated error.
+ // > more klee-last/*.abort.err
+ //
+ // Find the error on the source code and fix it.
+ // Hint, use *wrapping arithmetics*.
+ //
+ // Repeat the code generation, run KLEE agian and fix errors until
+ // no more errors are found.
+ //
+ // How many errors were identified?
+ // ** your answer here **
+ //
+ // For one of the arithmetic operations, no error was found.
+ // Explain why this is no error.
+ // ** your answer here **
+ //
+ // Why didn't KLEE report all the errors initially?
+ // Scroll back and compare the stack traces of the generated errors.
+ // Hint, for each line in the code KLEE will spot ONE error.
+ // ** your answer here **
+ //
+ // Assignment 2.
+ // KLEE has now generated tests covering EACH feasible path for EACH task.
+ // Now we will analyse the exection time for each such test.
+ //
+ // In order to do that comiple your application.
+ // > xargo build --example resource --release --features wcet_bkpt --target thumbv7em-none-eabihf
+ //
+ // We build in --release for optimizing the performance.
+ // The --features wcet_bkpt will insert a `bkpt` instruction on LOCK ond UNLOCK of
+ // of each resource. This allows you to monitor the number of clock cyckles using gdb.
+ //
+ // Connect your Nucleo64 board with the `stm32f401re` (or `stm32f411re`) MCU.
+ // Start openocd in a separate terminal (and let it run there).
+ //
+ // > openocd -f interface/stlink.cfg -f target/stm32f4x.cfg
+ // (You may use `-f inteface/stlink-v2-1.cfg`, if `stlink.cfg` is missing.)
+ //
+ // Start gdb.
+ // > arm-none-eabi-gdb -x gdbinit_manual target/thumbv7em-none-eabihf/release/examples/resource
+ //
+ // The `gdbinit_manual` has the following content.
+ // ```
+ // target remote :3333
+ // mon reset halt
+ // load
+ // tb main
+ // continue
+ //
+ // Line by line, it:
+ // - connects to the target (the MCU)
+ // - resets the MCU
+ // - loads the binary, in this case set to target/thumbv7em-none-eabihf/release/examples/resource
+ // - sets a temporary breakpoint to `main`, and
+ // - continues executing until `main` is reached.
+ //
+ // At the point the MCU hits `main` it stops.
+ // (You may be promted to continue working <return> or quit, in such case press <return>.)
+ //
+ // Now you can inspect where the processor halted.
+ // > (gdb) list
+ // 560 // be executed *before* enabling the FPU and that would generate an
+ // 561 // exception
+ // 562 #[inline(never)]
+ // 563 fn main() {
+ // 564 unsafe {
+ // 565 ::main(0, ::core::ptr::null());
+ // 566 }
+ // 567 }
+ // 568
+ // 569 main()
+ //
+ // As you see this is not part of your program, rather it originates from the library startup code.
+ //
+ // This is perfect, now the MCU is initiated and under your control.
+ //
+ // At this point the memory (resources), holds their initial values from the
+ // your application (this was set by the library code prior to hitting main).
+ // You can inspect the global reasources (they are prepended by `_`).
+ //
+ // (gdb) p resource::_X
+ // $1 = 0
+ // (gdb) p resource::_Y
+ // $2 = 0
+ //
+ // Before calling our tasks we need to enable the debug timer (cycle counter in the DWT unit of the MCU).
+ //
+ // (gdb) mon mww 0xe0001000 1
+ //
+ // and set the counter value to 0
+ //
+ // (gdb) mon mww 0xe0001004 0
+ //
+ // Now we can call the task(s). Lets start easy with EXTI3.
+ // (gdb) call stub_EXTI3()
+ // (gdb) mon mrw 0xe0001004
+ // 9
+ //
+ // Wow, it took only 9 clock cycles to run the complete task!!!!
+ // (Compare to a threaded OS that would require several 100 clock cycles to start a thread/task)
+ //
+ // But hey, where did my claim go? Wasn't I supposed to hit a breakpoint when claiming the resource?
+ // (In this case the resource X)
+ // Well Rust RTFM is smart enough to know that you are already at sufficient threshold (priority)
+ // in order to grant you the resource dircectly. Let us look at the code.
+ //
+ // (gdb) disassemble stub_EXTI3
+ // Dump of assembler code for function stub_EXTI3:
+ // 0x08000268 <+0>: movw r0, #0
+ // 0x0800026c <+4>: movt r0, #8192 ; 0x2000
+ // 0x08000270 <+8>: ldr r1, [r0, #0]
+ // 0x08000272 <+10>: adds r1, #1
+ // 0x08000274 <+12>: str r1, [r0, #0]
+ // 0x08000276 <+14>: bx lr
+ // End of assembler dump.
+ //
+ // Here you go, cannot be simpler that this, it:
+ // - sets up the address to X in r0
+ // - reads the old value
+ // - adds 1 (wrapping arithmetics)
+ // - stores the new value in X, and
+ // - it returns
+ // (On Cortex M functions and inerrupt handlers are essentially treated the same way)
+ //
+ // So now you can check the value of X. See above...
+ // ** your answer here **
+ //
+ // Now let us turn to EXTI2.
+ // (gdb) mon mww 0xe0001004 0
+ // (gdb) call stub_EXTI2()
+ // (gdb) mon mrw 0xe0001004
+ // 13
+ //
+ // Also in this case we see that the resource (`Y`) was granted without overhead
+ // The code took a few additional clock cycles (its contians a condition, right).
+ // Figure out which path was triggered by this test.
+ // ** your answer here **
+ //
+ // Now figure out how to test the other branch
+ // you can use
+ // (gdb) set resource::_Y=...
+ // to set a value in memory
+ //
+ // Make a call to the `stub_EXTI2()` with the set value of `_Y`.
+ // How many clock cycles did you get (rember to set the counter to 0 before calling)
+ // ** your answer here **
+ //
+ // Check the nwe value of `_Y`.
+ // ** your answer here **
+ //
+ // Hint, if done correctly, you should have the same number of cycles for both paths.
+ // Ok, so the cycle count was the same ;)
+ // How so, lets have a look at the generated assembly.
+ //
+ // (gdb) disassemble stub_EXTI2
+ // Dump of assembler code for function stub_EXTI2:
+ // 0x080002aa <+0>: movw r0, #0
+ // 0x080002ae <+4>: mov.w r2, #4294967295 ; 0xffffffff
+ // 0x080002b2 <+8>: movt r0, #8192 ; 0x2000
+ // 0x080002b6 <+12>: ldr r1, [r0, #4]
+ // 0x080002b8 <+14>: cmp r1, #10
+ // 0x080002ba <+16>: it cc
+ // 0x080002bc <+18>: movcc r2, #1
+ // 0x080002be <+20>: add r1, r2
+ // 0x080002c0 <+22>: str r1, [r0, #4]
+ // 0x080002c2 <+24>: bx lr
+ // End of assembler dump.
+ //
+ // This one is a bit harder to understand.
+ // What it does essentially is:
+ // - read `Y` into r1,
+ // - store -1 in r2
+ // - conditionally overwrite the r2 by a 1 if `Y < 10`
+ // - add r2 to r1 (the value of `Y`),
+ // - update `Y`.
+ //
+ // So this is beautiful, the COSTLY branch is replaced by a CHEAP
+ // condtitonal assigmnet `movcc`.
+ // You can read more on this on
+ // http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0553a/BABEHFEF.html
+ //
+ // Ok, back to the program...
+ // Now recall the KLEE generated test cases.
+ // Spot the ones regarding EXTI2.
+ // What assignments would KLEE suggest to `Y` to test both paths.
+ // ** your answers here **
+ //
+ // So, your test assignments or the ones from KLEE, which ones is better?
+ // ** your answer here **
+
+ // (We will return to optimising test cases later... so put this on your mental stack :)
+ //
+ // Now lets have a look at the tricky one EXTI1.
+ // (gdb) mon mww 0xe0001004 0
+ // (gdb) call stub_EXTI1()
+ // Program received signal SIGTRAP, Trace/breakpoint trap.
+ // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+ // at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+ // 167 bkpt();
+ // The program being debugged was signaled while in a function called from GDB.
+ // GDB remains in the frame where the signal was received.
+ // To change this behavior use "set unwindonsignal on".
+ // Evaluation of the expression containing the function
+ // (stub_EXTI1) will be abandoned.
+ // When the function is done executing, GDB will silently stop.
+ //
+ // So what is happening here is that it runs into the (first) brkp intstruction (LOCK `X`).
+ // You may ignore the verbose output at this point....
+ //
+ // Run
+ // (gdb) mon mrw 0xe0001004
+ // 15
+ //
+ // So all in all it took 15 cycles to get there, `claim X`.
+ // We can look at the code causing the `bkpt`
+ // (gdb) list
+ // 162 }
+ // 163
+ // 164 // wcet_bkpt mode
+ // 165 // put breakpoint at raise ceiling, for tracing execution time
+ // 166 if cfg!(feature = "wcet_bkpt") {
+ // 167 bkpt();
+ // 168 }
+ //
+ // That makes sense, we are in the RTFM library handling the `claim X`
+ // (gdb) c
+ // Continuing.
+ // Program received signal SIGTRAP, Trace/breakpoint trap.
+ // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+ // at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+ // 167 bkpt();
+ // (gdb) mon mrw 0xe0001004
+ // 19
+ //
+ // So after 19 clock cycles we claim `Y`
+ //
+ // Now lets have a look at the generated assembly.
+ // (gdb) disassemble
+ // ...
+ // 0x080002f6 <+4>: bcs.n 0x8000334 <resource::<impl rtfm_core::Resource for resource::EXTI1::X>::claim+66>
+ // 0x080002f8 <+6>: movs r1, #224 ; 0xe0
+ // 0x080002fa <+8>: movs r2, #208 ; 0xd0
+ // 0x080002fc <+10>: mrs r12, BASEPRI
+ // 0x08000300 <+14>: msr BASEPRI, r1
+ // 0x08000304 <+18>: bkpt 0x0000
+ // 0x08000306 <+20>: mrs r1, BASEPRI
+ // 0x0800030a <+24>: msr BASEPRI, r2
+ // 0x0800030e <+28>: movw r2, #0
+ // => 0x08000312 <+32>: bkpt 0x0000
+ // 0x08000314 <+34>: movt r2, #8192 ; 0x2000
+ // 0x08000318 <+38>: ldr r3, [r2, #0]
+ // 0x0800031a <+40>: subs r0, r3, #1
+ // 0x0800031c <+42>: cmp r0, #8
+ // 0x0800031e <+44>: ittt ls
+ // 0x08000320 <+46>: ldrls r0, [r2, #4]
+ // 0x08000322 <+48>: addls r0, r3
+ // 0x08000324 <+50>: strls r0, [r2, #4]
+ // 0x08000326 <+52>: bkpt 0x0000
+ // 0x08000328 <+54>: msr BASEPRI, r1
+ // ...
+ //
+ // We are now inside the critital sections of both X and Y and have access to both resources for the loop.
+ // (gdb) c
+ // Continuing.
+ //
+ // Program received signal SIGTRAP, Trace/breakpoint trap.
+ // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+ // at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+ //
+ // We are now releasing `Y`.
+ // (gdb) mon mrw 0xe0001004
+ // 29
+ //
+ // How long (in cycles) was the critical section on `Y`?
+ // ** your answer here **
+
+ // (gdb) disassemble
+ // ...
+ // 0x08000322 <+48>: addls r0, r3
+ // 0x08000324 <+50>: strls r0, [r2, #4]
+ // => 0x08000326 <+52>: bkpt 0x0000
+ // 0x08000328 <+54>: msr BASEPRI, r1
+ // ...
+ //
+ // Let us continue
+ // (gdb) c
+ // Continuing.
+
+ // Program received signal SIGTRAP, Trace/breakpoint trap.
+ // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+ // at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+ // 181 bkpt();
+ //
+ // (gdb) mon mrw 0xe0001004
+ // 30
+ //
+ // How long (in cycles) was the critical section on `X`?
+ // ** your answer here **
+ //
+ // (gdb) disassemble
+ // ...
+ // 0x08000326 <+52>: bkpt 0x0000
+ // 0x08000328 <+54>: msr BASEPRI, r1
+ // => 0x0800032c <+58>: bkpt 0x0000
+ // 0x0800032e <+60>: msr BASEPRI, r12
+ // 0x08000332 <+64>: bx lr
+ //
+ // At this point we can contiue
+ // (gdb) c
+ // Continuing.
+ // EXTI1 has now run to completion.
+ //
+ // What was the total excecution time for EXTI1?
+ // ** your answer here **
+ //
+ // What is the value of the resouce X?
+ // ** your answer here **
+ //
+ // Just by looking at the code, what would the worst case assignment of X be?
+ // I.e., the assingnment of `X' that gives the worst case execution time.
+ // ** your answer here **
+ //
+ // Measure that execution time. What did you get.
+ // ** your answer here **
+ //
+ // Your answer might blow your mind!!! How the heck is that even possible?
+ //
+ // At this point you should find that the worst case time stays the same ...
+ //
+ // Well, this one is not due to RTFM, its due to Rust and the cleverness of LLVM.
+ // What it does is that it figures out that we actually increase `Y`, by the value of `X`.
+ // So the loop is all gone, optimized out, and replaced by a simple addition.
+ //
+ // Now lets look at best case execution time.
+ // Figure out an assignment of `X`, that might actually reduce the execution time.
+ // ** your answer here **
+ //
+ // Redo the experiment with this value. How many clock cycles did you get?
+ // ** your answer here **
+ //
+ // Assignment 3.
+ // In assignment 2 we analysed EXTI1
+ // We found that for the examples, Rust RTFM was able to generate extremely efficient
+ // implementations, replacing branching with contdiditonal assignments and
+ // even remove comlete loops.
+ //
+ // Now lets have a look at using optimized LLVM and how it affects the number of tests.
+ // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
+ //
+ // and now start a docker for the optimized build
+ // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+ //
+ // and in the docker run
+ // > klee resource*.bc
+ //
+ // Look at the generated tests.
+ // Motivate for each of the 5 test cases, which one it matches of the hand generated tests from Assignment 2.
+ // ** your answers (5) here **
+ //
+ // Were the optimized tests sufficient to cover the execution time behavior.
+ // ** your answer here **
+ //
+ // Can you come up with a case where --release mode based analysis would miss cricital cases.
+ // ** your answer here, --- actually a research question, we will discuss in class --- **
+ //
+ // On a side note.
+ // Rust in --release mode makes the job for KLEE much easier. Look the number of instuctions carried out.
+ // In dev/debug you had som 10 000 instuctions executed for generating the test cases.
+ // In --relesase you had 34!!!!!
+ //
+ // This vastly improves on the performance of analysis, allowing larger applications to be scrutenized.
+ // The code we looked at here was by intention simple (to facilitate inspection).
+ // However, the code is NOT trivial, under the hood it utilizes advanced language features, such as
+ // closures and intence use of abstractions, such as Traits/genecics etc. It indeed covers a large
+ // degree of the Rust, for which it demonstrates that our approach to based program analysis
+ // actually works.
+ //
+ // For the future we intend the framework to cover the reading and writing to peripherals, and the
+ // sequenced access to resources. In class we will further discuss current limitations, and
+ // oportunities to improvements.
+ if !(t.value() >= 3u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 3u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &_Y }
+ }
+ fn borrow_mut<'cs>(&'cs mut self, t: &'cs Threshold) -> &'cs mut Self::Data {
+ if !(t.value() >= 3u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 3u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &mut _Y }
+ }
+ fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+ fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI2::Y {
+ type Target = u32;
+ fn deref(&self) -> &Self::Target {
+ unsafe { &_Y }
+ }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI2::Y {
+ fn deref_mut(&mut self) -> &mut Self::Target {
+ unsafe { &mut _Y }
+ }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI2"]
+pub unsafe extern "C" fn _EXTI2() {
+ let f: fn(&mut rtfm::Threshold, EXTI2::Resources) = exti2;
+ f(
+ &mut if 3u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+ rtfm::Threshold::new(::core::u8::MAX)
+ } else {
+ rtfm::Threshold::new(3u8)
+ },
+ EXTI2::Resources::new(),
+ )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI2() {
+ #[allow(unsafe_code)]
+ unsafe {
+ _EXTI2();
+ }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI2 {
+ use core::marker::PhantomData;
+ #[allow(dead_code)]
+ #[deny(const_err)]
+ const CHECK_PRIORITY: (u8, u8) = (3u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 3u8);
+ #[allow(non_camel_case_types)]
+ pub struct Y {
+ _0: PhantomData<*const ()>,
+ }
+ #[allow(non_snake_case)]
+ pub struct Resources {
+ pub Y: Y,
+ }
+ #[allow(unsafe_code)]
+ impl Resources {
+ pub unsafe fn new() -> Self {
+ Resources {
+ Y: Y { _0: PhantomData },
+ }
+ }
+ }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::Y {
+ type Data = u32;
+ fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+ if !(t.value() >= 3u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 3u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &_Y }
+ }
+ fn borrow_mut<'cs>(&'cs mut self, t: &'cs Threshold) -> &'cs mut Self::Data {
+ if !(t.value() >= 3u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 3u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &mut _Y }
+ }
+ fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+ fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::X {
+ type Data = u32;
+ fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+ if !(t.value() >= 2u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 2u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &_X }
+ }
+ fn borrow_mut<'cs>(&'cs mut self, t: &'cs Threshold) -> &'cs mut Self::Data {
+ if !(t.value() >= 2u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 2u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &mut _X }
+ }
+ fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+ fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI1"]
+pub unsafe extern "C" fn _EXTI1() {
+ let f: fn(&mut rtfm::Threshold, EXTI1::Resources) = exti1;
+ f(
+ &mut if 1u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+ rtfm::Threshold::new(::core::u8::MAX)
+ } else {
+ rtfm::Threshold::new(1u8)
+ },
+ EXTI1::Resources::new(),
+ )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI1() {
+ #[allow(unsafe_code)]
+ unsafe {
+ _EXTI1();
+ }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI1 {
+ use core::marker::PhantomData;
+ #[allow(dead_code)]
+ #[deny(const_err)]
+ const CHECK_PRIORITY: (u8, u8) = (1u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 1u8);
+ #[allow(non_camel_case_types)]
+ pub struct Y {
+ _0: PhantomData<*const ()>,
+ }
+ #[allow(non_camel_case_types)]
+ pub struct X {
+ _0: PhantomData<*const ()>,
+ }
+ #[allow(non_snake_case)]
+ pub struct Resources {
+ pub Y: Y,
+ pub X: X,
+ }
+ #[allow(unsafe_code)]
+ impl Resources {
+ pub unsafe fn new() -> Self {
+ Resources {
+ Y: Y { _0: PhantomData },
+ X: X { _0: PhantomData },
+ }
+ }
+ }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI3::X {
+ type Data = u32;
+ fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+ if !(t.value() >= 2u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 2u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &_X }
+ }
+ fn borrow_mut<'cs>(&'cs mut self, t: &'cs Threshold) -> &'cs mut Self::Data {
+ if !(t.value() >= 2u8) {
+ {
+ ::panicking::panic(&(
+ "assertion failed: t.value() >= 2u8",
+ "examples/resource.rs",
+ 19u32,
+ 1u32,
+ ))
+ }
+ };
+ unsafe { &mut _X }
+ }
+ fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+ fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+ where
+ F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+ {
+ unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+ }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI3::X {
+ type Target = u32;
+ fn deref(&self) -> &Self::Target {
+ unsafe { &_X }
+ }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI3::X {
+ fn deref_mut(&mut self) -> &mut Self::Target {
+ unsafe { &mut _X }
+ }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI3"]
+pub unsafe extern "C" fn _EXTI3() {
+ let f: fn(&mut rtfm::Threshold, EXTI3::Resources) = exti3;
+ f(
+ &mut if 2u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+ rtfm::Threshold::new(::core::u8::MAX)
+ } else {
+ rtfm::Threshold::new(2u8)
+ },
+ EXTI3::Resources::new(),
+ )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI3() {
+ #[allow(unsafe_code)]
+ unsafe {
+ _EXTI3();
+ }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI3 {
+ use core::marker::PhantomData;
+ #[allow(dead_code)]
+ #[deny(const_err)]
+ const CHECK_PRIORITY: (u8, u8) = (2u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 2u8);
+ #[allow(non_camel_case_types)]
+ pub struct X {
+ _0: PhantomData<*const ()>,
+ }
+ #[allow(non_snake_case)]
+ pub struct Resources {
+ pub X: X,
+ }
+ #[allow(unsafe_code)]
+ impl Resources {
+ pub unsafe fn new() -> Self {
+ Resources {
+ X: X { _0: PhantomData },
+ }
+ }
+ }
+}
+extern crate cortex_m;
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+pub fn wcet_start() {
+ unsafe { bkpt_3() };
+ let x = k_read(&stub_EXTI2);
+ unsafe { core::ptr::read_volatile(&x) };
+ let x = k_read(&stub_EXTI1);
+ unsafe { core::ptr::read_volatile(&x) };
+ let x = k_read(&stub_EXTI3);
+ unsafe { core::ptr::read_volatile(&x) };
+}
+#[allow(private_no_mangle_fns)]
+#[allow(unsafe_code)]
+fn main() {
+ wcet_start();
+ let idle: fn() -> ! = idle;
+ idle();
+}
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+ X.claim(t, |x, t1| {
+ Y.claim_mut(t1, |y, _| {
+ if *x < 10 {
+ for _ in 0..*x {
+ *y += 1;
+ }
+ }
+ });
+ });
+}
+#[allow(non_snake_case)]
+fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
+ r.Y.claim_mut(t, |y, _| {
+ if *y < 10 {
+ *y += 1;
+ } else {
+ *y -= 1;
+ }
+ });
+}
+#[allow(non_snake_case)]
+fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
+ r.X.claim_mut(t, |x, _| {
+ *x += 1;
+ });
+}
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals, _r: init::Resources) {}
+#[inline(never)]
+#[allow(dead_code)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+fn idle() -> ! {
+ let r = stub_EXTI1;
+ k_read(&r());
+ loop {
+ rtfm::nop();
+ }
+}
diff --git a/klee.py b/klee.py
index d5d7246636abec6378ef1acbf96c3c3b03530d9b..2961ae4a59f161465287b7bb8270067f7cc6e19d 100644
--- a/klee.py
+++ b/klee.py
@@ -45,6 +45,7 @@ def gdb_call(task):
try:
gdb.execute('call %s' % "stub_" + task + "()")
print("<<<<<<<<<<<<<<<<< after call >>>>>>>>>>>>>>>>>")
+
except gdb.error:
print("!!!!!!!!!!!!!!!!! after call !!!!!!!!!!!!!!!!!")
@@ -59,38 +60,58 @@ def gdb_setup():
print("gbd init")
gdb.execute("set confirm off")
gdb.execute("set pagination off")
- gdb.execute("set verbose off")
- gdb.execute("set height 0")
+ # gdb.execute("set verbose off")
+ # gdb.execute("set height 0")
# gdb.execute("set unwindonsignal off")
+ # gdb.execute("set unwind-on-terminating-exception off")
gdb.execute("set unwindonsignal on")
+ # gdb.execute("set unwind-on-terminating-exception on")
+
+ gdb.execute("show unwindonsignal")
+ gdb.execute("show unwind-on-terminating-exception")
-# Event handling
+# Event handling
# GDB event, called on breakpoint
def stop_event(evt):
print("#### stop event %r" % evt)
-
+ gdb.execute("break")
imm = gdb_bkpt_read()
print(" imm = {}".format(imm))
+ if imm == 0:
+ print("-- ordinary breakpoint --")
+ # gdb.execute("return")
+ # gdb_continue()
+
if imm == 1:
print("Enter")
- gdb_continue()
+ # gdb.execute("return")
+ # gdb_continue()
if imm == 2:
print("Exit")
- gdb_continue()
+ # gdb.execute("return")
+ # gdb_continue()
if imm == 3:
print("Finished")
- gdb_continue()
+ # gdb.execute("return")
+
+
+def exit_handler(event):
+ print("event type: exit")
+ print("exit code: %d" % (event.exit_code))
+
+
+# gdb.events.inferior_call_post.connect(exit_handler)
# globals
-tasks = ["EXTI2", "EXTI3", "EXTI1"]
+tasks = ["EXTI1"]
task_nr = 0
print("simple python script started")
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index 52044219ae206d843aec228f9537609a08c9a2a5..0c032fe20aa808688f8ce2c9320c179a79e48234 100644
--- a/klee/src/lib.rs
+++ b/klee/src/lib.rs
@@ -109,10 +109,10 @@ macro_rules! k_visit {
}
}
-#[cfg(feature = "klee_mode")]
+//[cfg(feature = "klee_mode")]
pub fn k_read<T>(p: &T) {
unsafe { core::ptr::read_volatile(p) };
}
-#[cfg(not(feature = "klee_mode"))]
-pub fn k_read<T>(_p: &T) {}
+// #[cfg(not(feature = "klee_mode"))]
+// pub fn k_read<T>(_p: &T) {}
diff --git a/macros/src/trans.rs b/macros/src/trans.rs
index 585fbcf55e76476edeb48f4a493cf72dc1f2506e..01cb0de140989ff8b655852fcf9ec75b1e31c622 100644
--- a/macros/src/trans.rs
+++ b/macros/src/trans.rs
@@ -29,12 +29,7 @@ pub fn app(app: &App, ownerships: &Ownerships) -> Tokens {
quote!(#(#root)*)
}
-fn idle(
- app: &App,
- ownerships: &Ownerships,
- main: &mut Vec<Tokens>,
- root: &mut Vec<Tokens>,
-) {
+fn idle(app: &App, ownerships: &Ownerships, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
let krate = krate();
let mut mod_items = vec![];
@@ -552,10 +547,9 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
for rname in &task.resources {
let ceiling = ownerships[rname].ceiling();
let _rname = Ident::new(format!("_{}", rname.as_ref()));
- let resource = app.resources.get(rname).expect(&format!(
- "BUG: resource {} has no definition",
- rname
- ));
+ let resource = app.resources
+ .get(rname)
+ .expect(&format!("BUG: resource {} has no definition", rname));
let ty = &resource.ty;
let _static = if resource.expr.is_some() {
@@ -713,7 +707,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
fn #_stub_tname() {
#[allow(unsafe_code)]
unsafe { #_tname(); }
- unsafe { bkpt_3(); }
+ //unsafe { bkpt_3(); }
}
});
}
@@ -741,7 +735,8 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
let _name = Ident::new(format!("stub_{}", name.as_ref()));
stubs.push(quote!{
//#_name();
- let _ = k_read(&#_name);
+ let x = k_read(&#_name);
+ unsafe { core::ptr::read_volatile(&x) };
});
}
@@ -749,9 +744,9 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
extern crate cortex_m;
#[inline(never)]
#[allow(private_no_mangle_fns)]
- #[no_mangle]
+ //#[no_mangle]
pub fn wcet_start() {
-
+ unsafe { bkpt_3() };
#(#stubs)*
}