Skip to content
Snippets Groups Projects
Commit 1dd67ca2 authored by Per's avatar Per
Browse files

symbolic task sets (explicit version)

parent 01867246
No related branches found
No related tags found
No related merge requests found
......@@ -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",
......
......@@ -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();
}
......@@ -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();
}
......
......@@ -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) {}
......@@ -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
......
......@@ -405,6 +405,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
main.push(quote! {
// type check
let init: fn(#(#tys,)*) #ret = #init;
......@@ -417,6 +420,32 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
#(#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>) {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment