Include more trait impls for aeneas

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)),
         }
     }
 

charon/src/transform/add_missing_info/reorder_decls.rs

@@ -344,8 +344,15 @@ fn compute_declarations_graph(ctx: &TransformCtx) -> DiGraphMap<ItemId, ()> {
                 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) => {

charon/tests/ui/regressions/issue-1172-missing-trait-impl.out

@@ -0,0 +1,82 @@
+# Final LLBC before serialization:
+
+// Full name: core::default::Default
+#[lang_item("Default")]
+pub trait Default<Self>
+{
+    fn default = core::default::Default::default<Self>[Self]
+    non-dyn-compatible
+}
+
+// Full name: core::array::{impl Default for [T; 29 : usize]}::default
+pub fn {impl Default for [T; 29 : usize]}::default<T>() -> [T; 29 : usize]
+where
+    [@TraitClause0]: Default<T>,
+= <opaque>
+
+// Full name: core::array::{impl Default for [T; 29 : usize]}
+impl<T> Default for [T; 29 : usize]
+where
+    [@TraitClause0]: Default<T>,
+{
+    fn default = {impl Default for [T; 29 : usize]}::default<T>[@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>() -> [T; 16 : usize]
+where
+    [@TraitClause0]: Default<T>,
+= <opaque>
+
+// Full name: core::array::{impl Default for [T; 16 : usize]}
+impl<T> Default for [T; 16 : usize]
+where
+    [@TraitClause0]: Default<T>,
+{
+    fn default = {impl Default for [T; 16 : usize]}::default<T>[@TraitClause0]
+    non-dyn-compatible
+}
+
+#[lang_item("default_fn")]
+pub fn core::default::Default::default<Self>() -> Self
+where
+    [@TraitClause0]: Default<Self>,
+= <opaque>
+
+// Full name: core::default::{impl Default for u8}::default
+pub fn {impl Default for u8}::default() -> u8
+= <opaque>
+
+// 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]}<u8>[{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
+}
+
+
+

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],
+}