Prusti 2.0: Coupling Graph

[JonasAlaif]

To test either the Free PCS or the Coupling Graph implementation, check out this branch and then use the following commands:

To try the FreePCS (owned stuff only) using the following command:

./x.py run --bin prusti-rustc -- --edition=2021 -Z dump_mir_dataflow -Ptest_free_pcs=true ./path/to/rust/file.rs

and make sure to put the following in the .rs file:

#![feature(core_intrinsics, rustc_attrs)] // At the top of the file

#[rustc_mir(borrowck_graphviz_postflow="log/analysis/foo/foo.dot")] // Above any fn you want to dump info on
fn foo( ... ) { ... }

Which will create a log/analysis/foo/free_pcs_foo.dot file (along with others from the compiler analyses)

To try out the Coupling Graph (borrows only), use the following:

./x.py run --bin prusti-rustc -- --edition=2021 -Z dump_mir_dataflow -Ptest_coupling_graph=true ./path/to/rust/file.rs

Which will dump the graphs under log/coupling (a combined .dot with all the graphs lives under log/coupling/all.dot). While looking at those, it can be useful to open e.g. log/analysis/foo/borrows_foo.dot in parallel to inspect the CFG.

TODO:

• Integrate with Free PCS
• Add comments to current implementation