Raise an error if old() appears in postcondition of pure functions

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

@@ -19,7 +19,7 @@ use crate::encoder::{
     },
     mir_encoder::PlaceEncoder,
     snapshot::interface::SnapshotEncoderInterface,
-    Encoder,
+    Encoder, interface::PureFunctionFormalArgsEncoderInterface,
 };
 use log::debug;
 use prusti_common::{config, vir::optimizations::functions::Simplifier, vir_local};
@@ -38,6 +38,8 @@ use vir_crate::{
     polymorphic::{self as vir, ExprIterator},
 };
 
+use super::PureFunctionEncoderInterface;
+
 pub(super) struct PureFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> {
     encoder: &'p Encoder<'v, 'tcx>,
     /// The function to be encoded.
@@ -50,7 +52,7 @@ pub(super) struct PureFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> {
     /// Span of the function declaration.
     span: Span,
     /// Signature of the function to be encoded.
-    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>>,
 }
@@ -137,6 +139,32 @@ 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> {
+    fn encoder(&self) -> &'p Encoder<'v, 'tcx> {
+        self.encoder
+    }
+
+    fn check_type(&self, var_span: Span, ty: ty::Binder<'tcx, ty::Ty<'tcx>>) -> SpannedEncodingResult<()> {
+        if !self
+            .encoder
+            .env()
+            .query
+            .type_is_copy(ty, self.parent_def_id)
+        {
+            Err(SpannedEncodingError::incorrect(
+                "pure function parameters must be Copy",
+                var_span,
+            ))
+        } else {
+            Ok(())
+        }
+    }
+
+    fn get_span(&self, local: mir::Local) -> Span {
+        self.get_local_span(local)
+    }
+}
+
 impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
     #[tracing::instrument(
         name = "PureFunctionEncoder::new",
@@ -314,7 +342,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
         let mut precondition = vec![type_precondition, func_precondition];
         let mut postcondition = vec![self.encode_postcondition_expr(&contract)?];
 
-        let formal_args = self.encode_formal_args()?;
+        let formal_args = self.encode_formal_args(self.sig)?;
         let return_type = self.encode_function_return_type()?;
 
         let res_value_range_pos = self.encoder.error_manager().register_error(
@@ -545,6 +573,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
             .replace_place(&encoded_return.into(), &pure_fn_return_variable.into())
             .set_default_pos(postcondition_pos);
 
+        if post.has_old_expression() {
+            return Err(SpannedEncodingError::incorrect(
+                "old expressions should not appear in the postconditions of pure functions",
+                self.span,
+            ));
+        }
+
         Ok(post)
     }
 
@@ -620,40 +655,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
             .with_span(self.span)
     }
 
-    fn encode_formal_args(&self) -> SpannedEncodingResult<Vec<vir::LocalVar>> {
-        let mut formal_args = vec![];
-        for local_idx in 0..self.sig.skip_binder().inputs().len() {
-            let local_ty = self.sig.input(local_idx);
-            let local = prusti_rustc_interface::middle::mir::Local::from_usize(local_idx + 1);
-            let var_name = format!("{local:?}");
-            let var_span = self.get_local_span(local);
-
-            if !self
-                .encoder
-                .env()
-                .query
-                .type_is_copy(local_ty, self.parent_def_id)
-            {
-                return Err(SpannedEncodingError::incorrect(
-                    "pure function parameters must be Copy",
-                    var_span,
-                ));
-            }
-
-            let var_type = self
-                .encoder
-                .encode_snapshot_type(local_ty.skip_binder())
-                .with_span(var_span)?;
-            formal_args.push(vir::LocalVar::new(var_name, var_type))
-        }
-        Ok(formal_args)
-    }
-
     pub fn encode_function_call_info(&self) -> SpannedEncodingResult<FunctionCallInfo> {
         Ok(FunctionCallInfo {
             name: self.encode_function_name(),
             type_arguments: self.encode_type_arguments()?,
-            formal_args: self.encode_formal_args()?,
+            formal_args: self.encode_formal_args(self.sig)?,
             return_type: self.encode_function_return_type()?,
         })
     }

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

@@ -2,6 +2,7 @@
 
 use super::encoder_poly::{FunctionCallInfo, FunctionCallInfoHigh, PureFunctionEncoder};
 use crate::encoder::{
+    Encoder,
     errors::{SpannedEncodingResult, WithSpan},
     mir::specifications::SpecificationsInterface,
     snapshot::interface::SnapshotEncoderInterface,
@@ -11,6 +12,7 @@ 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 rustc_hash::{FxHashMap, FxHashSet};
 
 use prusti_interface::specs::typed::ProcedureSpecificationKind;
@@ -331,10 +333,11 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
                 substs,
             );
 
+            let is_bodyless = self.is_trusted(proc_def_id, Some(substs))
+                || !self.env().query.has_body(proc_def_id);
+
             let maybe_identifier: SpannedEncodingResult<vir_poly::FunctionIdentifier> = (|| {
                 let proc_kind = self.get_proc_kind(proc_def_id, Some(substs));
-                let is_bodyless = self.is_trusted(proc_def_id, Some(substs))
-                    || !self.env().query.has_body(proc_def_id);
                 let mut function = if is_bodyless {
                     pure_function_encoder.encode_bodyless_function()?
                 } else {
@@ -393,13 +396,14 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
                 Err(error) => {
                     self.register_encoding_error(error);
                     debug!("Error encoding pure function: {:?}", proc_def_id);
-                    let body = self
-                        .env()
-                        .body
-                        .get_pure_fn_body(proc_def_id, substs, parent_def_id);
-                    // TODO(tymap): does stub encoder need substs?
-                    let stub_encoder = StubFunctionEncoder::new(self, proc_def_id, &body, substs);
-                    let function = stub_encoder.encode_function()?;
+                    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);
+                        encoder.encode_function()?
+                    } else {
+                        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());
                     let identifier = self.insert_function(function);
                     self.pure_function_encoder_state

prusti-viper/src/encoder/mod.rs

@@ -12,6 +12,7 @@ mod encoder;
 mod errors;
 mod foldunfold;
 mod initialisation;
+mod interface;
 mod loop_encoder;
 mod mir_encoder;
 mod mir_successor;

prusti-viper/src/encoder/stub_function_encoder.rs

@@ -4,6 +4,7 @@
 // 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,
@@ -14,57 +15,71 @@ use crate::encoder::{
 use log::debug;
 use prusti_rustc_interface::{
     hir::def_id::DefId,
-    middle::{mir, ty::GenericArgsRef},
+    middle::{mir, mir::Local, ty, ty::GenericArgsRef, ty::Binder},
+    span::Span,
 };
 use vir_crate::polymorphic as vir;
 
+use super::mir::specifications::SpecificationsInterface;
+
 pub struct StubFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> {
     encoder: &'p Encoder<'v, 'tcx>,
-    mir: &'p mir::Body<'tcx>,
-    mir_encoder: MirEncoder<'p, 'v, 'tcx>,
+    mir: Option<&'p mir::Body<'tcx>>,
+    mir_encoder: Option<MirEncoder<'p, 'v, 'tcx>>,
     proc_def_id: DefId,
     substs: GenericArgsRef<'tcx>,
+    sig: ty::PolyFnSig<'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(())
+    }
+
+    fn encoder(&self) -> &'p Encoder<'v, 'tcx> {
+        self.encoder
+    }
+
+    fn get_span(&self, _local: mir::Local) -> Span {
+        self.encoder.get_spec_span(self.proc_def_id)
+    }
 }
 
 impl<'p, 'v: 'p, 'tcx: 'v> StubFunctionEncoder<'p, 'v, 'tcx> {
     #[tracing::instrument(name = "StubFunctionEncoder::new", level = "trace", skip(encoder, mir))]
     pub fn new(
         encoder: &'p Encoder<'v, 'tcx>,
         proc_def_id: DefId,
-        mir: &'p mir::Body<'tcx>,
+        mir: Option<&'p mir::Body<'tcx>>,
         substs: GenericArgsRef<'tcx>,
+        sig: ty::PolyFnSig<'tcx>
     ) -> Self {
         StubFunctionEncoder {
             encoder,
             mir,
-            mir_encoder: MirEncoder::new(encoder, mir, proc_def_id),
+            mir_encoder: mir.map(|m| MirEncoder::new(encoder, m, proc_def_id)),
             proc_def_id,
             substs,
+            sig
         }
     }
 
+    fn default_span(&self) -> Span {
+        self.mir.map(|m| m.span).unwrap_or_else(|| self.encoder.get_spec_span(self.proc_def_id))
+    }
+
     #[tracing::instrument(level = "debug", skip(self))]
     pub fn encode_function(&self) -> SpannedEncodingResult<vir::Function> {
         let function_name = self.encode_function_name();
         debug!("Encode stub function {}", function_name);
 
-        let formal_args: Vec<_> = self
-            .mir
-            .args_iter()
-            .map(|local| {
-                let var_name = self.mir_encoder.encode_local_var_name(local);
-                let mir_type = self.mir_encoder.get_local_ty(local);
-                self.encoder
-                    .encode_snapshot_type(mir_type)
-                    .map(|var_type| vir::LocalVar::new(var_name, var_type))
-            })
-            .collect::<Result<_, _>>()
-            .with_span(self.mir.span)?;
+        let formal_args = self.encode_formal_args(self.sig)?;
 
         let type_arguments = self
             .encoder
             .encode_generic_arguments(self.proc_def_id, self.substs)
-            .with_span(self.mir.span)?;
+            .with_span(self.default_span())?;
 
         let return_type = self.encode_function_return_type()?;
 
@@ -74,8 +89,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> StubFunctionEncoder<'p, 'v, 'tcx> {
             formal_args,
             return_type,
             pres: vec![false.into()],
-            // Note: Silicon is currently unsound when declaring a function that ensures `false`
-            // See: https://github.com/viperproject/silicon/issues/376
             posts: vec![],
             body: None,
         };
@@ -94,9 +107,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> StubFunctionEncoder<'p, 'v, 'tcx> {
     }
 
     pub fn encode_function_return_type(&self) -> SpannedEncodingResult<vir::Type> {
-        let ty = self.mir.return_ty();
-        let return_local = mir::Place::return_place().as_local().unwrap();
-        let span = self.mir_encoder.get_local_span(return_local);
-        self.encoder.encode_snapshot_type(ty).with_span(span)
+        let ty = self.sig.output();
+
+        self.encoder
+            .encode_snapshot_type(ty.skip_binder())
+            .with_span(self.encoder.get_spec_span(self.proc_def_id))
     }
 }