Don't translate overridden method in opaque impls

charon/src/bin/charon-driver/translate/translate_traits.rs

@@ -265,14 +265,28 @@ impl BodyTransCtx<'_, '_> {
                 hax::FullDefKind::AssocFn { .. } => {
                     match &impl_item.value {
                         Provided { is_override, .. } => {
-                            let fun_id = self.register_fun_decl_id(item_span, item_def_id);
                             let fun_def = self.t_ctx.hax_def(item_def_id)?;
                             let binder_kind = BinderKind::TraitMethod(trait_id, name.clone());
                             let fn_ref = self.translate_binder_for_def(
                                 item_span,
                                 binder_kind,
                                 &fun_def,
                                 |bt_ctx| {
+                                    // If the impl is opaque, we only translate the signature of a
+                                    // method with a default body if it's directly used somewhere
+                                    // else.
+                                    // We insert the `Binder<FunDeclRef>` unconditionally here, and
+                                    // remove the ones that correspond to untranslated functions in
+                                    // the `remove_unused_methods` pass.
+                                    let fun_id = if *is_override
+                                        && !item_meta.opacity.is_transparent()
+                                    {
+                                        bt_ctx
+                                            .register_fun_decl_id_no_enqueue(item_span, item_def_id)
+                                    } else {
+                                        bt_ctx.register_fun_decl_id(item_span, item_def_id)
+                                    };
+
                                     // TODO: there's probably a cleaner way to write this
                                     assert_eq!(bt_ctx.binding_levels.len(), 2);
                                     let fun_generics = bt_ctx

charon/src/transform/remove_unused_methods.rs

@@ -1,4 +1,4 @@
-//! Remove the trait methods that were not translated.
+//! Remove the trait/impl methods that were not translated.
 use crate::ast::*;
 
 use super::{ctx::TransformPass, TransformCtx};
@@ -13,9 +13,12 @@ impl TransformPass for Transform {
                 .is_some()
         };
         // Keep only the methods for which we translated the corresponding `FunDecl`. We ensured
-        // that this would be translated if the method is used or implemented.
+        // that this would be translated if the method is used or transparently implemented.
         for tdecl in ctx.translated.trait_decls.iter_mut() {
             tdecl.provided_methods.retain(method_is_translated);
         }
+        for timpl in ctx.translated.trait_impls.iter_mut() {
+            timpl.provided_methods.retain(method_is_translated);
+        }
     }
 }

charon/tests/ui/associated-types.out

@@ -6,7 +6,6 @@ trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
     fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-    fn clone_from<'_0, '_1> = core::clone::Clone::clone_from<'_0_0, '_0_1, Self>
 }
 
 trait core::marker::Copy<Self>
@@ -51,19 +50,13 @@ where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::clone::Clone<T>,
 
-fn core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone_from<'_0, '_1, T>(@1: &'_0 mut (core::option::Option<T>[@TraitClause0]), @2: &'_1 (core::option::Option<T>[@TraitClause0]))
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::clone::Clone<T>,
-
 impl<T> core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5<T> : core::clone::Clone<core::option::Option<T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::clone::Clone<T>,
 {
     parent_clause0 = core::marker::Sized<core::option::Option<T>[@TraitClause0]>
     fn clone<'_0> = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone<'_0_0, T>[@TraitClause0, @TraitClause1]
-    fn clone_from<'_0, '_1> = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone_from<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1]
 }
 
 fn test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>(@1: core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]
@@ -310,8 +303,6 @@ where
 
 fn test_crate::Foo::use_item_required<'a, Self, Self_Item>(@1: Self_Item) -> Self_Item
 
-fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
-
 fn alloc::borrow::ToOwned::to_owned<'_0, Self, Self_Owned>(@1: &'_0 (Self)) -> Self_Owned
 
 fn core::borrow::Borrow::borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed)

charon/tests/ui/call-to-known-trait-method.out

@@ -58,7 +58,6 @@ trait core::clone::Clone<Self>
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
 }
 
 fn test_crate::{impl test_crate::Trait<B, (A, B)> for test_crate::Struct<A>[@TraitClause0]}::method<A, B, C>()
@@ -110,12 +109,9 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::eq<'_0, '_1>(@1: &'_0 (bool), @2: &'_1 (bool)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::ne<'_0, '_1>(@1: &'_0 (bool), @2: &'_1 (bool)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19 : core::cmp::PartialEq<bool, bool>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::ne<'_0_0, '_0_1>
 }
 
 fn test_crate::main()
@@ -148,7 +144,5 @@ fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 
 

charon/tests/ui/issue-297-cfg.out

@@ -93,22 +93,11 @@ fn core::slice::{Slice<T>}::chunks<'_0, T>(@1: &'_0 (Slice<T>), @2: usize) -> co
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
 trait core::iter::traits::iterator::Iterator<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
     type Item
     fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
 }
 
 fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
@@ -120,38 +109,13 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Chunks<'a, T>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::count<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice<T>)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Chunks<'a, T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
 {
     parent_clause0 = core::marker::Sized<&'_ (Slice<T>)>
     type Item = &'a (Slice<T>)
     fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'a, '_0_0, T>[@TraitClause0]
-    fn size_hint<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::size_hint<'a, '_0_0, T>[@TraitClause0]
-    fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::count<'a, T>[@TraitClause0]
-    fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>[@TraitClause0]
-    fn nth<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_0_0, T>[@TraitClause0]
-    fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
 }
 
 fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) -> usize
@@ -411,18 +375,6 @@ where
 
 fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option<Self::Item>[Self::parent_clause0]
 
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
-
 trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -563,9 +515,11 @@ trait core::iter::traits::accum::Product<Self, A>
     fn product<I, [@TraitClause0]: core::marker::Sized<I>, [@TraitClause1]: core::iter::traits::iterator::Iterator<I>, @TraitClause1_1::Item = A> = core::iter::traits::accum::Product::product<Self, A, I>[@TraitClause0_0, @TraitClause0_1]
 }
 
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
 
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self