Use system KLEE,

Remove all references to docker

Cargo.lock

+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
 [[package]]
 name = "aligned"
 version = "0.1.1"
@@ -82,7 +84,7 @@ dependencies = [
 
 [[package]]
 name = "cortex-m-rtfm"
-version = "0.3.1"
+version = "0.3.2"
 dependencies = [
  "cortex-m 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)",
  "cortex-m-rt 0.3.13 (registry+https://github.com/rust-lang/crates.io-index)",

Cargo.toml

@@ -10,7 +10,7 @@ keywords = ["arm", "cortex-m"]
 license = "MIT OR Apache-2.0"
 name = "cortex-m-rtfm"
 repository = "https://github.com/japaric/cortex-m-rtfm"
-version = "0.3.1"
+version = "0.3.2"
 
 [dependencies]
 cortex-m = "0.4.0"

README.md

@@ -14,7 +14,11 @@
 ## Exam
 Details are found in `klee.py`
 
-## Complilation
+## Compilation
+
+Install this version of xargo:
+
+> cargo install xargo --version 0.3.10 --force
 
 Use a Rust toolchain with a llvm4 backend, e.g., nightly-2018-01-10-x86_64-unknown-linux-gnu.
 
@@ -60,10 +64,6 @@ panic = "abort"
 
 ## KLEE Analysis
 
-A docker daemon should be started/enabled.
-
-> systemctl start docker.service # if not already started/enabled
-
 In the current folder:
 
 ```
@@ -95,15 +95,7 @@ xargo build --release --example example_name  --features wcet_bkpt --target thum
 
 ### Running KLEE
 
-
-> docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-
-or 
-> docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-
-This starts a shell in the docker `llvm-klee-4`, with a shared mount to the examples directory, where your `panic1-xxxx.bc` is located.
-
-From there you can run various commands like:
+A native installation of KLEE required
 
 > klee panic1-xxxxx.bc
 

examples/panic1.rs

@@ -69,14 +69,8 @@ fn idle() -> ! {
 //
 // 2) As LLVM runs on our host we generate the `.bc` with x86 as target
 //
-// Start a docker with pre-installed KLEE tools
 //
-// 3>  docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-//
-// 3) This will start the docker with the right privileges and mount the directory
-//    where the example `.bc` file(s) are stored (shared/overlaid with the host file system).
-//
-// You can now let KLEE run on the `.bc` file.
+// 3) You can now let KLEE run on the `.bc` file.
 //
 // 4> klee panic1*.bc
 // ...

examples/resource.rs

@@ -103,13 +103,11 @@ fn idle() -> ! {
 // Build the application for KLEE analysis.
 // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
 //
-// Start the KLEE docker
-// > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
 //
 // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
-// of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+// of the generated LLVM IR code.
 //
-// Now run KLEE in the docker.
+// Now run KLEE
 // > klee resource-*.bc
 // KLEE: WARNING: executable has module level assembly (ignoring)
 // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -493,10 +491,7 @@ fn idle() -> ! {
 // Now lets have a look at using optimized LLVM and how it affects the number of tests.
 // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
 //
-// and now start a docker for the optimized build
-// > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-//
-// and in the docker run
+// and run
 // > klee resource*.bc
 //
 // Look at the generated tests.

expand_nop

@@ -65,13 +65,10 @@ unsafe impl rtfm::Resource for EXTI1::Y {
         // Build the application for KLEE analysis.
         // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // Start the KLEE docker
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
         // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
-        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        // of the generated LLVM IR code.
         //
-        // Now run KLEE in the docker.
+        // Now run KLEE.
         // > klee resource-*.bc
         // KLEE: WARNING: executable has module level assembly (ignoring)
         // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -455,10 +452,7 @@ unsafe impl rtfm::Resource for EXTI1::Y {
         // Now lets have a look at using optimized LLVM and how it affects the number of tests.
         // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // and now start a docker for the optimized build
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
-        // and in the docker run
+        // and run
         // > klee resource*.bc
         //
         // Look at the generated tests.

expand_nop.rs

@@ -65,13 +65,10 @@ unsafe impl rtfm::Resource for EXTI1::Y {
         // Build the application for KLEE analysis.
         // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // Start the KLEE docker
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
         // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
-        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        // of the generated LLVM IR code.
         //
-        // Now run KLEE in the docker.
+        // Now run KLEE.
         // > klee resource-*.bc
         // KLEE: WARNING: executable has module level assembly (ignoring)
         // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -455,10 +452,7 @@ unsafe impl rtfm::Resource for EXTI1::Y {
         // Now lets have a look at using optimized LLVM and how it affects the number of tests.
         // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // and now start a docker for the optimized build
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
-        // and in the docker run
+        // and run
         // > klee resource*.bc
         //
         // Look at the generated tests.

expand_wcet.rs

@@ -65,13 +65,10 @@ unsafe impl rtfm::Resource for EXTI2::Y {
         // Build the application for KLEE analysis.
         // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // Start the KLEE docker
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
         // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
-        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        // of the generated LLVM IR code.
         //
-        // Now run KLEE in the docker.
+        // Now run KLEE.
         // > klee resource-*.bc
         // KLEE: WARNING: executable has module level assembly (ignoring)
         // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -455,10 +452,7 @@ unsafe impl rtfm::Resource for EXTI2::Y {
         // Now lets have a look at using optimized LLVM and how it affects the number of tests.
         // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // and now start a docker for the optimized build
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
-        // and in the docker run
+        // and run
         // > klee resource*.bc
         //
         // Look at the generated tests.

expand_wcet_bkpt.rs

@@ -75,13 +75,10 @@ unsafe impl rtfm::Resource for EXTI2::Y {
         // Build the application for KLEE analysis.
         // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // Start the KLEE docker
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
         // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
-        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        // of the generated LLVM IR code.
         //
-        // Now run KLEE in the docker.
+        // Now run KLEE
         // > klee resource-*.bc
         // KLEE: WARNING: executable has module level assembly (ignoring)
         // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -465,10 +462,7 @@ unsafe impl rtfm::Resource for EXTI2::Y {
         // Now lets have a look at using optimized LLVM and how it affects the number of tests.
         // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
         //
-        // and now start a docker for the optimized build
-        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
-        //
-        // and in the docker run
+        // and run
         // > klee resource*.bc
         //
         // Look at the generated tests.

klee_stm_gdb.1.py

@@ -390,9 +390,6 @@ def ktest_iterate():
         print(rustoutputfolder + "not found. Need to run\n")
         print("xargo build --example " + example_name + " --features" +
               "klee_mode --target x86_64-unknown-linux-gnu ")
-        print("\nand docker run --rm --user (id -u):(id -g)" +
-              "-v $PWD" + "/" + klee_out_folder + ":/mnt" +
-              "-w /mnt -it afoht/llvm-klee-4 /bin/bash ")
         if autobuild:
             xargo_run("klee")
             klee_run()
@@ -494,13 +491,8 @@ def klee_run():
         print(PWD + "/" + klee_out_folder)
         print(bc_file)
 
-    klee_cmd = ("docker run --rm --user " +
-                user_id[:-1] + ":" + group_id[:-1] +
-                " -v '"
-                + PWD + "/"
-                + klee_out_folder + "':'/mnt'" +
-                " -w /mnt -it afoht/llvm-klee-4 " +
-                "/bin/bash -c 'klee %s'" % bc_file)
+    klee_cmd = ("klee %s" % bc_file)
+
     if debug:
         print(klee_cmd)
     call(klee_cmd, shell=True)