diff --git a/.cargo/config b/.cargo/config
index 1ab52827c2bfa858bc120a5e4f7a33137de3649c..db63f627d5ec01272dad07f3fe36091b94eb52c9 100644
--- a/.cargo/config
+++ b/.cargo/config
@@ -30,5 +30,13 @@ rustflags = [
"-Z", "linker-flavor=ld",
]
+# used when building for klee
+# must build in --release as we are not doing any (post) linking
+[target.x86_64-unknown-linux-gnu]
+rustflags = [
+ "--emit=llvm-bc,llvm-ir",
+ "-C", "linker=true"
+]
+
[build]
-target = "thumbv7em-none-eabihf"
\ No newline at end of file
+target = "thumbv7em-none-eabihf"
diff --git a/.vscode/tasks.json b/.vscode/tasks.json
index c81d405dcde19a226273819fc97ae1fc8e6b1f17..33db0f2305cb7c538c0defe598ec624fd9d51db8 100644
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -15,6 +15,18 @@
"$rustc"
]
},
+ {
+ "label": "xargo build --example empty --features klee_mode --release --target x86_64-unknown-linux-gnu",
+ "type": "shell",
+ "command": "xargo build --example empty --features klee_mode --release --target x86_64-unknown-linux-gnu",
+ "group": {
+ "kind": "build",
+ "isDefault": true
+ },
+ "problemMatcher": [
+ "$rustc"
+ ]
+ },
{
"label": "xargo build --example nested",
"type": "shell",
diff --git a/Cargo.toml b/Cargo.toml
index 3f64f5b9aa6c8e154fd0e0895aa217801741eee2..48fdb0e11e89daba8f2c5d582c17347b73551636 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -18,8 +18,8 @@ untagged-option = "0.1.1"
rtfm-core = "0.1.0"
cortex-m-rtfm-macros = { path = "macros" }
-[target.'cfg(target_arch = "x86_64")'.dev-dependencies]
-compiletest_rs = "0.2.8"
+#[target.'cfg(target_arch = "x86_64")'.dev-dependencies]
+#compiletest_rs = "0.2.8"
[dev-dependencies.cortex-m-rt]
features = ["abort-on-panic"]
@@ -30,15 +30,20 @@ git = "https://gitlab.henriktjader.com/pln/STM32F40x"
features = ["rt"]
version = "0.2.0"
+[dev-dependencies.klee]
+path = "./klee"
+
[features]
wcet_bkpt = []
wcet_nop = []
-klee = []
+klee_mode = ["cortex-m-rtfm-macros/klee_mode"]
[profile.dev]
codegen-units = 1
incremental = false
+panic = "abort"
[profile.release]
lto = true
debug = true
+panic = "abort"
diff --git a/README.md b/README.md
index 240e2f8fa726ac52363401899afb4dacd8928493..e80322c5870a1dc4504a34145f29dd3055ab77ae 100644
--- a/README.md
+++ b/README.md
@@ -18,6 +18,70 @@ Licensed under either of
at your option.
+# Klee based analysis.
+
+## Complilation
+
+Use a Rust toolchain with a llwm4 backend.
+
+
+> xargo build --example empty --features klee_mode --release --target x86_64-unknown-linux-gnu
+
+The `--features klee_mode` implies the following:
+
+- the set of tasks is generated in ./klee/tasks.txt
+- the example is built without HW dependencies
+ claim does NOT affect basepri register
+
+The `--target x86_64-unknown-linux-gnu` implies the following:
+
+``` text
+rustflags = [
+ "--emit=llvm-bc,llvm-ir",
+ "-C", "linker=true"
+]
+```
+
+So both `.bc` and `.ll` are generated for the application at hande (`empty.rs`). (Only `.bc` is indeed needed/used for KLEE analysis, but the `.ll` is neat as being human readable for code inspection).
+
+The files will contain all symbols besides the *weakly* defined default handlers (which should not be analysed by KLEE in any case).
+
+TODO: there is still a warning on module level assembly.
+
+The `--relesase` flag implies:
+
+``` text
+[profile.release]
+lto = true
+debug = true
+panic = "abort"
+```
+
+`lto = true` ensures pre-llvm linknig of dependencies for the generated `.bc` and `.ll` files.
+
+`panic = "abort"` is required to override the default panic (unwrap) behavior of the x86 (host) target.
+
+
+
+## KLEE Analysis
+
+A docker daemon should be started/enabled.
+
+> systemctl start docker.service # if not already started/enabled
+
+In the current folder:
+
+> docker run --rm --user $(id -u):$(id -g) -v ($PDW)/klee-examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+
+This starts a shell in the docker `llvm-klee-4`, with a shared mount to the examples directory, where your `empty-xxxx.bc` is located.
+
+From there you can run various commands like:
+
+> klee empty-xxxxx.bc
+
+See KLEE for detailed information.
+
+
## Contribution
Unless you explicitly state otherwise, any contribution intentionally submitted
diff --git a/examples/empty.rs b/examples/empty.rs
new file mode 100644
index 0000000000000000000000000000000000000000..216137ef82e310998e45178cf21c9eaf15260188
--- /dev/null
+++ b/examples/empty.rs
@@ -0,0 +1,39 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f40x; // the device crate
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert};
+
+// import the procedural macro
+use rtfm::app;
+
+app! {
+ // this is the path to the device crate
+ device: stm32f40x,
+}
+
+static mut X: u32 = 32;
+
+#[inline(never)]
+fn init(_p: init::Peripherals) {
+ k_symbol!(X, "X");
+ k_assert(unsafe { X } == 33);
+}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ k_abort();
+}
diff --git a/klee/.gitignore b/klee/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..ffa3bbd20ea4d6c2a64af9a17260e5ad4460ffa2
--- /dev/null
+++ b/klee/.gitignore
@@ -0,0 +1 @@
+Cargo.lock
\ No newline at end of file
diff --git a/klee/Cargo.toml b/klee/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..de26d8c8a877e86d91a548922da3b7e253e9eed8
--- /dev/null
+++ b/klee/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+authors = ["Jorge Aparicio <jorge@japaric.io>"]
+name = "klee"
+version = "0.1.0"
+
+[dependencies]
+cstr_core = "0.1.0"
+cty = "0.1.5"
diff --git a/klee/src/lang_items.rs b/klee/src/lang_items.rs
new file mode 100644
index 0000000000000000000000000000000000000000..f81e9e09ebd7a311765546bb55bba86b0a67a2dd
--- /dev/null
+++ b/klee/src/lang_items.rs
@@ -0,0 +1,25 @@
+#[lang = "panic_fmt"]
+unsafe extern "C" fn panic_fmt(_: ::core::fmt::Arguments, _: &'static str, _: u32, _: u32) -> ! {
+ ::abort()
+}
+
+#[lang = "start"]
+extern "C" fn start<T>(main: fn() -> T, _argc: isize, _argv: *const *const u8) -> isize
+ where
+ T: Termination,
+{
+ main();
+
+ 0
+}
+
+#[lang = "termination"]
+pub trait Termination {
+ fn report(self) -> i32;
+}
+
+impl Termination for () {
+ fn report(self) -> i32 {
+ 0
+ }
+}
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
new file mode 100644
index 0000000000000000000000000000000000000000..1d1949e3e35cbad0e17d68f10430fec5a1566b0b
--- /dev/null
+++ b/klee/src/lib.rs
@@ -0,0 +1,76 @@
+#![no_std]
+#![feature(compiler_builtins_lib)]
+#![feature(lang_items)]
+
+extern crate compiler_builtins;
+extern crate cstr_core;
+extern crate cty;
+
+// mod lang_items;
+mod ll;
+
+use core::mem;
+
+use cty::c_void;
+
+#[doc(hidden)]
+pub use cstr_core::CStr;
+
+#[doc(hidden)]
+#[inline]
+pub fn k_symbol<T>(name: &CStr) -> T {
+ let mut t: T = unsafe { mem::uninitialized() };
+ unsafe {
+ ll::klee_make_symbolic(
+ &mut t as *mut T as *mut c_void,
+ mem::size_of::<T>(),
+ name.as_ptr(),
+ )
+ }
+ t
+}
+
+#[doc(hidden)]
+#[inline]
+pub fn k_mk_symbol<T>(t: &mut T, name: &CStr) {
+ unsafe {
+ ll::klee_make_symbolic(
+ t as *mut T as *mut c_void,
+ mem::size_of::<T>(),
+ name.as_ptr(),
+ )
+ }
+}
+
+#[inline(never)]
+pub fn k_abort() -> ! {
+ unsafe { ll::abort() }
+}
+
+/// assume a condition involving symbolic variables
+#[inline(never)]
+pub fn k_assume(cond: bool) {
+ unsafe {
+ ll::klee_assume(cond);
+ }
+}
+
+/// assert a condition involving symbolic variables
+#[inline(never)]
+pub fn k_assert(e: bool) {
+ if !e {
+ k_abort();
+ }
+}
+
+/// make a variable symbolic
+#[macro_export]
+macro_rules! k_symbol {
+ ($id:ident, $name:expr) => {
+ #[allow(unsafe_code)]
+ $crate::k_mk_symbol(
+ unsafe { &mut $id },
+ unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
+ )
+ }
+}
diff --git a/klee/src/ll.rs b/klee/src/ll.rs
new file mode 100644
index 0000000000000000000000000000000000000000..a7f44ce52334ed33f0e5ac97991e40dc6ebaf373
--- /dev/null
+++ b/klee/src/ll.rs
@@ -0,0 +1,7 @@
+use cty::{c_char, c_void};
+
+extern "C" {
+ pub fn abort() -> !;
+ pub fn klee_assume(cond: bool);
+ pub fn klee_make_symbolic(ptr: *mut c_void, size: usize, name: *const c_char);
+}
diff --git a/klee/tasks.txt b/klee/tasks.txt
new file mode 100644
index 0000000000000000000000000000000000000000..fb62ad331f6b05c445c05a4cdfee52e0cc01d985
--- /dev/null
+++ b/klee/tasks.txt
@@ -0,0 +1,2 @@
+// autogenertated file
+ []
\ No newline at end of file
diff --git a/macros/Cargo.toml b/macros/Cargo.toml
index 748637c16971d5a4d1fde13f85b3c22acbdaf23a..afa5bd660d64e8a7c719fc13c9891928ed389e92 100644
--- a/macros/Cargo.toml
+++ b/macros/Cargo.toml
@@ -17,3 +17,6 @@ syn = "0.11.11"
[lib]
proc-macro = true
+
+[features]
+klee_mode = []
diff --git a/macros/src/lib.rs b/macros/src/lib.rs
index f488eb32c4c776939088b76da27cd4d55545b958..9183e248619ece7af09b8d7d686079f4f9c93c2e 100644
--- a/macros/src/lib.rs
+++ b/macros/src/lib.rs
@@ -184,17 +184,19 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
let ownerships = analyze::app(&app);
let tokens = trans::app(&app, &ownerships);
- println!("tasks");
- let mut tasks = Vec::new();
- for (id, _task) in app.tasks {
- println!("{}", id);
- tasks.push(format!("{}", id));
- }
+ if cfg!(feature = "klee_mode") {
+ println!("tasks");
+ let mut tasks = Vec::new();
+ for (id, _task) in app.tasks {
+ println!("{}", id);
+ tasks.push(format!("{}", id));
+ }
- let path = std::path::Path::new("klee/tasks.txt");
+ let path = std::path::Path::new("klee/tasks.txt");
- let mut file = File::create(path).unwrap();
- write!(file, "// autogenertated file \n {:?}", tasks).unwrap();
+ let mut file = File::create(path).unwrap();
+ write!(file, "// autogenertated file \n {:?}", tasks).unwrap();
+ }
Ok(format!("{}", tokens)
.parse()
diff --git a/src/lib.rs b/src/lib.rs
index 0bb4ee95c498aab556be9e163206120c9f17bcad..ee73521ccce6349cca6ef606b1428d0a9f6de328 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -142,14 +142,14 @@ where
let mut old = 0;
// klee mode code generation
// the generated code should not access the hardware
- if !cfg!(feature = "klee") {
+ if !cfg!(feature = "klee_mode") {
old = basepri::read();
}
let hw = (max_priority - ceiling) << (8 - _nvic_prio_bits);
// klee mode code generation
// the generated code should not access the hardware
- if !cfg!(feature = "klee") {
+ if !cfg!(feature = "klee_mode") {
basepri::write(hw);
}
@@ -181,7 +181,7 @@ where
// klee mode code generation
// the generated code should not access the hardware
- if !cfg!(feature = "klee") {
+ if !cfg!(feature = "klee_mode") {
basepri::write(old);
}
ret