Merge branch 'main' into automate-subtree-update

Author: tautschnig

.github/workflows/goto-transcoder.yml

@@ -0,0 +1,37 @@
+# This workflow executes the supported contracts in goto-transcoder
+
+name: Run GOTO Transcoder (ESBMC)
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/goto-transcoder.yml'
+      - 'scripts/run-kani.sh'
+      - 'scripts/run-goto-transcoder.sh'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  verify-rust-std:
+    name: Verify contracts with goto-transcoder
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Generate contracts programs
+      - name: Generate contracts
+        run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts
+
+      # Step 3: Run goto-transcoder
+      - name: Run goto-transcoder
+        run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out

.gitignore

@@ -48,6 +48,8 @@ package-lock.json
 ## Kani
 *.out
 
+## GOTO-Transcoder
+goto-transcoder
 # Added by cargo
 #
 # already existing elements were commented out

doc/src/SUMMARY.md

@@ -8,6 +8,7 @@
 
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
+  - [GOTO Transcoder](./tools/goto-transcoder.md)
 
 ---
 
@@ -26,4 +27,4 @@
   - [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
   - [13: Safety of `CStr`](./challenges/0013-cstr.md)
   - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md)
-  - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0014-intrinsics-simd.md)
+  - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)

doc/src/challenges/0015-intrinsics-simd.md

@@ -1,4 +1,4 @@
-# Challenge 14: Contracts and Tests for SIMD Intrinsics
+# Challenge 15: Contracts and Tests for SIMD Intrinsics
 
 - **Status:** Open
 - **Reward:** 

doc/src/tools.md

@@ -12,6 +12,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 | Tool                | CI Status |
 |---------------------|-------|
  | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
+ | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml)      |
 
 
 

doc/src/tools/goto-transcoder.md

@@ -0,0 +1,85 @@
+# GOTO-Transcoder (ESBMC)
+
+The [goto-transcoder](https://github.com/rafaelsamenezes/goto-transcoder) is an initiative to add a compatibility layer between GOTO programs generated from CPROVER tools (e.g., CBMC and goto-instrument). Specifically, it adds a compatibility layer between Kani and [ESBMC](https://github.com/esbmc/esbmc). ESBMC has a few differences to CBMC, including:
+- CBMC focuses on SAT-based encodings of unrolled programs, while ESBMC targets SMT-based encodings. The SMT support of ESBMC includes sending the full formula or using incremental-SMT.
+- CBMC's concurrency support is an entirely symbolic encoding of a concurrent program in one SAT formula, while ESBMC explores each interleaving individually using context-bounded verification.
+- ESBMC implements incremental-BMC and k-induction strategies.
+
+
+To install the tool, you may just download the source code and build it with `cargo build`. 
+For ESBMC, we recommend using [this release](https://github.com/esbmc/esbmc/releases/tag/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241).
+
+Additionally, we also depend on Kani to generate the GOTO files. You can find more information about how to install in [the installation section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
+
+# Steps to Use the Tool
+
+For these steps let's verify a Rust hello world, we will assume that you have Kani available in your system. We will start with
+the Hello World from the [Kani tutorial](https://model-checking.github.io/kani/kani-tutorial.html):
+
+```rust
+// File: test.rs
+#[kani::proof]
+fn main() {
+    assert!(1 == 2);
+}
+```
+
+## Use Kani to generate the CBMC GOTO program
+
+Invoke Kani and ask it to keep the intermediate files: `kani test.rs --keep-temps`. This generates a `.out` file that is in the GBF
+format. We can double-check this by invoking it with CBMC: `cbmc *test4main.out --show-goto-functions`:
+
+```
+[...]
+main /* _RNvCshu9GRFEWjwO_4test4main */
+        // 12 file test.rs line 3 column 10 function main
+        DECL _RNvCshu9GRFEWjwO_4test4main::1::var_0 : struct tag-Unit
+        // 13 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 9 function main
+        DECL _RNvCshu9GRFEWjwO_4test4main::1::var_1 : struct tag-Unit
+        // 14 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 22 function main
+        DECL _RNvCshu9GRFEWjwO_4test4main::1::var_2 : c_bool[8]
+[...]
+```
+
+## Convert the CBMC goto into ESBMC goto
+
+1. Clone goto-transcoder: `git clone https://github.com/rafaelsamenezes/goto-transcoder.git`
+2. Convert to the ESBMC file: `cargo run cbmc2esbmc  <kani-out>.out <entrypoint> <esbmc>.goto`
+
+```
+Running: goto-transcoder file.cbmc.out  _RNvCshu9GRFEWjwO_4test4main file.esbmc.goto
+[2024-10-09T13:07:20Z INFO  gototranscoder] Converting CBMC input into ESBMC
+[2024-10-09T13:07:20Z INFO  gototranscoder] Done
+```
+
+This will generate the `file.esbmc.goto`, which can be used as the ESBMC input.
+
+## Invoke ESBMC
+
+1. Invoke ESBMC with the program: `esbmc --binary file.esbmc.goto`.
+
+```
+Solving with solver Z3 v4.13.0
+Runtime decision procedure: 0.001s
+Building error trace
+
+[Counterexample]
+
+
+State 1 file test.rs line 4 column 5 function main thread 0
+----------------------------------------------------
+Violated property:
+  file test.rs line 4 column 5 function main
+  KANI_CHECK_ID_test.cbacc14fa409fc10::test_0
+  0
+
+
+VERIFICATION FAILED
+```
+
+
+## Using GOTO-Transcoder to verify the Rust Standard Library
+
+1. Follow the same procedure for Kani to add new properties.
+2. Run Kani with the following extra args: `--keep-temps --only-codegen`.
+3. You can then run each contract individually.