search

rust-lang-nursery / wg-verification

Verification working group
Apache License 2.0
104 stars 10 forks source link

Extract lifetimes from compiler #13

Open avadacatavra opened 6 years ago

vakaras commented 6 years ago

This is currently blocked until the NLL design gets stabilized.

vakaras commented 5 years ago

It seems that the borrow checker information that consumers would need is:

  1. The Polonius input facts. (Consumers can get output facts by running Polonius themselves. Also, I know at least one case where it is useful to modify the input facts before feeding them into Polonius.)
  2. The mapping between reference typed MIR places and region identifiers used in Polonius.

As far as I know, the only way to get Polonius input facts is to pass -Znll-facts flag to the compiler and then parse the emitted CSV files. The most hacky part of this is parsing strings to restore actual IDs used in MIR.

Obtaining the mapping requires passing the -Zdump-mir=renumber flag to the compiler that makes it to dump a diagnostics file, which can then be parsed to obtain the mapping.

An ideal solution for me would be to have a query (or queries) on TyCtxt that returns Polonius input facts and a mapping between MIR places and region IDs. Having such a query would not only simplify verifiers that need Polonius information, but would also enable showing visualisations of borrows in the IDE (we already have some code for this).