dfs

Cargo.toml

@@ -5,16 +5,13 @@ authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.
 
 [dependencies]
 klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+enumset = "0.3.16"
+panic-abort = "0.3.1"
 # panic-abort = "0.3.1"
 
 [dependencies.cortex-m]
 version = "0.6.0"
 
-[patch.crates-io]
-vcell = { git = "https://github.com/perlindgren/vcell.git" }
-volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
-cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
-
 [dependencies.volatile-register]
 version = "0.3.0"
 
@@ -24,6 +21,11 @@ git = "https://gitlab.henriktjader.com/pln/stm32f413.git"
 branch = "klee-analysis" 
 optional = true
 
+[patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git" }
+volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
 [[examples]]
 name = "gpioa"
 path = "examples/gpioa.rs"
@@ -31,7 +33,7 @@ path = "examples/gpioa.rs"
 
 [profile.dev]
 incremental = false
-# lto = true
+lto = true
 
 [profile.release]
 debug = true

examples/eq_dfs.rs

+#![allow(non_snake_case)]
+#![no_main]
+#![no_std]
+
+extern crate panic_abort;
+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 = 2;
+// const HORIZON: usize = (2 * DISCREPANCY + 5) as usize;
+const HORIZON: usize = 100 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() };
+    // 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
+
+    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));
+        }
+
+        // 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]) };
+
+        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;
+                    }
+                }
+            }
+        }
+
+        if is_visited {
+            break;
+        }
+        i += 1;
+        if i == HORIZON {
+            kassert!(false);
+        }
+    }
+}
+
+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,
+        },
+    };
+}