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.

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

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

Merged
merged 62 commits into from
Jan 10, 2025
Merged
Show file tree
Hide file tree
Changes from 52 commits
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
e7f4152
add support for enum, struct, tuple in mod.rs, add some tests
thanhnguyen-aws Nov 15, 2024
0937022
revert changes
thanhnguyen-aws Nov 15, 2024
bb789a7
format code
thanhnguyen-aws Nov 15, 2024
cebeff5
edit according to clippy suggestions
thanhnguyen-aws Nov 15, 2024
694f7ac
add new line at the send of basic0/expected, remove comments in mod.rs
thanhnguyen-aws Nov 18, 2024
6998703
remove more commented functions
thanhnguyen-aws Nov 18, 2024
75dcb09
format code
thanhnguyen-aws Nov 18, 2024
ad57da7
Merge branch 'model-checking:main' into thanh-llbc
thanhnguyen-aws Nov 18, 2024
7ac77f3
add end lines to expected files for the 4 test cases
thanhnguyen-aws Nov 18, 2024
4d40b53
remove comments
thanhnguyen-aws Nov 18, 2024
7977233
update s2n-quic
thanhnguyen-aws Nov 18, 2024
28395c5
re-run kani and fix the expected file
thanhnguyen-aws Nov 18, 2024
2d2f6ce
change function namne find_type_decl_id to get_type_decl_id
thanhnguyen-aws Nov 19, 2024
c729818
change function namne find_type_decl_id to get_type_decl_id
thanhnguyen-aws Nov 19, 2024
dbd7215
added the translation for generic params, fixed the formatting
thanhnguyen-aws Nov 20, 2024
e3bb0ca
Merge branch 'main' into thanh-llbc
thanhnguyen-aws Nov 20, 2024
997db12
comment change
thanhnguyen-aws Nov 20, 2024
3ec593d
fixed the expected testes
thanhnguyen-aws Nov 20, 2024
000d098
fixed clippy
thanhnguyen-aws Nov 20, 2024
4107f81
fixed format
thanhnguyen-aws Nov 20, 2024
43bd739
group use statements and add a test that use generic args
thanhnguyen-aws Nov 21, 2024
137008c
fixed unreachable -> todo
thanhnguyen-aws Nov 21, 2024
df89b51
fixed format
thanhnguyen-aws Nov 21, 2024
2cb0e56
changing some test folders' names
thanhnguyen-aws Nov 22, 2024
0b89120
Merge branch 'model-checking:main' into thanh-llbc
thanhnguyen-aws Nov 25, 2024
24a30a3
Some support for generic
thanhnguyen-aws Nov 25, 2024
6f5347c
translating traits
thanhnguyen-aws Nov 25, 2024
f798051
Merge branch 'main' into generic-llbc
thanhnguyen-aws Nov 26, 2024
30026cc
added trait clauses
thanhnguyen-aws Nov 26, 2024
11f5f10
more on trait
thanhnguyen-aws Nov 27, 2024
28b11e1
save
thanhnguyen-aws Nov 27, 2024
659f83b
save
thanhnguyen-aws Nov 27, 2024
e668d44
save
thanhnguyen-aws Nov 28, 2024
00c9513
update toolchain
thanhnguyen-aws Nov 29, 2024
9f5774c
translate trait
thanhnguyen-aws Dec 30, 2024
7c286c8
editing code
thanhnguyen-aws Dec 31, 2024
865bdd9
fixed clippy
thanhnguyen-aws Dec 31, 2024
0b7c527
update charon
thanhnguyen-aws Jan 2, 2025
d7c91f5
update charon
thanhnguyen-aws Jan 2, 2025
215d11d
fix small bugs
thanhnguyen-aws Jan 2, 2025
5e3fd23
save
thanhnguyen-aws Jan 2, 2025
103603f
update projection
thanhnguyen-aws Jan 3, 2025
d84c48e
merging main
thanhnguyen-aws Jan 3, 2025
f585369
fixed println
thanhnguyen-aws Jan 3, 2025
f336b0a
adding an expected test for trait
thanhnguyen-aws Jan 3, 2025
53983dd
fixed the test
thanhnguyen-aws Jan 3, 2025
3bc4e6d
fix some comments
thanhnguyen-aws Jan 6, 2025
dd8c642
Merge branch 'main' into update-charon
thanhnguyen-aws Jan 7, 2025
7d28582
add comments
thanhnguyen-aws Jan 7, 2025
5459810
add more comments
thanhnguyen-aws Jan 7, 2025
1efa472
formating
thanhnguyen-aws Jan 7, 2025
bd88440
remove expected
thanhnguyen-aws Jan 7, 2025
e28169a
Update kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
thanhnguyen-aws Jan 8, 2025
e80166b
add example test for option
thanhnguyen-aws Jan 8, 2025
7930902
comments
thanhnguyen-aws Jan 8, 2025
06d0525
add tests/expected/llbc/option/expected
thanhnguyen-aws Jan 8, 2025
2a2a462
revert change to s2n-quic
thanhnguyen-aws Jan 9, 2025
1799aa6
Merge branch 'main' into update-charon
thanhnguyen-aws Jan 9, 2025
954317d
fixed formating
thanhnguyen-aws Jan 9, 2025
6c76375
add expected for trait impl
thanhnguyen-aws Jan 9, 2025
5cbbbae
Merge branch 'main' into update-charon
thanhnguyen-aws Jan 9, 2025
0a58fb1
Merge branch 'main' into update-charon
thanhnguyen-aws Jan 10, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ impl LlbcCodegenBackend {

// Translate all the items
for item in &items {
debug!("Translating: {item:?}");
match item {
MonoItem::Fn(instance) => {
let mut fcx = Context::new(
Expand Down Expand Up @@ -387,12 +388,14 @@ where
fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
let options = TransformOptions {
no_code_duplication: false,
hide_marker_traits: false,
hide_marker_traits: true,
thanhnguyen-aws marked this conversation as resolved.
Show resolved Hide resolved
no_merge_goto_chains: false,
item_opacities: Vec::new(),
};
let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
let mut translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
//This option setting is for Aeneas compatibility
translated.options.hide_marker_traits = true;
let errors = ErrorCtx::new(true, false);
TransformCtx { options, translated, errors }
}
Loading
Loading