From 20d479354d55affa1195ea2214c83a68dfef4b35 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 27 May 2026 08:59:17 +0200 Subject: [PATCH 1/2] Add test --- .../issue-1172-missing-trait-impl.out | 73 +++++++++++++++++++ .../issue-1172-missing-trait-impl.rs | 8 ++ 2 files changed, 81 insertions(+) create mode 100644 charon/tests/ui/regressions/issue-1172-missing-trait-impl.out create mode 100644 charon/tests/ui/regressions/issue-1172-missing-trait-impl.rs diff --git a/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out b/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out new file mode 100644 index 000000000..abb58c43e --- /dev/null +++ b/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out @@ -0,0 +1,73 @@ +# Final LLBC before serialization: + +// Full name: core::default::Default +#[lang_item("Default")] +pub trait Default +{ + fn default = core::default::Default::default[Self] + non-dyn-compatible +} + +// Full name: core::array::{impl Default for [T; 16 : usize]}::default +pub fn {impl Default for [T; 16 : usize]}::default() -> [T; 16 : usize] +where + [@TraitClause0]: Default, += + +// Full name: core::array::{impl Default for [T; 16 : usize]} +impl Default for [T; 16 : usize] +where + [@TraitClause0]: Default, +{ + fn default = {impl Default for [T; 16 : usize]}::default[@TraitClause0] + non-dyn-compatible +} + +// Full name: core::array::{impl Default for [T; 29 : usize]}::default +pub fn {impl Default for [T; 29 : usize]}::default() -> [T; 29 : usize] +where + [@TraitClause0]: Default, += + +#[lang_item("default_fn")] +pub fn core::default::Default::default() -> Self +where + [@TraitClause0]: Default, += + +// Full name: core::default::{impl Default for u8}::default +pub fn {impl Default for u8}::default() -> u8 += + +// Full name: core::default::{impl Default for u8} +impl Default for u8 { + fn default = {impl Default for u8}::default + non-dyn-compatible +} + +// Full name: test_crate::Key +pub struct Key { + round_keys: [[u8; 16 : usize]; 29 : usize], +} + +// Full name: test_crate::{impl Default for Key}::default +pub fn {impl Default for Key}::default() -> Key +{ + let _0: Key; // return + let _1: [[u8; 16 : usize]; 29 : usize]; // anonymous local + + storage_live(_1) + _1 = {impl Default for [T; 29 : usize]}::default<[u8; 16 : usize]>[{impl Default for [T; 16 : usize]}[{impl Default for u8}]]() + _0 = Key { round_keys: move _1 } + storage_dead(_1) + return +} + +// Full name: test_crate::{impl Default for Key} +impl Default for Key { + fn default = {impl Default for Key}::default + non-dyn-compatible +} + + + diff --git a/charon/tests/ui/regressions/issue-1172-missing-trait-impl.rs b/charon/tests/ui/regressions/issue-1172-missing-trait-impl.rs new file mode 100644 index 000000000..ede474a68 --- /dev/null +++ b/charon/tests/ui/regressions/issue-1172-missing-trait-impl.rs @@ -0,0 +1,8 @@ +//@ charon-args=--preset=aeneas +//@ no-default-options +// The `Default` impl indirectly uses the one for `[[u8; 16]; 29]`, but that impl doesn't end up in +// `ordered_decls` because it's unused. +#[derive(Default)] +pub struct Key { + round_keys: [[u8; 16]; 29], +} From 6d0d40d01ecca97a3f064afb6ce346c152ce1cac Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 27 May 2026 09:20:46 +0200 Subject: [PATCH 2/2] Include more trait impls for aeneas --- charon/src/options.rs | 5 +++++ .../add_missing_info/reorder_decls.rs | 11 ++++++++-- .../issue-1172-missing-trait-impl.out | 21 +++++++++++++------ 3 files changed, 29 insertions(+), 8 deletions(-) diff --git a/charon/src/options.rs b/charon/src/options.rs index b8b5d3407..419092333 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -623,6 +623,10 @@ pub struct TranslateOptions { pub add_destruct_bounds: bool, /// Translate drop glue for poly types, knowing that this may cause ICEs. pub translate_poly_drop_glue: bool, + /// By default an impl is included in `ordered_decls` only if it's used directly (e.g. in a + /// `TraitRef`). A direct call to an impl method would not cause the impl to be included. This + /// includes them anyway. + pub include_method_impls_in_ordered_decls: bool, } impl TranslateOptions { @@ -764,6 +768,7 @@ impl TranslateOptions { desugar_drops: options.desugar_drops, add_destruct_bounds: options.precise_drops, translate_poly_drop_glue: options.precise_drops, + include_method_impls_in_ordered_decls: matches!(options.preset, Some(Preset::Aeneas)), } } diff --git a/charon/src/transform/add_missing_info/reorder_decls.rs b/charon/src/transform/add_missing_info/reorder_decls.rs index 256a71431..bc61926b8 100644 --- a/charon/src/transform/add_missing_info/reorder_decls.rs +++ b/charon/src/transform/add_missing_info/reorder_decls.rs @@ -344,8 +344,15 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> DiGraphMap { let _ = generics.drive(&mut visitor); let _ = signature.drive(&mut visitor); let _ = body.drive(&mut visitor); - if let ItemSource::TraitDecl { trait_ref, .. } = src { - visitor.insert_edge(trait_ref.id); + match src { + ItemSource::TraitDecl { trait_ref, .. } => visitor.insert_edge(trait_ref.id), + // Include the impl without adding a dependency edge to it. + ItemSource::TraitImpl { impl_ref, .. } + if ctx.options.include_method_impls_in_ordered_decls => + { + visitor.insert_node(impl_ref.id) + } + _ => {} } } ItemRef::TraitDecl(d) => { diff --git a/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out b/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out index abb58c43e..c4e5b9e9c 100644 --- a/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out +++ b/charon/tests/ui/regressions/issue-1172-missing-trait-impl.out @@ -8,6 +8,21 @@ pub trait Default non-dyn-compatible } +// Full name: core::array::{impl Default for [T; 29 : usize]}::default +pub fn {impl Default for [T; 29 : usize]}::default() -> [T; 29 : usize] +where + [@TraitClause0]: Default, += + +// Full name: core::array::{impl Default for [T; 29 : usize]} +impl Default for [T; 29 : usize] +where + [@TraitClause0]: Default, +{ + fn default = {impl Default for [T; 29 : usize]}::default[@TraitClause0] + non-dyn-compatible +} + // Full name: core::array::{impl Default for [T; 16 : usize]}::default pub fn {impl Default for [T; 16 : usize]}::default() -> [T; 16 : usize] where @@ -23,12 +38,6 @@ where non-dyn-compatible } -// Full name: core::array::{impl Default for [T; 29 : usize]}::default -pub fn {impl Default for [T; 29 : usize]}::default() -> [T; 29 : usize] -where - [@TraitClause0]: Default, -= - #[lang_item("default_fn")] pub fn core::default::Default::default() -> Self where