From 435742aead915b9f8b5d3aa24ab461ecfaf023cf Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Thu, 9 Jan 2020 00:09:31 +0100
Subject: [PATCH] major update to examples
---
.cargo/config | 28 ++
Cargo.lock | 270 +++++++++++++++++++
Cargo.toml | 39 +--
README.md | 31 ++-
build.rs | 18 ++
examples/assume_assert.rs | 80 ++++++
examples/cortex_m_test1.rs | 108 ++++++++
examples/cortex_m_test2.rs | 27 --
examples/cortex_m_test_nightly.rs | 100 ++++---
examples/f401_minimal.rs | 31 +++
examples/klee_init.rs | 52 ----
examples/paths.rs | 92 ++++++-
examples/{rtfm_init.rs => rtfm_init.rs_todo} | 0
memory.x | 34 +++
openocd.cfg | 15 ++
openocd.gdb | 40 +++
16 files changed, 823 insertions(+), 142 deletions(-)
create mode 100644 .cargo/config
create mode 100644 Cargo.lock
create mode 100644 build.rs
create mode 100644 examples/assume_assert.rs
create mode 100644 examples/cortex_m_test1.rs
delete mode 100644 examples/cortex_m_test2.rs
create mode 100644 examples/f401_minimal.rs
delete mode 100644 examples/klee_init.rs
rename examples/{rtfm_init.rs => rtfm_init.rs_todo} (100%)
create mode 100644 memory.x
create mode 100644 openocd.cfg
create mode 100644 openocd.gdb
diff --git a/.cargo/config b/.cargo/config
new file mode 100644
index 0000000..ceb90b9
--- /dev/null
+++ b/.cargo/config
@@ -0,0 +1,28 @@
+[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
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..7a17f6b
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,270 @@
+# 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"
diff --git a/Cargo.toml b/Cargo.toml
index b39720d..f6ebd3e 100644
--- 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
diff --git a/README.md b/README.md
index 71ed944..8c716c8 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,34 @@
# 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
diff --git a/build.rs b/build.rs
new file mode 100644
index 0000000..98f603e
--- /dev/null
+++ b/build.rs
@@ -0,0 +1,18 @@
+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");
+}
diff --git a/examples/assume_assert.rs b/examples/assume_assert.rs
new file mode 100644
index 0000000..8ad40eb
--- /dev/null
+++ b/examples/assume_assert.rs
@@ -0,0 +1,80 @@
+#![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!!!!
diff --git a/examples/cortex_m_test1.rs b/examples/cortex_m_test1.rs
new file mode 100644
index 0000000..02dcb7d
--- /dev/null
+++ b/examples/cortex_m_test1.rs
@@ -0,0 +1,108 @@
+#![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!
diff --git a/examples/cortex_m_test2.rs b/examples/cortex_m_test2.rs
deleted file mode 100644
index 34bbd97..0000000
--- a/examples/cortex_m_test2.rs
+++ /dev/null
@@ -1,27 +0,0 @@
-#![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 };
-// }
diff --git a/examples/cortex_m_test_nightly.rs b/examples/cortex_m_test_nightly.rs
index c38f294..00dae90 100644
--- a/examples/cortex_m_test_nightly.rs
+++ b/examples/cortex_m_test_nightly.rs
@@ -1,31 +1,57 @@
-// > 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!
diff --git a/examples/f401_minimal.rs b/examples/f401_minimal.rs
new file mode 100644
index 0000000..1d1a734
--- /dev/null
+++ b/examples/f401_minimal.rs
@@ -0,0 +1,31 @@
+// 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
diff --git a/examples/klee_init.rs b/examples/klee_init.rs
deleted file mode 100644
index f9838a5..0000000
--- a/examples/klee_init.rs
+++ /dev/null
@@ -1,52 +0,0 @@
-//! 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() {}
diff --git a/examples/paths.rs b/examples/paths.rs
index d91544d..5ecad1b 100644
--- 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.
+//
+//
diff --git a/examples/rtfm_init.rs b/examples/rtfm_init.rs_todo
similarity index 100%
rename from examples/rtfm_init.rs
rename to examples/rtfm_init.rs_todo
diff --git a/memory.x b/memory.x
new file mode 100644
index 0000000..48c9685
--- /dev/null
+++ b/memory.x
@@ -0,0 +1,34 @@
+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
diff --git a/openocd.cfg b/openocd.cfg
new file mode 100644
index 0000000..35412d0
--- /dev/null
+++ b/openocd.cfg
@@ -0,0 +1,15 @@
+# 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
diff --git a/openocd.gdb b/openocd.gdb
new file mode 100644
index 0000000..f505bdc
--- /dev/null
+++ b/openocd.gdb
@@ -0,0 +1,40 @@
+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
--
GitLab