Implement lifetime-checking by forking rustc_mir_build

[tjhance]

This pull request will OBSOLETE lifetime_generate.

This PR contains a fork of the rustc_mir_build crate, which contains the lowering HIR -> THIR. We modify the lowering to remove all spec code, leaving only exec+proof code.

It currently passes most tests in rust_verify_test/tests/lifetime.rs.

Benefits:

• Conceptually much simpler than emitting source-level rust code
• Much nicer error messages that don't get mangled

Snags:

For the most part, erasing calls and variables is pretty easy. There is one exception: closure captures. Consider something like:

let f = || {
    assert(x == x);
    let j = &x.a;
}

Rustc infers that x will be captured, but since the assert is erased, only x.a is captured. Computing the correct capture-set is more involved than the other erasure-related activities, and may require forking some additional code. I've been experimenting with a strategy that seems to work, but it needs to be documented and made robust.

Implementation notes:

After running our modes.rs pass, Verus creates an object called VerusErasureCtxt which contains information about which HIR nodes need to be erased. We then make this information available to the rustc_mir_build fork.

We modify rustc_mir_build/src/thir/cx/expr.rs to check this context object to decide when to erase stuff. I attempted to make the changes to rustc_mir_build/src/thir/cx/expr.rs as minimal as possible. Almost all nontrivial logic is delegated to the rustc_mir_build_additional_files/verus.rs

Most important files:

• source/rustc_mir_build_additional_files/verus.rs
• source/rustc_mir_build/src/thir/cx/expr.rs
• source/rust_verify/src/erase.rs

The upvar.rs and expr_use_visitor.rs files are also forks of rustc files, related to closure captures.

To make this easier to review, I have made the base of the PR a commit that already contains the rustc_mir_build crate as-is from rustc 1.88.0. Therefore, the PR's diff should only show the Verus-relevant changes.

TODO:

• fix a few more corner cases to get all the lifetime tests passing
• merge with change the encoding for consts and const fns #1563 to fix const-related tests
• streamline and document the process for updating the rustc_mir_build fork when bumping versions
• finalize approach to closure captures

[tjhance]

@Chris-Hawblitzel do you think you could help me figure out what's going on with the external_traits test failures? Seems to be some kind of mismatch between the function names in erasure_hints.resolved_calls and the function names in the VIR crate.

[tjhance]

There are two minor failing tests:

FAIL [   0.186s] rust_verify_test::regression test_no_unsupported_trait_imports
FAIL [   0.087s] rust_verify_test::safe_api opaque_closure_type_returned

The first one fails because it relies on no-auto-import-builtin, whereas lifetime-generate relies on having builtin DefIds. This seems like an odd feature to support, I'm not sure what to do about the test to make sure it's testing the right thing.

The second fails, I think, because the use of an opaque type causes rustc_mir_build to run early, before we get a chance to do mode-checking. I'm not sure what to do about this one, either. It's not a huge deal now, since we don't support opaque types, but there's work-in-progress to support it so we should have a plan.

In addition to this, there's the issue with trait spec extensions. Right now, I got these passing through a hack that should be fixed. Basically, the problem is that we create ResolvedCall info during the rust_to_vir pass, but then later (in traits.rs) we do a bunch of renaming. Thus the name in the ResolvedCall is not the same as the name we use in VIR. My current solution isn't very robust (see the FIXME in erase.rs).

[tjhance]

This is ready for review as there are only minor outstanding issues.

• decide what to do about the opaque types issue
• fix the trait extension spec fn issue
• add the forked code as subtrees and document the update process
• add LICENSE information for forked code

[tjhance]

By the way, the issue I mentioned last week — about having to find-and-replace a bunch of identifiers throughout the fork — I was able to workaround it so we no longer have to do that. That should simplify the forking process a lot.

[tjhance]

I added a script to apply rustc changes.

I tried to do it with subtrees. However, this turned out to be really annoying because we aren't forking the entire rustc repository, just a single directory and a few isolated files. And the rustc repository is massive with a massive history, so doing 'subtree-split' took hours.

Instead, I added a handrolled script that basically does the same thing as subtree, but it's really quick, it just makes 2 commits with all the relevant files, diffs 'em, and imports it as a commit into your local repository. Then you can cherry-pick it and resolve any conflicts. I also included instructions in our docs directory.

It's kind of jank, but it's easy to use and I think it should do the job.

[tjhance]

@dschoepe let me know if you have any comments on the fork-updating process

[dschoepe]

@dschoepe let me know if you have any comments on the fork-updating process

I'll try out the instructions for the upgrade to 1.89, hopefully next week.

[Chris-Hawblitzel]

As long as the tests pass and everyone is ok with the rust version upgrade process, this looks good to me.

[dschoepe]

Sorry for not getting back to you here. I tried the instructions and everything works, though I haven't finished the 1.89 upgrade yet.