Skip to content

Commit 76a619d

Browse files
added goto-transcoder.md
1 parent d3c7c0b commit 76a619d

File tree

1 file changed

+85
-0
lines changed

1 file changed

+85
-0
lines changed

doc/src/tools/goto-transcoder.md

Lines changed: 85 additions & 0 deletions
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.

0 commit comments

Comments
 (0)