diff --git a/prusti-viper/src/encoder/middle/core_proof/references/interface.rs b/prusti-viper/src/encoder/middle/core_proof/references/interface.rs index 0dcb3e669a9..384987e6006 100644 --- a/prusti-viper/src/encoder/middle/core_proof/references/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/references/interface.rs @@ -50,6 +50,14 @@ pub(in super::super) trait ReferencesInterface { current_snapshot: vir_low::Expression, position: vir_low::Position, ) -> SpannedEncodingResult; + fn unique_reference_snapshot_constructor( + &mut self, + ty: &vir_mid::Type, + address: vir_low::Expression, + current_snapshot: vir_low::Expression, + final_snapshot: vir_low::Expression, + position: vir_low::Position, + ) -> SpannedEncodingResult; fn reference_deref_place( &mut self, place: vir_low::Expression, @@ -110,6 +118,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> ReferencesInterface for Lowerer<'p, 'v, 'tcx> { )? .set_default_position(position)) } + fn unique_reference_snapshot_constructor( + &mut self, + ty: &vir_mid::Type, + address: vir_low::Expression, + current_snapshot: vir_low::Expression, + final_snapshot: vir_low::Expression, + position: vir_low::Position, + ) -> SpannedEncodingResult { + self.ensure_type_definition(ty)?; + let domain_name = self.encode_snapshot_domain_name(ty)?; + Ok(self + .snapshot_constructor_constant_call( + // FIXME: Why is the function called “constant”? + &domain_name, + vec![address, current_snapshot, final_snapshot], + )? + .set_default_position(position)) + } fn reference_deref_place( &mut self, place: vir_low::Expression, diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/mod.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/mod.rs index 21f3d23f056..f7c1ea82761 100644 --- a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/mod.rs +++ b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/mod.rs @@ -13,6 +13,7 @@ mod validity; /// constructor. mod constructor; +#[derive(Debug, Clone)] pub(in super::super::super::super) enum PredicateKind { Owned, FracRef { diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/self_framing.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/self_framing.rs index 1d1da1eefce..6ba468b17b4 100644 --- a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/self_framing.rs +++ b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/self_framing.rs @@ -1,16 +1,19 @@ use super::PredicateKind; use crate::encoder::{ errors::{SpannedEncodingError, SpannedEncodingResult}, + high::types::HighTypeEncoderInterface, middle::core_proof::{ addresses::AddressesInterface, builtin_methods::CallContext, + lifetimes::LifetimesInterface, lowerer::{FunctionsLowererInterface, Lowerer}, places::PlacesInterface, pointers::PointersInterface, predicates::{PredicatesMemoryBlockInterface, PredicatesOwnedInterface}, + references::ReferencesInterface, snapshots::{ - into_snapshot::utils::bound_variable_stack::BoundVariableStack, IntoSnapshotLowerer, - SnapshotValuesInterface, SnapshotVariablesInterface, + into_snapshot::utils::bound_variable_stack::BoundVariableStack, IntoSnapshot, + IntoSnapshotLowerer, SnapshotValuesInterface, SnapshotVariablesInterface, }, type_layouts::TypeLayoutsInterface, }, @@ -18,7 +21,9 @@ use crate::encoder::{ use rustc_hash::FxHashMap; use std::collections::BTreeMap; use vir_crate::{ - common::{identifier::WithIdentifier, position::Positioned}, + common::{ + builtin_constants::ADDRESS_FIELD_NAME, identifier::WithIdentifier, position::Positioned, + }, low::{self as vir_low}, middle::{self as vir_mid, operations::ty::Typed}, }; @@ -209,7 +214,27 @@ impl SelfFramingAssertionToSnapshot { address: vir_low::Expression, position: vir_low::Position, ) -> SpannedEncodingResult { - match &self.predicate_kind { + self.snap_call_with_predicate_kind( + lowerer, + ty, + self.predicate_kind.clone(), + place, + address, + position, + ) + } + + // FIXME: Code duplication. + fn snap_call_with_predicate_kind<'p, 'v, 'tcx>( + &mut self, + lowerer: &mut Lowerer<'p, 'v, 'tcx>, + ty: &vir_mid::Type, + predicate_kind: PredicateKind, + place: vir_low::Expression, + address: vir_low::Expression, + position: vir_low::Position, + ) -> SpannedEncodingResult { + match predicate_kind { PredicateKind::Owned => lowerer.owned_non_aliased_snap( self.call_context(), ty, @@ -816,6 +841,111 @@ impl<'p, 'v: 'p, 'tcx: 'v> IntoSnapshotLowerer<'p, 'v, 'tcx> for SelfFramingAsse eval_in: &vir_mid::EvalIn, expect_math_bool: bool, ) -> SpannedEncodingResult { + if eval_in.context_kind == vir_mid::EvalInContextKind::SafeConstructor { + let ty = eval_in.context.get_type(); + let type_decl = lowerer.encoder.get_type_decl_mid(ty)?; + let place = &*eval_in.context; + let position = eval_in.position; + let constructor_call = match &type_decl { + vir_mid::TypeDecl::Reference(decl) => { + match decl.uniqueness { + vir_mid::ty::Uniqueness::Unique => { + // FIXME: This is currently not implemented since we + // just hope that the specification needs only the + // deref of the reference than the actual reference + // itself. + true.into() + // for (place, snap_call) in &self.snap_calls { + // eprintln!("place: {}", place); + // eprintln!(" {}", place.get_type()); + // } + // let address_place = vir_mid::Expression::field( + // place.clone(), + // vir_mid::FieldDecl::new( + // ADDRESS_FIELD_NAME, + // 0usize, + // vir_mid::Type::Int(vir_mid::ty::Int::Usize), + // ), + // position, + // ); + // let reference_type = ty.clone().unwrap_reference(); + // let target_type = *reference_type.target_type; + // let Some((_, target_address_snapshot)) = self.snap_calls.iter().find(|(place, _)| { + // place == &address_place + // }) else { + // unreachable!("Failed to find the address place: {address_place}"); + // }; + // let pointer_type = &lowerer.reference_address_type(ty)?; + // let target_address = lowerer.pointer_address( + // pointer_type, + // target_address_snapshot.clone(), + // position, + // )?; + // let lifetime = reference_type.lifetime; + // let deref_place = vir_mid::Expression::deref( + // place.clone(), + // target_type.clone(), + // position, + // ); + // let Some((_, current_snapshot)) = self.snap_calls.iter().find(|(place, _)| { + // place == &deref_place + // }) else { + // unreachable!("Failed to find the address place: {address_place}"); + // }; + // let target_place = lowerer.encode_expression_as_place(&deref_place)?; + // let lifetime = lowerer + // .encode_lifetime_const_into_procedure_variable(&lifetime)? + // .into(); + // let TODO_target_slice_len = None; + // let final_snapshot = lowerer.unique_ref_snap( + // self.call_context(), + // ty, + // ty, + // target_place, + // target_address.clone(), + // lifetime, + // TODO_target_slice_len, + // true, + // position, + // )?; + // // use vir_low::macros::*; + // // let pointer_type = &lowerer.reference_address_type(ty)?; + // // let size_of = lowerer + // // .encode_type_size_expression2(ty, &type_decl)?; + // // let bytes = lowerer + // // .encode_memory_block_bytes_expression(address.into(), size_of)?; + // // let from_bytes = self.type_to_snapshot(lowerer, pointer_type)?; + // // let pointer_snapshot = expr! { + // // Snap::from_bytes([bytes]) + // // }; + // // let target_address = lowerer.pointer_address( + // // pointer_type, + // // pointer_snapshot.clone(), + // // position, + // // )?; + // lowerer.unique_reference_snapshot_constructor( + // &target_type, + // target_address.clone(), + // current_snapshot.clone(), + // final_snapshot, + // eval_in.position, + // )? + } + vir_mid::ty::Uniqueness::Shared => todo!(), + } + } + vir_mid::TypeDecl::Struct(decl) => { + assert!(decl.structural_invariant.is_none(), "report a proper error message that structs with invariants cannot be automatically folded"); + // TODO: construct_struct_snapshot + unimplemented!("{decl}"); + } + _ => unimplemented!("{type_decl}"), + }; + self.snap_calls.push((place.clone(), constructor_call)); + let result = self.expression_to_snapshot(lowerer, &eval_in.body, expect_math_bool)?; + self.snap_calls.pop(); + return Ok(result); + } let box vir_mid::Expression::AccPredicate(predicate) = &eval_in.context else { unimplemented!("A proper error message that this must be a predicate: {}", eval_in.context); }; @@ -828,8 +958,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> IntoSnapshotLowerer<'p, 'v, 'tcx> for SelfFramingAsse .. }) = &predicate.place { + assert_eq!(eval_in.context_kind, vir_mid::EvalInContextKind::Old); (&**base, Some(label)) } else { + assert_eq!(eval_in.context_kind, vir_mid::EvalInContextKind::Predicate); (&predicate.place, None) }; let ty = predicate.place.get_type(); @@ -840,8 +972,29 @@ impl<'p, 'v: 'p, 'tcx: 'v> IntoSnapshotLowerer<'p, 'v, 'tcx> for SelfFramingAsse } else { lowerer.encode_expression_as_place_address(&predicate_place)? }; - let mut snap_call = - self.snap_call(lowerer, ty, place, address, predicate.place.position())?; + let predicate_kind = + if let Some((lifetime, uniqueness)) = predicate_place.get_dereference_kind() { + let lifetime = lowerer + .encode_lifetime_const_into_procedure_variable(lifetime)? + .into(); + match uniqueness { + vir_mid::ty::Uniqueness::Unique => PredicateKind::UniqueRef { + lifetime, + is_final: false, + }, + vir_mid::ty::Uniqueness::Shared => PredicateKind::FracRef { lifetime }, + } + } else { + PredicateKind::Owned + }; + let mut snap_call = self.snap_call_with_predicate_kind( + lowerer, + ty, + predicate_kind, + place, + address, + predicate.place.position(), + )?; if let Some(old_label) = old_label { snap_call = vir_low::Expression::labelled_old( Some(old_label.to_string()),