diff --git a/.vscode/tasks.json b/.vscode/tasks.json
index 15335af1836813e5426c2f387c71e7bf315cec75..615a4dfe06dc41d2b0760402acd315c984bad1f1 100644
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -3,6 +3,30 @@
// for the documentation about the tasks.json format
"version": "2.0.0",
"tasks": [
+ {
+ "label": "xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu",
+ "type": "shell",
+ "command": "xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu",
+ "group": {
+ "kind": "build",
+ "isDefault": true
+ },
+ "problemMatcher": [
+ "$rustc"
+ ]
+ },
+ {
+ "label": "xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu",
+ "type": "shell",
+ "command": "xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu",
+ "group": {
+ "kind": "build",
+ "isDefault": true
+ },
+ "problemMatcher": [
+ "$rustc"
+ ]
+ },
{
"label": "xargo build --example empty --features klee_mode --release --target x86_64-unknown-linux-gnu",
"type": "shell",
@@ -15,6 +39,18 @@
"$rustc"
]
},
+ {
+ "label": "xargo build --example empty --features klee_mode --target x86_64-unknown-linux-gnu",
+ "type": "shell",
+ "command": "xargo build --example empty --features klee_mode --target x86_64-unknown-linux-gnu",
+ "group": {
+ "kind": "build",
+ "isDefault": true
+ },
+ "problemMatcher": [
+ "$rustc"
+ ]
+ },
{
"label": "xargo build --example empty2 --features klee_mode --release --target x86_64-unknown-linux-gnu",
"type": "shell",
diff --git a/examples/empty.rs b/examples/empty.rs
index e0bf34e9b645082a70a290790e6b238f2c2e74da..e2e0581531594d29e72507b7dd6317bf0b467e31 100644
--- a/examples/empty.rs
+++ b/examples/empty.rs
@@ -20,20 +20,30 @@ app! {
device: stm32f103xx,
}
-static mut X: u32 = 32;
+fn t(x: &mut i32) -> i32 {
+ let mut y = 0;
+ if *x < 10 {
+ for _ in 0..*x {
+ y += 1;
+ k_visit!()
+ }
+ }
+ y
+}
-#[inline(never)]
-fn init(_p: init::Peripherals) {
- k_symbol!(X, "X");
- k_assert(unsafe { X } == 33);
+pub fn t2() {
+ let mut x = 0;
+ let x: &mut i32 = &mut x;
+ k_symbol!(x, "x");
+
+ let mut y = 0;
+ let y: &mut i32 = &mut y;
+ k_symbol!(y, "y");
+
+ t(x) + t(y);
}
-// 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();
+fn init(_p: init::Peripherals) {
+ t2();
}
diff --git a/examples/empty2.rs b/examples/empty2.rs
index 97e6be0327e6056e39156ff868a7a67b2b96e6b8..01521103f6730519dc0b22cd3dd5e39f8d3a39a0 100644
--- a/examples/empty2.rs
+++ b/examples/empty2.rs
@@ -20,16 +20,15 @@ app! {
device: stm32f103xx,
}
-#[inline(never)]
+//#[inline(never)]
fn t() -> i32 {
- let mut x = unsafe { core::mem::uninitialized() };
+ let mut x = 0;
+ let x: &mut i32 = &mut x;
let mut y = 0;
k_symbol!(x, "x");
- if x < 10 {
- for _ in 0..x {
+ if *x < 10 {
+ for _ in 0..*x {
y += 1;
- // unsafe { core::ptr::read_volatile(&y) };
- // k_abort();
}
}
y
@@ -37,20 +36,6 @@ fn t() -> i32 {
#[inline(never)]
fn init(_p: init::Peripherals) {
- // let mut x = unsafe { core::mem::uninitialized() };
- // let mut y = 0;
- // k_symbol!(x, "x");
- // if x < 10 {
- // for _ in 0..x {
- // y += 1;
- // unsafe { core::ptr::read_volatile(&y) };
- // // k_abort();
- // }
- // }
-
- // unsafe {
- // k_assert(core::ptr::read_volatile(&y) == 0);
- // }
t();
}
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index e760d50996380412d872b2d303d0820cfbe48727..0ae4873045128215bf8540911939c3750a972487 100644
--- a/klee/src/lib.rs
+++ b/klee/src/lib.rs
@@ -68,11 +68,34 @@ pub fn k_assert(e: bool) {
/// make a variable symbolic
#[macro_export]
macro_rules! k_symbol {
- ($id:ident, $name:expr) => {
+ ($id:expr, $name:expr) => {
+ {
#[allow(unsafe_code)]
+ #[allow(warnings)]
$crate::k_mk_symbol(
- unsafe { &mut $id },
+ unsafe { $id },
unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
)
+ }
}
}
+
+#[macro_export]
+macro_rules! k_visit {
+ ()=> {
+ {
+ #[allow(unsafe_code)]
+ unsafe {
+ core::ptr::read_volatile(&0);
+ }
+ }
+ }
+}
+
+#[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) {}
diff --git a/macros/Cargo.toml b/macros/Cargo.toml
index 01b5fabe3bbebb09bd1e394450244e4d07d32287..a2f12f7eb7869c72e68debdfc3a23e1906c5aa08 100644
--- a/macros/Cargo.toml
+++ b/macros/Cargo.toml
@@ -15,6 +15,9 @@ quote = "0.3.15"
rtfm-syntax = "0.2.1"
syn = "0.11.11"
+[dependencies.klee]
+path = "../klee"
+
[lib]
proc-macro = true
diff --git a/macros/src/trans.rs b/macros/src/trans.rs
index 8579974e0cb49b46630530a2c22dedb1d4de78ea..81eb4e9e7178967070377a2018ac9012af508a4d 100644
--- a/macros/src/trans.rs
+++ b/macros/src/trans.rs
@@ -405,18 +405,47 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
}
let init = &app.init.path;
- main.push(quote! {
- // type check
- let init: fn(#(#tys,)*) #ret = #init;
- #krate::atomic(unsafe { &mut #krate::Threshold::new(0) }, |_t| unsafe {
- let _late_resources = init(#(#exprs,)*);
- #(#late_resource_init)*
+ if !cfg!(feature = "klee_mode") {
+ // code generation for normal mode
+ main.push(quote! {
+ // type check
+ let init: fn(#(#tys,)*) #ret = #init;
- #(#exceptions)*
- #(#interrupts)*
+ #krate::atomic(unsafe { &mut #krate::Threshold::new(0) }, |_t| unsafe {
+ let _late_resources = init(#(#exprs,)*);
+ #(#late_resource_init)*
+
+ #(#exceptions)*
+ #(#interrupts)*
+ });
});
- });
+ } else {
+ // code generation for klee mode
+ main.push(quote! {
+ // type check
+ //let init: fn(#(#tys,)*) #ret = #init;
+
+ unsafe {
+ // init(#(#exprs,)*);
+ // }
+
+ // make each resource symbolic
+ // later we can theink of "type invariants"
+ k_symbol!(&mut _X, "X");
+
+ // task set as symbolic
+ // will generate a set of tests for each task
+ let mut task = 0;
+ k_symbol!(&mut task, "task");
+ match task {
+ 0 => { _EXTI1(); },
+ 1 => { _EXTI2(); },
+ _ => {},
+ }
+ }
+ });
+ }
}
fn resources(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {