How to avoid creating the wrapper?

[LDY1998]

• [x] remove extern_spec map
• [x] add def_spec map
• [x] look up specifications in def_spec
• [x] merge extern specs into def_spec
• [x] add trusted and pure into def_spec
• [x] loop invariants

Summary

The goal is for attribute lookups to become unnecessary in encoder. SpecCollector now collects all the specifications into a map of DefIds -> specs. This is also a prerequisite for a much nicer #138 without #[stmt_expr_attributes].

Future work

As discussed in our meetings, eventually we should convert all the MIR bodies we would need during verification (specifications and un-trusted function bodies) into VIR during the SpecCollector visit. This would allow external specs to work without creating a wrapper function, and would result in a cleaner separation of the Viper encoder from the Rust internals. However, a more generic (incl. type parameters) VIR is required before such an encoding can be done.

How is the MIR encoded process affect the decision of creating wrapper or not? Why would moving the MIR->VIR encoding into SpecCollector visit solve the wrapper problem?

[Aurel300]

If I remember correctly the change would be something like:

// currently
fn wrapper_for_foo(a: i32, b: bool, ...) {
  foo(a, b, ...);
}

// with the change
fn wrapper_for_foo() {
  foo;
}

This still lets us resolve foo to the correct DefId, but we don't need to worry about generics or arguments when desugaring. To be honest, I don't fully remember how I planned to deal with arguments mentioned in the specs. Anyway, the full VIR encoding will most likely not be available during your internship (as it is happening in a parallel internship), and this might be low-priority depending on how well we can desugar with the existing approach.