Update LLBC backend for Trait support and translation of projection by thanhnguyen-aws · Pull Request #3807 · model-checking/kani

thanhnguyen-aws · 2025-01-02T17:47:00Z

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

zhassan-aws

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

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

tests/expected/llbc/traitimpl/expected

tests/perf/s2n-quic

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

zhassan-aws

Looks good! Can you revert the change to the s2n-quic submodule as @carolynzech pointed out?

zhassan-aws

Thanks

thanhnguyen-aws added 30 commits November 15, 2024 08:36

add support for enum, struct, tuple in mod.rs, add some tests

e7f4152

revert changes

0937022

format code

bb789a7

edit according to clippy suggestions

cebeff5

add new line at the send of basic0/expected, remove comments in mod.rs

694f7ac

remove more commented functions

6998703

format code

75dcb09

Merge branch 'model-checking:main' into thanh-llbc

ad57da7

add end lines to expected files for the 4 test cases

7ac77f3

remove comments

4d40b53

update s2n-quic

7977233

re-run kani and fix the expected file

28395c5

change function namne find_type_decl_id to get_type_decl_id

2d2f6ce

change function namne find_type_decl_id to get_type_decl_id

c729818

added the translation for generic params, fixed the formatting

dbd7215

Merge branch 'main' into thanh-llbc

e3bb0ca

comment change

997db12

fixed the expected testes

3ec593d

fixed clippy

000d098

fixed format

4107f81

group use statements and add a test that use generic args

43bd739

fixed unreachable -> todo

137008c

fixed format

df89b51

changing some test folders' names

2cb0e56

Merge branch 'model-checking:main' into thanh-llbc

0b89120

Some support for generic

24a30a3

translating traits

6f5347c

Merge branch 'main' into generic-llbc

f798051

added trait clauses

30026cc

more on trait

11f5f10

thanhnguyen-aws changed the title ~~Update LLBC backend for new version of Charon~~ Update LLBC backend for Trait support Jan 6, 2025

thanhnguyen-aws changed the title ~~Update LLBC backend for Trait support~~ Update LLBC backend for Trait support and translation of projection Jan 6, 2025

thanhnguyen-aws added 2 commits January 6, 2025 09:08

fix some comments

3bc4e6d

Merge branch 'main' into update-charon

dd8c642

thanhnguyen-aws requested review from carolynzech and zhassan-aws January 7, 2025 17:55

zhassan-aws reviewed Jan 7, 2025

View reviewed changes

thanhnguyen-aws added 3 commits January 7, 2025 11:34

add comments

7d28582

add more comments

5459810

formating

1efa472

carolynzech reviewed Jan 7, 2025

View reviewed changes

tests/expected/llbc/traitimpl/expected Outdated Show resolved Hide resolved

carolynzech reviewed Jan 7, 2025

View reviewed changes

tests/perf/s2n-quic Show resolved Hide resolved

remove expected

bd88440

zhassan-aws reviewed Jan 8, 2025

View reviewed changes

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

thanhnguyen-aws and others added 4 commits January 7, 2025 16:47

Update kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

e28169a

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

add example test for option

e80166b

comments

7930902

add tests/expected/llbc/option/expected

06d0525

zhassan-aws reviewed Jan 8, 2025

View reviewed changes

thanhnguyen-aws added 5 commits January 8, 2025 16:32

revert change to s2n-quic

2a2a462

Merge branch 'main' into update-charon

1799aa6

fixed formating

954317d

add expected for trait impl

6c76375

Merge branch 'main' into update-charon

5cbbbae

zhassan-aws approved these changes Jan 10, 2025

View reviewed changes

Merge branch 'main' into update-charon

0a58fb1

thanhnguyen-aws added this pull request to the merge queue Jan 10, 2025

Merged via the queue into model-checking:main with commit f1b0877 Jan 10, 2025
28 checks passed

thanhnguyen-aws deleted the update-charon branch January 10, 2025 22:34

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Update LLBC backend for Trait support and translation of projection#3807
thanhnguyen-aws merged 62 commits intomodel-checking:mainfrom
thanhnguyen-aws:update-charon

thanhnguyen-aws commented Jan 2, 2025 •

edited

Loading

Uh oh!

zhassan-aws left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zhassan-aws left a comment

Uh oh!

zhassan-aws left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

thanhnguyen-aws commented Jan 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

thanhnguyen-aws commented Jan 2, 2025 •

edited

Loading