Skip to content

Commit

Permalink
Ugly commit 29.30
Browse files Browse the repository at this point in the history
  • Loading branch information
@vakaras
vakaras committed Feb 4, 2024
1 parent f4423df commit d6ceef4
Show file tree
Hide file tree
Showing 8 changed files with 207 additions and 82 deletions.
12 changes: 12 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 @@ -354,6 +354,12 @@ pub fn set_lifetime_for_raw_pointer_reference_casts(_tokens: TokenStream) -> Tok
TokenStream::new()
}

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

#[cfg(not(feature = "prusti"))]
#[proc_macro]
pub fn join(_tokens: TokenStream) -> TokenStream {
Expand Down Expand Up @@ -843,6 +849,12 @@ pub fn set_lifetime_for_raw_pointer_reference_casts(tokens: TokenStream) -> Toke
prusti_specs::set_lifetime_for_raw_pointer_reference_casts(tokens.into()).into()
}

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

#[cfg(feature = "prusti")]
#[proc_macro]
pub fn join(tokens: TokenStream) -> TokenStream {
Expand Down
9 changes: 9 additions & 0 deletions prusti-contracts/prusti-contracts/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,6 +186,9 @@ pub use prusti_contracts_proc_macros::end_loan;
/// casts.
pub use prusti_contracts_proc_macros::set_lifetime_for_raw_pointer_reference_casts;

/// Attach the lifetime to the drop handler.
pub use prusti_contracts_proc_macros::attach_drop_lifetime;

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

Expand Down Expand Up @@ -667,6 +670,12 @@ pub fn prusti_set_lifetime_for_raw_pointer_reference_casts<T>(_arg: T) {
unreachable!();
}

#[doc(hidden)]
#[trusted]
pub fn prusti_attach_drop_lifetime<T1, T2>(_guard: T1, _reference: T2) {
unreachable!();
}

#[doc(hidden)]
#[trusted]
pub fn prusti_join_place<T>(_arg: T) {
Expand Down
7 changes: 7 additions & 0 deletions prusti-contracts/prusti-specs/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1815,6 +1815,13 @@ pub fn set_lifetime_for_raw_pointer_reference_casts(tokens: TokenStream) -> Toke
})
}

pub fn attach_drop_lifetime(tokens: TokenStream) -> TokenStream {
parse_expressions!(tokens, syn::Token![,] => drop, reference);
unsafe_spec_function_call(quote! {
prusti_attach_drop_lifetime(std::ptr::addr_of!(#drop), std::ptr::addr_of!(#reference))
})
}

pub fn join(tokens: TokenStream) -> TokenStream {
generate_place_function(tokens, quote! {prusti_join_place})
}
Expand Down
13 changes: 13 additions & 0 deletions prusti-interface/src/environment/mir_body/borrowck/facts/patch.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,19 @@ pub fn apply_patch_to_borrowck<'tcx>(
.collect();

borrowck_input_facts.cfg_edge.sort();

// Recompute `var_dropped_at` facts.
borrowck_input_facts.var_dropped_at.clear();
for (block, data) in patched_body.basic_blocks.iter_enumerated() {
match data.terminator().kind {
mir::TerminatorKind::Drop { place, .. } => {
let point = lt_patcher.start_point(block.index(), data.statements.len());
let variable = place.as_local().unwrap();
borrowck_input_facts.var_dropped_at.push((variable, point));
}
_ => {}
}
}
}

struct LocationTablePatcher<'a> {
Expand Down
4 changes: 4 additions & 0 deletions prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -253,6 +253,10 @@ impl<'p, 'v, 'tcx> BuiltinFuncAppEncoder<'p, 'v, 'tcx> for super::ProcedureEncod
// Do nothing, this function is used only by the drop
// elaboration pass.
}
"prusti_contracts::prusti_attach_drop_lifetime" => {
// Do nothing, this function is used only by the drop
// elaboration pass.
}
"prusti_contracts::Int::new"
| "prusti_contracts::Int::new_usize"
| "prusti_contracts::Int::new_isize" => make_builtin_call(
Expand Down
179 changes: 126 additions & 53 deletions prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/pointer_reborrow.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,67 +27,140 @@ pub(super) fn add_pointer_reborrow_facts<'v, 'tcx: 'v>(
if let ty::TyKind::FnDef(called_def_id, _) = literal.ty().kind() {
let full_called_function_name =
encoder.env().name.get_absolute_item_name(*called_def_id);
if full_called_function_name
== "prusti_contracts::prusti_set_lifetime_for_raw_pointer_reference_casts"
{
assert_eq!(args.len(), 1);
let arg = &args[0];
let mut statement_index = data.statements.len() - 1;
let argument_place = if let mir::Operand::Move(place) = arg {
place
} else {
unreachable!()
};
let (place, borrow_use) = loop {
if let Some(statement) = data.statements.get(statement_index) {
if let mir::StatementKind::Assign(box (target_place, rvalue)) =
&statement.kind
{
if target_place == argument_place {
match rvalue {
mir::Rvalue::AddressOf(_, place) => {
let point_mid = location_table.location_to_point(
RichLocation::Mid(mir::Location {
block,
statement_index,
}),
);
let mut variable = None;
for (var, point) in
&borrowck_input_facts.var_used_at
{
if *point == point_mid {
assert!(variable.is_none());
variable = Some(*var);
match full_called_function_name.as_str() {
"prusti_contracts::prusti_set_lifetime_for_raw_pointer_reference_casts" => {
assert_eq!(args.len(), 1);
let arg = &args[0];
let mut statement_index = data.statements.len() - 1;
let argument_place = if let mir::Operand::Move(place) = arg {
place
} else {
unreachable!()
};
let (place, borrow_use) = loop {
if let Some(statement) = data.statements.get(statement_index) {
if let mir::StatementKind::Assign(box (target_place, rvalue)) =
&statement.kind
{
if target_place == argument_place {
match rvalue {
mir::Rvalue::AddressOf(_, place) => {
let point_mid = location_table
.location_to_point(RichLocation::Mid(
mir::Location {
block,
statement_index,
},
));
let mut variable = None;
for (var, point) in
&borrowck_input_facts.var_used_at
{
if *point == point_mid {
assert!(variable.is_none());
variable = Some(*var);
}
}
}
let mut path = None;
for (accessed_path, point) in
&borrowck_input_facts.path_accessed_at_base
{
if *point == point_mid {
assert!(path.is_none());
path = Some(*accessed_path);
let mut path = None;
for (accessed_path, point) in
&borrowck_input_facts.path_accessed_at_base
{
if *point == point_mid {
assert!(path.is_none());
path = Some(*accessed_path);
}
}
break (
place,
(variable.unwrap(), path.unwrap()),
);
}
_ => {
unimplemented!("rvalue: {:?}", rvalue);
}
break (place, (variable.unwrap(), path.unwrap()));
}
_ => {
unimplemented!("rvalue: {:?}", rvalue);
}
}
}
statement_index -= 1;
} else {
unreachable!();
}
statement_index -= 1;
};
let ty::TyKind::Ref(reference_region, _, _) = place.ty(body, tcx).ty.kind() else {
unreachable!("place {place:?} must be a reference");
};
assert!(lifetime_with_borrow_use.is_none(), "the function can have only single prusti_set_lifetime_for_raw_pointer_reference_casts call");
lifetime_with_borrow_use = Some((*reference_region, borrow_use));
}
"prusti_contracts::prusti_attach_drop_lifetime" => {
assert_eq!(args.len(), 2);
let guard_arg = &args[0];
let reference_arg = &args[1];
let guard_place = if let mir::Operand::Move(place) = guard_arg {
place
} else {
unreachable!()
};
let reference_place = if let mir::Operand::Move(place) = reference_arg {
place
} else {
unreachable!();
}
};
let ty::TyKind::Ref(reference_region, _, _) = place.ty(body, tcx).ty.kind() else {
unreachable!("place {place:?} must be a reference");
};
assert!(lifetime_with_borrow_use.is_none(), "the function can have only single prusti_set_lifetime_for_raw_pointer_reference_casts call");
lifetime_with_borrow_use = Some((*reference_region, borrow_use));
unreachable!()
};
let mut statement_index = data.statements.len() - 1;
let guard_local = loop {
if let Some(statement) = data.statements.get(statement_index) {
if let mir::StatementKind::Assign(box (target_place, rvalue)) =
&statement.kind
{
if target_place == guard_place {
match rvalue {
mir::Rvalue::AddressOf(_, place) => {
break place.as_local().unwrap();
}
_ => {
unimplemented!("rvalue: {:?}", rvalue);
}
}
}
}
statement_index -= 1;
} else {
unreachable!();
}
};
let mut statement_index = data.statements.len() - 1;
let reference_place = loop {
if let Some(statement) = data.statements.get(statement_index) {
if let mir::StatementKind::Assign(box (target_place, rvalue)) =
&statement.kind
{
if target_place == reference_place {
match rvalue {
mir::Rvalue::AddressOf(_, place) => {
break *place;
}
_ => {
unimplemented!("rvalue: {:?}", rvalue);
}
}
}
}
statement_index -= 1;
} else {
unreachable!();
}
};
let ty::TyKind::Ref(reference_region, _, _) = reference_place.ty(body, tcx).ty.kind() else {
unreachable!("place {reference_place:?} must be a reference");
};
let ty::RegionKind::ReVar(reference_lifetime_id) = reference_region.kind() else {
unreachable!("reference_region: {:?}", reference_region);
};
borrowck_input_facts
.drop_of_var_derefs_origin
.push((guard_local, reference_lifetime_id));
}
_ => (),
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -845,7 +845,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, '
ErrorCtxt::LifetimeEncoding,
vir_high::Statement::dead_inclusion_no_pos(encoded_target, encoded_value),
)?);
self.derived_lifetimes_yet_to_kill.remove(&lifetime);
// self.derived_lifetimes_yet_to_kill.remove(&lifetime);
break;
}
}
Expand Down
Loading

0 comments on commit d6ceef4

Please sign in to comment.