eq.rs

#![allow(non_snake_case)]
#![no_main]

extern crate klee;
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;

    // 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 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));
    }

    // 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] {
        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),

      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);
      }
      _ => {}
    }

    // // 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]) };
  }
}

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,
    },
  };
}