update to latest KLEE and llvm 12

.vscode/settings.json

 {
     "cSpell.ignoreWords": [
+        "Runtest",
         "deps",
         "is",
+        "istats",
         "ktest",
         "libc",
         "llvm",
+        "muloti",
+        "rtlib",
         "rustc"
     ]
 }
\ No newline at end of file

README.md

@@ -2,18 +2,18 @@
 
 KLEE is a symbolic execution engine, based on the LLVM compiler infrastructure. KLEE generates test cases aiming to cover (all) reachable paths of the input program. KLEE infers further checks for common program errors, e.g., out of bounds indexing and division by zero.
 
-Rust as being designed for safety, catches such errors and panics in precence of such faults. For analysis, a Rust `panic` implies an `abort`, which is detected as an error by KLEE, thus our `klee` tool spots potential `panic`ing behavior of the application at hand.
+Rust as being designed for safety, catches such errors and panics in presence of such faults. For analysis, a Rust `panic` implies an `abort`, which is detected as an error by KLEE, thus our `klee` tool spots potential `panic`ing behavior of the application at hand.
 
-In effect, a Rust program passing KLEE analysis is thus ensured to be panic free at run-time, and thus the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code), without jeopardizing memory safety and robustness for programs. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficient to re-run KLEE if the source program is changed. In the general case of adopting unchecked operations safety can be ensured by adding assertions to the source. If those assertions are conditionally compiled (e.g. under a `klee-analysis` feature) the assertions (and their implied overhead) will be omitted in a production build.
+In effect, a Rust program passing KLEE analysis is thus ensured to be panic free at run-time. That granted, the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code) without jeopardizing memory safety and robustness for the application at hand. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficient to re-run KLEE if the source program is changed. In the general case of adopting unchecked operations safety can be ensured by adding corresponding assertions to the source code. If those assertions are conditionally compiled (e.g. under a `klee-analysis` feature) the assertions (and their implied overhead) will be omitted in a production build.
 
 ## Requirements
 
-- LLVM KLEE installed from recent package
-- LLVM llc and clang for building replay binaries
+- LLVM KLEE installed, (version 2.3pre, currently based on LLVM-v12).
+- LLVM llc and clang for building replay binaries (currently based on LLVM-v12).
 - GNU gdb for executing replay binaries
-- Rust tool-chain (edition-2018), tested with rustc 1.48.0 (7eac88abb 2020-11-16).
+- Rust tool-chain (edition-2018), tested with stable `rustc 1.56.1 (59eed8a2a 2021-11-01)`.
   
-The `klee` tools (executables) needs to be installed and accessible in path, the `klee` libraries are assumed to be accessible under `/usr/lib`. The tool has been tested on the master branch of [KLEE](https://github.com/klee/klee) 2.2 as of 2020-12-08, built under arch linux with the system LLVM (v11).
+The `klee` tools (executables) needs to be installed and accessible in path, the KLEE libraries are assumed to be accessible under `/usr/lib`. The tool has been tested on the master branch of [KLEE](https://github.com/klee/klee) 2.3pre as of 2021-11-04, built under arch linux with the system LLVM (v12). You may use a custom install of KLEE, set the `LD_LIBRARY_PATH` to include the location of `kleeRuntest.so.1.0` (used by cargo-klee to dynamically link the library for replay of tests in gdb).
 
 ## Limitations
 
@@ -62,6 +62,12 @@ KLEE: done: generated tests = 3
 
 You may analyse code using either `--bin` or `--examples`.
 
+## Caveats
+
+LLVM and `rustc` are both moving targets, and incompatibilities between versions of KLEE, LLVM and `rustc` may occur, and thus the tooling is somewhat fragile. The current release (0.4) has been tested on arch linux as of 2021-11-02 with the latest packages of `clang` and `llvm`. KLEE has been built from source to match the LLVM-12.
+
+Cargo-klee compiles binaries without dependency to the Rust std library with the focus to verification of embedded applications.
+
 ## License
 
 All rights reserved, use restricted for non-commercial purpose

cargo-klee/Cargo.toml

 [package]
 authors = ["Lulea University of Technology (LTU)"]
 name = "cargo-klee"
-version = "0.3.0"
+version = "0.4.0"
 edition = "2018"
 
 [dependencies]

cargo-klee/src/main.rs

@@ -124,7 +124,7 @@ fn run() -> Result<i32, failure::Error> {
         // verbose output for debugging purposes
         .arg("-v");
 
-    // set features, always inclidung `klee-analysis`
+    // set features, always including `klee-analysis`
     if matches.is_present("all-features") {
         cargo.arg("--all-features");
     } else {
@@ -260,6 +260,7 @@ fn run() -> Result<i32, failure::Error> {
 
             clang
                 .arg(obj)
+                .arg("--rtlib=compiler-rt")
                 .arg("-lkleeRuntest")
                 .args(&["-o", replay_name.to_str().unwrap()]);
 
@@ -278,7 +279,8 @@ fn run() -> Result<i32, failure::Error> {
     // klee analysis
     if is_ktest || !is_replay {
         let mut klee = Command::new("klee");
-        klee
+        // --disable-very to suppress know issue in klee https://github.com/klee/klee/issues/937
+        klee.arg("--disable-verify")
             // ll file to analyse
             .arg(ll.unwrap());
 

klee-examples/examples/get_sign.rs

@@ -37,7 +37,7 @@ fn main() {
 //
 // KLEE: Using Z3 solver backend
 //
-// KLEE: done: total instructions = 92
+// KLEE: done: total instructions = 89
 // KLEE: done: completed paths = 3
 // KLEE: done: generated tests = 3
 //
@@ -49,7 +49,7 @@ fn main() {
 //
 // > ktest-tool target/debug/examples/klee-last/test000001.ktest
 // ktest file : 'target/debug/examples/klee-last/test000001.ktest'
-// args       : ['/home/pln/courses/d7020e/cargo-klee/klee-examples/target/debug/examples/get_sign-672cfed85f9cca07.ll']
+// args       : ['.../target/debug/examples/get_sign-<SOME_HASH>.ll']
 // num objects: 1
 // object 0: name: 'a'
 // object 0: size: 4
@@ -59,6 +59,8 @@ fn main() {
 // object 0: uint: 2147483648
 // object 0: text: ....
 //
+// (The order of test cases is non-deterministic, so your output might be different.)
+//
 // To replay test cases in `gdb`.
 //
 // > cargo klee --replay --gdb --example get_sign
@@ -80,3 +82,17 @@ fn main() {
 //
 // For convenience the current working directory is set by default to coincide
 // with the generated binary and KLEE tests.
+//
+// Problem shooting!!!
+//
+// For replay, the `kleeRuntest.so.1.0` library is dynamically linked.
+// If not present in the default path you need to set `LD_LIBRARY_PATH` to include
+// the location of this library.
+//
+// An error might look like this:
+//
+// (gdb) r
+// Starting program: ...cargo-klee/klee-examples/target/debug/examples/get_sign.replay:
+// error while loading shared libraries: libkleeRuntest.so.1.0:
+// cannot open shared object file: No such file or directory
+//