diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs index 8449c50e9b6291694e9d1f12a6b0b407e97e9e69..c3813692434f91fc73aebc4917b318d2502b315f 100644 --- a/examples/eq_paper.rs +++ b/examples/eq_paper.rs @@ -2,8 +2,8 @@ #![no_main] #![no_std] -extern crate klee; extern crate panic_abort; +extern crate klee; use klee::{kassert, kassume, ksymbol}; #[derive(Debug, Copy, Clone)] @@ -33,79 +33,85 @@ const F: bool = false; #[no_mangle] fn main() { - let mut DATA: [Data; HORIZON] = - unsafe { core::mem::uninitialized() }; + let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() }; ksymbol!(&mut DATA, "DATA"); - let mut STATE = S8001; - let mut STATE_H: [State; HORIZON] = - unsafe { core::mem::uninitialized() }; // STATE_HISTORY - let mut CNTR: u32 = - unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR + let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; - // TIMEOUT_CNTR_HISTORY - let mut CNTR_H: [u32; HORIZON] = - unsafe { core::mem::uninitialized() }; + let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() }; - for i in 0..HORIZON { - eq(&mut STATE, &mut CNTR, &mut DATA[i]); + let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() }; + let mut STATE = S8001; - STATE_H[i] = STATE; // update STATE history - CNTR_H[i] = CNTR; // update CNTR history + for i in 0..HORIZON { + eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]); + STATE_H[i] = STATE; + CNTR_H[i] = TIMEOUT_CNTR; + + // invariants + // (1) S8000 -> a & b + // ensures that Enable implies that both a and b are true + // this is the main safety condition + if STATE == S8000 { + kassert!(DATA[i].a & DATA[i].b); + } - // (1) !a | !b -> !S8000 + // (2) !a | !b -> !S8000 + // ensures that if any input is false we cannot enter the Enable state + // this can also be seen as a safty condition + // (can it be derived from the first condition, but we keep is as + // an indication that the verification works as expected) + // Indeed the number of spanned paths remains the same + // (with or without the below assertion, so its proven redundant by KLEE) if !DATA[i].a | !DATA[i].b { kassert!(!(STATE == S8000)); } - // (2) S8000 -> a & b - if STATE == S8000 { - kassert!(DATA[i].a & DATA[i].b); + // S8001 -> !a & !b + // we can only stay or enter the Init state unless either (or both) inputs are false + if STATE == S8001 { + kassert!(!DATA[i].a | !DATA[i].b); } + // transition invariants if i > 0 { match STATE_H[i - 1] { - // (3) C001 | C002 | C003 => { - kassert!( - (STATE == S8001) - | (STATE == STATE_H[i - 1]) - ); + // (3) + // transitions from error + kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1])); } - // (4) S8005 => { - kassert!( - (STATE == S8001) - | (STATE == C003) - | (STATE == STATE_H[i - 1]) - ); + // (4) + kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1])); } _ => (), } } + // // DISCREPANCY related invariants match STATE { + // Error -> timeout // (5) - C001 | C002 | C003 => kassert!(CNTR == 0), + C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0), S8004 | S8005 | S8014 => { // (6) + // remaining in a waiting state decreases the counter if i > 0 { - if STATE_H[i - 1] == STATE { - kassert!(CNTR_H[i] < CNTR_H[i - 1]); + if STATE_H[i - 1] == STATE_H[i] { + kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]); } } } _ => {} } + + unsafe { core::ptr::read_volatile(&STATE_H[i]) }; } } -fn eq( - STATE: &mut State, - TIMEOUT_CNTR: &mut u32, - data: &Data, -) { +fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) { *STATE = match STATE { S8000 => match (data.a, data.b) { (F, F) => S8001,