plcopen + klee

.gitignore

+/target
+**/*.rs.bk
\ No newline at end of file

Cargo.lock

+[[package]]
+name = "cfg-if"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "cstr_core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "memchr 2.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cty"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "klee"
+version = "0.2.0"
+source = "git+https://gitlab.henriktjader.com/pln/cargo-klee#7d2f3699a763a2ef06c37b255afe1dd6ad9b2cdd"
+dependencies = [
+ "cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "memchr"
+version = "2.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cfg-if 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "plcopen"
+version = "0.1.0"
+dependencies = [
+ "klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)",
+]
+
+[[package]]
+name = "version_check"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[metadata]
+"checksum cfg-if 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)" = "082bb9b28e00d3c9d39cc03e64ce4cea0f1bb9b3fde493f0cbc008472d22bdf4"
+"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
+"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
+"checksum klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)" = "<none>"
+"checksum memchr 2.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "db4c41318937f6e76648f42826b1d9ade5c09cafb5aef7e351240a70f39206e9"
+"checksum version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "914b1a6776c4c929a602fafd8bc742e06365d4bcbe48c30f9cca5824f70dc9dd"

Cargo.toml

+[package]
+name = "plcopen"
+version = "0.1.0"
+authors = ["Per Lindgren <per.lindgren@ltu.se>"]
+edition = "2018"
+
+[dependencies]
+klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+
+[[bin]]
+name = "main"
+path = "src/main.rs"
+
+[features]
+klee-analysis = ["klee/klee-analysis"]
+
+[profile.dev]
+incremental = false
+# lto = true
+
+[profile.release]
+debug = true
+panic = "abort"
+lto = true
\ No newline at end of file

README.md

+cargo klee --bin main --release
\ No newline at end of file

src/main.rs

+#![allow(non_snake_case)]
+#![no_main]
+
+use klee::{kassert, ksymbol};
+
+#[no_mangle]
+fn main() {
+    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() };
+    ksymbol!(&mut TIMEOUT_CNTR, "TIMEOUT_CNTR");
+
+    let mut STATE_HISTORY: [State; (DISCREPENCY + 1) as usize] =
+        unsafe { core::mem::uninitialized() };
+
+    DATA[0] = Data { a: false, b: false };
+    TIMEOUT_CNTR = 0;
+    let mut STATE = S8001;
+
+    for i in 0..(DISCREPENCY + 1) as usize {
+        periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+
+        // invariants
+        // S8000 -> a & b
+        if STATE == S8000 {
+            kassert!(DATA[i].a & DATA[i].b);
+        }
+        // !a | !b -> ! S8000
+        if !DATA[i].a | !DATA[i].b {
+            kassert!(!(STATE == S8000));
+        }
+        // S8001 -> !a & !b
+        if STATE == S8001 {
+            kassert!(!DATA[i].a | !DATA[i].b);
+        }
+        // !a & !b -> S8001
+        if !DATA[i].a & !DATA[i].b {
+            kassert!(STATE == S8001);
+        }
+
+        // error states implies timeout
+        match STATE {
+            C001 | C002 | C002 => kassert!(TIMEOUT_CNTR == 0),
+            _ => {}
+        }
+
+        if i > 0 {
+            match STATE_HISTORY[i - 1] {
+                C001 | C002 | C003 | S8005 => {
+                    kassert!(!(STATE == S8000));
+                }
+                _ => {
+                    if DATA[i].a & DATA[i].b {
+                        kassert!(STATE == S8000);
+                    }
+                }
+            }
+        }
+        STATE_HISTORY[i] = STATE;
+    }
+}
+
+#[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 DISCREPENCY: u32 = 4;
+const T: bool = true;
+const F: bool = false;
+
+fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
+    // we start directly in the init state S80001
+    // static mut STATE: State = State::S8001;
+    // static mut TIMEOUT_CNTR: u32 = 0;
+
+    let 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,
+        },
+        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,
+        },
+        C003 => match (data.a, data.b) {
+            (F, F) => S8001,
+            _ => C003,
+        },
+    };
+}