Skip to content

Commit

Permalink
Ugly commit 29.29
Browse files Browse the repository at this point in the history
  • Loading branch information
@vakaras
vakaras committed Jan 28, 2024
1 parent 0039957 commit f4423df
Show file tree
Hide file tree
Showing 8 changed files with 187 additions and 59 deletions.
24 changes: 24 additions & 0 deletions prusti-contracts/prusti-contracts-proc-macros/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -324,6 +324,18 @@ pub fn unpack_mut_ref(_tokens: TokenStream) -> TokenStream {
TokenStream::new()
}

#[cfg(not(feature = "prusti"))]
#[proc_macro]
pub fn pack_mut_ref_obligation(_tokens: TokenStream) -> TokenStream {
TokenStream::new()
}

#[cfg(not(feature = "prusti"))]
#[proc_macro]
pub fn unpack_mut_ref_obligation(_tokens: TokenStream) -> TokenStream {
TokenStream::new()
}

#[cfg(not(feature = "prusti"))]
#[proc_macro]
pub fn take_lifetime(_tokens: TokenStream) -> TokenStream {
Expand Down Expand Up @@ -801,6 +813,18 @@ pub fn unpack_mut_ref(tokens: TokenStream) -> TokenStream {
prusti_specs::unpack_mut_ref(tokens.into()).into()
}

#[cfg(feature = "prusti")]
#[proc_macro]
pub fn pack_mut_ref_obligation(tokens: TokenStream) -> TokenStream {
prusti_specs::pack_mut_ref_obligation(tokens.into()).into()
}

#[cfg(feature = "prusti")]
#[proc_macro]
pub fn unpack_mut_ref_obligation(tokens: TokenStream) -> TokenStream {
prusti_specs::unpack_mut_ref_obligation(tokens.into()).into()
}

#[cfg(feature = "prusti")]
#[proc_macro]
pub fn take_lifetime(tokens: TokenStream) -> TokenStream {
Expand Down
18 changes: 18 additions & 0 deletions prusti-contracts/prusti-contracts/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,12 @@ pub use prusti_contracts_proc_macros::pack_mut_ref;
/// A macro to manually unpack a place capability.
pub use prusti_contracts_proc_macros::unpack_mut_ref;

/// A macro to manually pack a place capability.
pub use prusti_contracts_proc_macros::pack_mut_ref_obligation;

/// A macro to manually unpack a place capability.
pub use prusti_contracts_proc_macros::unpack_mut_ref_obligation;

/// A macro to obtain a lifetime of a place.
pub use prusti_contracts_proc_macros::take_lifetime;

Expand Down Expand Up @@ -631,6 +637,18 @@ pub fn prusti_unpack_mut_ref_place<T>(_lifetime_name: &'static str, _arg: T) {
unreachable!();
}

#[doc(hidden)]
#[trusted]
pub fn prusti_pack_mut_ref_place_obligation<T>(_lifetime_name: &'static str, _arg: T) {
unreachable!();
}

#[doc(hidden)]
#[trusted]
pub fn prusti_unpack_mut_ref_place_obligation<T>(_lifetime_name: &'static str, _arg: T) {
unreachable!();
}

#[doc(hidden)]
#[trusted]
pub fn prusti_take_lifetime<T>(_arg: T, _lifetime_name: &'static str) -> Lifetime {
Expand Down
9 changes: 9 additions & 0 deletions prusti-contracts/prusti-specs/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1642,6 +1642,15 @@ pub fn unpack_mut_ref(tokens: TokenStream) -> TokenStream {
pack_unpack_ref(tokens, quote! {prusti_unpack_mut_ref_place})
}

pub fn pack_mut_ref_obligation(tokens: TokenStream) -> TokenStream {
// generate_place_function(tokens, quote! {prusti_pack_mut_ref_place})
pack_unpack_ref(tokens, quote! {prusti_pack_mut_ref_place_obligation})
}

pub fn unpack_mut_ref_obligation(tokens: TokenStream) -> TokenStream {
pack_unpack_ref(tokens, quote! {prusti_unpack_mut_ref_place_obligation})
}

fn pack_unpack_ref(tokens: TokenStream, function: TokenStream) -> TokenStream {
// let (lifetime_name, reference) =
// handle_result!(parse_two_expressions::<syn::Token![,]>(tokens));
Expand Down
10 changes: 8 additions & 2 deletions prusti-viper/src/encoder/high/procedures/inference/semantics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -880,12 +880,18 @@ impl CollectPermissionChanges for vir_typed::Unpack {
if self.place.is_behind_pointer_dereference() {
consumed_permissions.push(Permission::Owned(self.place.clone()));
} else {
eprintln!("Unpack: {}", self);
let type_decl = encoder.encode_type_def_typed(self.place.get_type())?;
if let vir_typed::TypeDecl::Struct(decl) = type_decl {
if decl.is_manually_managed_type() {
consumed_permissions.push(Permission::Owned(self.place.clone()));
add_struct_expansion(&self.place, decl, produced_permissions);
if !matches!(
self.predicate_kind,
vir_typed::ast::statement::PredicateKind::UniqueRef(_)
) || self.with_obligation.is_some()
{
// unique_mut_ref resolves fields of types with invariants.
add_struct_expansion(&self.place, decl, produced_permissions);
}
} else {
consumed_permissions.push(Permission::Owned(self.place.clone()));
add_struct_expansion(&self.place, decl, produced_permissions);
Expand Down
136 changes: 86 additions & 50 deletions prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
// .transpose()?;
// let encoded_statement = vir_mid::Statement::fold_owned(place, None, position);
// FIXME: Code duplication.
let mut additional_statements = Vec::new();
let encoded_statement = match pack_statement.predicate_kind {
vir_typed::ast::statement::PredicateKind::Owned => {
vir_mid::Statement::fold_owned(place, None, permission, position)
Expand All @@ -340,6 +341,19 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
// unreachable!()
// };
// let lifetime = reference.lifetime.clone();
if let Some(obligation) = pack_statement.with_obligation {
// FIXME: This should be done at the lowering to low instead of here and with permission amount that is unknown like with open.
let permission = obligation.typed_to_middle_expression(self.encoder)?;
let lifetime = predicate_kind
.lifetime
.clone()
.typed_to_middle_type(self.encoder)?;
let lifetime_token =
vir_mid::Predicate::lifetime_token(lifetime, permission, position);
let inhale =
vir_mid::Statement::inhale_predicate(lifetime_token, position);
additional_statements.push(inhale);
}
vir_mid::Statement::fold_ref(
place,
predicate_kind.lifetime.typed_to_middle_type(self.encoder)?,
Expand All @@ -351,6 +365,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
vir_typed::ast::statement::PredicateKind::FracRef(_) => todo!(),
};
self.current_statements.push(encoded_statement);
self.current_statements.extend(additional_statements);
}
vir_typed::Statement::Unpack(unpack_statement) => {
// state.insert_manually_managed(unpack_statement.place.clone())?;
Expand Down Expand Up @@ -385,63 +400,84 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
)?
{
if let Some(invariant) = type_decl.structural_invariant {
struct Checker {
span: MultiSpan,
};
impl ExpressionFallibleWalker for Checker {
type Error = SpannedEncodingError;
fn fallible_walk_expression(
&mut self,
expression: &vir_typed::Expression,
) -> SpannedEncodingResult<()>
{
if expression.is_place() {
if expression.is_behind_pointer_dereference() {
error_unsupported!(self.span.clone() => "Invariant cannot contain a place behind a dereference");
if let Some(obligation) = unpack_statement.with_obligation {
// FIXME: This should be done at the lowering to low instead of here and with permission amount that is unknown like with open.
let permission =
obligation.typed_to_middle_expression(self.encoder)?;
let lifetime = predicate_kind
.lifetime
.clone()
.typed_to_middle_type(self.encoder)?;
let lifetime_token = vir_mid::Predicate::lifetime_token(
lifetime, permission, position,
);
let exhale = vir_mid::Statement::exhale_predicate(
lifetime_token,
position,
);
additional_statements.push(exhale);
} else {
struct Checker {
span: MultiSpan,
};
impl ExpressionFallibleWalker for Checker {
type Error = SpannedEncodingError;
fn fallible_walk_expression(
&mut self,
expression: &vir_typed::Expression,
) -> SpannedEncodingResult<()>
{
if expression.is_place() {
if expression.is_behind_pointer_dereference() {
error_unsupported!(self.span.clone() => "Invariant cannot contain a place behind a dereference");
}
return Ok(());
} else {
vir_typed::visitors::default_fallible_walk_expression(
self, expression,
)
}
return Ok(());
} else {
vir_typed::visitors::default_fallible_walk_expression(
}
}
impl PredicateFallibleWalker for Checker {
type Error = SpannedEncodingError;
fn fallible_walk_expression(
&mut self,
expression: &vir_typed::Expression,
) -> SpannedEncodingResult<()>
{
ExpressionFallibleWalker::fallible_walk_expression(
self, expression,
)
}
}
}
impl PredicateFallibleWalker for Checker {
type Error = SpannedEncodingError;
fn fallible_walk_expression(
&mut self,
expression: &vir_typed::Expression,
) -> SpannedEncodingResult<()>
{
let span = self
.encoder
.error_manager()
.position_manager()
.get_span(position.into())
.cloned()
.unwrap();
let mut checker = Checker { span };
for expression in &invariant {
ExpressionFallibleWalker::fallible_walk_expression(
self, expression,
)
&mut checker,
expression,
)?;
}
for field in type_decl.fields {
let field =
field.typed_to_middle_expression(self.encoder)?;
let field_place = place.clone().field(field, position);
additional_statements.push(
vir_mid::Statement::dead_reference(
field_place,
None,
None,
position,
),
);
}
}
let span = self
.encoder
.error_manager()
.position_manager()
.get_span(position.into())
.cloned()
.unwrap();
let mut checker = Checker { span };
for expression in &invariant {
ExpressionFallibleWalker::fallible_walk_expression(
&mut checker,
expression,
)?;
}
for field in type_decl.fields {
let field = field.typed_to_middle_expression(self.encoder)?;
let field_place = place.clone().field(field, position);
additional_statements.push(vir_mid::Statement::dead_reference(
field_place,
None,
None,
position,
));
}
}
}
Expand Down
14 changes: 12 additions & 2 deletions prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1070,8 +1070,18 @@ impl IntoLow for vir_mid::Statement {
// TODO: These should be method calls.
let statements = match uniqueness {
vir_mid::ty::Uniqueness::Unique => {
let final_snapshot =
statement.target.to_procedure_final_snapshot(lowerer)?;
let mut place_encoder =
PlaceToSnapshot::for_place(PredicateKind::UniqueRef {
lifetime: lifetime.clone().into(),
is_final: true,
});
let final_snapshot = place_encoder.expression_to_snapshot(
lowerer,
&statement.target,
false,
)?;
// let final_snapshot =
// statement.target.to_procedure_final_snapshot(lowerer)?;
let label = lowerer.fresh_label("dead_reference_label")?;
lowerer.save_old_label(label.clone())?;
let (current_snapshot, predicate) = if let Some(reborrowing_lifetime) =
Expand Down
Loading

0 comments on commit f4423df

Please sign in to comment.