Skip to content

Commit

Permalink
Ugly commit 3ei4.
Browse files Browse the repository at this point in the history
  • Loading branch information
@vakaras
vakaras committed Mar 12, 2023
1 parent ed2bad7 commit 2a326de
Show file tree
Hide file tree
Showing 3 changed files with 186 additions and 6 deletions.
26 changes: 26 additions & 0 deletions prusti-viper/src/encoder/middle/core_proof/references/interface.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,14 @@ pub(in super::super) trait ReferencesInterface {
current_snapshot: vir_low::Expression,
position: vir_low::Position,
) -> SpannedEncodingResult<vir_low::Expression>;
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<vir_low::Expression>;
fn reference_deref_place(
&mut self,
place: vir_low::Expression,
Expand Down Expand Up @@ -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<vir_low::Expression> {
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,
Expand Down
1 change: 1 addition & 0 deletions prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ mod validity;
/// constructor.
mod constructor;

#[derive(Debug, Clone)]
pub(in super::super::super::super) enum PredicateKind {
Owned,
FracRef {
Expand Down
165 changes: 159 additions & 6 deletions ...ti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/self_framing.rs
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,29 @@
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,
},
};
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},
};
Expand Down Expand Up @@ -209,7 +214,27 @@ impl SelfFramingAssertionToSnapshot {
address: vir_low::Expression,
position: vir_low::Position,
) -> SpannedEncodingResult<vir_low::Expression> {
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<vir_low::Expression> {
match predicate_kind {
PredicateKind::Owned => lowerer.owned_non_aliased_snap(
self.call_context(),
ty,
Expand Down Expand Up @@ -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<vir_low::Expression> {
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<pointer_type>::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);
};
Expand All @@ -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();
Expand All @@ -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()),
Expand Down

0 comments on commit 2a326de

Please sign in to comment.