From c4e10e680f8249fff410b147416eaf648d17543b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Fri, 17 Jan 2025 11:37:36 +0000 Subject: [PATCH 01/12] added goto-transcoder flow fixes on action script removed checkout subfolder fixed typo --- .github/workflows/goto-transcoder.yml | 37 ++++++++++++++++++++ scripts/run-goto-transcoder.sh | 49 +++++++++++++++++++++++++++ 2 files changed, 86 insertions(+) create mode 100644 .github/workflows/goto-transcoder.yml create mode 100755 scripts/run-goto-transcoder.sh diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml new file mode 100644 index 0000000000000..b414e96b8c500 --- /dev/null +++ b/.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 + + # Step 3: Run goto-transcoder + - name: Run goto-transcoder + run: ./scripts/run-goto-transcoder diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh new file mode 100755 index 0000000000000..4758325bff1db --- /dev/null +++ b/scripts/run-goto-transcoder.sh @@ -0,0 +1,49 @@ +#!/bin/bash + +set -e + +############## +# PARAMETERS # +############## +contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps +supported_regex=checked_unchecked.*.out +unsupported_regex=neg + +goto_transcoder_git=https://github.com/rafaelsamenezes/goto-transcoder +esbmc_url=https://github.com/esbmc/esbmc/releases/download/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241/esbmc-linux.zip + +########## +# SCRIPT # +########## + +echo "Checking contracts with goto-transcoder" + +if [ ! -d "goto-transcoder" ]; then + echo "goto-transcoder not found. Downloading..." + git clone $goto_transcoder_git + cd goto-transcoder + wget $esbmc_url + unzip esbmc-linux.zip + chmod +x ./linux-release/bin/esbmc + cd .. +fi + +ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-transcoder/_contracts.txt + +cd goto-transcoder +while IFS= read -r line; do + contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'` + echo "Processing: $contract" + if [[ -z "$contract" ]]; then + continue + fi + if echo "$contract" | grep -q "$unsupported_regex"; then + continue + fi + echo "Running: goto-transcoder $contract $contract_folder/$line $contract.esbmc.goto" + cargo run cbmc2esbmc $contract ../$contract_folder/$line $contract.esbmc.goto + ./linux-release/bin/esbmc --binary $contract.esbmc.goto +done < "_contracts.txt" + +rm "_contracts.txt" +cd .. From a0cde2a15c1949ff290463662a94f7e601746518 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Fri, 17 Jan 2025 11:59:53 +0000 Subject: [PATCH 02/12] added missing .sh --- .github/workflows/goto-transcoder.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index b414e96b8c500..3dcba4e7cf58b 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.github/workflows/goto-transcoder.yml @@ -34,4 +34,4 @@ jobs: # Step 3: Run goto-transcoder - name: Run goto-transcoder - run: ./scripts/run-goto-transcoder + run: ./scripts/run-goto-transcoder.sh From 20840c3207dad59e67c32b2157def01a43fc4422 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Fri, 24 Jan 2025 09:36:57 +0000 Subject: [PATCH 03/12] added goto-transcoder to .gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index 5bfc180d4d58e..104a12f318810 100644 --- a/.gitignore +++ b/.gitignore @@ -46,6 +46,9 @@ package-lock.json ## Kani *.out +## GOTO-Transcoder +goto-transcoder + # Added by cargo # From e5732656b0f62dd74c28942b646c874c124edb52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Fri, 24 Jan 2025 09:38:15 +0000 Subject: [PATCH 04/12] run-goto-transcoder.sh now gets the contract as a parameter --- .github/workflows/goto-transcoder.yml | 2 +- scripts/run-goto-transcoder.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index 3dcba4e7cf58b..9f9f8991fce94 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.github/workflows/goto-transcoder.yml @@ -34,4 +34,4 @@ jobs: # Step 3: Run goto-transcoder - name: Run goto-transcoder - run: ./scripts/run-goto-transcoder.sh + run: ./scripts/run-goto-transcoder.sh checked_unchecked.*.out diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index 4758325bff1db..082e331b4b564 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -6,7 +6,7 @@ set -e # PARAMETERS # ############## contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps -supported_regex=checked_unchecked.*.out +supported_regex=$1 unsupported_regex=neg goto_transcoder_git=https://github.com/rafaelsamenezes/goto-transcoder From 8cd0743c3b421dcd7a12c0d653ca7b3c5663e34b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Fri, 24 Jan 2025 09:45:29 +0000 Subject: [PATCH 05/12] added comment for run-goto-transcoder.sh --- scripts/run-goto-transcoder.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index 082e331b4b564..a86d60a6482bc 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -32,6 +32,9 @@ ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-tra cd goto-transcoder while IFS= read -r line; do + # I expect each line to be similar to 'core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out' + # The entrypoint of the contract would be _RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8 + # So we use awk to extract this name. contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'` echo "Processing: $contract" if [[ -z "$contract" ]]; then From a5fce7396f338215ea0cfc3e84403d3e8c52385e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Fri, 24 Jan 2025 10:14:44 +0000 Subject: [PATCH 06/12] added goto-transcoder entry to book --- doc/src/tools.md | 1 + rust-toolchain.toml | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/src/tools.md b/doc/src/tools.md index 0eaba7c40d4d8..cb5ebababb1ee 100644 --- a/doc/src/tools.md +++ b/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) | diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 00f10cd5d5c3a..138554ef598fe 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,4 +1,4 @@ -# This version should be updated whenever we update the version of the Rust +f# This version should be updated whenever we update the version of the Rust # standard library we currently track. [toolchain] From ee45c1c441001647db40b17c3af8be4bbc18aa60 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Mon, 27 Jan 2025 17:20:50 +0000 Subject: [PATCH 07/12] removed spurious change --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 138554ef598fe..00f10cd5d5c3a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,4 +1,4 @@ -f# This version should be updated whenever we update the version of the Rust +# This version should be updated whenever we update the version of the Rust # standard library we currently track. [toolchain] From a2c732292f569833ca3e1435aa1564667e2f6730 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Mon, 27 Jan 2025 17:23:18 +0000 Subject: [PATCH 08/12] added --target-dir to kani output --- .github/workflows/goto-transcoder.yml | 8 ++++++-- scripts/run-goto-transcoder.sh | 4 ++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index 9f9f8991fce94..8c560f1c8d5fc 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.github/workflows/goto-transcoder.yml @@ -30,8 +30,12 @@ jobs: # Step 2: Generate contracts programs - name: Generate contracts - run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen + run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir contracts + + # Debug: Check contracts + - name: List contracts found + run: ls contracts # Step 3: Run goto-transcoder - name: Run goto-transcoder - run: ./scripts/run-goto-transcoder.sh checked_unchecked.*.out + run: ./scripts/run-goto-transcoder.sh contracts checked_unchecked.*.out diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index a86d60a6482bc..1d8a459358be5 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -5,8 +5,8 @@ set -e ############## # PARAMETERS # ############## -contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps -supported_regex=$1 +contract_folder=$1 +supported_regex=$2 unsupported_regex=neg goto_transcoder_git=https://github.com/rafaelsamenezes/goto-transcoder From dc6945cbe7c4a7c1c7005e132695327d11a69deb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Mon, 27 Jan 2025 19:59:31 +0000 Subject: [PATCH 09/12] changed path for contracts --- .github/workflows/goto-transcoder.yml | 6 +++--- scripts/run-goto-transcoder.sh | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index 8c560f1c8d5fc..5723a4d5cc335 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.github/workflows/goto-transcoder.yml @@ -30,12 +30,12 @@ jobs: # Step 2: Generate contracts programs - name: Generate contracts - run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir contracts + run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts # Debug: Check contracts - name: List contracts found - run: ls contracts + run: ls kani/contracts # Step 3: Run goto-transcoder - name: Run goto-transcoder - run: ./scripts/run-goto-transcoder.sh contracts checked_unchecked.*.out + run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index 1d8a459358be5..a29dfbd34b492 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -5,7 +5,7 @@ set -e ############## # PARAMETERS # ############## -contract_folder=$1 +contract_folder=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps supported_regex=$2 unsupported_regex=neg From b454135b5dbf8d6ddb521d9ee9d3460211c18b5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Mon, 27 Jan 2025 20:12:57 +0000 Subject: [PATCH 10/12] update --- .github/workflows/goto-transcoder.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index 5723a4d5cc335..f77e8f7eca9c5 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.github/workflows/goto-transcoder.yml @@ -33,8 +33,10 @@ jobs: run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts # Debug: Check contracts - - name: List contracts found - run: ls kani/contracts + - uses: actions/upload-artifact@v4 + with: + name: contracts + path: kani/contracts # Step 3: Run goto-transcoder - name: Run goto-transcoder From 76a619daa65af8c830b57fc371e57086127709e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Wed, 29 Jan 2025 06:57:02 +0000 Subject: [PATCH 11/12] added goto-transcoder.md --- doc/src/tools/goto-transcoder.md | 85 ++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 doc/src/tools/goto-transcoder.md diff --git a/doc/src/tools/goto-transcoder.md b/doc/src/tools/goto-transcoder.md new file mode 100644 index 0000000000000..7ddfdf59a5d96 --- /dev/null +++ b/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 .out .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. From b9126f2f6c763ba07550e6208e9080e0612b4913 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Wed, 29 Jan 2025 19:46:05 +0000 Subject: [PATCH 12/12] removed debug step from goto-transcoder.yml --- .github/workflows/goto-transcoder.yml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index f77e8f7eca9c5..7272f2d657a0f 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.github/workflows/goto-transcoder.yml @@ -32,12 +32,6 @@ jobs: - name: Generate contracts run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts - # Debug: Check contracts - - uses: actions/upload-artifact@v4 - with: - name: contracts - path: kani/contracts - # Step 3: Run goto-transcoder - name: Run goto-transcoder run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out