rtfm-klee

.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"

.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",

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"

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

examples/empty.rs

+//! 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();
+}

klee/.gitignore

+Cargo.lock
\ No newline at end of file

klee/Cargo.toml

+[package]
+authors = ["Jorge Aparicio <jorge@japaric.io>"]
+name = "klee"
+version = "0.1.0"
+
+[dependencies]
+cstr_core = "0.1.0"
+cty = "0.1.5"

klee/src/lang_items.rs

+#[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
+    }
+}

klee/src/lib.rs

+#![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()) }
+        )
+    }
+}

klee/src/ll.rs

+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);
+}

klee/tasks.txt

+// autogenertated file 
+ []
\ No newline at end of file

macros/Cargo.toml

@@ -17,3 +17,6 @@ syn = "0.11.11"
 
 [lib]
 proc-macro = true
+
+[features]
+klee_mode = [] 

macros/src/lib.rs

@@ -184,6 +184,7 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
     let ownerships = analyze::app(&app);
     let tokens = trans::app(&app, &ownerships);
 
+    if cfg!(feature = "klee_mode") {
         println!("tasks");
         let mut tasks = Vec::new();
         for (id, _task) in app.tasks {
@@ -195,6 +196,7 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
 
         let mut file = File::create(path).unwrap();
         write!(file, "// autogenertated file \n {:?}", tasks).unwrap();
+    }
 
     Ok(format!("{}", tokens)
         .parse()

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