diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..98e5fcf315729b070be65d7d1618df603ef4d91f
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+target
+**/*.rs.bk
+Cargo.lock
diff --git a/.vscode/settings.json b/.vscode/settings.json
index 7f80cba6a616ba006b21d3fc624534a77fd98f69..8ce88ac07d36756f6dcf7950398ce2f3db7528bb 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,13 +1,18 @@
{
"cSpell.ignoreWords": [
+ "cmake",
"core",
"cstr",
"datatypes",
"ktest",
"libklee",
+ "libz",
"llvm",
+ "mkdir",
"runtest",
"rustc",
- "satisfiability"
+ "satisfiability",
+ "skylake",
+ "znver"
]
}
\ No newline at end of file
diff --git a/README.md b/README.md
index c23c8c423b5b1a415bffc618d0791ed564f2f0b6..e7b7a9809f0049249aa17b50dab0d8a40a97259d 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,10 @@
# KLEE tutorial
-Installing and testing klee.
+- Installing and testing klee.
+
+- Manual use of the KLEE tools for C and Rust programs.
+
+- Simplified usage adopting `klee-sys` and `cargo klee`.
## Dependencies
@@ -28,7 +32,6 @@ Under arch with `yay` installed simply:
> sudo apt install z3 libz3-4 libz3-cil libz3-dev libz3-java libz3-jni libz3-ocaml-de
-
## Install KLEE from source
The instructions recommend LLVM 9, but the current master (2.2-pre) supports LLVM 11 (which is what you would have under arch as of 2020-12-07).
@@ -107,8 +110,24 @@ Here you learn:
---
+## klee-sys and Cargo-klee
+
+See the `cargo-klee-examples` folder.
+
+Here you learn:
+
+- an easy way to compile and run KLEE on Rust code
+- an easy way to replay test cases for Rust programs
+
+TODO:
+
+More interesting verification problems using `cargo klee`.
+
+--
+
+
## Why KLEE on Rust
Out the box, Rust provides superior memory safety and guarantees to well defined behavior. However there are cases where the Rust compiler (rustc) cannot statically (at compile time) ensure these guarantees. For such cases (e.g., division by zero, slice/array indexing etc.) Rust injects code for run-time verification that emit a `panic!` (with appropriate error message). While still being safe (the code never runs into memory unsafety or undefined behavior) this limits the reliability (availability) of the system (as its very hard to recover from a `panic!`.) In practice, the developer would typically reboot/reset the system (and store some error code/trace for post-mortem analysis).
-With KLEE we can do better! We bind Rust `panic!` to KLEE `abort` (a path termination), and let. For all reachable `panic!`s, KLEE will provide a concrete test, which we can replay and address in our source code. When done, we have a proof of `panic` freedom and thus defined behavior, with huge impact to reliability (and security) of the system at hand.
\ No newline at end of file
+With KLEE we can do better! We bind Rust `panic!` to KLEE `abort` (a path termination), and let. For all reachable `panic!`s, KLEE will provide a concrete test, which we can replay and address in our source code. When done, we have a proof of `panic` freedom and thus defined behavior, with huge impact to reliability (and security) of the system at hand.
diff --git a/cargo_klee_examples/.gitignore b/cargo_klee_examples/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..693699042b1a8ccf697636d3cd34b200f3a8278b
--- /dev/null
+++ b/cargo_klee_examples/.gitignore
@@ -0,0 +1,3 @@
+/target
+**/*.rs.bk
+Cargo.lock
diff --git a/cargo_klee_examples/Cargo.toml b/cargo_klee_examples/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..259380e8da2f3f27f5cdcd16f3befb544cb4398d
--- /dev/null
+++ b/cargo_klee_examples/Cargo.toml
@@ -0,0 +1,30 @@
+[package]
+name = "cargo_klee_examples"
+version = "0.1.0"
+authors = ["pln <Per Lindgren>"]
+edition = "2018"
+
+[dependencies.klee-sys]
+git = "https://gitlab.henriktjader.com/KLEE/klee-sys.git"
+version = "0.2.0"
+
+[dependencies.panic-klee]
+git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
+version = "0.1.0"
+
+
+[profile.dev]
+panic = "abort"
+incremental = false # better optimization
+lto = true # better optimization
+codegen-units = 1 # better optimization
+
+[profile.release]
+panic = "abort"
+debug = true # better debugging
+incremental = false # better optimization
+lto = true # better optimization
+codegen-units = 1 # better optimization
+
+[features]
+klee-analysis = ["klee-sys/klee-analysis"]
diff --git a/cargo_klee_examples/README.md b/cargo_klee_examples/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..1bde70405f82626484533eb75e36b3bebf5b8f4f
--- /dev/null
+++ b/cargo_klee_examples/README.md
@@ -0,0 +1,12 @@
+# Examples on `cargo-klee` usage
+
+## Install
+
+Clone the [cargo-klee](https://gitlab.henriktjader.com/pln/cargo-klee).
+
+Follow install instructions.
+
+## Examples
+
+- `examples/get_sign.rs`, same simple example again but now using the `cargo klee` cargo sub-command. The example also uses `klee-sys` bindings.
+
diff --git a/cargo_klee_examples/examples/get_sign.rs b/cargo_klee_examples/examples/get_sign.rs
new file mode 100644
index 0000000000000000000000000000000000000000..0136817566cb8889edf91cad2deb35087e76ea0b
--- /dev/null
+++ b/cargo_klee_examples/examples/get_sign.rs
@@ -0,0 +1,106 @@
+// get_sign.rs
+// Showcase how we automatically can interface Rust to KLEE
+//
+
+#![no_std]
+#![no_main]
+
+use klee_sys::klee_make_symbolic;
+use panic_klee as _;
+
+fn get_sign(x: i32) -> i32 {
+ if x == 0 {
+ return 0;
+ }
+ if x < 0 {
+ return -1;
+ } else {
+ return 1;
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let mut a: i32 = 0;
+ klee_make_symbolic!(&mut a, "a");
+ get_sign(a);
+}
+
+// A) Compile a Rust program for KLEE analysis.
+//
+// The bindings to klee are abstracted into `klee-sys`.
+// The panic handler into `panic_klee` (essentially KLEE `abort`).
+// The tedious build process into `cargo klee`.
+//
+// > cargo klee -help
+//
+// The default is to generate LLVM-IR run KLEE on the generated LLVM-IR.
+// This enables the `klee-analysis` feature of `klee-sys`.
+//
+// Using the `-v` option we see verbose output.
+//
+// > cargo klee -v --example get_sign
+// "cargo" "rustc" "-v" "--features" "klee-analysis" "--example" "get_sign" "--color=always" "--" "-C" "linker=true" "-C" "lto" "--emit=llvm-ir"
+// ...
+//
+// KLEE: Using Z3 solver backend
+//
+// KLEE: done: total instructions = 92
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+// This should be familiar to the build you did in the previous exercise.
+//
+// Now locate the generated tests. Give the relative path to `klee-last`.
+//
+// [your answer here]
+//
+// B) Replay test cases
+//
+// By giving the `-r` (or `--replay`), you can easily replay the test cases:
+//
+// > cargo klee -v -r -g --example get_sign
+//
+// (gdb) set environment KTEST_FILE=klee-last/test000001.ktest
+// (gdb) break get_sign
+// (gdb) run
+//
+// What path of the program does this path trigger?
+//
+// [your answer here]
+//
+// Just out of curiosity, you may test the other test cases as well...
+//
+// B) UX/IX
+//
+// Compare to the "stock KLEE for C" experience.
+//
+// How does `klee-sys` and `cargo-klee` score on a 0..5 scale?
+//
+// [your answer here]
+//
+// If below 5, what could be done to improve the UX/IX?
+//
+// [your answer here]
+//
+// C) Inner workings.
+//
+// Have a look on the source code of `klee-sys`.
+// You will find that it is very similar to the code you saw in the
+// previous exercise.
+//
+// Try to follow the `klee-analysis` feature.
+// What modules in `klee-sys` does this feature enable?
+//
+// [your answer here]
+//
+// Have a look at the source code of `cargo klee`.
+// (The actual sub-command is in the folder `cargo-klee`.)
+//
+// Try to figure out how the correct `.ll` file is determined.
+// Which one will it pick, and why?
+//
+// [your answer here]
+//
+// Actually this is one of the "bad seeds" in the internal design.
+// Seems there is no "stable" way of controlling/retrieving the "metadata"
+// (i.e., the hashing). Ideas welcome!