erase asserts

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/src/lib.rs

@@ -41,6 +41,10 @@ use rustc_middle::util::Providers;
 
 rustc_fluent_macro::fluent_messages! { "../messages.ftl" }
 
+pub fn verus_provide(providers: &mut Providers) {
+    providers.thir_body = thir::cx::thir_body;
+}
+
 pub fn provide(providers: &mut Providers) {
     providers.check_match = thir::pattern::check_match;
     providers.lit_to_const = thir::constant::lit_to_const;

source/rustc_mir_build/src/thir/cx/expr.rs

@@ -258,7 +258,29 @@ impl<'tcx> Cx<'tcx> {
             }
 
             hir::ExprKind::Call(fun, ref args) => {
-                if self.typeck_results().is_method_call(expr) {
+                let fake = match &fun.kind {
+                    hir::ExprKind::Path(qpath) => {
+                        let res = self.typeck_results().qpath_res(&qpath, fun.hir_id);
+                        match res {
+                            hir::def::Res::Def(_, def_id) => {
+                                let f_name = tcx.def_path_str(def_id);
+                                if f_name == "builtin::assert_" {
+                                    Some(ExprKind::Tuple {
+                                        fields: Box::new([]),
+                                    })
+                                } else {
+                                    None
+                                }
+                            }
+                            _ => None
+                        }
+                    }
+                    _ => None
+                };
+
+                if fake.is_some() {
+                    fake.unwrap()
+                } else if self.typeck_results().is_method_call(expr) {
                     // The callee is something implementing Fn, FnMut, or FnOnce.
                     // Find the actual method implementation being called and
                     // build the appropriate UFCS call expression with the