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

Update LLBC backend for Trait support and translation of projection #3807

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

Update LLBC backend for Trait support and translation of projection #3807

wants to merge 57 commits into from

Conversation

thanhnguyen-aws
Copy link
Contributor

@thanhnguyen-aws thanhnguyen-aws commented Jan 2, 2025 •
edited
Loading

  1. Update LLBC backend to adapt to the changes of Charon submodule to AeneasVerif/charon@adc0a85: Changing translate_place to fit with the current place representation of Charon.
  2. Support translation of programs that use Trait, but translating the trait impl functions into monomorphized functions.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@thanhnguyen-aws
add support for enum, struct, tuple in mod.rs, add some tests
e7f4152
@thanhnguyen-aws
revert changes
0937022
@thanhnguyen-aws
format code
bb789a7
@thanhnguyen-aws
edit according to clippy suggestions
cebeff5
@thanhnguyen-aws
add new line at the send of basic0/expected, remove comments in mod.rs
694f7ac
@thanhnguyen-aws
remove more commented functions
6998703
@thanhnguyen-aws
format code
75dcb09
@thanhnguyen-aws
Merge branch 'model-checking:main' into thanh-llbc
ad57da7
@thanhnguyen-aws
add end lines to expected files for the 4 test cases
7ac77f3
@thanhnguyen-aws
remove comments
4d40b53
@thanhnguyen-aws
update s2n-quic
7977233
@thanhnguyen-aws
re-run kani and fix the expected file
28395c5
@thanhnguyen-aws
change function namne find_type_decl_id to get_type_decl_id
2d2f6ce
@thanhnguyen-aws
change function namne find_type_decl_id to get_type_decl_id
c729818
@thanhnguyen-aws
added the translation for generic params, fixed the formatting
dbd7215
@thanhnguyen-aws
Merge branch 'main' into thanh-llbc
e3bb0ca
@thanhnguyen-aws
comment change
997db12
@thanhnguyen-aws
fixed the expected testes
3ec593d
@thanhnguyen-aws
fixed clippy
000d098
@thanhnguyen-aws
fixed format
4107f81
@thanhnguyen-aws
group use statements and add a test that use generic args
43bd739
@thanhnguyen-aws
fixed unreachable -> todo
137008c
@thanhnguyen-aws
fixed format
df89b51
@thanhnguyen-aws
changing some test folders' names
2cb0e56
@thanhnguyen-aws
Merge branch 'model-checking:main' into thanh-llbc
0b89120
@thanhnguyen-aws
Some support for generic
24a30a3
@thanhnguyen-aws
translating traits
6f5347c
@thanhnguyen-aws
Merge branch 'main' into generic-llbc
f798051
@thanhnguyen-aws
added trait clauses
30026cc
@thanhnguyen-aws
more on trait
11f5f10
carolynzech
carolynzech reviewed Jan 2, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

(Had a bit of a race condition with Zyad reviewing, so there may be some repetition with the comments here.)

As a more high-level comment, it'd be great to write some more thorough documentation for each function so that people unfamiliar with Charon can have a basic intuition for what's going on. Nothing too crazy--just 1/2 sentences above each function would help a lot.

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
@zhassan-aws
Copy link
Contributor

Now that #3801 is merged, please change the title of this PR and its description.

@thanhnguyen-aws thanhnguyen-aws changed the title Update charon submodule version Update LLBC backend for new version of Charon Jan 3, 2025
@zhassan-aws
Copy link
Contributor

Update LLBC backend for new version of Charon

I'm not sure the updated title accurately captures what this PR is doing. Are any of the updates needed for the new version of Charon? I thought all such updates were made in #3801.

It seems to me that this PR is primarily about adding support for traits? If so, the title and description should capture that.

@thanhnguyen-aws thanhnguyen-aws changed the title Update LLBC backend for new version of Charon Update LLBC backend for Trait support Jan 6, 2025
@thanhnguyen-aws thanhnguyen-aws changed the title Update LLBC backend for Trait support Update LLBC backend for Trait support and translation of projection Jan 6, 2025
zhassan-aws
zhassan-aws reviewed Jan 7, 2025
View reviewed changes
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

I second @carolynzech's request of adding doc comments to functions, even if it is just a simple description to help the reader understand what a function is doing.

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Show resolved Hide resolved
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Show resolved Hide resolved
carolynzech
carolynzech reviewed Jan 7, 2025
View reviewed changes
tests/perf/s2n-quic Outdated
Copy link
Contributor

Choose a reason for hiding this comment

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

Please revert this change.

zhassan-aws
zhassan-aws reviewed Jan 8, 2025
View reviewed changes
Copy link
Contributor

@zhassan-aws zhassan-aws 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! Can you revert the change to the s2n-quic submodule as @carolynzech pointed out?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@zhassan-aws zhassan-aws zhassan-aws left review comments

@carolynzech carolynzech carolynzech left review comments

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@thanhnguyen-aws @zhassan-aws @carolynzech