From be22f4a184ad65902ee243217443c36e2dc89b3b Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Thu, 2 Jan 2020 19:19:13 +0100
Subject: [PATCH] examples
---
Cargo.lock | 326 -----------------------
Cargo.toml | 8 +-
examples/expand.rs | 51 ----
examples/klee_cortex_m_rt_test3.rs | 97 +++++--
examples/{klee_only_test.rs => paths.rs} | 0
5 files changed, 81 insertions(+), 401 deletions(-)
delete mode 100644 Cargo.lock
delete mode 100644 examples/expand.rs
rename examples/{klee_only_test.rs => paths.rs} (100%)
diff --git a/Cargo.lock b/Cargo.lock
deleted file mode 100644
index 911b013..0000000
--- a/Cargo.lock
+++ /dev/null
@@ -1,326 +0,0 @@
-# This file is automatically @generated by Cargo.
-# It is not intended for manual editing.
-[[package]]
-name = "aligned"
-version = "0.2.0"
-source = "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 = "autocfg"
-version = "0.1.7"
-source = "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 = "byteorder"
-version = "1.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-
-[[package]]
-name = "cortex-m"
-version = "0.6.1"
-dependencies = [
- "aligned 0.2.0 (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"
-dependencies = [
- "cortex-m 0.6.1",
- "cortex-m-rt-macros 0.1.7",
- "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"
-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.12 (registry+https://github.com/rust-lang/crates.io-index)",
-]
-
-[[package]]
-name = "cortex-m-rtfm"
-version = "0.5.1"
-dependencies = [
- "cortex-m 0.6.1",
- "cortex-m-rt 0.6.11",
- "cortex-m-rtfm-macros 0.5.0",
- "heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
- "rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
-]
-
-[[package]]
-name = "cortex-m-rtfm-macros"
-version = "0.5.0"
-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)",
- "rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
- "syn 1.0.12 (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",
-]
-
-[[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 = "hash32"
-version = "0.1.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-dependencies = [
- "byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
-]
-
-[[package]]
-name = "heapless"
-version = "0.5.1"
-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)",
- "generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
- "hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
-]
-
-[[package]]
-name = "indexmap"
-version = "1.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-dependencies = [
- "autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
-]
-
-[[package]]
-name = "klee-examples"
-version = "0.1.0"
-dependencies = [
- "cortex-m 0.6.1",
- "cortex-m-rt 0.6.11",
- "cortex-m-rtfm 0.5.1",
- "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)",
- "vcell 0.1.2",
- "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",
-]
-
-[[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 = "rtfm-core"
-version = "0.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-
-[[package]]
-name = "rtfm-syntax"
-version = "0.4.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-dependencies = [
- "indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
- "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
- "syn 1.0.12 (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 = "syn"
-version = "1.0.12"
-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"
-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",
-]
-
-[metadata]
-"checksum aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "d39da9b88ae1a81c03c9c082b8db83f1d0e93914126041962af61034ab44c4a5"
-"checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
-"checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
-"checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
-"checksum byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a7c3dd8985a7111efc5c80b44e23ecdd8c007de8ade3b96595387e812b957cf5"
-"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 hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "d4041af86e63ac4298ce40e5cca669066e75b6f1aa3390fe2561ffa5e1d9f4cc"
-"checksum heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "f339aa7d51777fc0af6aa7cbeb277dfc6e6c029cbdeda48d0fbb92c2337f0e69"
-"checksum indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "712d7b3ea5827fcb9d4fda14bf4da5f136f0db2ae9c8f4bd4e2d1c6fde4e6db2"
-"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 rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "9ec893edb2aa5b70320b94896ffea22a7ebb1cf3f942bb67cd5b60a865a63493"
-"checksum rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "4455e23c34df3d66454e7e218a4d76a7f83321d04a806be614463341cec4116e"
-"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 syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)" = "ddc157159e2a7df58cd67b1cace10b8ed256a404fb0070593f137d8ba6bef4de"
-"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 volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
diff --git a/Cargo.toml b/Cargo.toml
index 43d6663..ec8aee6 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -37,14 +37,14 @@ optional = true
# #features = ["inline-asm", "klee-analysis"]
[patch.crates-io]
-#vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
-vcell = { path = "../vcell" }
+vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
+#vcell = { path = "../vcell" }
#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git", branch = "trustit" }
#volatile-register = { path = "../volatile-register" }
-#cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
-cortex-m = { path = "../cortex-m" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
+#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" }
diff --git a/examples/expand.rs b/examples/expand.rs
deleted file mode 100644
index c7a40ef..0000000
--- a/examples/expand.rs
+++ /dev/null
@@ -1,51 +0,0 @@
-#![feature(prelude_import)]
-#![no_std]
-#![no_main]
-#[prelude_import]
-use core::prelude::v1::*;
-#[macro_use]
-extern crate core;
-#[macro_use]
-extern crate compiler_builtins;
-
-use cortex_m_rt::{entry, exception, pre_init};
-use panic_klee as _;
-
-use klee_sys::{klee_abort, klee_make_symbolic};
-
-use cortex_m::peripheral::Peripherals;
-
-static mut S: u32 = 100;
-
-#[doc(hidden)]
-#[export_name = "main_klee"]
-pub unsafe extern "C" fn __cortex_m_rt_main_trampoline() {
- __cortex_m_rt_main()
-}
-unsafe fn __cortex_m_rt_main() -> ! {
- let peripherals = Peripherals::take().unwrap();
- let mut dwt = peripherals.DWT;
- let a = dwt.cyccnt.read();
- if a == unsafe { S } {
- ::core::panicking::panic("explicit panic", ::core::intrinsics::caller_location());
- }
- unsafe { ::klee_sys::ll::abort() };
-}
-#[export_name = "__pre_init"]
-pub unsafe fn pre_init() {
- let mut a = 0;
- ::klee_sys::klee_make_symbolic(unsafe { &mut a }, unsafe {
- ::klee_sys::CStr::from_bytes_with_nul_unchecked("a\u{0}".as_bytes())
- });
- if a == 100 {
- unsafe { ::klee_sys::ll::abort() };
- }
-}
-#[doc(hidden)]
-#[export_name = "DefaultHandler"]
-fn __cortex_m_rt_DefaultHandler(_irqn: i16) -> ! {
- if _irqn > 255 {
- unsafe { ::klee_sys::ll::abort() };
- }
- unsafe { ::klee_sys::ll::abort() };
-}
diff --git a/examples/klee_cortex_m_rt_test3.rs b/examples/klee_cortex_m_rt_test3.rs
index 4743c4f..e608e78 100644
--- a/examples/klee_cortex_m_rt_test3.rs
+++ b/examples/klee_cortex_m_rt_test3.rs
@@ -1,7 +1,7 @@
#![no_std]
#![no_main]
-use cortex_m_rt::{entry, exception, pre_init};
+use cortex_m_rt::{entry, exception, pre_init, ExceptionFrame};
use panic_klee as _;
use klee_sys::{klee_abort, klee_make_symbolic};
@@ -12,33 +12,90 @@ static mut S: u32 = 100;
#[entry]
unsafe fn main() -> ! {
- let peripherals = Peripherals::take().unwrap();
- let mut dwt = peripherals.DWT;
- let a = dwt.cyccnt.read();
- if a == unsafe { S } {
- panic!();
- }
+ // let peripherals = Peripherals::take().unwrap();
+ // let mut dwt = peripherals.DWT;
+ // let a = dwt.cyccnt.read();
+ // if a == unsafe { S } {
+ // panic!();
+ // }
klee_abort!();
}
#[pre_init]
unsafe fn pre_init() {
- let mut a = 0;
- klee_make_symbolic!(&mut a, "a");
- if a == 100 {
- klee_abort!();
- }
+ // let mut a = 0;
+ // klee_make_symbolic!(&mut a, "a");
+ // if a == 100 {
+ // klee_abort!();
+ // }
}
#[exception]
fn DefaultHandler(irqn: i16) -> ! {
- static mut X: i16 = 0;
- if irqn > 255 {
- unsafe { core::ptr::write_volatile(&mut X, irqn) };
- klee_abort!();
- } else {
- unsafe { core::ptr::write_volatile(&mut X, 0) };
- klee_abort!();
- }
+ // static mut X: i16 = 0;
+ // if irqn > 255 {
+ // unsafe { core::ptr::write_volatile(&mut X, irqn) };
+ // klee_abort!();
+ // } else {
+ // unsafe { core::ptr::write_volatile(&mut X, 0) };
+ // klee_abort!();
+ // }
+ klee_abort!();
+}
+
+#[exception]
+fn NonMaskableInt() -> ! {
+ klee_abort!();
+}
+
+#[exception]
+fn HardFault(eh: &ExceptionFrame) -> ! {
+ // match eh.xpsr {
+ // 0 => klee_abort!(),
+ // 1 => klee_abort!(),
+ // 2 => klee_abort!(),
+ // _ => (),
+ // }
+ klee_abort!();
+}
+
+#[exception]
+fn MemoryManagement() {
+ // klee_abort!();
+}
+
+#[exception]
+fn BusFault() {
+ //klee_abort!();
+}
+
+#[exception]
+fn UsageFault() {
+ //klee_abort!();
+}
+
+#[exception]
+fn SecureFault() {
+ //klee_abort!();
+}
+
+#[exception]
+fn SVCall() {
+ //klee_abort!();
+}
+
+#[exception]
+fn DebugMonitor() {
+ //klee_abort!();
+}
+
+#[exception]
+fn PendSV() {
+ //klee_abort!();
+}
+
+#[exception]
+fn SysTick() {
+ //klee_abort!();
}
diff --git a/examples/klee_only_test.rs b/examples/paths.rs
similarity index 100%
rename from examples/klee_only_test.rs
rename to examples/paths.rs
--
GitLab