diff --git a/examples/eq_dfs.rs b/examples/eq_dfs.rs
index c800ec24b60a5ff6d5cb6b0753bea5cb8ac002e7..fcccef2190b211b9cea82f87c570e2b63334eb5c 100644
--- a/examples/eq_dfs.rs
+++ b/examples/eq_dfs.rs
@@ -2,231 +2,250 @@
#![no_main]
#![no_std]
-extern crate panic_abort;
extern crate klee;
+extern crate panic_abort;
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::*;
const DISCREPANCY: u32 = 2;
// const HORIZON: usize = (2 * DISCREPANCY + 5) as usize;
-const HORIZON: usize = 100 as usize;
+const HORIZON: usize = (DISCREPANCY * 3 + 4) as usize;
const T: bool = true;
const F: bool = false;
#[no_mangle]
fn main() {
- let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
- ksymbol!(&mut DATA, "DATA");
+ let mut DATA: [Data; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut DATA, "DATA");
+
+ let mut STATE_H: [State; HORIZON + 1] = unsafe { core::mem::uninitialized() };
- let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
+ let mut CNTR_H: [u32; HORIZON + 1] = unsafe { core::mem::uninitialized() };
- let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
+ let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+ // initial state, Init
+ let mut i = 0;
+ let mut TIMEOUT_CNTR: u32 = DISCREPANCY;
+ let mut STATE = S8001;
+ STATE_H[i] = STATE;
+ CNTR_H[i] = TIMEOUT_CNTR;
+ i += 1; // next state index
- let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
- // initial state, Init
- let mut i = 0;
- let mut TIMEOUT_CNTR: u32 = DISCREPANCY;
- let mut STATE = S8001;
+ loop {
+ eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
STATE_H[i] = STATE;
CNTR_H[i] = TIMEOUT_CNTR;
- i += 1; // next state index
-
- loop {
- eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
- STATE_H[i] = STATE;
- CNTR_H[i] = TIMEOUT_CNTR;
-
- // 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);
- }
- // !a | !b -> !S8000
- // ensures that if any input is false we cannot enter the Enable state
- // this can also be seen as a safety 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 safety 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));
+ }
- // transition invariants
- if i > 0 {
- match STATE_H[i - 1] {
- C001 | C002 | C003 => {
- // transitions from error
- kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
- }
- S8005 => {
- kassert!(
- (STATE_H[i] == S8001)
- | (STATE == C003)
- | (STATE == STATE_H[i - 1])
- );
- }
- _ => (),
- }
- }
+ // 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);
+ }
- // // 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 {
- if STATE_H[i - 1] == STATE_H[i] {
- kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
- }
- }
- // // Waiting states -> !timeout
- // // Waiting states implies that TIMEOUT_CNTR has not yet expired
- // // and that the time remaining is not longer than the DISCREPANCY
- // kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
- // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
- }
- _ => {}
+ // transition invariants
+ if i > 0 {
+ match STATE_H[i - 1] {
+ C001 | C002 | C003 => {
+ // transitions from error
+ kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+ }
+ S8005 => {
+ kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
}
+ _ => (),
+ }
+ }
+
+ // // DISCREPANCY related invariants
+ match STATE {
+ // Error -> timeout
+ C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
- // // liveness?
- // if i == HORIZON - 1 {
- // let mut ok = false;
- // for j in 0..=i {
- // if STATE_H[j] == S8001 {
- // ok = true;
- // }
- // }
- // kassert!(ok);
- // }
-
- // if i > 0 {
- // match STATE_H[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);
- // }
- // }
- // }
- // }
-
- unsafe { core::ptr::read_volatile(&STATE_H[i]) };
-
- let mut is_visited = false;
- match STATE {
- S8004 | S8005 | S8014 => {}
- _ => {
- for j in 0..i {
- if (STATE_H[i] == STATE_H[j]) {
- is_visited = true;
- }
- }
- }
+ S8004 | S8005 | S8014 => {
+ // // remaining in a waiting state decreases the counter
+ if i > 0 {
+ if STATE_H[i - 1] == STATE_H[i] {
+ kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
+ }
}
+ // // Waiting states -> !timeout
+ // // Waiting states implies that TIMEOUT_CNTR has not yet expired
+ // // and that the time remaining is not longer than the DISCREPANCY
+ // kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
+ // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
+ }
+ _ => {}
+ }
- if is_visited {
- break;
+ // // liveness?
+ // if i == HORIZON - 1 {
+ // let mut ok = false;
+ // for j in 0..=i {
+ // if STATE_H[j] == S8001 {
+ // ok = true;
+ // }
+ // }
+ // kassert!(ok);
+ // }
+
+ // if i > 0 {
+ // match STATE_H[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);
+ // }
+ // }
+ // }
+ // }
+
+
+ let mut is_visited = false;
+ match STATE {
+ S8004 | S8005 | S8014 => {
+ for j in 0..i {
+ if (STATE_H[i] == STATE_H[j] && CNTR_H[i] == CNTR_H[j]) {
+ is_visited = true;
+ }
}
- i += 1;
- if i == HORIZON {
- kassert!(false);
+ }
+ _ => {
+ for j in 0..i {
+ if (STATE_H[i] == STATE_H[j]) {
+ is_visited = true;
+ }
}
+ }
+ }
+
+ if is_visited {
+ break;
}
+
+ if i == HORIZON {
+ kassert!(false);
+ }
+
+ i += 1;
+ }
}
-fn eq(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 = DISCREPANCY;
- S8005
- }
- (T, T) => S8000,
- },
- S8001 => match (data.a, data.b) {
- (F, F) => S8001,
- (F, T) => {
- *TIMEOUT_CNTR = DISCREPANCY;
- S8014
- }
- (T, F) => {
- *TIMEOUT_CNTR = DISCREPANCY;
- S8004
- }
- (T, T) => S8000,
- },
- S8004 => match *TIMEOUT_CNTR {
- 0 => C001,
- _ => {
- *TIMEOUT_CNTR -= 1;
- match (data.a, data.b) {
- (F, _) => S8001,
- (_, T) => S8000,
- _ => S8004,
- }
- }
- },
- S8014 => match *TIMEOUT_CNTR {
- 0 => C002,
- _ => {
- *TIMEOUT_CNTR -= 1;
- match (data.a, data.b) {
- (_, F) => S8001,
- (T, _) => S8000,
- _ => S8014,
- }
- }
- },
- S8005 => match *TIMEOUT_CNTR {
- 0 => C003,
- _ => {
- *TIMEOUT_CNTR -= 1;
- match (data.a, data.b) {
- (F, F) => S8001,
- _ => S8005,
- }
- }
- },
- C001 | C002 | C003 => match (data.a, data.b) {
- (F, F) => S8001,
- _ => *STATE,
- },
- };
+fn eq(
+ 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 = DISCREPANCY;
+ S8005
+ }
+ (T, T) => S8000,
+ },
+ S8001 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8014
+ }
+ (T, F) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8004
+ }
+ (T, T) => S8000,
+ },
+ S8004 => match *TIMEOUT_CNTR {
+ 0 => C001,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8014
+ }
+ (T, T) => S8000,
+ _ => S8004,
+ }
+ }
+ },
+ S8014 => match *TIMEOUT_CNTR {
+ 0 => C002,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
+ (F, F) => S8001,
+ (T, F) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8004
+ }
+ (T, T) => S8000,
+ _ => S8014,
+ }
+ }
+ },
+ S8005 => match *TIMEOUT_CNTR {
+ 0 => C003,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ 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,
+ },
+ };
}