to marcus

Cargo.toml

@@ -33,6 +33,11 @@ version = "0.2.0"
 [features]
 wcet_bkpt = [] 
 wcet_nop = []
+klee = [] 
+
+[profile.dev]
+codegen-units = 1
+incremental = false
 
 [profile.release]
 lto = true

macros/src/check.rs

@@ -6,6 +6,7 @@ use syntax::{self, Resources, Statics};
 
 use syntax::error::*;
 
+#[derive(Debug)]
 pub struct App {
     pub device: Path,
     pub idle: Idle,
@@ -17,6 +18,7 @@ pub struct App {
 pub type Tasks = HashMap<Ident, Task>;
 
 #[allow(non_camel_case_types)]
+#[derive(Debug)]
 pub enum Exception {
     PENDSV,
     SVCALL,
@@ -42,11 +44,13 @@ impl Exception {
     }
 }
 
+#[derive(Debug)]
 pub enum Kind {
     Exception(Exception),
     Interrupt { enabled: bool },
 }
 
+#[derive(Debug)]
 pub struct Task {
     pub kind: Kind,
     pub path: Path,
@@ -63,16 +67,15 @@ pub fn app(app: check::App) -> Result<App> {
         tasks: app.tasks
             .into_iter()
             .map(|(k, v)| {
-                let v = ::check::task(k.as_ref(), v)
-                    .chain_err(|| format!("checking task `{}`", k))?;
+                let v =
+                    ::check::task(k.as_ref(), v).chain_err(|| format!("checking task `{}`", k))?;
 
                 Ok((k, v))
             })
             .collect::<Result<_>>()?,
     };
 
-    ::check::resources(&app)
-        .chain_err(|| "checking `resources`")?;
+    ::check::resources(&app).chain_err(|| "checking `resources`")?;
 
     Ok(app)
 }

macros/src/lib.rs

@@ -181,6 +181,9 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
     let ownerships = analyze::app(&app);
     let tokens = trans::app(&app, &ownerships);
 
+    println!("here we are");
+    println!("{:?}", app.tasks);
+
     Ok(format!("{}", tokens)
         .parse()
         .map_err(|_| "BUG: error parsing the generated code")?)

src/lib.rs

@@ -85,6 +85,7 @@ extern crate untagged_option;
 use core::u8;
 
 pub use rtfm_core::{Resource, Static, Threshold};
+#[cfg(not(klee))]
 pub use cortex_m::asm::{bkpt, nop, wfi};
 pub use cortex_m_rtfm_macros::app;
 #[doc(hidden)]
@@ -92,6 +93,7 @@ pub use untagged_option::UntaggedOption;
 
 use cortex_m::interrupt::{self, Nr};
 #[cfg(not(armv6m))]
+#[cfg(not(klee))]
 use cortex_m::register::basepri;
 
 pub mod examples;
@@ -137,17 +139,51 @@ where
                 if ceiling == max_priority {
                     atomic(t, |t| f(data, t))
                 } else {
-                    let old = basepri::read();
+                    let mut old = 0;
+                    // klee mode code generation
+                    // the generated code should not access the hardware
+                    if !cfg!(feature = "klee") {
+                        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") {
                         basepri::write(hw);
-                    if cfg!(feature = "wcet_bkpt") { bkpt(); } 
-                    if cfg!(feature = "wcet_nop") { nop(); }
+                    }
+
+                    // wcet_bkpt mode
+                    // put breakpoint at raise ceiling, for tracing execution time
+                    if cfg!(feature = "wcet_bkpt") {
+                        bkpt();
+                    }
+
+                    // wcet_nop mode
+                    // leave nop in the production code, to keep memory layout the same
+                    if cfg!(feature = "wcet_nop") {
+                        nop();
+                    }
 
                     let ret = f(data, &mut Threshold::new(ceiling));
 
-                    if cfg!(feature = "wcet_bkpt") { bkpt(); } 
-                    if cfg!(feature = "wcet_nop") { nop(); }
+                    // wcet_bkpt mode
+                    // put breakpoint at lower ceiling, for tracing execution time
+                    if cfg!(feature = "wcet_bkpt") {
+                        bkpt();
+                    }
+
+                    // wcet_nop mode
+                    // leave nop in the production code, to keep memory layout the same
+                    if cfg!(feature = "wcet_nop") {
+                        nop();
+                    }
+
+                    // klee mode code generation
+                    // the generated code should not access the hardware
+                    if !cfg!(feature = "klee") {
                         basepri::write(old);
+                    }
                     ret
                 }
             }