Skip to content

Commit 566cd13

Browse files
rafaelsamenezesrafaelsamenezes
authored
Goto-transcoder action (model-checking#236)
Resolves model-checking#108 This PR enables the use of goto-transcoder for the following contracts: ``` core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_mul_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_mul_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shl_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shl_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shr_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shr_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_sub_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_sub_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_mul_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_mul_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_add_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_add_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shl_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shl_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shr_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shr_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_sub_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_sub_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_add_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_add_usize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shl_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shl_usize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shr_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shr_usize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_sub_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_sub_usize.out ``` The version of ESBMC used contains the following solvers: - Boolector (default) - Z3 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 01e4976 commit 566cd13

File tree

5 files changed

+177
-0
lines changed

5 files changed

+177
-0
lines changed

‎.github/workflows/goto-transcoder.yml

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# This workflow executes the supported contracts in goto-transcoder
2+
3+
name: Run GOTO Transcoder (ESBMC)
4+
on:
5+
workflow_dispatch:
6+
merge_group:
7+
pull_request:
8+
branches: [ main ]
9+
push:
10+
paths:
11+
- 'library/**'
12+
- '.github/workflows/goto-transcoder.yml'
13+
- 'scripts/run-kani.sh'
14+
- 'scripts/run-goto-transcoder.sh'
15+
16+
defaults:
17+
run:
18+
shell: bash
19+
20+
jobs:
21+
verify-rust-std:
22+
name: Verify contracts with goto-transcoder
23+
runs-on: ubuntu-latest
24+
steps:
25+
# Step 1: Check out the repository
26+
- name: Checkout Repository
27+
uses: actions/checkout@v4
28+
with:
29+
submodules: true
30+
31+
# Step 2: Generate contracts programs
32+
- name: Generate contracts
33+
run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts
34+
35+
# Step 3: Run goto-transcoder
36+
- name: Run goto-transcoder
37+
run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,8 @@ package-lock.json
4848
## Kani
4949
*.out
5050

51+
## GOTO-Transcoder
52+
goto-transcoder
5153
# Added by cargo
5254
#
5355
# already existing elements were commented out

‎doc/src/tools.md

+1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
1212
| Tool | CI Status |
1313
|---------------------|-------|
1414
| 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) |
15+
| 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) |
1516

1617

1718

‎doc/src/tools/goto-transcoder.md

+85
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
# GOTO-Transcoder (ESBMC)
2+
3+
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:
4+
- 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.
5+
- 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.
6+
- ESBMC implements incremental-BMC and k-induction strategies.
7+
8+
9+
To install the tool, you may just download the source code and build it with `cargo build`.
10+
For ESBMC, we recommend using [this release](https://github.com/esbmc/esbmc/releases/tag/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241).
11+
12+
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).
13+
14+
# Steps to Use the Tool
15+
16+
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
17+
the Hello World from the [Kani tutorial](https://model-checking.github.io/kani/kani-tutorial.html):
18+
19+
```rust
20+
// File: test.rs
21+
#[kani::proof]
22+
fn main() {
23+
assert!(1 == 2);
24+
}
25+
```
26+
27+
## Use Kani to generate the CBMC GOTO program
28+
29+
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
30+
format. We can double-check this by invoking it with CBMC: `cbmc *test4main.out --show-goto-functions`:
31+
32+
```
33+
[...]
34+
main /* _RNvCshu9GRFEWjwO_4test4main */
35+
// 12 file test.rs line 3 column 10 function main
36+
DECL _RNvCshu9GRFEWjwO_4test4main::1::var_0 : struct tag-Unit
37+
// 13 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 9 function main
38+
DECL _RNvCshu9GRFEWjwO_4test4main::1::var_1 : struct tag-Unit
39+
// 14 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 22 function main
40+
DECL _RNvCshu9GRFEWjwO_4test4main::1::var_2 : c_bool[8]
41+
[...]
42+
```
43+
44+
## Convert the CBMC goto into ESBMC goto
45+
46+
1. Clone goto-transcoder: `git clone https://github.com/rafaelsamenezes/goto-transcoder.git`
47+
2. Convert to the ESBMC file: `cargo run cbmc2esbmc <kani-out>.out <entrypoint> <esbmc>.goto`
48+
49+
```
50+
Running: goto-transcoder file.cbmc.out _RNvCshu9GRFEWjwO_4test4main file.esbmc.goto
51+
[2024-10-09T13:07:20Z INFO gototranscoder] Converting CBMC input into ESBMC
52+
[2024-10-09T13:07:20Z INFO gototranscoder] Done
53+
```
54+
55+
This will generate the `file.esbmc.goto`, which can be used as the ESBMC input.
56+
57+
## Invoke ESBMC
58+
59+
1. Invoke ESBMC with the program: `esbmc --binary file.esbmc.goto`.
60+
61+
```
62+
Solving with solver Z3 v4.13.0
63+
Runtime decision procedure: 0.001s
64+
Building error trace
65+
66+
[Counterexample]
67+
68+
69+
State 1 file test.rs line 4 column 5 function main thread 0
70+
----------------------------------------------------
71+
Violated property:
72+
file test.rs line 4 column 5 function main
73+
KANI_CHECK_ID_test.cbacc14fa409fc10::test_0
74+
0
75+
76+
77+
VERIFICATION FAILED
78+
```
79+
80+
81+
## Using GOTO-Transcoder to verify the Rust Standard Library
82+
83+
1. Follow the same procedure for Kani to add new properties.
84+
2. Run Kani with the following extra args: `--keep-temps --only-codegen`.
85+
3. You can then run each contract individually.

‎scripts/run-goto-transcoder.sh

+52
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
##############
6+
# PARAMETERS #
7+
##############
8+
contract_folder=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps
9+
supported_regex=$2
10+
unsupported_regex=neg
11+
12+
goto_transcoder_git=https://github.com/rafaelsamenezes/goto-transcoder
13+
esbmc_url=https://github.com/esbmc/esbmc/releases/download/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241/esbmc-linux.zip
14+
15+
##########
16+
# SCRIPT #
17+
##########
18+
19+
echo "Checking contracts with goto-transcoder"
20+
21+
if [ ! -d "goto-transcoder" ]; then
22+
echo "goto-transcoder not found. Downloading..."
23+
git clone $goto_transcoder_git
24+
cd goto-transcoder
25+
wget $esbmc_url
26+
unzip esbmc-linux.zip
27+
chmod +x ./linux-release/bin/esbmc
28+
cd ..
29+
fi
30+
31+
ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-transcoder/_contracts.txt
32+
33+
cd goto-transcoder
34+
while IFS= read -r line; do
35+
# I expect each line to be similar to 'core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out'
36+
# The entrypoint of the contract would be _RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8
37+
# So we use awk to extract this name.
38+
contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'`
39+
echo "Processing: $contract"
40+
if [[ -z "$contract" ]]; then
41+
continue
42+
fi
43+
if echo "$contract" | grep -q "$unsupported_regex"; then
44+
continue
45+
fi
46+
echo "Running: goto-transcoder $contract $contract_folder/$line $contract.esbmc.goto"
47+
cargo run cbmc2esbmc $contract ../$contract_folder/$line $contract.esbmc.goto
48+
./linux-release/bin/esbmc --binary $contract.esbmc.goto
49+
done < "_contracts.txt"
50+
51+
rm "_contracts.txt"
52+
cd ..

0 commit comments

Comments
 (0)