diff --git a/examples/eq.rs b/examples/eq.rs
index 0dfcd6d716b7a3a0a60a4ecac1b3ebd040993993..021e81ca585caa854f4462ad1aed3964047c67ac 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -6,20 +6,20 @@ use klee::{kassert, kassume, ksymbol};
#[derive(Debug, Copy, Clone)]
pub struct Data {
- a: bool,
- b: bool,
+ a: bool,
+ b: bool,
}
#[derive(Debug, Copy, Clone, PartialEq)]
pub enum State {
- S8000,
- S8001,
- S8004,
- S8014,
- S8005,
- C001,
- C002,
- C003,
+ S8000,
+ S8001,
+ S8004,
+ S8014,
+ S8005,
+ C001,
+ C002,
+ C003,
}
use State::*;
@@ -30,140 +30,162 @@ const F: bool = false;
#[no_mangle]
fn main() {
- let mut DATA: [Data; (DISCREPENCY + 3) as usize] = unsafe { core::mem::uninitialized() };
- ksymbol!(&mut DATA, "DATA");
+ let mut DATA: [Data; (DISCREPENCY + 3) as usize] = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut DATA, "DATA");
- let mut STATE_HISTORY: [State; (DISCREPENCY + 3) as usize] =
- unsafe { core::mem::uninitialized() };
+ let mut STATE_HISTORY: [State; (DISCREPENCY + 3) as usize] =
+ unsafe { core::mem::uninitialized() };
- let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
- let mut STATE = S8001;
+ let mut CNTR_HISTORY: [u32; (DISCREPENCY + 3) as usize] = unsafe { core::mem::uninitialized() };
- for i in 0..(DISCREPENCY + 3) as usize {
- periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+ let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+ let mut STATE = S8001;
- // invariants
- // 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);
- }
+ for i in 0..(DISCREPENCY + 3) as usize {
+ periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
- // !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));
- }
+ // invariants
+ // 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);
+ }
- // 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);
- }
+ // !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));
+ }
-
-
- // DISCREPANCY related invariants
- match STATE {
- // Error -> timeout
- C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
-
- // Waiting states -> !timeout
- // Waiting states implies that TIMEOUT_CNTR has not yet expired
- // and that the time remaining is not longer than the discrepency
- S8004 | S8005 | S8014 => {
- kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
- }
- _ => {}
+ // 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_HISTORY[i - 1] {
+ C001 | C002 | C003 => {
+ // transitions from error
+ kassert!((STATE == S8001) | (STATE == STATE_HISTORY[i - 1]));
}
+ S8005 => {
+ kassert!((STATE == S8001) | (STATE == C003) | (STATE == STATE_HISTORY[i - 1]));
+ }
+ _ => (),
+ }
+ }
- // transition invariants
+ // DISCREPANCY related invariants
+ match STATE {
+ // Error -> timeout
+ C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+
+ S8004 | S8005 | S8014 => {
+ // remaining in a waiting state decreases the counter
if i > 0 {
- match STATE_HISTORY[i - 1] {
- C001 | C002 | C003 | S8005 => {
- // no (immediate) transition from error / recover to Enable state
- kassert!(!(STATE == S8000));
- }
- _ => {
- // liveness from Init and Wait states, Enable is ensured
- if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
- kassert!(STATE == S8000);
- }
- }
- }
+ if STATE_HISTORY[i - 1] == STATE {
+ kassert!(TIMEOUT_CNTR < CNTR_HISTORY[i - 1]);
+ }
}
- STATE_HISTORY[i] = STATE;
- unsafe { core::ptr::read_volatile(&STATE_HISTORY[i]) };
+ // Waiting states -> !timeout
+ // Waiting states implies that TIMEOUT_CNTR has not yet expired
+ // and that the time remaining is not longer than the discrepency
+ kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY);
+ }
+ _ => {}
}
+
+ // if i > 0 {
+ // match STATE_HISTORY[i - 1] {
+ // C001 | C002 | C003 | S8005 => {
+ // // no (immediate) transition from error / recover to Enable state
+ // kassert!(!(STATE == S8000));
+ // }
+ // _ => {
+ // // liveness from Init and Wait states, Enable is ensured
+ // if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
+ // kassert!(STATE == S8000);
+ // }
+ // }
+ // }
+ // }
+
+ STATE_HISTORY[i] = STATE;
+ CNTR_HISTORY[i] = TIMEOUT_CNTR;
+
+ unsafe { core::ptr::read_volatile(&STATE_HISTORY[i]) };
+ }
}
fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
- *STATE = match STATE {
- S8000 => match (data.a, data.b) {
- (F, F) => S8001,
- (F, T) | (T, F) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8005
- }
- (T, T) => S8000,
- },
- S8001 => match (data.a, data.b) {
- (F, F) => S8001,
- (F, T) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8014
- }
- (T, F) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8004
- }
- (T, T) => S8000,
+ *STATE = match STATE {
+ S8000 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) | (T, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8005
+ }
+ (T, T) => S8000,
+ },
+ S8001 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8014
+ }
+ (T, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8004
+ }
+ (T, T) => S8000,
+ },
+ S8004 => {
+ *TIMEOUT_CNTR -= 1;
+ match *TIMEOUT_CNTR {
+ 0 => C001,
+ _ => match (data.a, data.b) {
+ (F, _) => S8001,
+ (_, T) => S8000,
+ _ => S8004,
},
- S8004 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C001,
- _ => match (data.a, data.b) {
- (F, _) => S8001,
- (_, T) => S8000,
- _ => S8004,
- },
- }
- }
- S8014 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C002,
- _ => match (data.a, data.b) {
- (_, F) => S8001,
- (T, _) => S8000,
- _ => S8014,
- },
- }
- }
- S8005 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C003,
- _ => match (data.a, data.b) {
- (F, F) => S8001,
- _ => S8005,
- },
- }
- }
- C001 | C002 => match (data.a, data.b) {
- (F, F) => S8001,
- _ => *STATE,
+ }
+ }
+ S8014 => {
+ *TIMEOUT_CNTR -= 1;
+ match *TIMEOUT_CNTR {
+ 0 => C002,
+ _ => match (data.a, data.b) {
+ (_, F) => S8001,
+ (T, _) => S8000,
+ _ => S8014,
},
- C003 => match (data.a, data.b) {
- (F, F) => S8001,
- _ => C003,
+ }
+ }
+ S8005 => {
+ *TIMEOUT_CNTR -= 1;
+ match *TIMEOUT_CNTR {
+ 0 => C003,
+ _ => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => S8005,
},
- };
+ }
+ }
+ C001 | C002 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => *STATE,
+ },
+ C003 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => C003,
+ },
+ };
}
diff --git a/src/main.rs b/src/main.rs
index 75165be098600d7d550fe29844cb9e8691feff40..1ee0085e4262e17e0b3946ddabda7dc40862afba 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -5,8 +5,7 @@ use klee::{kassert, ksymbol};
#[no_mangle]
fn main() {
- let mut DATA: [Data; (DISCREPENCY + 1) as usize] =
- unsafe { core::mem::uninitialized() };
+ let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA");
let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };