Skip to content
Snippets Groups Projects
Commit edc46b48 authored by Henrik Tjäder's avatar Henrik Tjäder
Browse files

Merge branch 'klee' of gitlab.henriktjader.com:KLEE/cortex-m-rtfm-klee into klee

parents 723a91d2 e77ce578
No related branches found
No related tags found
No related merge requests found
......@@ -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"]
......
......@@ -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();
......
......@@ -23,3 +23,4 @@ proc-macro = true
[features]
klee_mode = []
wcet_bkpt = []
\ No newline at end of file
......@@ -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!{
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment