Translate defaulted trait methods implementations

[Nadrieril]

Provided trait methods are tricky to handle for consumers of charon: they can be individually overriden, and mutually recursive with other trait methods (overriden or not). To simplify their task, charon could hide the difference between provided and required trait methods.

I see the following steps:

1. Duplicate all provided methods, so that any given trait impl specifies all trait methods;
2. Deduplicate simple cases, by sharing a single method definition for all trait impls that don't override it;
3. Deduplicate more cases, by defining shared methods that take function pointers as inputs.

Step 3 is necessary for e.g. Iterator, which has many provided methods all defined in terms of self.next().

[msprotz]

I recently tracked down an issue in compiling core::cmp::min which boiled down to exactly this. At call-site, the trait impl defines only one required method, the others are provided -- but I am expecting even provided methods to be provided at call-site by the trait impl, because I don't know how to resolve potential overrides.

[Nadrieril]

Current plan is to simply reuse the default method by passing it the right arguments, which is enabled by #512 and #514. We may later duplicate methods to remove dependency cycles if needed.

[sonmarcho]

Current plan is to simply reuse the default method by passing it the right arguments, which is enabled by #512 and #514. We may later duplicate methods to remove dependency cycles if needed.

Following your plan what would be the LLBC of the following code?

trait Trait { fn f(&self); fn g(&self) { self.f() }

impl Trait for i32 { fn f(&self) { self.g() }
impl Trait for u32 { fn f(&self) { self.g() } fn g(&self) { self.f() } }

[Nadrieril]

It would be:

• Trait decl

trait test_crate::Trait<Self>
{
    fn f = test_crate::Trait::f<Self>[Self]
    fn g = test_crate::Trait::g<Self>[Self]
}

fn test_crate::Trait::f<Self>(@1: Self)
where
    [@TraitClause0]: test_crate::Trait<Self>,

fn test_crate::Trait::g<Self>(@1: Self)
where
    [@TraitClause0]: test_crate::Trait<Self>,
{
    @0 := @TraitClause0::f(move (@2))
    return
}

• Impl for i32:

fn test_crate::{impl test_crate::Trait for i32}::f(@1: i32)
{
    @0 := test_crate::Trait::g<i32>[test_crate::{impl test_crate::Trait for i32}](move (@2))
    return
}

impl test_crate::{impl test_crate::Trait for i32} : test_crate::Trait<i32>
{
    fn f = test_crate::{impl test_crate::Trait for i32}::f
    fn g = test_crate::Trait::g<i32>[test_crate::{impl test_crate::Trait for i32}]
}

• Impl for u32:

fn test_crate::{impl test_crate::Trait for u32}#1::f(@1: u32)
{
    @0 := test_crate::{impl test_crate::Trait for u32}#1::g(move (@2))
    return
}

fn test_crate::{impl test_crate::Trait for u32}#1::g(@1: u32)
{
    @0 := test_crate::{impl test_crate::Trait for u32}#1::f(move (@2))
    return
}

impl test_crate::{impl test_crate::Trait for u32}#1 : test_crate::Trait<u32>
{
    fn f = test_crate::{impl test_crate::Trait for u32}#1::f
    fn g = test_crate::{impl test_crate::Trait for u32}#1::g
}

The impl for i32 is self-recursive, and as you expected this causes issues in aeneas. Since yesterday I have updated my plan to include duplicating defaulted methods to remove the cycle.

[sonmarcho]

Thanks for the explanations! Yes, I expected you would have to duplicate the default methods if you really want to make that work (i.e., I don't see an in-between solution which allows to do strictly more than what we already support).

[Nadrieril]

The current solution does support defaulted methods as long as they don't call any other method, because then we remove the unnecessary Self clause. However in most cases defaulted methods do call other methods so that may not be very useful.