Adding support for type aliases to associated types

[ThomasMayerl]

Upon trying to verify the stdlib definitions, Prusti crashed when encountering an unresolved type alias. Usually, rustc already resolves the aliases. However, when using associated types, rustc cannot do so statically. Therefore, this PR adds support for this.

[ThomasMayerl]

PCG currently does not support type aliases. In the impl of FunctionDataShapeDataSource of PCG, we check if there are aliases. The temporary fix is to comment out this check, but I don't know if it breaks anything.

[Aurel300]

I don't think this is a very good solution. The type-to-type functions that map a generic to an associated type of a trait should not be defined by the GenericParamsEnc. We should have an encoder that handles traits specifically, as well as one for impl blocks; some of the responsibilities of these encoders are outlined in the hack.md document: assoc. type functions, domains/axioms for trait method specifications, function to determine if a given Type implements the trait or not.

[ThomasMayerl]

I don't think this is a very good solution. The type-to-type functions that map a generic to an associated type of a trait should not be defined by the GenericParamsEnc. We should have an encoder that handles traits specifically, as well as one for impl blocks; some of the responsibilities of these encoders are outlined in the hack.md document: assoc. type functions, domains/axioms for trait method specifications, function to determine if a given Type implements the trait or not.

So you would say we should instead, upon trait encoding, generate the function, and, upon encoding the implementation, the axioms, and that the GenericParamsEnc should only call the assoc function? But does the MIR even still contain the traits/impls or just the result of the resolution? What I mean is, do we even encode traits/impls in Prusti?

[Aurel300]

Thanks, mostly looks good now. We can merge, but you could please check that all the tests from #52 pass with this also?

Apart from that I only wonder (probably not for this PR anymore) about the choice of using trait impls from the current crate vs all visible ones, which may include ones that are coming from dependencies. We should also do something for the latter, avoiding verification (since we won't see the impl bodies) but emitting axioms about which assoc. types map to what, which types implement which traits, etc.

[ThomasMayerl]

Thanks, mostly looks good now. We can merge, but you could please check that all the tests from #52 pass with this also?

The tests pass. However, two of the files (such as local-testing/generics/fail/trait_post.rs in #52) result in a consistency error because of a variable being s_Param but the bound expression being s_UInt_u32. Verifying the output Viper code works, though. I will still merge the PR because this issue also happens without the changes from this PR.