Remove trait indirection when the type is known

charon/src/ast/types_utils.rs

@@ -136,6 +136,16 @@ impl GenericArgs {
             },
         )
     }
+
+    /// Concatenate this set of arguments with another one. Use with care, you must manage the
+    /// order of arguments correctly.
+    pub fn concat(mut self, other: Self) -> Self {
+        self.regions.extend(other.regions);
+        self.types.extend(other.types);
+        self.const_generics.extend(other.const_generics);
+        self.trait_refs.extend(other.trait_refs);
+        self
+    }
 }
 
 impl TypeDecl {

charon/src/driver.rs

@@ -3,6 +3,7 @@ use crate::export;
 use crate::get_mir::MirLevel;
 use crate::reorder_decls;
 use crate::transform::remove_arithmetic_overflow_checks;
+use crate::transform::skip_trait_refs_when_known;
 use crate::transform::{
     index_to_function_calls, insert_assign_return_unit, ops_to_function_calls, reconstruct_asserts,
     remove_drop_never, remove_dynamic_checks, remove_nops, remove_read_discriminant,
@@ -259,6 +260,11 @@ pub fn translate(
         info!("# ULLBC after translation from MIR:\n\n{}\n", ctx);
     }
 
+    // # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl`
+    // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove
+    // some sources of mutual recursion.
+    skip_trait_refs_when_known::transform(&mut ctx);
+
     // # Reorder the graph of dependencies and compute the strictly
     // connex components to:
     // - compute the order in which to extract the definitions

charon/src/ids/map.rs

@@ -23,7 +23,7 @@ impl<Id, T> Default for Map<Id, T> {
     }
 }
 
-impl<Id: std::cmp::Ord, T> Map<Id, T> {
+impl<Id: Ord, T> Map<Id, T> {
     #[allow(clippy::new_without_default)]
     pub fn new() -> Self {
         Map {
@@ -64,10 +64,15 @@ impl<Id: std::cmp::Ord, T> Map<Id, T> {
     }
 }
 
-impl<'a, Id, T> IntoIterator for &'a Map<Id, T>
-where
-    T: Clone,
-{
+impl<Id: Ord, T> std::ops::Index<Id> for Map<Id, T> {
+    type Output = T;
+
+    fn index(&self, index: Id) -> &Self::Output {
+        &self.map[&index]
+    }
+}
+
+impl<'a, Id, T> IntoIterator for &'a Map<Id, T> {
     type Item = (&'a Id, &'a T);
     type IntoIter = std::collections::btree_map::Iter<'a, Id, T>;
 

charon/src/transform/mod.rs

@@ -9,4 +9,5 @@ pub mod remove_nops;
 pub mod remove_read_discriminant;
 pub mod remove_unused_locals;
 pub mod simplify_constants;
+pub mod skip_trait_refs_when_known;
 pub mod update_closure_signatures;

charon/src/transform/skip_trait_refs_when_known.rs

@@ -0,0 +1,54 @@
+use crate::{
+    formatter::{Formatter, IntoFormatter},
+    gast::TraitInstanceId,
+    llbc_ast::{Call, FnOperand, FunId, FunIdOrTraitMethodRef},
+    translate_ctx::TransformCtx,
+    ullbc_ast::RawTerminator,
+};
+
+fn transform_call(ctx: &mut TransformCtx, call: &mut Call) {
+    // We find calls to a trait method where the impl is known; otherwise we return.
+    let FnOperand::Regular(fn_ptr) = &mut call.func else {
+        return;
+    };
+    let FunIdOrTraitMethodRef::Trait(trait_ref, name, _) = &fn_ptr.func else {
+        return;
+    };
+    let TraitInstanceId::TraitImpl(impl_id) = &trait_ref.trait_id else {
+        return;
+    };
+    let trait_impl = &ctx.translated.trait_impls[*impl_id];
+    // Find the function declaration corresponding to this impl.
+    let Some((_, fun_decl_id)) = trait_impl
+        .required_methods
+        .iter()
+        .chain(trait_impl.provided_methods.iter())
+        .find(|(n, _)| n == name)
+    else {
+        return;
+    };
+    let fn_generics = &fn_ptr.generics;
+    let trait_generics = &trait_ref.generics;
+    // Move the trait generics to the function call.
+    // FIXME: make a better API than `concat`.
+    fn_ptr.generics = trait_generics.clone().concat(fn_generics.clone());
+    // Set the call operation to use the function directly.
+    fn_ptr.func = FunIdOrTraitMethodRef::Fun(FunId::Regular(*fun_decl_id));
+}
+
+pub fn transform(ctx: &mut TransformCtx) {
+    ctx.iter_unstructured_bodies(|ctx, name, b| {
+        let fmt_ctx = ctx.into_fmt();
+        trace!(
+            "# About to skip trait refs in function: {}:\n{}",
+            name.fmt_with_ctx(&fmt_ctx),
+            fmt_ctx.format_object(&*b)
+        );
+
+        for block in b.body.iter_mut() {
+            if let RawTerminator::Call { call, .. } = &mut block.terminator.content {
+                transform_call(ctx, call)
+            };
+        }
+    });
+}

charon/tests/crate_data.rs

@@ -186,8 +186,8 @@ fn known_trait_method_call() -> Result<(), Box<dyn Error>> {
     let FnOperand::Regular(fn_ptr) = &call.func else {
         panic!()
     };
-    // For now this call goes through a trait ref. FIXME: call the function directly.
-    let FunIdOrTraitMethodRef::Trait(..) = &fn_ptr.func else {
+    // Assert that this call referes to the method directly, without using a trait ref.
+    let FunIdOrTraitMethodRef::Fun(..) = &fn_ptr.func else {
         panic!()
     };
     Ok(())

charon/tests/ui/arrays.out

@@ -234,25 +234,11 @@ trait core::slice::index::SliceIndex<Self, T>
     fn index_mut : core::slice::index::SliceIndex::index_mut
 }
 
-trait core::ops::index::Index<Self, Idx>
-{
-    type Output
-    fn index : core::ops::index::Index::index
-}
-
 fn core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}::index<'_0, T, I>(@1: &'_0 (Slice<T>), @2: I) -> &'_0 (@TraitClause0::Output)
 where
     // Inherited clauses:
     [@TraitClause0]: core::slice::index::SliceIndex<I, Slice<T>>,
 
-impl<T, I> core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<T, I> : core::ops::index::Index<Slice<T>, I>
-where
-    [@TraitClause0]: core::slice::index::SliceIndex<I, Slice<T>>,
-{
-    type Output = @TraitClause0::Output with []
-    fn index = core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}::index
-}
-
 impl core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for core::ops::range::Range<usize>#1} : core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>
 
 fn core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}::get<'_0, T>(@1: core::ops::range::Range<usize>, @2: &'_0 (Slice<T>)) -> core::option::Option<&'_0 (Slice<T>)>
@@ -279,8 +265,6 @@ impl<T> core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for c
     fn index_mut = core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}::index_mut
 }
 
-fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output)
-
 fn test_crate::slice_subslice_shared_<'_0>(@1: &'_0 (Slice<u32>), @2: usize, @3: usize) -> &'_0 (Slice<u32>)
 {
     let @0: &'_ (Slice<u32>); // return
@@ -300,7 +284,7 @@ fn test_crate::slice_subslice_shared_<'_0>(@1: &'_0 (Slice<u32>), @2: usize, @3:
     @7 := core::ops::range::Range { start: move (@8), end: move (@9) }
     drop @9
     drop @8
-    @5 := core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]::index(move (@6), move (@7))
+    @5 := core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}::index<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>](move (@6), move (@7))
     drop @7
     drop @6
     @4 := &*(@5)
@@ -310,27 +294,11 @@ fn test_crate::slice_subslice_shared_<'_0>(@1: &'_0 (Slice<u32>), @2: usize, @3:
     return
 }
 
-trait core::ops::index::IndexMut<Self, Idx>
-{
-    parent_clause_0 : [@TraitClause0]: core::ops::index::Index<Self, Idx>
-    fn index_mut : core::ops::index::IndexMut::index_mut
-}
-
 fn core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}::index_mut<'_0, T, I>(@1: &'_0 mut (Slice<T>), @2: I) -> &'_0 mut (@TraitClause0::Output)
 where
     // Inherited clauses:
     [@TraitClause0]: core::slice::index::SliceIndex<I, Slice<T>>,
 
-impl<T, I> core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<T, I> : core::ops::index::IndexMut<Slice<T>, I>
-where
-    [@TraitClause0]: core::slice::index::SliceIndex<I, Slice<T>>,
-{
-    parent_clause0 = core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<T, I>[@TraitClause0]
-    fn index_mut = core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}::index_mut
-}
-
-fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut ((parents(Self)::[@TraitClause0])::Output)
-
 fn test_crate::slice_subslice_mut_<'_0>(@1: &'_0 mut (Slice<u32>), @2: usize, @3: usize) -> &'_0 mut (Slice<u32>)
 {
     let @0: &'_ mut (Slice<u32>); // return
@@ -351,7 +319,7 @@ fn test_crate::slice_subslice_mut_<'_0>(@1: &'_0 mut (Slice<u32>), @2: usize, @3
     @8 := core::ops::range::Range { start: move (@9), end: move (@10) }
     drop @10
     drop @9
-    @6 := core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]::index_mut(move (@7), move (@8))
+    @6 := core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}::index_mut<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>](move (@7), move (@8))
     drop @8
     drop @7
     @5 := &mut *(@6)
@@ -390,17 +358,23 @@ fn test_crate::array_to_slice_mut_<'_0>(@1: &'_0 mut (Array<u32, 32 : usize>)) -
     return
 }
 
+trait core::ops::index::Index<Self, Idx>
+{
+    type Output
+    fn index : core::ops::index::Index::index
+}
+
 fn core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}::index<'_0, T, I, const N : usize>(@1: &'_0 (Array<T, const N : usize>), @2: I) -> &'_0 (core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<T, I, const N : usize>[@TraitClause0]::Output)
 where
     // Inherited clauses:
     [@TraitClause0]: core::ops::index::Index<Slice<T>, I>,
 
-impl<T, I, const N : usize> core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<T, I, const N : usize> : core::ops::index::Index<Array<T, const N : usize>, I>
+impl<T, I> core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<T, I> : core::ops::index::Index<Slice<T>, I>
 where
-    [@TraitClause0]: core::ops::index::Index<Slice<T>, I>,
+    [@TraitClause0]: core::slice::index::SliceIndex<I, Slice<T>>,
 {
     type Output = @TraitClause0::Output with []
-    fn index = core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}::index
+    fn index = core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}::index
 }
 
 fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array<u32, 32 : usize>), @2: usize, @3: usize) -> &'_0 (Slice<u32>)
@@ -422,7 +396,7 @@ fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array<u32, 32 : usize>), @2
     @7 := core::ops::range::Range { start: move (@8), end: move (@9) }
     drop @9
     drop @8
-    @5 := core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<u32, core::ops::range::Range<usize>, 32 : usize>[core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]]::index(move (@6), move (@7))
+    @5 := core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}::index<u32, core::ops::range::Range<usize>, 32 : usize>[core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]](move (@6), move (@7))
     drop @7
     drop @6
     @4 := &*(@5)
@@ -432,17 +406,31 @@ fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array<u32, 32 : usize>), @2
     return
 }
 
+trait core::ops::index::IndexMut<Self, Idx>
+{
+    parent_clause_0 : [@TraitClause0]: core::ops::index::Index<Self, Idx>
+    fn index_mut : core::ops::index::IndexMut::index_mut
+}
+
+impl<T, I, const N : usize> core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<T, I, const N : usize> : core::ops::index::Index<Array<T, const N : usize>, I>
+where
+    [@TraitClause0]: core::ops::index::Index<Slice<T>, I>,
+{
+    type Output = @TraitClause0::Output with []
+    fn index = core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}::index
+}
+
 fn core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}::index_mut<'_0, T, I, const N : usize>(@1: &'_0 mut (Array<T, const N : usize>), @2: I) -> &'_0 mut (core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<T, I, const N : usize>[(parents(@TraitClause0)::[@TraitClause0])]::Output)
 where
     // Inherited clauses:
     [@TraitClause0]: core::ops::index::IndexMut<Slice<T>, I>,
 
-impl<T, I, const N : usize> core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}<T, I, const N : usize> : core::ops::index::IndexMut<Array<T, const N : usize>, I>
+impl<T, I> core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<T, I> : core::ops::index::IndexMut<Slice<T>, I>
 where
-    [@TraitClause0]: core::ops::index::IndexMut<Slice<T>, I>,
+    [@TraitClause0]: core::slice::index::SliceIndex<I, Slice<T>>,
 {
-    parent_clause0 = core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<T, I, const N : usize>[(parents(@TraitClause0)::[@TraitClause0])]
-    fn index_mut = core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}::index_mut
+    parent_clause0 = core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<T, I>[@TraitClause0]
+    fn index_mut = core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}::index_mut
 }
 
 fn test_crate::array_subslice_mut_<'_0>(@1: &'_0 mut (Array<u32, 32 : usize>), @2: usize, @3: usize) -> &'_0 mut (Slice<u32>)
@@ -465,7 +453,7 @@ fn test_crate::array_subslice_mut_<'_0>(@1: &'_0 mut (Array<u32, 32 : usize>), @
     @8 := core::ops::range::Range { start: move (@9), end: move (@10) }
     drop @10
     drop @9
-    @6 := core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}<u32, core::ops::range::Range<usize>, 32 : usize>[core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]]::index_mut(move (@7), move (@8))
+    @6 := core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}::index_mut<u32, core::ops::range::Range<usize>, 32 : usize>[core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]](move (@7), move (@8))
     drop @8
     drop @7
     @5 := &mut *(@6)
@@ -1002,7 +990,7 @@ fn test_crate::range_all()
     @fake_read(x@1)
     @6 := &mut x@1
     @7 := core::ops::range::Range { start: const (1 : usize), end: const (3 : usize) }
-    @5 := core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}<u32, core::ops::range::Range<usize>, 4 : usize>[core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]]::index_mut(move (@6), move (@7))
+    @5 := core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}::index_mut<u32, core::ops::range::Range<usize>, 4 : usize>[core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>#1}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]](move (@6), move (@7))
     drop @7
     drop @6
     @4 := &mut *(@5)
@@ -1351,7 +1339,7 @@ fn test_crate::f4<'_0>(@1: &'_0 (Array<u32, 32 : usize>), @2: usize, @3: usize)
     @7 := core::ops::range::Range { start: move (@8), end: move (@9) }
     drop @9
     drop @8
-    @5 := core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<u32, core::ops::range::Range<usize>, 32 : usize>[core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]]::index(move (@6), move (@7))
+    @5 := core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}::index<u32, core::ops::range::Range<usize>, 32 : usize>[core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>#4}<u32>]](move (@6), move (@7))
     drop @7
     drop @6
     @4 := &*(@5)
@@ -1655,6 +1643,8 @@ fn test_crate::sum_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>)) -> u32
     return
 }
 
+fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output)
+
 fn core::slice::index::SliceIndex::get<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> core::option::Option<&'_0 (Self::Output)>
 
 fn core::slice::index::SliceIndex::get_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> core::option::Option<&'_0 mut (Self::Output)>
@@ -1667,5 +1657,15 @@ fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -
 
 fn core::slice::index::SliceIndex::index_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> &'_0 mut (Self::Output)
 
+fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut ((parents(Self)::[@TraitClause0])::Output)
+
+impl<T, I, const N : usize> core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}<T, I, const N : usize> : core::ops::index::IndexMut<Array<T, const N : usize>, I>
+where
+    [@TraitClause0]: core::ops::index::IndexMut<Slice<T>, I>,
+{
+    parent_clause0 = core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>#15}<T, I, const N : usize>[(parents(@TraitClause0)::[@TraitClause0])]
+    fn index_mut = core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>#16}::index_mut
+}
+
 
 

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

@@ -64,8 +64,6 @@ impl core::default::{impl core::default::Default for bool#1} : core::default::De
     fn default = core::default::{impl core::default::Default for bool#1}::default
 }
 
-fn test_crate::Trait::method<Self, B, C>()
-
 opaque type alloc::string::String
 
 fn test_crate::main()
@@ -78,9 +76,9 @@ fn test_crate::main()
 
     _x@1 := (const (0 : u8), const (false))
     @fake_read(_x@1)
-    _y@2 := test_crate::{impl core::default::Default for test_crate::Struct<A>#1}<bool>[core::default::{impl core::default::Default for bool#1}]::default()
+    _y@2 := test_crate::{impl core::default::Default for test_crate::Struct<A>#1}::default<bool>[core::default::{impl core::default::Default for bool#1}]()
     @fake_read(_y@2)
-    @3 := test_crate::{impl test_crate::Trait<B> for test_crate::Struct<A>}<u8, bool>::method<alloc::string::String>()
+    @3 := test_crate::{impl test_crate::Trait<B> for test_crate::Struct<A>}::method<u8, bool, alloc::string::String>()
     drop @3
     @4 := ()
     @0 := move (@4)
@@ -90,5 +88,7 @@ fn test_crate::main()
     return
 }
 
+fn test_crate::Trait::method<Self, B, C>()
+