Enable compiler consumers to obtain mir::Body with Polonius facts. by vakaras ·...
source link: https://github.com/rust-lang/rust/pull/86977
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
This PR adds a function (get_body_with_borrowck_facts) that can be used by compiler consumers to obtain mir::Body with accompanying borrow checker information.
The most important borrow checker information that our verifier called Prusti needs is lifetime constraints. I have not found a reasonable way to compute the lifetime constraints on the Prusti side. In the compiler, the constraints are computed during the borrow checking phase and then dropped. This PR adds an additional parameter to the do_mir_borrowck function that tells it to return the computed information instead of dropping it.
The additionally returned information by do_mir_borrowck contains a mir::Body with non-erased lifetime regions and Polonius facts. I have decided to reuse the Polonius facts because this way I needed fewer changes to the compiler and Polonius facts contains other useful information that we otherwise would need to recompute.
Just FYI: up to now, Prusti was obtaining this information by parsing the compiler logs. This is not only a hacky approach, but we also reached its limits.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK