#![allow(non_snake_case)] #![no_main] #![no_std] extern crate klee; extern crate panic_abort; use klee::{kassert, kassume, ksymbol}; #[derive(Debug, Copy, Clone)] pub struct Data { a: bool, b: bool, } #[derive(Debug, Copy, Clone, PartialEq)] pub enum State { S8000, S8001, S8004, S8014, S8005, C001, C002, C003, } use State::*; const DISCREPANCY: u32 = 1; const HORIZON: usize = (DISCREPANCY + 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 STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() }; let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() }; let mut STATE = S8001; for i in 0..HORIZON { eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]); STATE_H[i] = STATE; CNTR_H[i] = TIMEOUT_CNTR; // (1) !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 // (2) 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); } // transition invariants if i > 0 { match STATE_H[i - 1] { C001 | C002 | C003 => { // (3) // transitions from error kassert!( (STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]) ); } S8005 => { // (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!(TIMEOUT_CNTR == 0), S8004 | S8005 | S8014 => { // (6) // 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]); } } } _ => {} } } } 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 => match (data.a, data.b) { (F, F) => S8001, _ => *STATE, }, C003 => match (data.a, data.b) { (F, F) => S8001, _ => C003, }, }; }