Proof of concept for erasure-by-THIR modification.

source/rust_verify/Cargo.toml

@@ -20,6 +20,7 @@ internals_interface = { path = "../tools/internals_interface" }
 indicatif = "0.17.7"
 console = { version = "0.15", default-features = false, features = ["ansi-parsing"] }
 indexmap = { version = "1" }
+rustc_mir_build_verus = { path = "../rustc_mir_build" }
 
 [target.'cfg(windows)'.dependencies]
 win32job = "1"

source/rust_verify/src/config.rs

@@ -109,6 +109,7 @@ pub struct ArgsX {
     pub solver: SmtSolver,
     #[cfg(feature = "axiom-usage-info")]
     pub axiom_usage_info: bool,
+    pub new_lifetime: bool,
 }
 
 impl ArgsX {
@@ -153,6 +154,7 @@ impl ArgsX {
             solver: Default::default(),
             #[cfg(feature = "axiom-usage-info")]
             axiom_usage_info: Default::default(),
+            new_lifetime: Default::default(),
         }
     }
 }
@@ -211,6 +213,7 @@ pub fn parse_args_with_imports(
     const OPT_NO_EXTERNAL_BY_DEFAULT: &str = "no-external-by-default";
     const OPT_NO_VERIFY: &str = "no-verify";
     const OPT_NO_LIFETIME: &str = "no-lifetime";
+    const OPT_NEW_LIFETIME: &str = "new-lifetime";
     const OPT_NO_AUTO_RECOMMENDS_CHECK: &str = "no-auto-recommends-check";
     const OPT_TIME: &str = "time";
     const OPT_TIME_EXPANDED: &str = "time-expanded";
@@ -359,6 +362,7 @@ pub fn parse_args_with_imports(
     opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]");
     opts.optflag("", OPT_NO_VERIFY, "Do not run verification");
     opts.optflag("", OPT_NO_LIFETIME, "Do not run lifetime checking on proofs");
+    opts.optflag("", OPT_NEW_LIFETIME, "New lifetime checking");
     opts.optflag(
         "",
         OPT_NO_AUTO_RECOMMENDS_CHECK,
@@ -561,6 +565,7 @@ pub fn parse_args_with_imports(
         no_external_by_default: matches.opt_present(OPT_NO_EXTERNAL_BY_DEFAULT),
         no_verify: matches.opt_present(OPT_NO_VERIFY),
         no_lifetime: matches.opt_present(OPT_NO_LIFETIME),
+        new_lifetime: matches.opt_present(OPT_NEW_LIFETIME),
         no_auto_recommends_check: matches.opt_present(OPT_NO_AUTO_RECOMMENDS_CHECK),
         time: matches.opt_present(OPT_TIME) || matches.opt_present(OPT_TIME_EXPANDED),
         time_expanded: matches.opt_present(OPT_TIME_EXPANDED),

source/rust_verify/src/verifier.rs

@@ -2816,25 +2816,34 @@ fn hir_crate<'tcx>(tcx: TyCtxt<'tcx>, _: ()) -> rustc_hir::Crate<'tcx> {
 
 impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
     fn config(&mut self, config: &mut rustc_interface::interface::Config) {
-        config.override_queries = Some(|_session, providers| {
-            providers.hir_crate = hir_crate;
-
-            // Hooking mir_const_qualif solves constness issue in function body,
-            // but const-eval will still do check-const when evaluating const
-            // value. Thus const_header_wrapper is still needed.
-            providers.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default();
-            // Prevent the borrow checker from running, as we will run our own lifetime analysis.
-            // Stopping after `after_expansion` used to be enough, but now borrow check is triggered
-            // by const evaluation through the mir interpreter.
-            providers.mir_borrowck = |tcx, _local_def_id| {
-                tcx.arena.alloc(rustc_middle::mir::BorrowCheckResult {
-                    concrete_opaque_types: rustc_data_structures::fx::FxIndexMap::default(),
-                    closure_requirements: None,
-                    used_mut_upvars: smallvec::SmallVec::new(),
-                    tainted_by_errors: None,
-                })
-            };
-        });
+        if !self.verifier.args.new_lifetime {
+            config.override_queries = Some(|_session, providers| {
+                providers.hir_crate = hir_crate;
+
+                // Hooking mir_const_qualif solves constness issue in function body,
+                // but const-eval will still do check-const when evaluating const
+                // value. Thus const_header_wrapper is still needed.
+                providers.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default();
+
+                // Prevent the borrow checker from running, as we will run our own lifetime analysis.
+                // Stopping after `after_expansion` used to be enough, but now borrow check is triggered
+                // by const evaluation through the mir interpreter.
+                providers.mir_borrowck = |tcx, _local_def_id| {
+                    tcx.arena.alloc(rustc_middle::mir::BorrowCheckResult {
+                        concrete_opaque_types: rustc_data_structures::fx::FxIndexMap::default(),
+                        closure_requirements: None,
+                        used_mut_upvars: smallvec::SmallVec::new(),
+                        tainted_by_errors: None,
+                    })
+                };
+            });
+        } else {
+            config.override_queries = Some(|_session, providers| {
+                providers.hir_crate = hir_crate;
+                providers.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default();
+                rustc_mir_build_verus::verus_provide(providers);
+            });
+        }
     }
 
     fn after_expansion<'tcx>(
@@ -3004,6 +3013,10 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
                 }
             );
         }
-        rustc_driver::Compilation::Stop
+        if self.verifier.args.new_lifetime {
+            rustc_driver::Compilation::Continue
+        } else {
+            rustc_driver::Compilation::Stop
+        }
     }
 }

source/rustc_mir_build/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "rustc_mir_build_verus"
+version = "0.0.0"
+edition = "2021"
+
+[dependencies]
+# tidy-alphabetical-start
+itertools = "0.12"
+tracing = "0.1"
+# tidy-alphabetical-end