Skip to content

Commit

Permalink
simplify reference predicates: only include the Ref, no generics
Browse files Browse the repository at this point in the history
  • Loading branch information
@Aurel300
Aurel300 committed Nov 22, 2024
1 parent 9faa7fa commit c7a0b0e
Show file tree
Hide file tree
Showing 5 changed files with 100 additions and 96 deletions.
18 changes: 3 additions & 15 deletions prusti-encoder/src/encoders/const.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::<RustTySnapshotsEnc>(str_ty)?
.generic_snapshot
.specifics
.expect_structlike();
let cast = deps.require_local::<RustTyCastersEnc<CastTypePure>>(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()),
Expand Down
33 changes: 10 additions & 23 deletions prusti-encoder/src/encoders/mir_impure.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -454,19 +454,23 @@ impl<'vir, 'enc, E: TaskEncoder> ImpureEncVisitor<'vir, 'enc, E> {
.deps
.require_ref::<RustTyPredicatesEnc>(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::<RustTyCastersEnc<CastTypeImpure>>(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),
}
Expand Down Expand Up @@ -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::<RustTyPredicatesEnc>(rvalue_ty).unwrap();

let place_ty = place.ty(self.local_decls, self.vcx.tcx());
let ty = self.deps.require_ref::<RustTyPredicatesEnc>(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::<RustTyCastersEnc<CastTypePure>>(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>) => {}
Expand Down
45 changes: 36 additions & 9 deletions prusti-encoder/src/encoders/type/domain.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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<DomainDataEnum<'vir>>),
Expand All @@ -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,
Expand Down Expand Up @@ -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::<LiftedTyEnc<EncodeGenericsAsParamTy>>(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(_) => {
Expand Down Expand Up @@ -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<FieldTy<'vir>>) -> DomainEncSpecifics<'vir> {
let specifics = self.mk_field_functions(&fields, None, false);
DomainEncSpecifics::StructLike(specifics)
Expand Down Expand Up @@ -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,
Expand Down
6 changes: 3 additions & 3 deletions prusti-encoder/src/encoders/type/most_generic_ty.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ impl<'tcx> MostGenericTy<'tcx> {
TyKind::Tuple(tys) => tys.iter().map(as_param_ty).collect::<Vec<_>>(),
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(_)
Expand Down Expand Up @@ -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
Expand Down
94 changes: 48 additions & 46 deletions prusti-encoder/src/encoders/type/predicate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<vir::Expr<'vir>>,
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)]
Expand Down Expand Up @@ -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},
Expand Down Expand Up @@ -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::<LiftedTyEnc<EncodeGenericsAsLifted>>(inner)
.unwrap();
let inner = deps
.require_ref::<RustTyPredicatesEnc>(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());
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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
Expand All @@ -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))
}
Expand Down

0 comments on commit c7a0b0e

Please sign in to comment.