From 132b7de731f7aa81340d40798a974889c4dcc289 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 3 Nov 2020 16:54:04 +0100
Subject: [PATCH] 2020 updates, wip
---
.vscode/settings.json | 28 ++++++++++++++++++++++++++++
README.md | 7 +++----
examples/README.md | 14 ++++++++++++++
examples/assume_assert.rs | 6 +++---
examples/register_test.rs | 8 +++++---
5 files changed, 53 insertions(+), 10 deletions(-)
create mode 100644 .vscode/settings.json
create mode 100644 examples/README.md
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..8a9128b
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,28 @@
+{
+ "cSpell.ignoreWords": [
+ "backtrace",
+ "eabihf",
+ "em",
+ "fffffffd",
+ "file",
+ "istats",
+ "ktest",
+ "ktest file",
+ "libc",
+ "libcore",
+ "lldb",
+ "llvm",
+ "maybe",
+ "maybe uninit",
+ "openocd",
+ "satisfiability",
+ "sigabrt",
+ "thumbv",
+ "thumbv em",
+ "trustit",
+ "uninit",
+ "vcell",
+ "x",
+ "x fffffffd"
+ ]
+}
\ No newline at end of file
diff --git a/README.md b/README.md
index 58b6799..e053d2d 100644
--- a/README.md
+++ b/README.md
@@ -6,10 +6,9 @@ See section `Cargo.toml` for detailed information on features introduced.
### General dependencies
-- LLVM toolchain tested with (9.0.1)
-- rustup tested with 1.40.0 (73528e339 2019-12-16)
-- klee tested with KLEE 2.1-pre (https://klee.github.io)
-
+- LLVM toolchain tested with (9.0.1 and 10.0.1)
+- rustup tested with rust toolchain 1.47.0 (18bf6b4f0 2020-10-07) and 1.49.0-nightly (ffa2e7ae8 2020-10-24)
+- klee tested with KLEE 2.1 (https://klee.github.io)
- cargo-klee (installed from git)
---
diff --git a/examples/README.md b/examples/README.md
new file mode 100644
index 0000000..8980c29
--- /dev/null
+++ b/examples/README.md
@@ -0,0 +1,14 @@
+# Examples
+
+## assume_assert
+
+Exercises the ability to introduce assumptions in order to prove assertions.
+
+This leads into possibilities for contracts.
+
+## register_test
+
+Exercises the ability to automatically treat hardware read accesses as streams of unknown values,
+and hardware write accesses as no operations. In this way, we can *pessimistically* analyse low-level
+code such as drivers. More detailed information (assumptions) on the behavior of the hardware can be
+modelled as mocks for the corresponding register blocks.
\ No newline at end of file
diff --git a/examples/assume_assert.rs b/examples/assume_assert.rs
index 788ae13..7a11143 100644
--- a/examples/assume_assert.rs
+++ b/examples/assume_assert.rs
@@ -50,7 +50,7 @@ fn f1(a: u32) -> u32 {
// #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
+// #400000088 in main () at examples/assume_assert.rs:13
//
// So its line 19, (a + 1)
//
@@ -74,7 +74,7 @@ fn f1(a: u32) -> u32 {
// So KLEE tracks the "path condition", i.e., at line 18 it knows (assumes) that that
// a < u32::MAX, and finds that the assumption a == u32::MAX cannot be satisfied.
//
-// This is extremely powerful as KLEE tracks all known "constraints" and all their raliaitons
+// This is extremely powerful as KLEE tracks all known "constraints" and all their relations
// 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!!!!
// This is the way!
@@ -102,7 +102,7 @@ fn f1(a: u32) -> u32 {
// a + 1
// }
//
-// It might even be possible to derive post condtitions from pre conditions,
+// It might even be possible to derive post conditions from pre-conditions,
// and report them to the user. Problem is that the conditions are
// represented as "first order logic" (FOL) constraints, which need to be
// converted into readable form (preferably Rust expressions.)
diff --git a/examples/register_test.rs b/examples/register_test.rs
index e429a75..e9c4041 100644
--- a/examples/register_test.rs
+++ b/examples/register_test.rs
@@ -27,7 +27,7 @@ fn main() {
// embedded Rust ecosystem.
//
// When analyzed by KLEE, we make the return value symbolic, thus each access
-// givs a new unique symbol. Even if we write a value to it, the next read
+// gives a new unique symbol. Even if we write a value to it, the next read
// will still be treated as a new symbol. That might be overly pessimistic
// but is a safe approximation for the worst case behavior of the hardware.
//
@@ -104,7 +104,7 @@ fn main() {
// object 1: uint: 2
// object 1: text: ....
//
-// The first read gives 1, the second 2, and we hit unreacable.
+// The first read gives 1, the second 2, and we hit unreachable.
//
// We can replay the last test to gather more information:
// $ cargo klee --example register_test -r -k -g -v
@@ -136,7 +136,9 @@ fn main() {
// (gdb) print read_2
// $2 = 2
//
-// If this does not work its a gdb problem, try lldb the LLVM debugger
+// If this does not work its a gdb problem, try `lldb` (or `rust-lldb`) the LLVM debugger
// (debug info may not be completely compatible)
//
+// https://lldb.llvm.org/use/map.html
+//
// This is the way!
--
GitLab