Skip to content

Function shape creation fails with ContainsAliasType, even when aliases can be resolved to concrete types #139

@zgrannan

Description

@zgrannan

For example:

trait MyTrait {
    type Output;
    fn call() -> Self::Output;
}

impl MyTrait for i32 {
    type Output = i32;
    fn call() -> i32 { 0 }
}

fn main() {
    let x = i32::call();
}

causes PCG to generate a warning: Error getting signature shape at ../test-files/220_alias.rs:12:13: 12:24 (#0): ContainsAliasType.

However, it should be possible to generate the shape because the Output type can be resolved to the concrete type i32.

As a side note: the current behaviour in the PCG for when the shape cannot be computed is to infer the shape by comparing the return and argument places at the call-site. This is sound in the sense that the shape will contain all edges in the callee shape, but imprecise because it may contain additional edges due to other constraints by the caller. However, this behaviour is unsound for tools like Prusti where the shape of caller and callee needs to match.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions