Resolve trait methods during stubbing

[aaronbembenek-aws]

Right now, we do not support stubbing methods declared in traits. Consider this example:

trait A {
    fn foo(&self) -> u32;

    fn bar(&self) -> u32;
}

trait B {
    fn bar(&self) -> u32;
}

struct X {}

impl X {
    fn new() -> Self {
        Self {}
    }
}

impl A for X {
    fn foo(&self) -> u32 {
        100
    }

    fn bar(&self) -> u32 {
        200
    }
}

impl B for X {
    fn bar(&self) -> u32 {
        300
    }
}

#[kani::proof]
fn harness() {
    let x = X::new();
    assert_eq!(x.foo(), 1);
    assert_eq!(A::bar(&x), 2);
    assert_eq!(<X as B>::bar(&x), 3);
}

It is currently not possible to stub X's implementation of A::foo, A::bar, or B::bar. To do so, we'd need to do two things.

First, we'd need to come up with a way to refer to trait methods in our kani::stub attributes. In rustc, these are stringified as <X as B>::bar, but paths in attribute arguments are not allowed to have spaces or symbols like < and > (they are simple paths). We could accept string arguments or come up with some other convention, e.g.:

#[kani::stub("<X as B>::bar", ...)]
// or
#[kani::stub(X__as__B::bar), ...)]

Second, we'd need to improve our path resolution algorithm to also search through trait implementations.

[adpaco-aws]

Adding the T-User label as a few of users are hitting this.

[celinval]

What if we create something like:

#[kani::stub(trait_impl(Trait::function for Type), stub_funtion)]

I.e.: The example would look like:

#[kani::stub(trait_impl(A::bar for X), empty_debug)]

[JustusAdam]

I think it makes sense to use rust's syntax, e.g. <Type<'lifetimes, Generics> as Trait>::method for consistency, the tricky part is how do we deal with lifetimes and monomorphization which is almost independent from syntax. It may be necessary at least to distinguish 'a and 'static. On the flip side if you have an instance impl<T> Trait for Type<T>, how does this get stubbed and how does it get resolved? There are a few options here and it is not clear to me which is preferable.

1. Syntactic, e.g. you refer to this instance as <Type<T> as Trait>::method. Note that T here must be the same name as in the impl. This is sadly brittle and we also have yo somehow figure out that T in the impl has that name.
2. Only concrete types allowed. You cannot use e.g. <Type<T> as Trait>::method but you have to use something like <Type<usize> as Trait>::method or <Type<String> as Trait>::method. This is limiting but could be a good first step.
3. Allow something like for. E.g. for <T> <Type<T> as Trait>::method. This this is probably the most general as for instance for <G> <Type<G> as Trait>::method would still match the impl. Though I'm not sure how the resolution and matching would be implemented.

[celinval]

For sure it would, but per the issue description, the attribute expects a simple path. Thus, the type as trait syntax does not work.

[JustusAdam]

I don't think so. The name of the attribute needs to be a simple path, yes, but the contents of the attribute is arbitrary. The attribute contents is a TokenTree which can contain, for instance, the <, > characters as well as an as ident.

Ideally we could just use syn::parse to get an ExprPath which would be exactly what we need. However I don't know of a way to convert the rustc TokenTree to the proc_macro::TokenTree.

[JustusAdam]

After inspecting the rustc documentation a bit it may be possible to use existing infrastructure here. Parser::new could be used to create an ad-hoc parser instance that consumes TokenTrees, then an Expr could be parsed, which we would expect to be of the Path variant.

[celinval]

That would unblock this work. Thanks @JustusAdam for the update.

[celinval]

I wonder if we can just use for parsing the attribute. We would also need to extend our name resolution to handle that case. In theory, users should be able to specify a simple path as well if there is no conflicting method name.

[celinval]

@JustusAdam, your tip was great! I was able to retrieve a syn::TypePath for each path. Unfortunately, implementing this will require a bit more work, since we will no longer be able to represent a stub with a single DefId.

[JustusAdam]

@celinval that depends. If you restrict it to non-parameterized traits, then the Instance it resolves to should have no generic arguments and be basically just a DefId.