rustfmt, commit more files

prusti-viper/src/encoder/interface.rs

@@ -0,0 +1,56 @@
+use crate::encoder::{
+    errors::{SpannedEncodingResult, WithSpan},
+    mir::specifications::SpecificationsInterface,
+    snapshot::interface::SnapshotEncoderInterface,
+    stub_function_encoder::StubFunctionEncoder,
+    Encoder,
+};
+use log::{debug, trace};
+use prusti_common::config;
+use prusti_interface::data::ProcedureDefId;
+use prusti_rustc_interface::{
+    middle::{
+        mir, ty,
+        ty::{Binder, GenericArgsRef},
+    },
+    span::Span,
+};
+use rustc_hash::{FxHashMap, FxHashSet};
+
+use prusti_interface::specs::typed::ProcedureSpecificationKind;
+use std::cell::RefCell;
+use vir_crate::{common::identifier::WithIdentifier, high as vir_high, polymorphic as vir_poly};
+
+pub(crate) trait PureFunctionFormalArgsEncoderInterface<'p, 'v: 'p, 'tcx: 'v> {
+    fn encoder(&self) -> &'p Encoder<'v, 'tcx>;
+
+    fn check_type(
+        &self,
+        var_span: Span,
+        ty: Binder<'tcx, ty::Ty<'tcx>>,
+    ) -> SpannedEncodingResult<()>;
+
+    fn get_span(&self, local: mir::Local) -> Span;
+
+    fn encode_formal_args(
+        &self,
+        sig: ty::PolyFnSig<'tcx>,
+    ) -> SpannedEncodingResult<Vec<vir_poly::LocalVar>> {
+        let mut formal_args = vec![];
+        for local_idx in 0..sig.skip_binder().inputs().len() {
+            let local_ty = sig.input(local_idx);
+            let local = mir::Local::from_usize(local_idx + 1);
+            let var_name = format!("{local:?}");
+            let var_span = self.get_span(local);
+
+            self.check_type(var_span, local_ty)?;
+
+            let var_type = self
+                .encoder()
+                .encode_snapshot_type(local_ty.skip_binder())
+                .with_span(var_span)?;
+            formal_args.push(vir_poly::LocalVar::new(var_name, var_type))
+        }
+        Ok(formal_args)
+    }
+}

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

@@ -7,6 +7,7 @@
 use crate::encoder::{
     errors::{ErrorCtxt, SpannedEncodingError, SpannedEncodingResult, WithSpan},
     high::{generics::HighGenericsEncoderInterface, types::HighTypeEncoderInterface},
+    interface::PureFunctionFormalArgsEncoderInterface,
     mir::{
         contracts::{ContractsEncoderInterface, ProcedureContract},
         pure::{
@@ -19,7 +20,7 @@ use crate::encoder::{
     },
     mir_encoder::PlaceEncoder,
     snapshot::interface::SnapshotEncoderInterface,
-    Encoder, interface::PureFunctionFormalArgsEncoderInterface,
+    Encoder,
 };
 use log::debug;
 use prusti_common::{config, vir::optimizations::functions::Simplifier, vir_local};
@@ -52,7 +53,7 @@ pub(super) struct PureFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> {
     /// Span of the function declaration.
     span: Span,
     /// Signature of the function to be encoded.
-    pub (crate) sig: ty::PolyFnSig<'tcx>,
+    pub(crate) sig: ty::PolyFnSig<'tcx>,
     /// Spans of MIR locals, when encoding a local pure function.
     local_spans: Option<Vec<Span>>,
 }
@@ -139,12 +140,18 @@ fn encode_mir<'p, 'v: 'p, 'tcx: 'v>(
     Ok(body_expr)
 }
 
-impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionFormalArgsEncoderInterface<'p, 'v, 'tcx> for PureFunctionEncoder<'p, 'v, 'tcx> {
+impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionFormalArgsEncoderInterface<'p, 'v, 'tcx>
+    for PureFunctionEncoder<'p, 'v, 'tcx>
+{
     fn encoder(&self) -> &'p Encoder<'v, 'tcx> {
         self.encoder
     }
 
-    fn check_type(&self, var_span: Span, ty: ty::Binder<'tcx, ty::Ty<'tcx>>) -> SpannedEncodingResult<()> {
+    fn check_type(
+        &self,
+        var_span: Span,
+        ty: ty::Binder<'tcx, ty::Ty<'tcx>>,
+    ) -> SpannedEncodingResult<()> {
         if !self
             .encoder
             .env()
@@ -538,6 +545,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
         let encoded_return = self.encode_local(contract.returned_value.into())?;
         debug!("encoded_return: {:?}", encoded_return);
 
+        eprintln!("IN IT");
+
         for (assertion, assertion_substs) in
             contract.functional_postcondition(self.encoder.env(), self.substs)
         {

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

@@ -2,17 +2,19 @@
 
 use super::encoder_poly::{FunctionCallInfo, FunctionCallInfoHigh, PureFunctionEncoder};
 use crate::encoder::{
-    Encoder,
     errors::{SpannedEncodingResult, WithSpan},
     mir::specifications::SpecificationsInterface,
     snapshot::interface::SnapshotEncoderInterface,
     stub_function_encoder::StubFunctionEncoder,
+    Encoder,
 };
 use log::{debug, trace};
 use prusti_common::config;
 use prusti_interface::data::ProcedureDefId;
-use prusti_rustc_interface::middle::{mir, ty, ty::GenericArgsRef};
-use prusti_rustc_interface::span::Span;
+use prusti_rustc_interface::{
+    middle::{mir, ty, ty::GenericArgsRef},
+    span::Span,
+};
 use rustc_hash::{FxHashMap, FxHashSet};
 
 use prusti_interface::specs::typed::ProcedureSpecificationKind;
@@ -397,11 +399,26 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
                     self.register_encoding_error(error);
                     debug!("Error encoding pure function: {:?}", proc_def_id);
                     let function = if !is_bodyless {
-                        let pure_fn_body = self.env().body.get_pure_fn_body(proc_def_id, substs, parent_def_id);
-                        let encoder = StubFunctionEncoder::new(self, proc_def_id, Some(&pure_fn_body), substs, pure_function_encoder.sig);
+                        let pure_fn_body =
+                            self.env()
+                                .body
+                                .get_pure_fn_body(proc_def_id, substs, parent_def_id);
+                        let encoder = StubFunctionEncoder::new(
+                            self,
+                            proc_def_id,
+                            Some(&pure_fn_body),
+                            substs,
+                            pure_function_encoder.sig,
+                        );
                         encoder.encode_function()?
                     } else {
-                        let encoder = StubFunctionEncoder::new(self, proc_def_id, None, substs, pure_function_encoder.sig);
+                        let encoder = StubFunctionEncoder::new(
+                            self,
+                            proc_def_id,
+                            None,
+                            substs,
+                            pure_function_encoder.sig,
+                        );
                         encoder.encode_function()?
                     };
                     self.log_vir_program_before_viper(function.to_string());

prusti-viper/src/encoder/stub_function_encoder.rs

@@ -4,18 +4,23 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use crate::encoder::interface::PureFunctionFormalArgsEncoderInterface;
 use crate::encoder::{
     errors::{SpannedEncodingResult, WithSpan},
     high::generics::HighGenericsEncoderInterface,
+    interface::PureFunctionFormalArgsEncoderInterface,
     mir_encoder::{MirEncoder, PlaceEncoder},
     snapshot::interface::SnapshotEncoderInterface,
     Encoder,
 };
 use log::debug;
 use prusti_rustc_interface::{
     hir::def_id::DefId,
-    middle::{mir, mir::Local, ty, ty::GenericArgsRef, ty::Binder},
+    middle::{
+        mir,
+        mir::Local,
+        ty,
+        ty::{Binder, GenericArgsRef},
+    },
     span::Span,
 };
 use vir_crate::polymorphic as vir;
@@ -28,11 +33,12 @@ pub struct StubFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> {
     mir_encoder: Option<MirEncoder<'p, 'v, 'tcx>>,
     proc_def_id: DefId,
     substs: GenericArgsRef<'tcx>,
-    sig: ty::PolyFnSig<'tcx>
+    sig: ty::PolyFnSig<'tcx>,
 }
 
-impl <'p, 'v, 'tcx> PureFunctionFormalArgsEncoderInterface<'p, 'v, 'tcx> for StubFunctionEncoder<'p, 'v, 'tcx> {
-
+impl<'p, 'v, 'tcx> PureFunctionFormalArgsEncoderInterface<'p, 'v, 'tcx>
+    for StubFunctionEncoder<'p, 'v, 'tcx>
+{
     fn check_type(&self, _span: Span, _ty: Binder<ty::Ty<'tcx>>) -> SpannedEncodingResult<()> {
         Ok(())
     }
@@ -53,20 +59,22 @@ impl<'p, 'v: 'p, 'tcx: 'v> StubFunctionEncoder<'p, 'v, 'tcx> {
         proc_def_id: DefId,
         mir: Option<&'p mir::Body<'tcx>>,
         substs: GenericArgsRef<'tcx>,
-        sig: ty::PolyFnSig<'tcx>
+        sig: ty::PolyFnSig<'tcx>,
     ) -> Self {
         StubFunctionEncoder {
             encoder,
             mir,
             mir_encoder: mir.map(|m| MirEncoder::new(encoder, m, proc_def_id)),
             proc_def_id,
             substs,
-            sig
+            sig,
         }
     }
 
     fn default_span(&self) -> Span {
-        self.mir.map(|m| m.span).unwrap_or_else(|| self.encoder.get_spec_span(self.proc_def_id))
+        self.mir
+            .map(|m| m.span)
+            .unwrap_or_else(|| self.encoder.get_spec_span(self.proc_def_id))
     }
 
     #[tracing::instrument(level = "debug", skip(self))]

vir/defs/polymorphic/ast/expr.rs

@@ -1454,6 +1454,20 @@ impl Expr {
         PlaceReplacer { replacements }.fold(self)
     }
 
+    pub fn has_old_expression(&self) -> bool {
+        struct OldFinder {
+            has_old: bool,
+        }
+        impl ExprWalker for OldFinder {
+            fn walk_labelled_old(&mut self, _labelled_old: &LabelledOld) {
+                self.has_old = true;
+            }
+        }
+        let mut walker = OldFinder { has_old: false };
+        walker.walk(self);
+        walker.has_old
+    }
+
     /// Replaces expressions like `old[l5](old[l5](_9.val_ref).foo.bar)`
     /// into `old[l5](_9.val_ref.foo.bar)`
     #[must_use]