diff --git a/prusti-encoder/src/encoders/const.rs b/prusti-encoder/src/encoders/const.rs index a540b54d5c4..08bbfffa27e 100644 --- a/prusti-encoder/src/encoders/const.rs +++ b/prusti-encoder/src/encoders/const.rs @@ -73,25 +73,13 @@ impl TaskEncoder for ConstEnc { assert_eq!(s.field_snaps_to_snap.arity().args().len(), 0); vir::with_vcx(|vcx| s.field_snaps_to_snap.apply(vcx, &[])) } - // Encode `&str` constants to an opaque domain. If we ever want to perform string reasoning + // Encode `&str` constants to null references. If we ever want to perform string reasoning // we will need to revisit this encoding, but for the moment this allows assertions to avoid // crashing Prusti. ConstValue::Slice { .. } if ty.peel_refs().is_str() => { - let ref_ty = kind.expect_structlike(); - let str_ty = ty.peel_refs(); - let str_snap = deps - .require_local::(str_ty)? - .generic_snapshot - .specifics - .expect_structlike(); - let cast = deps.require_local::>(str_ty)?; + let ref_ty = kind.expect_ref(); vir::with_vcx(|vcx| { - // first, we create a string snapshot - let snap = str_snap.field_snaps_to_snap.apply(vcx, &[]); - // upcast it to a param - let snap = cast.cast_to_generic_if_necessary(vcx, snap); - // wrap it in a ref - ref_ty.field_snaps_to_snap.apply(vcx, &[snap]) + ref_ty.snap_to_prim.apply(vcx, [vcx.mk_null()]) }) } ConstValue::Slice { .. } => todo!("ConstValue::Slice : {:?}", const_.ty()), diff --git a/prusti-encoder/src/encoders/mir_impure.rs b/prusti-encoder/src/encoders/mir_impure.rs index 15d53737419..69fd631cf72 100644 --- a/prusti-encoder/src/encoders/mir_impure.rs +++ b/prusti-encoder/src/encoders/mir_impure.rs @@ -454,19 +454,23 @@ impl<'vir, 'enc, E: TaskEncoder> ImpureEncVisitor<'vir, 'enc, E> { .deps .require_ref::(place_ty.ty) .unwrap(); - let ref_field = e_ty.generic_predicate.expect_ref().ref_field; - let expr = self.vcx.mk_field_expr(expr, ref_field); + let projection_p = e_ty.generic_predicate.expect_ref().ref_to_deref; + let expr_deref = projection_p.apply(self.vcx, [expr]); + // TODO: we are writing directly to the deref; is a cast ever + // needed? + /* let inner_ty = place_ty.ty.builtin_deref(true).unwrap(); if let Some(cast_stmts) = self .deps .require_local::>(inner_ty) .unwrap() - .cast_to_concrete_if_possible(self.vcx, expr) + .cast_to_concrete_if_possible(self.vcx, expr_deref) { self.stmt(cast_stmts.apply_cast_stmt); - return (expr, Some(cast_stmts.unapply_cast_stmt)); + return (expr_deref, Some(cast_stmts.unapply_cast_stmt)); } - (expr, None) + */ + (expr_deref, None) } _ => todo!("Unsupported ProjectionElem {:?}", elem), } @@ -726,27 +730,10 @@ impl<'vir, 'enc, E: TaskEncoder> mir::visit::Visitor<'vir> for ImpureEncVisitor< } mir::Rvalue::Ref(_reg, _kind, place) => { let e_rvalue_ty = self.deps.require_ref::(rvalue_ty).unwrap(); - - let place_ty = place.ty(self.local_decls, self.vcx.tcx()); - let ty = self.deps.require_ref::(place_ty.ty).unwrap(); let place_expr = self.encode_place(Place::from(*place)).expr; - eprintln!("{rvalue_ty:?} {place_ty:?}"); - let cast = self - .deps - .require_local::>(place_ty.ty) - .unwrap(); - let inner = e_rvalue_ty.generic_predicate.expect_ref(); - let generic = cast.cast_to_generic_if_necessary(self.vcx, ty.ref_to_snap(self.vcx, place_expr)); - - eprintln!("{place_expr:?} -> {generic:?}"); - let ref_ = inner.snap_data.field_snaps_to_snap.apply(self.vcx, &[generic]); - eprintln!("{ref_:?}"); - // e_rvalue_ty.generic_predicate.expect_ref().snap_data.field_snaps_to_snap.apply(self.vcx, inner_ref_to_args); - // e_rvalue_ty.ref_to_snap(self.vcx, place_expr) - ref_ + inner.snap_data.snap_to_prim.apply(self.vcx, [place_expr]) } - // TODO: HERE IS THE CODE TO WRITE Xavier //mir::Rvalue::Discriminant(Place<'vir>) => {} //mir::Rvalue::ShallowInitBox(Operand<'vir>, Ty<'vir>) => {} diff --git a/prusti-encoder/src/encoders/type/domain.rs b/prusti-encoder/src/encoders/type/domain.rs index 242d212d305..b1071b6d08b 100644 --- a/prusti-encoder/src/encoders/type/domain.rs +++ b/prusti-encoder/src/encoders/type/domain.rs @@ -36,6 +36,13 @@ pub struct DomainDataPrim<'vir> { pub prim_to_snap: FunctionIdent<'vir, UnaryArity<'vir>>, } #[derive(Clone, Copy, Debug)] +pub struct DomainDataRef<'vir> { + /// Construct domain from snapshot of referee and the `Ref` value. + pub snap_to_prim: FunctionIdent<'vir, UnaryArity<'vir>>, + /// Function to access the referee. + pub deref_access: FunctionIdent<'vir, UnaryArity<'vir>>, +} +#[derive(Clone, Copy, Debug)] pub struct DomainDataStruct<'vir> { /// Construct domain from snapshots of fields or for primitive types /// from the single Viper primitive value. @@ -72,6 +79,7 @@ pub enum DiscrBounds<'vir> { pub enum DomainEncSpecifics<'vir> { Param, Primitive(DomainDataPrim<'vir>), + Ref(DomainDataRef<'vir>), // structs, tuples StructLike(DomainDataStruct<'vir>), EnumLike(Option>), @@ -87,8 +95,8 @@ pub struct DomainEncOutputRef<'vir> { } impl<'vir> DomainEncOutputRef<'vir> { - /// Takes as input a snapshot encoding of a rust value, and returns - /// the `idx`th type parameter of it's type. + /// Takes as input a snapshot encoding of a Rust value, and returns + /// the `idx`th type parameter of its type. pub fn ty_param_from_snap( &self, vcx: &'vir vir::VirCtxt, @@ -273,15 +281,11 @@ impl TaskEncoder for DomainEnc { let specifics = enc.mk_enum_specifics(None); Ok((Some(enc.finalize(task_key)), specifics)) } - &TyKind::Ref(_, inner, _) => { - let generics = vec![deps - .require_local::>(inner)? - .expect_generic()]; - let mut enc = DomainEncData::new(vcx, task_key, generics, deps); + &TyKind::Ref(..) => { + let mut enc = DomainEncData::new(vcx, task_key, Vec::new(), deps); enc.deps .emit_output_ref(*task_key, enc.output_ref(base_name))?; - let field_tys = vec![FieldTy::from_ty(vcx, enc.deps, inner)?]; - let specifics = enc.mk_struct_specifics(field_tys); + let specifics = enc.mk_ref_specifics(); Ok((Some(enc.finalize(task_key)), specifics)) } &TyKind::Param(_) => { @@ -431,6 +435,23 @@ impl<'vir, 'enc> DomainEncData<'vir, 'enc> { } DomainEncSpecifics::Primitive(specifics) } + pub fn mk_ref_specifics(&mut self) -> DomainEncSpecifics<'vir> { + let data = self.mk_field_functions( + &[FieldTy { + ty: &vir::TypeData::Ref, + rust_ty_data: None, + }], + None, + false, + ); + let snap_to_prim = data.field_snaps_to_snap.to_known(); + let deref_access = data.field_access[0].read; + let specifics = DomainDataRef { + snap_to_prim, + deref_access, + }; + DomainEncSpecifics::Ref(specifics) + } pub fn mk_struct_specifics(&mut self, fields: Vec>) -> DomainEncSpecifics<'vir> { let specifics = self.mk_field_functions(&fields, None, false); DomainEncSpecifics::StructLike(specifics) @@ -835,6 +856,12 @@ impl<'vir> DomainEncSpecifics<'vir> { _ => panic!("expected primitive"), } } + pub fn expect_ref(self) -> DomainDataRef<'vir> { + match self { + Self::Ref(data) => data, + _ => panic!("expected ref"), + } + } pub fn expect_structlike(self) -> DomainDataStruct<'vir> { match self { Self::StructLike(data) => data, diff --git a/prusti-encoder/src/encoders/type/most_generic_ty.rs b/prusti-encoder/src/encoders/type/most_generic_ty.rs index 74a07adda75..688edfcbcdd 100644 --- a/prusti-encoder/src/encoders/type/most_generic_ty.rs +++ b/prusti-encoder/src/encoders/type/most_generic_ty.rs @@ -101,7 +101,7 @@ impl<'tcx> MostGenericTy<'tcx> { TyKind::Tuple(tys) => tys.iter().map(as_param_ty).collect::>(), TyKind::Array(orig, _) => vec![as_param_ty(*orig)], TyKind::Slice(orig) => vec![as_param_ty(*orig)], - TyKind::Ref(_, orig, _) => vec![as_param_ty(*orig)], + TyKind::Ref(_, _, _) => vec![], TyKind::Bool | TyKind::Char | TyKind::Float(_) @@ -164,10 +164,10 @@ pub fn extract_type_params<'tcx>( let ty = tcx.mk_ty_from_kind(TyKind::Slice(ty)); (MostGenericTy(ty), vec![orig]) } - TyKind::Ref(_, orig, m) => { + TyKind::Ref(_, _, m) => { let ty = to_placeholder(tcx, None); let ty = tcx.mk_ty_from_kind(TyKind::Ref(tcx.lifetimes.re_erased, ty, m)); - (MostGenericTy(ty), vec![orig]) + (MostGenericTy(ty), Vec::new()) } TyKind::Param(_) => (MostGenericTy(to_placeholder(tcx, None)), Vec::new()), TyKind::Bool diff --git a/prusti-encoder/src/encoders/type/predicate.rs b/prusti-encoder/src/encoders/type/predicate.rs index 9e6a1d35cf9..1209ab763e5 100644 --- a/prusti-encoder/src/encoders/type/predicate.rs +++ b/prusti-encoder/src/encoders/type/predicate.rs @@ -4,8 +4,7 @@ use prusti_rustc_interface::{ }; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{ - add_debug_note, CallableIdent, FunctionIdent, MethodIdent, NullaryArity, PredicateIdent, - TypeData, UnaryArity, UnknownArity, VirCtxt, + add_debug_note, CallableIdent, DomainParamData, FunctionIdent, MethodIdent, NullaryArity, PredicateIdent, TypeData, UnaryArity, UnknownArity, VirCtxt }; /// Takes a `MostGenericTy` and returns various Viper predicates and functions for @@ -43,8 +42,9 @@ pub struct PredicateEncDataVariant<'vir> { #[derive(Clone, Copy, Debug)] pub struct PredicateEncDataRef<'vir> { pub ref_field: vir::Field<'vir>, - pub perm: Option>, - pub snap_data: DomainDataStruct<'vir>, + pub snap_data: DomainDataRef<'vir>, + /// Ref to self as argument. Returns Ref to borrowed place. + pub ref_to_deref: FunctionIdent<'vir, UnaryArity<'vir>>, } #[derive(Clone, Copy, Debug)] @@ -181,7 +181,7 @@ pub struct PredicateEncOutput<'vir> { use crate::encoders::GenericEnc; use super::{ - domain::{DiscrBounds, DomainDataEnum, DomainDataPrim, DomainDataStruct}, + domain::{DiscrBounds, DomainDataEnum, DomainDataPrim, DomainDataRef, DomainDataStruct}, lifted::{ generic::LiftedGeneric, ty::{EncodeGenericsAsLifted, LiftedTy, LiftedTyEnc}, @@ -374,18 +374,19 @@ impl TaskEncoder for PredicateEnc { Ok((enc.mk_enum(None), ())) } - &TyKind::Ref(_, inner, m) => { - let snap_data = snap.specifics.expect_structlike(); - let specifics = enc.mk_ref_ref(snap_data, m.is_mut()); + &TyKind::Ref(..) => { + // Unlike other types, we don't want to encode the generics of + // a reference as type arguments, so here we construct the + // encoder helper again, but with no generics passed. + enc = vir::with_vcx(|vcx| { + PredicateEncValues::new(vcx, &snap.base_name, snap.snapshot, &[]) + }); + + let snap_data = snap.specifics.expect_ref(); + let specifics = enc.mk_ref_ref(snap_data); deps.emit_output_ref(*task_key, enc.output_ref(PredicateEncData::Ref(specifics)))?; - let lifted_ty = deps - .require_local::>(inner) - .unwrap(); - let inner = deps - .require_ref::(inner)? - .generic_predicate; - Ok((enc.mk_ref(inner, lifted_ty, specifics), ())) + Ok((enc.mk_ref(specifics), ())) } TyKind::Str => { let specifics = enc.mk_struct_ref(None, snap.specifics.expect_structlike()); @@ -545,21 +546,38 @@ impl<'vir, 'tcx> PredicateEncValues<'vir, 'tcx> { } pub fn mk_ref_ref( &mut self, - snap_data: DomainDataStruct<'vir>, - mutbl: bool, + snap_data: DomainDataRef<'vir>, ) -> PredicateEncDataRef<'vir> { let name = vir::vir_format_identifier!(self.vcx, "{}_ref", self.ref_to_pred.name()); let ref_field = self.vcx.mk_field(name.to_str(), &vir::TypeData::Ref); self.fields.push(ref_field); - let perm = if mutbl { - None - } else { - Some(self.vcx.mk_wildcard()) - }; + let name = vir::vir_format_identifier!( + self.vcx, + "{}_deref", + self.ref_to_pred.name(), + ); + + let field = self.vcx.mk_function( + name.to_str(), + self.self_decl, + &vir::TypeData::Ref, + self.vcx + .alloc_slice(&[self.vcx.mk_predicate_app_expr(self.self_pred_read)]), + &[], + Some(self.vcx + .mk_unfolding_expr(self.self_pred_read, self.vcx.mk_field_expr(self.self_ex, ref_field))), + ); + self.ref_to_field_refs.push(field); + let ref_to_deref = FunctionIdent::new( + name, + UnaryArity::new(&[&vir::TypeData::Ref]), + &vir::TypeData::Ref, + ); + PredicateEncDataRef { ref_field, - perm, snap_data, + ref_to_deref, } } pub fn mk_enum_ref( @@ -687,8 +705,6 @@ impl<'vir, 'tcx> PredicateEncValues<'vir, 'tcx> { pub fn mk_ref( mut self, - inner: PredicateEncOutputRef<'vir>, - lifted_ty: LiftedTy<'vir, LiftedGeneric<'vir>>, data: PredicateEncDataRef<'vir>, ) -> PredicateEncOutput<'vir> { let self_field = self @@ -699,33 +715,19 @@ impl<'vir, 'tcx> PredicateEncValues<'vir, 'tcx> { let non_null = self .vcx .mk_bin_op_expr(vir::BinOpKind::CmpNe, self_ref, self.vcx.mk_null()); - let inner_ref_to_args = inner.ref_to_args(self.vcx, lifted_ty, self_ref); - let inner_pred = self.vcx.mk_predicate_app_expr(inner.ref_to_pred.apply( - self.vcx, - inner_ref_to_args, - data.perm, - )); - let predicate = self.vcx.mk_conj(&[self_field, non_null, inner_pred]); + let predicate = self.vcx.mk_conj(&[self_field, non_null]); self.predicates.push(self.vcx.mk_predicate( self.ref_to_pred, self.ref_to_decls, Some(predicate), )); - let inner_snap = inner.ref_to_snap.apply(self.vcx, inner_ref_to_args); - let snap = if data.perm.is_none() { - // `Ref` is only part of snapshots for mutable references. - data.snap_data - .field_snaps_to_snap - .apply(self.vcx, &[inner_snap, - // TODO: Re-enable this once its purpose is understood - // self_ref - ]) - } else { - data.snap_data - .field_snaps_to_snap - .apply(self.vcx, &[inner_snap]) - }; + // TODO: we might want to include the deref snapshot in the Ref snapshot + // at some point. + //let inner_snap = inner.ref_to_snap.apply(self.vcx, inner_ref_to_args); + let snap = data.snap_data + .snap_to_prim + .apply(self.vcx, [self_ref]); let fn_snap_body = self.vcx.mk_unfolding_expr(self.self_pred_read, snap); self.finalize(Some(fn_snap_body)) }