Ugly commit 26.01.

prusti-interface/src/environment/body.rs

@@ -138,11 +138,15 @@ impl<'tcx> EnvBody<'tcx> {
     /// Get local MIR body of spec or pure functions. Retrieves the body from
     /// the compiler (relatively cheap).
     fn load_local_mir(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> MirBody<'tcx> {
-        let body = tcx
-            .mir_promoted(ty::WithOptConstParam::unknown(def_id))
-            .0
-            .borrow();
-        MirBody(Rc::new(body.clone()))
+        if config::unsafe_core_proof() {
+            Self::load_local_mir_with_facts(tcx, def_id).body
+        } else {
+            let body = tcx
+                .mir_promoted(ty::WithOptConstParam::unknown(def_id))
+                .0
+                .borrow();
+            MirBody(Rc::new(body.clone()))
+        }
     }
 
     fn get_monomorphised(
@@ -286,7 +290,13 @@ impl<'tcx> EnvBody<'tcx> {
             return body;
         }
         let body = self.pure_fns.expect(def_id);
-        self.set_monomorphised(def_id, substs, Some(caller_def_id), body, false)
+        self.set_monomorphised(
+            def_id,
+            substs,
+            Some(caller_def_id),
+            body,
+            config::unsafe_core_proof(),
+        )
     }
 
     /// Get the MIR body of a local or external expression (e.g. any spec or predicate),
@@ -304,7 +314,13 @@ impl<'tcx> EnvBody<'tcx> {
             .specs
             .get(def_id)
             .unwrap_or_else(|| self.predicates.expect(def_id));
-        self.set_monomorphised(def_id, substs, Some(caller_def_id), body, false)
+        self.set_monomorphised(
+            def_id,
+            substs,
+            Some(caller_def_id),
+            body,
+            config::unsafe_core_proof(),
+        )
     }
 
     /// Get the MIR body of a local or external spec (pres/posts/pledges/type-specs),
@@ -319,7 +335,13 @@ impl<'tcx> EnvBody<'tcx> {
             return body;
         }
         let body = self.specs.expect(def_id);
-        self.set_monomorphised(def_id, substs, Some(caller_def_id), body, false)
+        self.set_monomorphised(
+            def_id,
+            substs,
+            Some(caller_def_id),
+            body,
+            config::unsafe_core_proof(),
+        )
     }
 
     /// Get Polonius facts of a local procedure.
@@ -356,9 +378,14 @@ impl<'tcx> EnvBody<'tcx> {
 
     pub(crate) fn load_predicate_body(&mut self, def_id: LocalDefId) {
         assert!(!self.predicates.local.contains_key(&def_id));
-        self.predicates
-            .local
-            .insert(def_id, Self::load_local_mir(self.tcx, def_id));
+        self.predicates.local.insert(
+            def_id,
+            if config::unsafe_core_proof() {
+                Self::load_local_mir_with_facts(self.tcx, def_id).body
+            } else {
+                Self::load_local_mir(self.tcx, def_id)
+            },
+        );
     }
 
     pub(crate) fn load_pure_fn_body(&mut self, def_id: LocalDefId) {

prusti-viper/src/encoder/middle/core_proof/utils/place_domain_encoder.rs

@@ -93,6 +93,10 @@ pub(in super::super) trait PlaceExpressionDomainEncoder {
             vir_mid::Expression::EvalIn(expression) => {
                 self.encode_expression(&expression.body, lowerer)?
             }
+            vir_mid::Expression::AddrOf(expression) => {
+                let parent = expression.base.clone().drop_last_reference_dereference();
+                self.encode_expression(&parent, lowerer)?
+            }
             x => unimplemented!("{}", x),
         };
         Ok(result)

prusti-viper/src/encoder/mir/procedures/encoder/mod.rs

@@ -4389,7 +4389,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         bb,
                         self.def_id,
                         cl_substs,
-                        false,
+                        true,
                     )?,
                     span,
                     error_ctxt.clone(),

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

@@ -15,6 +15,7 @@ use crate::encoder::{
     Encoder,
 };
 
+use prusti_common::config;
 use prusti_rustc_interface::{
     hir::def_id::DefId,
     middle::{ty, ty::subst::SubstsRef},
@@ -213,7 +214,7 @@ pub(super) fn encode_quantifier_high<'tcx>(
                 encoded_qvars.clone(),
                 parent_def_id,
                 trigger_substs,
-                false,
+                config::unsafe_core_proof(),
             )?;
             encoded_triggers.push(encoded_trigger);
         }
@@ -228,7 +229,7 @@ pub(super) fn encode_quantifier_high<'tcx>(
         encoded_qvars.clone(),
         parent_def_id,
         body_substs,
-        false,
+        config::unsafe_core_proof(),
     )?;
 
     // TODO: implement cache-friendly qvar renaming

vir/defs/high/operations_internal/expression.rs

@@ -284,6 +284,29 @@ impl Expression {
         }
     }
 
+    pub fn drop_last_reference_dereference(self) -> Self {
+        assert!(self.is_place());
+        struct Folder {
+            found_reference_dereference: bool,
+        }
+        impl ExpressionFolder for Folder {
+            fn fold_deref_enum(&mut self, expr: Deref) -> Expression {
+                if self.found_reference_dereference {
+                    Expression::Deref(expr)
+                } else {
+                    self.found_reference_dereference = true;
+                    *expr.base
+                }
+            }
+        }
+        let mut folder = Folder {
+            found_reference_dereference: false,
+        };
+        let result = folder.fold_expression(self);
+        assert!(folder.found_reference_dereference);
+        result
+    }
+
     /// Same as `get_last_dereferenced_reference`, just returns the first
     /// reference.
     pub fn get_first_dereferenced_reference(&self) -> Option<&Expression> {