Annotate SMIR with lifetime information

[xldenis]

The rust compiler intentionally hides all lifetime information to avoid introducing accidental dependencies on it during compilation and to improve the effectiveness of caching throughout the compiler. Tools like Prusti, Verus or Gillian-Rust on the other hand depend on having access to precise information about the borrows and lifetimes available in a given function.

Currently, a compromise solution has been reached with the compiler giving partial visibility into some of the information calculated by borrowck, allowing tool authors to mostly achieve their goals, though often with significant work on their end.

If SMIR included lifetime information, this would be a killer feature, providing something of huge value to external users while also allowing rustc keep its borrowck implementation private.

Specifically, I would like borrows to be annotated with their regions, and for those regions to have been unified throughout the MIR body. It should also be easy to regions are universal, and to answer outlives questions between regions.

[celinval]

@oli-obk any thoughts?

@xldenis Can you please point to an example on how this is used today?

[xldenis]

@xldenis Can you please point to an example on how this is used today?

Some are still currently private source, unfortunately. What I can say is that we need to know what the lifetimes of each borrow are and how they relate to the lifetime parameters of the fucntion. We also need to know how the lifetime parameters of called functions are instantiated.

@dewert99 used also lifetime information when compiling his specifications to Creusot's specification language.

Additionally, internally in Prusti lifetime information is also used during compilation to determine when to insert magic wands in the compiled Viper code.