major update to examples

435742ae · Per · 51dedf4e · 435742ae · 435742ae · 435742ae
Commit 435742ae authored 5 years ago by Per
--- a/.cargo/config
+++ b/.cargo/config
+[target.'cfg(all(target_arch = "arm", target_os = "none"))']
+# uncomment ONE of these three option to make `cargo run` start a GDB session
+# which option to pick depends on your system
+runner = "arm-none-eabi-gdb -q -x openocd.gdb"
+# runner = "gdb-multiarch -q -x openocd.gdb"
+# runner = "gdb -q -x openocd.gdb"
+
+rustflags = [
+  # LLD (shipped with the Rust toolchain) is used as the default linker
+  "-C", "link-arg=-Tlink.x"
+  # if you run into problems with LLD switch to the GNU linker by commenting out
+  # this line
+  # "-C", "linker=arm-none-eabi-ld",
+
+  # if you need to link to pre-compiled C libraries provided by a C toolchain
+  # use GCC as the linker by commenting out both lines above and then
+  # uncommenting the three lines below
+  # "-C", "linker=arm-none-eabi-gcc",
+  # "-C", "link-arg=-Wl,-Tlink.x",
+  # "-C", "link-arg=-nostartfiles",
+]
+
+[build]
+# Pick ONE of these compilation targets as default
+# target = "thumbv6m-none-eabi"    # Cortex-M0 and Cortex-M0+
+# target = "thumbv7m-none-eabi"    # Cortex-M3
+# target = "thumbv7em-none-eabi"   # Cortex-M4 and Cortex-M7 (no FPU)
+# target = "thumbv7em-none-eabihf" # Cortex-M4F and Cortex-M7F (with FPU)
\ No newline at end of file
--- a/Cargo.lock
+++ b/Cargo.lock
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+[[package]]
+name = "aligned"
+version = "0.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "as-slice"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "bare-metal"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m"
+version = "0.6.1"
+source = "git+https://github.com/perlindgren/cortex-m.git?branch=trustit#b2fa26f1044509a34006d4ad6303abc52ea09bce"
+dependencies = [
+ "aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
+ "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rt"
+version = "0.6.11"
+source = "git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit#8d2686097e168e8b82d51ae1ea17d9ebe6d567e0"
+dependencies = [
+ "cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
+ "cortex-m-rt-macros 0.1.7 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
+ "r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-rt-macros"
+version = "0.1.7"
+source = "git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit#8d2686097e168e8b82d51ae1ea17d9ebe6d567e0"
+dependencies = [
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.13 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cortex-m-semihosting"
+version = "0.3.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
+]
+
+[[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.2.1 (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 = "generic-array"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "generic-array"
+version = "0.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "klee-examples"
+version = "0.1.0"
+dependencies = [
+ "cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
+ "cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
+ "cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
+ "lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)",
+ "stm32f4 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+ "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "klee-sys"
+version = "0.1.0"
+source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#c8275a34cffb895984d6bdea80e9c6ff9079f769"
+dependencies = [
+ "cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "lm3s6965"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
+]
+
+[[package]]
+name = "memchr"
+version = "2.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "panic-halt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "panic-klee"
+version = "0.1.0"
+source = "git+https://gitlab.henriktjader.com/pln/panic-klee.git#3b0c897f49d7fff017424364e280bcb9dbaffa5d"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "r0"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rustc_version"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver-parser"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "stable_deref_trait"
+version = "1.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "stm32f4"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
+ "cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
+ "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+]
+
+[[package]]
+name = "syn"
+version = "1.0.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "typenum"
+version = "1.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "vcell"
+version = "0.1.2"
+source = "git+https://github.com/perlindgren/vcell.git?branch=trustit#4eb44a012d65860c596556d6a63af9e0fa31853a"
+dependencies = [
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
+]
+
+[[package]]
+name = "volatile-register"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+]
+
+[metadata]
+"checksum aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "eb1ce8b3382016136ab1d31a1b5ce807144f8b7eb2d5f16b2108f0f07edceb94"
+"checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
+"checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
+"checksum cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)" = "<none>"
+"checksum cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)" = "<none>"
+"checksum cortex-m-rt-macros 0.1.7 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)" = "<none>"
+"checksum cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
+"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 generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)" = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
+"checksum generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)" = "0ed1e761351b56f54eb9dcd0cfaca9fd0daecf93918e1cfc01c8a3d26ee7adcd"
+"checksum klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)" = "<none>"
+"checksum lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "8698042a7495160eac9f7298a32cd1ddbb6ad2780f766f5a99b4f0a6b915e0ad"
+"checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
+"checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
+"checksum panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)" = "<none>"
+"checksum proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)" = "0319972dcae462681daf4da1adeeaa066e3ebd29c69be96c6abb1259d2ee2bcc"
+"checksum quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
+"checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
+"checksum rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)" = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
+"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
+"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
+"checksum stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
+"checksum stm32f4 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "88640ad08c62e0651a1320187f38c3655d025ed580a10f0e4d85a2cc4829069f"
+"checksum syn 1.0.13 (registry+https://github.com/rust-lang/crates.io-index)" = "1e4ff033220a41d1a57d8125eab57bf5263783dfdcc18688b1dacc6ce9651ef8"
+"checksum typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
+"checksum unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
+"checksum vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)" = "<none>"
+"checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -9,12 +9,20 @@ panic-halt = "0.2.0"

 vcell = "0.1.2"
 volatile-register = "0.2.0"
-cortex-m-rt = "0.6.11"
+
+[dependencies.cortex-m-rt]
+version = "0.6.11"
+optional = true

 [dependencies.lm3s6965] 
 version = "0.1.3"
 optional = true

+[dependencies.stm32f4] 
+version = "0.9.0"
+features = ["stm32f401", "rt"]
+optional = true
+
 [dependencies.cortex-m-semihosting]
 version = "0.3.5"
 optional = true
@@ -27,39 +35,40 @@ version = "0.1.0"
 git = "https://gitlab.henriktjader.com/pln/klee-sys.git"
 version = "0.1.0"

-[dependencies.cortex-m-rtfm]
-path = "../cortex-m-rtpro"
-optional = true
+# [dependencies.cortex-m-rtfm]
+# path = "../cortex-m-rtpro"
+# optional = true

 [dependencies.cortex-m]
 version = "0.6.1"
 optional = true
-# #features = ["inline-asm", "klee-analysis"]

 [patch.crates-io]
 vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
 #vcell = { path = "../vcell" }

 cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
-#cortex-m = { path = "../cortex-m" }
+# cortex-m = { path = "../cortex-m" }

-#cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" }
-cortex-m-rt = { path = "../cortex-m-rt" }
+cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" }
+# cortex-m-rt = { path = "../cortex-m-rt" }

 [features] 
 klee-analysis = [ 
-    "vcell/klee-analysis",
-    "cortex-m/klee-analysis", 
-    "cortex-m-rt/klee-analysis" 
-    ]
+     "vcell/klee-analysis",
+     "cortex-m/klee-analysis", 
+     "cortex-m-rt/klee-analysis" 
+]
+
 inline-asm = ["cortex-m/inline-asm"]
-rtpro = [ "cortex-m-rtfm/klee-analysis", "cortex-m-rt/rtpro", "lm3s6965" ]
+# rtpro = [ "cortex-m-rtfm/klee-analysis", "cortex-m-rt/rtpro", "lm3s6965" ]
+f4 = ["stm32f4/stm32f401", "stm32f4/rt", "cortex-m-semihosting", "cortex-m-rt"]

 [profile.dev]
 panic = "abort"
-# incremental = false
+# incremental = false # used to be required due to bug in rust toolchain
 lto = true
-# codegen-units = 1
+# codegen-units = 1 # used to be required due to bug in rust toolchain

 [profile.release]
 debug = true

--- a/README.md
+++ b/README.md
 # klee-examples

-This repo contains a set of usage examples for `klee-sys` low-level KLEE bindings. 
+This repo contains a set of usage examples for `klee-sys` low-level KLEE bindings.

-## klee_only_test.rs
+## paths.rs

 This example showcase the different path termintaiton conditions possible and their effect to KLEE test case generation.

-> cargo klee --example klee_only_test
+## assume_assert.rs
+
+This example showcase contract based verification, and the possibilies to extract proofs.
+
+## vcell_test.rs
+
+Simple test to showcase low-level access.
+
+
+## f401_minimal.rs
+
+This example showcase the execution of code on the stm32f401 (and similar targets from the f4).
+
+### dependencies
+
+- stm32401 nucleo board or similiar with recent stlink firmware
+- (recent) openocd (tested with version 0.10.0)
+- arm-none-eabi-gdb (tested with version 0.8.3)
+- llvm target thumbv7em-none-eabi (`rustup target add thumbv7em-none-eabi`)
+
+
+## Licencse
+
+Copyright Per Lindgren.
+
+All rights reserved, use restricted for non-commercial purpose.
\ No newline at end of file
--- a/build.rs
+++ b/build.rs
+use std::env;
+use std::fs::File;
+use std::io::Write;
+use std::path::PathBuf;
+
+fn main() {
+    // Put the linker script somewhere the linker can find it
+    let out = &PathBuf::from(env::var_os("OUT_DIR").unwrap());
+    File::create(out.join("memory.x"))
+        .unwrap()
+        .write_all(include_bytes!("memory.x"))
+        .unwrap();
+    println!("cargo:rustc-link-search={}", out.display());
+
+    // Only re-run the build script when memory.x is changed,
+    // instead of when any part of the source code changes.
+    println!("cargo:rerun-if-changed=memory.x");
+}
--- a/examples/assume_assert.rs
+++ b/examples/assume_assert.rs
+#![no_std]
+#![no_main]
+
+use core::u32;
+use klee_sys::*;
+use panic_klee as _;
+
+#[no_mangle]
+fn main() {
+    let mut a: u32 = 0;
+    klee_make_symbolic!(&mut a, "a");
+
+    klee_assert!(f1(a) > a);
+}
+
+fn f1(a: u32) -> u32 {
+    // klee_assume(a < u32::MAX);
+    // klee_assume(a == u32::MAX);
+    let r = a + 1;
+    // klee_assert!(r > a);
+    r
+}
+
+// This example showcase how contracts can be encoded
+//
+// Let us start with the functian f1 (above).
+// Intuitively `f1(a) > a` right?
+//
+// Well let's check that....
+//
+// > cargo klee --example assume_assert
+// ...
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// ..
+// KLEE: done: total instructions = 147
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 2
+//
+// So obviously that is not the case. What then?
+// Here (again) we are exposed to an overflow on a + 1
+//
+// more target/debug/examples/klee-last/test000002.abort.err
+// Error: abort failure
+// File: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs
+// Line: 8
+// assembly.ll line: 23
+// Stack:
+//         #000000023 in rust_begin_unwind (=94422568770784) at /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8
+//         #100000193 in _ZN4core9panicking9panic_fmt17hdeb7979ab6591473E (=94422569870368, =94422566526016) at src/libcore/panicking.rs:139
+//         #200000227 in _ZN4core9panicking5panic17hb5daa85c7c72fc62E (=94422566525664, =28, =94422566526016) at src/libcore/panicking.rs:70
+//         #300000130 in _ZN13assume_assert2f117h371b5439de984e07E () at examples/assume_assert.rs:19
+//        #400000088 in main () at examples/assume_assert.rs:13
+//
+// So its line 19, (a + 1)
+//
+// Lets now make a contract, assuming that a < u32.MAX
+// uncomment `klee_assume!(a < core::u32::MAX)`
+//
+// > cargo klee --example assume_assert
+//
+// We can now finalize the contract, by uncommenting line 20 (with the post condition).
+//
+// So our pre-condition is that a < u32.MAX and the post condition is that r > a.
+//
+// Can assumptions go wrong?
+// Well they can? And we will spot it!
+//
+// Try uncommenting line 18, re-run `cargo klee`
+//
+// You should get...
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/klee-sys-7ee2aa8a1a6bbc46/c8275a3/src/lib.rs:19: invalid klee_assume call (provably false)
+//
+// So KLEE tracks the "path condition", i.e., at line 18 it knows (assumes) that that
+// a < u32::MAX, and finds that the assumtion a == u32::MAX cannot be satisfied.
+//
+// This is exeteremely powerful as KLEE tracks all known "constraints" and all their raliaitons
+// and mathematically checks for the satisfiability of each "assume" and "assert".
+//
+// So what we get here is not a mere test, but an actual proof!!!!
--- a/examples/cortex_m_test1.rs
+++ b/examples/cortex_m_test1.rs
+#![no_std]
+#![no_main]
+
+use klee_sys::klee_abort;
+extern crate cortex_m;
+extern crate panic_klee;
+
+use cortex_m::peripheral::Peripherals;
+
+static mut S: u32 = 100;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    let a = dwt.cyccnt.read();
+    if a == unsafe { S } {
+        panic!();
+        // klee_abort!();
+    }
+
+    klee_abort!();
+}
+
+// In this example we showcase
+// - how hardware reads are automatically made symbolic
+// - semantic paths (LLVM-IR vs source code)
+//
+// In the Cargo.toml we pass the "klee-analysis" feature to `vcell` and `cortex-m`.
+// This implies that hardware reads are made symbolic, while writes are surpressed.
+//
+// > cargo klee --example cortex_m_test1
+// ...
+// KLEE: ERROR: examples/cortex_m_test1.rs:22: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+//
+// KLEE: done: total instructions = 743
+// KLEE: done: completed paths = 4
+// KLEE: done: generated tests = 2
+//
+// In this case KLEE generates to tests leading up to the terminating lines (errors)
+// 18 and 22 respectively.
+//
+// This is due to that the `dwt.read` has rendered `a` as a symbolic value.
+//
+// Now let's comment out line 18 and uncamment line 19.
+//
+// > cargo klee --example cortex_m_test1
+// ...
+// KLEE: ERROR: examples/cortex_m_test1.rs:16: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+//
+// KLEE: done: total instructions = 663
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 1
+//
+// So, previously we made the claim that all `klee_abort` calls will render a unique test,
+// but clearly this is not the case here.
+//
+// What happened is that the LLVM-IR the code has already been optimized to
+// to semantically equivalent LLVM-IR representation.
+//
+// ; Function Attrs: nounwind nonlazybind
+// define void @main() unnamed_addr #4 !dbg !1013 {
+//     start:
+// ...
+//   call void @klee_make_symbolic(i8* %_3.i.i.i, i64 %24, i8* %27) #14, !dbg !1145
+//   %28 = load i32, i32* %symbolic_value.i.i, align 4, !dbg !1146
+//   store i32 %28, i32* %a, align 4, !dbg !1119
+//   call void @abort(), !dbg !1147
+//   unreachable, !dbg !1147
+// ...
+//
+// So what we see here, is that the if statement is nowhere to be found
+// and we call @obort(), and the code below is unreachable (as abort() -> !)
+//
+// This is semantically equivallent to:
+// if a == unsafe { S } {
+//     // panic!();
+//     klee_abort!(); // (A)
+// }
+// klee_abort!(); // (B)
+//
+// So LLVM-IR paths and source code paths are not necessarily equivalent.
+// rustc (the Rust compiler) and LLVM is free to make any choices of the representation
+// as long as the semantics (meaning) is preserved.
+//
+// Does that imply that (A) is unreachable (dead code)?
+//
+// Well that depends on the view...
+// rustc and/or LLVM has decided it is redundant and therefore not present in the LLVM-IR.
+//
+// What about code coverage?
+//
+// In this case there would be no "test" that visits this path, thus
+// "classical" coverage test, would indicate that we have not covered all source code paths.
+//
+// So classical code coverage would go down, indicating lower quality test (bad for certfication).
+// However we can proudly claim that the "classical" coverage as a measure of quality is
+// indeed at fault. It is not the source code we should worry about!
+//
+// Our test provides "complete" coverage regarding the semantics of the source code
+// (as we have not missed any potential error).
+//
+// This example is of course contrieved, but showcase that "classical" measures/
+// quality goals restated and certification procedures updated accordingly!
--- a/examples/cortex_m_test2.rs
+++ b/examples/cortex_m_test2.rs
-#![no_std]
-#![no_main]
-
-use klee_sys::klee_abort;
-extern crate cortex_m;
-extern crate panic_klee;
-
-use cortex_m::peripheral::Peripherals;
-
-static mut S: u32 = 100;
-
-#[no_mangle]
-fn main() {
-    let peripherals = Peripherals::take().unwrap();
-    let mut dwt = peripherals.DWT;
-    let a = dwt.cyccnt.read();
-    if a == unsafe { S } {
-        panic!();
-    }
-
-    klee_abort!();
-}
-
-// #[no_mangle]
-// pub fn some_interrupt() {
-//     unsafe { S = 0 };
-// }
--- a/examples/cortex_m_test_nightly.rs
+++ b/examples/cortex_m_test_nightly.rs
-// > cargo klee --example klee_cortex_m_test -r -k -g -v
+#![feature(core_intrinsics)] // intrinsic division requires nightly
+#![no_std]
+#![no_main]
+
+use klee_sys::klee_abort;
+extern crate cortex_m;
+extern crate panic_klee;
+
+use cortex_m::peripheral::Peripherals;
+
+use core::{intrinsics::unchecked_div, num::Wrapping, ptr::read_volatile};
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    // let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    dwt.enable_cycle_counter();
+    let a = dwt.cyccnt.read();
+    let b = dwt.cyccnt.read();
+    let c = dwt.cyccnt.read();
+    unsafe {
+        let some_time_quota = unchecked_div(a, (Wrapping(c) - (Wrapping(b) - Wrapping(100))).0);
+        read_volatile(&some_time_quota); // prevent optimization in release mode
+    }
+}
+
+// > cargo klee --example cortex_m_test_nightly -r -k -g -v
 // ...
-// KLEE: ERROR: examples/klee_cortex_m_test.rs:120: divide by zero
-// KLEE: NOTE: now ignoring this error at this location
-// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: WARNING: undefined reference to function: rust_eh_personality
+// KLEE: ERROR: examples/cortex_m_test_nightly.rs:23: divide by zero
 // KLEE: NOTE: now ignoring this error at this location
 //
-// KLEE: done: total instructions = 1454
-// KLEE: done: completed paths = 6
-// KLEE: done: generated tests = 4
+// KLEE: done: total instructions = 1446
+// KLEE: done: completed paths = 4
+// KLEE: done: generated tests = 3
 // ..
 //(gdb) shell ls klee-last
-// assembly.ll  info  messages.txt  run.istats  run.stats  test000001.div.err  test000001.kquery  test000001.ktest  test000002.ktest  warnings.txt
+// assembly.ll  info  messages.txt  run.istats  run.stats  test000001.div.err  test000001.kquery  test000001.ktest  test000002.ktest  test000003.ktest  warnings.txt
 //
 // So we see that test000001.ktest was causing a division error,
 // the other test case passed
 //
 // (gdb) set env KTEST_FILE=klee-last/test000001.ktest
 // (gdb) run
-// Starting program: /home/pln/rust/grepit/klee-examples/target/debug/examples/klee_cortex_m_test.replay
+// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/cortex_m_test_nightly.replay
 // Program received signal SIGFPE, Arithmetic exception.
-// 0x0000555555555528 in main () at examples/klee_cortex_m_test.rs:133
-// 133             let some_time_quota = unchecked_div(a, c - (b - 100));
+// 0x0000555555555525 in main () at examples/cortex_m_test_nightly.rs:23
+// 23              let some_time_quota = unchecked_div(a, (Wrapping(c) - (Wrapping(b) - Wrapping(100))).0);
 //
 // Let's look at the actual test
 // (gdb) shell ktest-tool klee-last/test000001.ktest
 // ktest file : 'klee-last/test000001.ktest'
-// args       : ['/home/pln/rust/grepit/klee-examples/target/debug/examples/klee_cortex_m_test-d9038188a1e4d0b0.ll']
+// args       : ['/home/pln/rust/trustit/klee-examples/target/debug/examples/cortex_m_test_nightly-dd58a25289c18430.ll']
 // num objects: 5
 // object 0: name: 'PRIMASK'
 // object 0: size: 4
@@ -63,8 +89,8 @@
 // object 4: uint: 0
 // object 4: text: ....
 //
-// (gdb) backtrace
-// #0  0x0000555555555528 in main () at examples/klee_cortex_m_test.rs:133
+// (gdb)  backtrace
+// #0  0x0000555555555525 in main () at examples/cortex_m_test_nightly.rs:23
 // (gdb) print a
 // $1 = 0
 // (gdb) print b
@@ -82,7 +108,7 @@
 // (Under the hood, `Peripherals.take` executes in a global critical section.)
 //
 // This access is along the "happy path" towards the error, so any value would
-// suffice (in this case 0x00000000 was selected by KLEE).
+// suffice (in this case 0x01010101 was selected by KLEE).
 //
 // The first `vcell` access: was done when enabling the cycle counter.
 // The rest of accesses stem from reading `a`, `b`, and `c`.
@@ -92,30 +118,20 @@
 // Notice here, that this error is spotted EVEN while we are telling
 // Rust to use the primitive (intrinsic) division for "unchecked_div" performance.
 //
-#![feature(core_intrinsics)] // intrinsic division requires nightly
-#![no_std]
-#![no_main]
-
-use klee_sys::klee_abort;
-extern crate cortex_m;
-extern crate panic_klee;
-
-use cortex_m::peripheral::Peripherals;
-
-use core::{intrinsics::unchecked_div, ptr::read_volatile};
-
-#[no_mangle]
-fn main() {
-    let peripherals = Peripherals::take().unwrap();
-    // let peripherals = Peripherals::take().unwrap();
-    let mut dwt = peripherals.DWT;
-    dwt.enable_cycle_counter();
-    let a = dwt.cyccnt.read();
-    let b = dwt.cyccnt.read();
-    let c = dwt.cyccnt.read();
-    unsafe {
-        let some_time_quota = unchecked_div(a, c - (b - 100));
-        read_volatile(&some_time_quota); // prevent optimization
-    }
-    klee_abort!();
-}
+// Now re-run the example in --release mode.
+// You should find that the error is spotted but the variables are in registers,
+// so `print` won't work.
+//
+// Discussion:
+// We can allow for AGGRESSIVE optimization by proving the absence of errors.
+// In this case we use the Wrapping for unchecked wrapping arithmetics (along the lines of C/C++)
+// and primitive unchecked (intrinsic) division.
+//
+// Checked arithmetics comes with a high prise at run-time, and for embedded not
+// only affects the execution time but also power consumption.
+//
+// We can fearlessly apply optimisations (including intrinsic/primitive operations)
+// and let the tool prove that the code is free of potential errors.
+//
+// Thus we get BOTH improved performance and improved reliability/correctness at the same time.
+// This is the Way!
--- a/examples/f401_minimal.rs
+++ b/examples/f401_minimal.rs
+// minimal example for the stm32-f401 (and the f4 series)
+//! Prints "Hello, world!" on the host console using semihosting
+
+#![no_main]
+#![no_std]
+
+extern crate panic_halt;
+
+use stm32f4::stm32f401 as stm32;
+
+use cortex_m_rt::entry;
+use cortex_m_semihosting::hprintln;
+
+#[entry]
+fn main() -> ! {
+    hprintln!("Hello, world!").unwrap();
+
+    loop {}
+}
+
+// See RM0368 Reference Manual for details
+// https://www.st.com/content/ccc/resource/technical/document/reference_manual/5d/b1/ef/b2/a1/66/40/80/DM00096844.pdf/files/DM00096844.pdf/jcr:content/translations/en.DM00096844.pdf
+//
+// Memory map is given in `memory.x`, in particular we define:
+// 96k RAM starting at 0x2000_0000, and
+// 256k Flash starting at 0x0800_0000
+//
+// Run in separate terminal:
+// openocd -f openocd.cfg
+//
+// cargo run --example f401_minimal --features f4 --target thumbv7em-none-eabihf
--- a/examples/klee_init.rs
+++ b/examples/klee_init.rs
-//! examples/init.rs
-
-// #![deny(unsafe_code)]
-// #![deny(warnings)]
-#![no_main]
-#![no_std]
-
-#[cfg(feature = "klee-analysis")]
-use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
-
-#[cfg(not(feature = "klee-analysis"))]
-use panic_halt as _;
-
-#[cfg(not(feature = "klee-analysis"))]
-use cortex_m_semihosting::{debug, hprintln};
-
-#[rtfm::app(device = lm3s6965)]
-const APP: () = {
-    #[init]
-    fn init(cx: init::Context) {
-        static mut X: u32 = 0;
-
-        // Safe access to local `static mut` variable
-        let _x: &'static mut u32 = X;
-        if cfg!(feature = "klee-analysis") {
-            fn_to_test();
-        } else {
-            hprintln!("init").unwrap();
-            debug::exit(debug::EXIT_SUCCESS);
-        }
-    }
-};
-
-#[cfg(feature = "klee-analysis")]
-fn fn_to_test() {
-    let mut a = 0;
-    klee_make_symbolic!(&mut a, "a");
-    match a {
-        0 => klee_abort!(),
-        1 => klee_abort!(),
-        2 => panic!(),
-        3 => panic!("3"), // just one instance of panic! will be spotted
-        4 => klee_assert!(false),
-        5 => klee_assert_eq!(false, true),
-        6 => klee_assert_eq!(false, true),
-        _ => (),
-    };
-    panic!("at end"); // just one instane of panic! will be spotted
-}
-
-#[cfg(not(feature = "klee-analysis"))]
-fn fn_to_test() {}
--- a/examples/paths.rs
+++ b/examples/paths.rs
@@ -8,10 +8,10 @@ use panic_klee as _;

 #[no_mangle]
 fn main() {
-    let mut a = 0;
+    let mut a: i32 = 0;
    klee_make_symbolic!(&mut a, "a");
-    // Rust panic on a == 200;
-    let _ = 100 / (a - 200);
+    // Rust panic on a == 200 (div by zero), or a - 200 (causing an arithmetic overflow).
+    let _ = 100 / (a - 200); // let _ = 100 / a.wrapping_sub(200);

    let _ = match a {
        0 => klee_abort!(),
@@ -25,3 +25,89 @@ fn main() {
    };
    panic!("at end"); // just one instane of panic! will be spotted
 }
+
+// KLEE will generate one test per explicit error:
+// namely lines 17,18,19,21,22,23,26.
+//
+// Rust panics are also caught but detected at the `panic-klee` trampoline
+// (and reported just once, either line 14, 20 or 26 we don't know.
+//
+// > cargo klee --example paths
+// ...
+// KLEE: ERROR: examples/paths.rs:22: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/paths.rs:17: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/paths.rs:19: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/paths.rs:21: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/paths.rs:23: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/paths.rs:18: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+//
+// KLEE: done: total instructions = 269
+// KLEE: done: completed paths = 10
+// KLEE: done: generated tests = 7
+//
+// (Notice here the order of generated tests is non-deterministic.)
+//
+// We can inspect the generated tests:
+//
+// > ls target/debug/examples/klee-last/
+// assembly.ll   run.istats            test000001.kquery     test000002.kquery     test000003.kquery     test000004.kquery     test000005.kquery     test000006.kquery     test000007.kquery
+// info          run.stats             test000001.ktest      test000002.ktest      test000003.ktest      test000004.ktest      test000005.ktest      test000006.ktest      test000007.ktest
+// messages.txt  test000001.abort.err  test000002.abort.err  test000003.abort.err  test000004.abort.err  test000005.abort.err  test000006.abort.err  test000007.abort.err  warnings.txt
+//
+// Let's try to find out the path leading up to the panic. In this case the last test.
+//
+// > more target/debug/examples/klee-last/test000007.abort.err
+// Error: abort failure
+// File: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs
+// Line: 8
+// assembly.ll line: 33
+// Stack:
+//         #000000033 in rust_begin_unwind (=94250200401696) at /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8
+//         #100000241 in _ZN4core9panicking9panic_fmt17hdeb7979ab6591473E (=94250202388144, =94250199410592) at src/libcore/panicking.rs:139
+//         #200000275 in _ZN4core9panicking5panic17hb5daa85c7c72fc62E (=94250198589360, =33, =94250199410592) at src/libcore/panicking.rs:70
+//         #300000204 in main () at examples/paths.rs:14
+//
+// We see that it was origin from line 14.
+//
+// We can look at the actual test.
+// > ktest-tool target/debug/examples/klee-last/test000007.ktest
+// ktest file : 'target/debug/examples/klee-last/test000007.ktest'
+// args       : ['/home/pln/rust/trustit/klee-examples/target/debug/examples/paths-cb1d2fb40e2b17af.ll']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x80'
+// object 0: hex : 0x00000080
+// object 0: int : -2147483648
+// object 0: uint: 2147483648
+// object 0: text: ....
+//
+// In this case the problem was the arithmetic overflow.
+// Change line 14 to
+// let _ = 100 / a.wrapping_sub(200);
+//
+// Now re-run KLEE.
+//
+// > ktest-tool target/debug/examples/klee-last/test000007.ktest
+// ktest file : 'target/debug/examples/klee-last/test000007.ktest'
+// args       : ['/home/pln/rust/trustit/klee-examples/target/debug/examples/paths-cb1d2fb40e2b17af.ll']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\xc8\x00\x00\x00'
+// object 0: hex : 0xc8000000
+// object 0: int : 200
+// object 0: uint: 200
+// object 0: text: ....
+//
+// In this case we see that the panic was triggered by the division by zero.
+//
+//
--- a/examples/rtfm_init.rs
+++ b/examples/rtfm_init.rs
--- a/memory.x
+++ b/memory.x
+MEMORY
+{
+  /* NOTE 1 K = 1 KiBi = 1024 bytes */
+  /* TODO Adjust these memory regions to match your device memory layout */
+  /* These values correspond to the LM3S6965, one of the few devices QEMU can emulate */
+  FLASH : ORIGIN = 0x08000000, LENGTH = 256K
+  RAM : ORIGIN = 0x20000000, LENGTH = 64K
+}
+
+/* This is where the call stack will be allocated. */
+/* The stack is of the full descending type. */
+/* You may want to use this variable to locate the call stack and static
+   variables in different memory regions. Below is shown the default value */
+/* _stack_start = ORIGIN(RAM) + LENGTH(RAM); */
+
+/* You can use this symbol to customize the location of the .text section */
+/* If omitted the .text section will be placed right after the .vector_table
+   section */
+/* This is required only on microcontrollers that store some configuration right
+   after the vector table */
+/* _stext = ORIGIN(FLASH) + 0x400; */
+
+/* Example of putting non-initialized variables into custom RAM locations. */
+/* This assumes you have defined a region RAM2 above, and in the Rust
+   sources added the attribute `#[link_section = ".ram2bss"]` to the data
+   you want to place there. */
+/* Note that the section will not be zero-initialized by the runtime! */
+/* SECTIONS {
+     .ram2bss (NOLOAD) : ALIGN(4) {
+       *(.ram2bss);
+       . = ALIGN(4);
+     } > RAM2
+   } INSERT AFTER .bss;
+*/
\ No newline at end of file
--- a/openocd.cfg
+++ b/openocd.cfg
+# Sample OpenOCD configuration for the STM32F3DISCOVERY development board
+
+# Depending on the hardware revision you got you'll have to pick ONE of these
+# interfaces. At any time only one interface should be commented out.
+
+# Revision C (newer revision)
+source [find interface/stlink-v2-1.cfg]
+
+# Revision A and B (older revisions)
+# source [find interface/stlink-v2.cfg]
+
+# for recent openocd you may use
+# source [find interface/stlink.cfg]
+
+source [find target/stm32f4x.cfg]
\ No newline at end of file
--- a/openocd.gdb
+++ b/openocd.gdb
+target extended-remote :3333
+
+# print demangled symbols
+set print asm-demangle on
+
+# set backtrace limit to not have infinite backtrace loops
+set backtrace limit 32
+
+# detect unhandled exceptions, hard faults and panics
+break DefaultHandler
+break HardFault
+break rust_begin_unwind
+# # run the next few lines so the panic message is printed immediately
+# # the number needs to be adjusted for your panic handler
+# commands $bpnum
+# next 4
+# end
+
+# *try* to stop at the user entry point (it might be gone due to inlining)
+break main
+
+monitor arm semihosting enable
+
+# # send captured ITM to the file itm.fifo
+# # (the microcontroller SWO pin must be connected to the programmer SWO pin)
+# # 8000000 must match the core clock frequency
+# monitor tpiu config internal itm.txt uart off 8000000
+
+# # OR: make the microcontroller SWO pin output compatible with UART (8N1)
+# # 8000000 must match the core clock frequency
+# # 2000000 is the frequency of the SWO pin
+# monitor tpiu config external uart off 8000000 2000000
+
+# # enable ITM port 0
+# monitor itm port 0 on
+
+load
+
+# start the process but immediately halt the processor
+stepi
\ No newline at end of file