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

Goto-transcoder action #236

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Goto-transcoder action #236

wants to merge 2 commits into from

Conversation

rafaelsamenezes
Copy link

@rafaelsamenezes rafaelsamenezes commented Jan 17, 2025 •
edited
Loading

Resolves #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.

@rafaelsamenezes
added goto-transcoder flow
c4e10e6 
fixes on action script

removed checkout subfolder

fixed typo
@rafaelsamenezes
added missing .sh
a0cde2a
@rafaelsamenezes rafaelsamenezes requested a review from a team as a code owner January 17, 2025 14:24
celinval
celinval reviewed Jan 21, 2025
View reviewed changes
Copy link

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. Thanks

scripts/run-goto-transcoder.sh

echo "Checking contracts with goto-transcoder"

if [ ! -d "goto-transcoder" ]; then
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can you please add this folder to the git ignore file?

scripts/run-goto-transcoder.sh
##############
# PARAMETERS #
##############
contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit... can you pass this as an argument to Kani script and the goto-transcoder script instead of relying here on the location where Kani stores their temporary files?

scripts/run-goto-transcoder.sh
# PARAMETERS #
##############
contract_folder=target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps
supported_regex=checked_unchecked.*.out
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you also make this an argument so users can easily try out their new harnesses.

scripts/run-goto-transcoder.sh

cd goto-transcoder
while IFS= read -r line; do
contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can you document what this is doing please?

scripts/run-goto-transcoder.sh
continue
fi
echo "Running: goto-transcoder $contract $contract_folder/$line $contract.esbmc.goto"
cargo run cbmc2esbmc $contract ../$contract_folder/$line $contract.esbmc.goto
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

does your Cargo.toml file define a workspace? Can you please make sure that running this command won't try to modify this repository root Cargo.toml? Thanks!

feliperodri
feliperodri requested changes Jan 22, 2025
View reviewed changes
.github/workflows/goto-transcoder.yml
@@ -0,0 +1,37 @@
# This workflow executes the supported contracts in goto-transcoder

name: Run GOTO Transcoder (ESBMC)
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need to include a section in our book about the new tool. See Kani example https://model-checking.github.io/verify-rust-std/tools.html

@feliperodri feliperodri added the Tool Application Used to tag tool application label Jan 22, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@celinval celinval celinval left review comments

@feliperodri feliperodri feliperodri requested changes

Requested changes must be addressed to merge this pull request.

Assignees

@rafaelsamenezes rafaelsamenezes

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

Successfully merging this pull request may close these issues.

Tool proposal: GOTO Transcoder (ESBMC)
3 participants
@rafaelsamenezes @feliperodri @celinval