Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Draft for tool proposal (goto-transcoder) #108

Open
6 tasks done
rafaelsamenezes opened this issue Oct 9, 2024 · 9 comments · May be fixed by #236
Open
6 tasks done

Draft for tool proposal (goto-transcoder) #108

rafaelsamenezes opened this issue Oct 9, 2024 · 9 comments · May be fixed by #236
Assignees
@rafaelsamenezes
Labels
Tool Application Used to tag tool application

Comments

@rafaelsamenezes
Copy link

Dear team, We are opening this issue to obtain feedback on our initial proposal. The tool idea started as a discussion with
@feliperodri at ETAPS and it would be great to see it moving forward.

Tool Name

Goto-transcoder (ESBMC)

Description

The goto-transcoder is an initiative to add a compatibility layer between GOTO programs generated from CPROVER tools (e.g., CBMC and goto-instrument). Specifically, we are interested in adding support to ESBMC. The main difference between ESBMC and CBMC is that ESBMC focuses on SMT and has support for other proof strategies such as incremental bounded model checking. For this proposal, we are concentrating in the conversion between CBMC goto -> ESBMC goto so that we can improve code reuse. Therefore, we can make use of Kani to generate a GOTO program for CBMC which can then be converted into an equivalent ESBMC input.

flowchart LR
    R[Rust source] --> K[Kani]
    K -->|CBMC GBF| G[goto-transcoder]
    G -->|ESBMC GBF| ESBMC
Loading

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.

Tool Information

  • Does the tool perform Rust verification?

Yes, by converting the Kani goto program into an ESBMC-compatible one.

  • Does the tool deal with unsafe Rust code?

Yes. Similarly to CBMC, ESBMC's main use is for the verification of C programs, it has support for checking classical memory properties such as buffer overflow, dangling pointers, and memory leaks.

  • Does the tool run independently in CI?

ESBMC is already integrated into the CI of industrial partners and it is also available in the GitHub actions marketplace for easy use. The transcoder is an independent Rust project that generates a binary that can be easily integrated into CI. We will need to work on the integration of Kani, goto-transcoder and ESBMC into a single CI job.

  • Is the tool open source?

Both ESBMC and goto-transcoder have public development under permissive licenses, i.e., MIT and Apache 2.0.

  • Is the tool under development?

ESBMC is a mature tool with active development, goto-transcoder is still in the initial phase (we have a list of what is currently supported).

  • Will you or your team be able to provide support for the tool?

Yes. ESBMC is a joint project of the Federal University of Amazonas (Brazil), the University of Manchester (UK), the University of Southampton (UK), and the University of Stellenbosch (South Africa).

The ESBMC development was supported by various research funding agencies, including CNPq (Brazil), CAPES (Brazil), FAPEAM (Brazil), EPSRC (UK), Royal Society (UK), British Council (UK), European Commission (Horizon 2020), and companies including ARM, Intel, Motorola Mobility, Nokia Institute of Technology and Samsung. The ESBMC development is currently funded by ARM, EPSRC grants EP/T026995/1 and EP/V000497/1, Ethereum Foundation, EU H2020 ELEGANT 957286, Intel, Motorola Mobility (through Agreement N° 4/2021), Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme, and XC5 Hong Kong Limited.

Licenses

  • goto-transcoder: MIT
  • ESBMC: Apache License 2.0.

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:

// 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 -- --mode 0 --input <kani-out>.out --output file-esbmc.goto
     Running `target/debug/gototranscoder --mode 0 --input main.goto --output 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. Download and install the latest version of ESBMC, at the time of this writing we used 7.7: https://github.com/esbmc/esbmc/releases/tag/v7.7
  2. 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

Artifacts

ESBMC originally came from the idea of using SMT to improve the performance of BMC tools. The original work was awarded at ASE'23 with
the Most Influential Paper award.

Awards

  • 35 awards from international competitions on software verification (SV-COMP) and testing (Test-Comp) 2012-2024 at TACAS/FASE (Strength: Bug Finding and Code Coverage).
  • Most Influential Paper Award at ASE’23
  • Best Tool Paper Award at SBSeg'23
  • Best Paper Award at SBESC’15
  • Distinguished Paper Award at ICSE’11

Links

Documentation

Selected publications

Users

  • ARM
  • Ethereum Foundation
  • Intel

CI & Versioning

ESBMC and goto-transcoder are both developed at GitHub using Git.

For CI pipelines the tools can either be invoked directly or integrated into a custom action. ESBMC already has an action.
@feliperodri feliperodri added the Tool Application Used to tag tool application label Oct 9, 2024
@tautschnig
Copy link
Member

Could you please describe the user-visible differences of goto-transcoder+ESBMC (to Kani, as the presently only tool in CI) that you'd know or expect?

@rafaelsamenezes
Copy link
Author

Could you please describe the user-visible differences of goto-transcoder+ESBMC (to Kani, as the presently only tool in CI) that you'd know or expect?

Could you clarify a bit? If I understood correctly you mean how a user will see the output of the tool:

  1. ESBMC has it own counterexample (as the screenshot above shows) which contains the program trace.
  2. We could also try to integrate goto-transcoder+ESBMC into Kani as a backend.

@tautschnig
Copy link
Member

Could you clarify a bit? If I understood correctly you mean how a user will see the output of the tool:

My apologies for the unclear request. What I am seeking to understand is what advantages (and possibly also: disadvantages) we should expect when using ESBMC. Looking at the idea of integrating goto-transcoder+ESBMC with Kani (the Kani team would very much appreciate a pull request to that effect!), can you describe scenarios where ESBMC would be able to prove properties that Kani with CBMC as back-end currently cannot prove (one idea that comes to my mind is the upcoming support for quantifiers in Kani)? Are there perhaps also situations where ESBMC would not be able to prove a property? Would you expect performance differences?

@rafaelsamenezes
Copy link
Author

Thanks for the clarification.

What I am seeking to understand is the advantages (and possibly also the disadvantages) we should expect when using ESBMC.

  • The main advantage is the support for k-induction, SMT solvers, and concurrency models.
  • The main disadvantage is that ESBMC, as a frontend/tool, is less documented compared to CBMC.

Can you describe scenarios where ESBMC would be able to prove properties that Kani with CBMC as a back-end currently cannot prove?

Regarding performance, quantifiers could indeed be translated directly into SMT formulas. As for concrete examples, I don't have any where k-induction + SMT outperforms BMC + SAT, considering we are still in the early stages.
One way to explore this is to check specific benchmarks at SV-COMP: SV-COMP 2024 results and identify similar C constructs.

Comparing the benchmarks where ESBMC returned a correct verdict and CBMC failed to reach a verdict (ignoring wrong results):

  • 3285 unique in reachability: Of these, 657 were from ECA/Loops (where k-induction excels), 119 were from Combinations/Product Lines (where our recent advances with interval analysis made them trivial), and most of the other benchmarks were related to hardware or floating-point operations.
  • 8 unique in memory safety: 2 were related to pthread, and the others involved loops and termination.

Now considering the cases where both ESBMC and CBMC returned the correct verdict (2207 benchmarks) in reachability:

  • CBMC took 27.8 hours and consumed 791 GB, whereas ESBMC took 20.6 hours and consumed 557 GB.

@tautschnig
Copy link
Member

Thanks @rafaelsamenezes and apologies for the delayed response. Could you please go ahead and create a (draft?) PR that integrates goto-transcoder/ESBMC into CI of this repository? Perhaps start with just one of the harnesses.

@rafaelsamenezes
Copy link
Author

rafaelsamenezes commented Dec 3, 2024 •
edited
Loading

Some updates. I have been focusing in enabling the transcoder to work with a contract, specifically: checked_unchecked_add_i8.

Unchecked add i8 contract

The contract is generated by the following macro:

macro_rules! generate_unchecked_math_harness {
        ($type:ty, $method:ident, $harness_name:ident) => {
            #[kani::proof_for_contract($type::$method)]
            pub fn $harness_name() {
                let num1: $type = kani::any::<$type>();
                let num2: $type = kani::any::<$type>();

                unsafe {
                    num1.$method(num2);
                }
            }
        }
}

generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);

The property here is that unchecked_add on two nondet variables can result in an overflow, which is an UB in Rust. This is asserted in this repo by adding an ensure at the unchecked_add: #[requires(!self.overflowing_add(rhs).1)]

Extracting the GOTO from this repo

To start, I had to somehow obtain the GBF from the contract. So I altered the script from run-kani.sh to keep the temporary folder. On the temporary folder I copied all the .out files from within target/x86_64-unknown-linux-gnu/debug/deps, which are the CBMC GBF files (see my initial post). At the end, the file core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8.out is used.

I expect this to be easier in the future with the merge of #170.

Finding the entry-point

The GBF file does not has a __CPROVER__start, this means that the entry-point must be manually set. However, using --function num::verify::checked_unchecked_add_i8 is not enough. We need the actual id (even in CBMC). Which is extracted by: cbmc ./resources/test/checked_unchecked_add_i8.goto --show-goto-functions | grep num::verify::checked_unchecked_add_i8 which yields _RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8 as the entry-point.

Using ESBMC to check this contract

The transcoder can already parse and convert this contract into ESBMC GBF. When executing with ESBMC we can even add the bounds-checks and pointer-checks if we want. There are some caveats, which I will go through later.

For now, ESBMC generates 20 claims:

Claims

Claim 1:
  file /home/vm/verify-rust-std/library/core/src/num/int_macros.rs line 527 column 17 function num::<impl i8>::unchecked_add::{closure#2}::{closure#0}
  attempt to compute `unchecked_add` which would overflow
  !((signed char)temp_0. != 0)

Claim 2:
  file /home/vm/verify-rust-std/library/core/src/ub_checks.rs line 71 column 21 function num::<impl i8>::unchecked_add::{closure#2}::{closure#0}::precondition_check
  Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md
  0

...

Verification Conditions

Updated:

file /home/vm/verify-rust-std/library/core/src/num/int_macros.rs line 527 column 17 function num::<impl i8>::unchecked_add::{closure#2}::{closure#0}
attempt to compute `unchecked_add` which would overflow
{-1} _RINvNtCsesPP5EAma4_4core4kani16any_raw_internalaEB4_::1::var_0?1!0&0#2 == nondet_symbol(symex::nondet6)
{-2} _RNvXsd_NtCsesPP5EAma4_4core4kaniaNtB5_9Arbitrary3any::1::var_0?1!0&0#2 == _RINvNtCsesPP5EAma4_4core4kani16any_raw_internalaEB4_::1::var_0?1!0&0#2
{-3} _RINvNtCsesPP5EAma4_4core4kani3anyaEB4_::1::var_0?1!0&0#2 == _RNvXsd_NtCsesPP5EAma4_4core4kaniaNtB5_9Arbitrary3any::1::var_0?1!0&0#2
{-4} _RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8::1::var_2::num1?1!0&0#2 == _RINvNtCsesPP5EAma4_4core4kani3anyaEB4_::1::var_0?1!0&0#2
{-5} _RINvNtCsesPP5EAma4_4core4kani16any_raw_internalaEB4_::1::var_0?2!0&0#2 == nondet_symbol(symex::nondet10)
{-6} _RNvXsd_NtCsesPP5EAma4_4core4kaniaNtB5_9Arbitrary3any::1::var_0?2!0&0#2 == _RINvNtCsesPP5EAma4_4core4kani16any_raw_internalaEB4_::1::var_0?2!0&0#2
{-7} _RINvNtCsesPP5EAma4_4core4kani3anyaEB4_::1::var_0?2!0&0#2 == _RNvXsd_NtCsesPP5EAma4_4core4kaniaNtB5_9Arbitrary3any::1::var_0?2!0&0#2
{-8} _RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8::1::var_3::num2?1!0&0#2 == _RINvNtCsesPP5EAma4_4core4kani3anyaEB4_::1::var_0?2!0&0#2
{-9} _RNvMNtCsesPP5EAma4_4core3numa13unchecked_add::1::var_1::self?1!0&0#1 == _RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8::1::var_2::num1?1!0&0#2
{-10} _RNvMNtCsesPP5EAma4_4core3numa13unchecked_add::1::var_2::rhs?1!0&0#1 == _RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8::1::var_3::num2?1!0&0#2
{-11} _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_6?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa13unchecked_add::1::var_1::self?1!0&0#1
{-12} _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_7?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa13unchecked_add::1::var_2::rhs?1!0&0#1
{-13} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_1::self?1!0&0#1 == _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_6?1!0&0#2
{-14} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_2::rhs?1!0&0#1 == _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_7?1!0&0#2
{-15} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::temp_0?1!0&0#2 == { .=_RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_1::self?1!0&0#1 + _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_2::rhs?1!0&0#1, .=overflow("+", _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_1::self?1!0&0#1, _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_2::rhs?1!0&0#1) }
{-16} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::$tmp::tmp_statement_expression?1!0&0#2 == { .=_RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::temp_0?1!0&0#2., .=(signed char)_RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::temp_0?1!0&0#2. }
{-17} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_5?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::$tmp::tmp_statement_expression?1!0&0#2
{-18} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_3::a?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_5?1!0&0#2.
{-19} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_4::b?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_5?1!0&0#2.
{-20} _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_0?1!0&0#2 == { .=_RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_3::a?1!0&0#2, .=_RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_4::b?1!0&0#2 }
{-21} _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_5?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa15overflowing_add::1::var_0?1!0&0#2
{-22} _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_4?1!0&0#2 == _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_5?1!0&0#2.
{-23} _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_3?1!0&0#2 == (signed char)(!(_RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_4?1!0&0#2 != 0))
{-24} _RNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_0B6_::1::var_3?1!0&0#2 != 0
{-25} _RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::var_7?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa13unchecked_add::1::var_1::self?1!0&0#1
{-26} _RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::var_8?1!0&0#2 == _RNvMNtCsesPP5EAma4_4core3numa13unchecked_add::1::var_2::rhs?1!0&0#1
{-27} _RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::temp_0?1!0&0#2 == { .=_RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::var_7?1!0&0#2 + _RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::var_8?1!0&0#2, .=overflow("+", _RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::var_7?1!0&0#2, _RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::var_8?1!0&0#2) }
|--------------------------
{1} execution_statet::\guard_exec?0!0 => !((signed char)_RNCNCNvMNtCsesPP5EAma4_4core3numa13unchecked_adds0_00B8_::1::temp_0?1!0&0#2. != 0)
...

TODOs

Running this contract in ESBMC will give the same result as CBMC, but it is still not fully implemented. There are 3 main todos right now:

  • The overflow check is implemented in a expression: overflow_add-+ which is currently not supported by ESBMC. Since this expression works in a well defined struct, I just returned zero for now. Issue.
  • This contract generates expressions of: object_size. Same as above, returning zero for now. Issue.
  • There is a bug in ESBMC that does not allow redefining the entry-point for a binary. I am setting the entry-point through the transcoder for now. Issue.

Once these issues are solved, goto-transcoder should be able to fully verify this harness.

Also, considering automation. I'd like to know if you have any suggestions for: automatically extract the GBF along their entry-points.

@carolynzech carolynzech mentioned this issue Dec 6, 2024
Open
@rafaelsamenezes
Copy link
Author

More updates. Goto transcoder has its first release: https://github.com/rafaelsamenezes/goto-transcoder/releases/tag/v0.1

This releases allows the verification of the unchecked operators for: add, sub, mul, shr

Plan for CI integration

  1. Run the run-kani.sh but keep the temp files.

  2. List all the contracts that are supported in the folder: ls $KANITMP/target/x86_64-unknown-linux-gnu/debug/deps/ | grep checked_unchecked | grep -v .symtab.out

This results in a list of GOTOs that can be used as input of the transcoder. Right now, it returns:

core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_i8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_add_u8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_mul_i8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_mul_u8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_neg_i8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_shl_i8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_shl_u8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_shr_i8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_shr_u8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_sub_i8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify24checked_unchecked_sub_u8.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_add_i16.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_add_i32.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_add_i64.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_add_u16.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_add_u32.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_add_u64.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_mul_i16.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_mul_u16.out
core-9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify25checked_unchecked_neg_i16.out
...
  1. Out of these, we currently filter out the checked_unchecked_shl and checked_unchecked_neg.
  2. The name of the entry point is part of the contract. For example: 9f0576398841789a__RNvNtNtCsesPP5EAma4_4core3num6verify27checked_unchecked_shl_usize.out uses _RNvNtNtCsesPP5EAma4_4core3num6verify27checked_unchecked_shl_usize as the entrypoint.
  3. We invoke gototranscoder cbmc2esbmc $entrypoint $contract $contract.esbmc.goto
  4. Invoke ESBMC with: esbmc --binary $contract.esbmc.goto

@celinval
Copy link

Hi @rafaelsamenezes, can you please go ahead and create a PR with the CI integration? I would also highly encourage you to add a script similar to run-kani.sh which will run the end-to-end flow with the goto-transcoder. This will allow contributors to experiment with goto-transcoder, and to verify new harnesses or debug any CI failure.

BTW, I would also recommend passing --only-codegen to Kani, so it doesn't unnecessarily run the verification stage. Note that the --only-cogen argument will not invoke goto-instrument, and you might have to do that explicitly if you want to apply any extra instrumentation.

@tautschnig
Copy link
Member

+1 to what Celina said, and also I left a few comments on the ESBMC/goto-transcoder issues that are listed as "TODO" above.

@rafaelsamenezes rafaelsamenezes linked a pull request Jan 17, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@rafaelsamenezes rafaelsamenezes

Labels
Tool Application Used to tag tool application
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Goto-transcoder action rafaelsamenezes/verify-rust-std
4 participants
@tautschnig @feliperodri @rafaelsamenezes @celinval