Use MIR without regions for pure functions.

Author: vakaras

prusti-interface/src/environment/body.rs

@@ -1,4 +1,3 @@
-use prusti_common::config;
 use prusti_rustc_interface::{
     macros::{TyDecodable, TyEncodable},
     middle::{
@@ -321,15 +320,11 @@ impl<'tcx> EnvBody<'tcx> {
 
     pub(crate) fn load_pure_fn_body(&mut self, def_id: LocalDefId) {
         assert!(!self.pure_fns.local.contains_key(&def_id));
-        if config::no_verify() {
-            let body = Self::load_local_mir(self.tcx, def_id);
-            self.pure_fns.local.insert(def_id, body);
-        } else {
-            let bwbf = Self::load_local_mir_with_facts(self.tcx, def_id);
-            self.pure_fns.local.insert(def_id, bwbf.body.clone());
-            // Also add to `impure_fns` since we'll also be encoding this as impure
-            self.local_impure_fns.borrow_mut().insert(def_id, bwbf);
-        }
+        let body = Self::load_local_mir(self.tcx, def_id);
+        self.pure_fns.local.insert(def_id, body);
+        let bwbf = Self::load_local_mir_with_facts(self.tcx, def_id);
+        // Also add to `impure_fns` since we'll also be encoding this as impure
+        self.local_impure_fns.borrow_mut().insert(def_id, bwbf);
     }
 
     pub(crate) fn load_closure_body(&mut self, def_id: LocalDefId) {

prusti-viper/src/encoder/mir/errors/interface.rs

@@ -27,12 +27,12 @@ pub(crate) trait ErrorInterface {
         error_ctxt: ErrorCtxt,
     ) -> vir_high::Position;
     fn set_surrounding_error_context(
-        &mut self,
+        &self,
         position: vir_high::Position,
         error_ctxt: ErrorCtxt,
     ) -> vir_high::Position;
     fn set_surrounding_error_context_for_expression(
-        &mut self,
+        &self,
         expression: vir_high::Expression,
         default_position: vir_high::Position,
         error_ctxt: ErrorCtxt,
@@ -93,7 +93,7 @@ impl<'v, 'tcx: 'v> ErrorInterface for super::super::super::Encoder<'v, 'tcx> {
         new_position.into()
     }
     fn set_surrounding_error_context(
-        &mut self,
+        &self,
         position: vir_high::Position,
         error_ctxt: ErrorCtxt,
     ) -> vir_high::Position {
@@ -106,14 +106,14 @@ impl<'v, 'tcx: 'v> ErrorInterface for super::super::super::Encoder<'v, 'tcx> {
     /// 1. `default_position` if `position.is_default()`.
     /// 2. With surrounding error context otherwise.
     fn set_surrounding_error_context_for_expression(
-        &mut self,
+        &self,
         expression: vir_high::Expression,
         default_position: vir_high::Position,
         error_ctxt: ErrorCtxt,
     ) -> vir_high::Expression {
         assert!(!default_position.is_default());
         struct Visitor<'p, 'v: 'p, 'tcx: 'v> {
-            encoder: &'p mut super::super::super::Encoder<'v, 'tcx>,
+            encoder: &'p super::super::super::Encoder<'v, 'tcx>,
             default_position: vir_high::Position,
             error_ctxt: ErrorCtxt,
         }

prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs

@@ -3,6 +3,7 @@ use crate::encoder::{
     errors::{ErrorCtxt, SpannedEncodingError, SpannedEncodingResult, WithSpan},
     mir::{
         contracts::{ContractsEncoderInterface, ProcedureContractMirDef},
+        errors::ErrorInterface,
         generics::MirGenericsEncoderInterface,
         pure::{
             interpreter::{
@@ -341,11 +342,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> {
                 self.parent_def_id,
                 assertion_substs,
             )?;
-            self.encoder.error_manager().set_error(
-                encoded_assertion.position().into(),
+            let original_position = encoded_assertion.position();
+            conjuncts.push(self.encoder.set_surrounding_error_context_for_expression(
+                encoded_assertion,
+                original_position,
                 ErrorCtxt::PureFunctionDefinition,
-            );
-            conjuncts.push(encoded_assertion);
+            ));
         }
         Ok(conjuncts.into_iter().conjoin())
     }

prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs

@@ -479,10 +479,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
                 self.parent_def_id,
                 assertion_substs,
             )?;
-            self.encoder
-                .error_manager()
-                .set_error(encoded_assertion.pos(), ErrorCtxt::PureFunctionDefinition);
-            func_spec.push(encoded_assertion);
+            let new_pos = self.encoder.error_manager().set_surrounding_error_context(
+                encoded_assertion.pos(),
+                ErrorCtxt::PureFunctionDefinition,
+            );
+            func_spec.push(encoded_assertion.set_pos(new_pos));
         }
 
         Ok((

prusti-viper/src/encoder/procedure_encoder.rs

@@ -5511,10 +5511,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
         } else {
             // FIXME: why are we getting the MIR body for this?
-            let mir = self.encoder.env().body.get_impure_fn_body(
+            let mir = self.encoder.env().body.get_impure_fn_body_identity(
                 containing_def_id.expect_local(),
-                // TODO(tymap): identity substs here are probably wrong?
-                self.encoder.env().query.identity_substs(containing_def_id),
             );
             let return_ty = mir.return_ty();
             let arg_tys = mir.args_iter().map(|arg| mir.local_decls[arg].ty).collect();