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

add support for enum, struct, tuple in llbc backend #3721

Merged
merged 24 commits into from
Nov 22, 2024
Merged

add support for enum, struct, tuple in llbc backend #3721

merged 24 commits into from
Nov 22, 2024

Conversation

thanhnguyen-aws
Copy link
Contributor

@thanhnguyen-aws thanhnguyen-aws commented Nov 15, 2024 •
edited
Loading

This pull request added some more features to Stable-mir to Ullbc translation:

  1. Added support for translation of enum, struct, tuple and the projection associated with them.
  2. Edited 3 Binops translation.
  3. Added 4 simple tests for enum, struct, tuple and the projection .
  4. If you had to perform any manual test, please describe them.

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 thanhnguyen-aws requested a review from a team as a code owner November 15, 2024 18:09
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Nov 15, 2024
@celinval
Copy link
Contributor

Can you please provide a better title to this PR? Something like "Add support for enum, struct, tuple in the llbc backend".

@thanhnguyen-aws thanhnguyen-aws changed the title add support for enum, struct, tuple in mod.rs, add some tests add support for enum, struct, tuple in llbc backend Nov 15, 2024
zhassan-aws
zhassan-aws reviewed Nov 16, 2024
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.

Thanks!

tests/expected/llbc/basic0/TestRNvCshcvyQEKZjUj4test4main.symtab.lean Outdated Show resolved Hide resolved
tests/expected/llbc/basic0/expected 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
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
zhassan-aws approved these changes Nov 19, 2024
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.

Please rename the function before merging.

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Outdated Show resolved Hide resolved
zhassan-aws
zhassan-aws reviewed Nov 21, 2024
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.

A few nits. Can you also add new tests (or update existing ones) for the new cases that are supported by the recent commits (e.g. having an argument with type Option<i32>)?

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
zhassan-aws
zhassan-aws approved these changes Nov 21, 2024
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.

Thanks!

Nit: can you remove the _test suffix from the test names? They're all tests, so the suffix is not needed.

@zhassan-aws zhassan-aws added this pull request to the merge queue Nov 22, 2024
Merged via the queue into model-checking:main with commit 88e6eaf Nov 22, 2024
26 checks passed
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 approved these changes

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 @celinval @zhassan-aws