wcet_bkpt code gen

Cargo.toml

@@ -35,7 +35,7 @@ version = "0.2.0"
 path = "./klee"
 
 [features]
-wcet_bkpt = [] 
+wcet_bkpt = ["cortex-m-rtfm-macros/wcet_bkpt"] 
 wcet_nop = []
 klee_mode = ["cortex-m-rtfm-macros/klee_mode", "klee/klee_mode"] 
 

examples/resource.rs

@@ -78,36 +78,36 @@ fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
 #[allow(dead_code)]
 fn init(_p: init::Peripherals, _r: init::Resources) {}
 
-extern crate cortex_m;
-use cortex_m::register::basepri;
-
-// for wcet should be autogenerated...
-
-#[inline(never)]
-#[no_mangle]
-fn readbasepri() -> u8 {
-    cortex_m::register::basepri::read()
-}
-#[inline(never)]
-#[allow(non_snake_case)]
-#[no_mangle]
-fn stub_EXTI1() {
-    unsafe { _EXTI1() };
-}
-#[inline(never)]
-#[no_mangle]
-#[allow(non_snake_case)]
-fn stub_EXTI2() {
-    unsafe { _EXTI2() };
-}
-#[inline(never)]
-#[no_mangle]
-#[allow(non_snake_case)]
-fn stub_EXTI3() {
-    unsafe {
-        _EXTI3();
-    }
-}
+// extern crate cortex_m;
+// use cortex_m::register::basepri;
+
+// // for wcet should be autogenerated...
+
+// #[inline(never)]
+// #[no_mangle]
+// fn readbasepri() -> u8 {
+//     cortex_m::register::basepri::read()
+// }
+// #[inline(never)]
+// #[allow(non_snake_case)]
+// #[no_mangle]
+// fn stub_EXTI1() {
+//     unsafe { _EXTI1() };
+// }
+// #[inline(never)]
+// #[no_mangle]
+// #[allow(non_snake_case)]
+// fn stub_EXTI2() {
+//     unsafe { _EXTI2() };
+// }
+// #[inline(never)]
+// #[no_mangle]
+// #[allow(non_snake_case)]
+// fn stub_EXTI3() {
+//     unsafe {
+//         _EXTI3();
+//     }
+// }
 
 // The idle loop.
 //
@@ -116,10 +116,10 @@ fn stub_EXTI3() {
 // endless loop.
 #[inline(never)]
 fn idle() -> ! {
-    readbasepri();
-    stub_EXTI1();
-    stub_EXTI2();
-    stub_EXTI3();
+    // readbasepri();
+    // stub_EXTI1(); // here to provide stub for gdb
+    // stub_EXTI2(); // here to provide stub for gdb
+    // stub_EXTI3(); // here to provide stub for gdb
 
     loop {
         rtfm::nop();

macros/Cargo.toml

@@ -23,3 +23,4 @@ proc-macro = true
 
 [features]
 klee_mode = [] 
+wcet_bkpt = [] 
\ No newline at end of file

macros/src/trans.rs

@@ -27,7 +27,12 @@ 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![];
@@ -406,7 +411,9 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
     let init = &app.init.path;
 
     if !cfg!(feature = "klee_mode") {
-        // code generation for normal mode
+        // code generation for normal/wcet mode
+        if !cfg!(feature = "wcet_bkpt") {
+            // normal mode
             main.push(quote! {
                 // type check
                 let init: fn(#(#tys,)*) #ret = #init;
@@ -420,7 +427,17 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
                 });
             });
         } else {
-        // code generation for klee mode
+            // wcet_mode
+            // panic!();
+            for (name, _task) in &app.tasks {
+                let _name = Ident::new(format!("stub_{}", name.as_ref()));
+                main.push(quote!{
+                    #_name();
+                });
+            }
+        }
+    } else {
+        // code generation for klee_mode
         let mut tasks = vec![];
         let mut index: u32 = 0;
 
@@ -514,9 +531,10 @@ 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() {
@@ -652,6 +670,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
 
         let path = &task.path;
         let _tname = Ident::new(format!("_{}", tname));
+        let _stub_tname = Ident::new(format!("stub_{}", tname));
         let export_name = Lit::Str(tname.as_ref().to_owned(), StrStyle::Cooked);
         root.push(quote! {
             #[allow(non_snake_case)]
@@ -662,6 +681,13 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
 
                 f(#(#exprs,)*)
             }
+
+            #[inline(never)]
+            #[no_mangle]
+            #[allow(non_snake_case)]
+            fn #_stub_tname() {
+                unsafe { #_tname(); }
+            }
         });
 
         root.push(quote!{