about summary refs log tree commit diff
path: root/compiler/rustc_llvm/llvm-wrapper/PassWrapper.cpp
diff options
context:
space:
mode:
authorbors <bors@rust-lang.org>2021-08-17 19:08:31 +0000
committerbors <bors@rust-lang.org>2021-08-17 19:08:31 +0000
commit30a0a9b694cde95cbab863f7ef4d554f0f46b606 (patch)
treee9d934aaf8f76049e69b07804e5809e527156292 /compiler/rustc_llvm/llvm-wrapper/PassWrapper.cpp
parentd83da1d05dc75ff3452c068299f40e5d99589d71 (diff)
parent9142d6ddf0634066ce4905793aca22948f0d2225 (diff)
downloadrust-30a0a9b694cde95cbab863f7ef4d554f0f46b606.tar.gz
rust-30a0a9b694cde95cbab863f7ef4d554f0f46b606.zip
Auto merge of #86977 - vakaras:body_with_borrowck_facts, r=nikomatsakis
Enable compiler consumers to obtain mir::Body with Polonius facts.

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](https://github.com/viperproject/prusti-dev) 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](https://github.com/viperproject/prusti-dev/blob/b58ced8dfd14ef30582b503d517167ccd771eaff/prusti-interface/src/environment/borrowck/regions.rs#L25-L39). This is not only a hacky approach, but we also reached its limits.

r? `@nikomatsakis`
Diffstat (limited to 'compiler/rustc_llvm/llvm-wrapper/PassWrapper.cpp')
0 files changed, 0 insertions, 0 deletions