Skip to content

Commit 6c1ffca

Browse files
vakarasvakaras
committed
Ugly commit 2
1 parent 4f58792 commit 6c1ffca

File tree

11 files changed

+318
-2
lines changed

11 files changed

+318
-2
lines changed

‎prusti-viper/src/encoder/high/procedures/inference/semantics.rs‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -273,13 +273,21 @@ fn extract_managed_predicate_place(
273273
vir_typed::Predicate::OwnedNonAliased(predicate) => {
274274
Ok(Some(Permission::Owned(predicate.place.clone())))
275275
}
276+
vir_typed::Predicate::UniqueRef(predicate) => {
277+
Ok(Some(Permission::Owned(predicate.place.clone())))
278+
}
279+
vir_typed::Predicate::FracRef(predicate) => {
280+
Ok(Some(Permission::Owned(predicate.place.clone())))
281+
}
276282
vir_typed::Predicate::MemoryBlockStackDrop(_)
277283
| vir_typed::Predicate::LifetimeToken(_)
278284
| vir_typed::Predicate::MemoryBlockHeap(_)
279285
| vir_typed::Predicate::MemoryBlockHeapRange(_)
280286
| vir_typed::Predicate::MemoryBlockHeapDrop(_)
281287
| vir_typed::Predicate::OwnedRange(_)
282-
| vir_typed::Predicate::OwnedSet(_) => {
288+
| vir_typed::Predicate::OwnedSet(_)
289+
| vir_typed::Predicate::UniqueRefRange(_)
290+
| vir_typed::Predicate::FracRefRange(_) => {
283291
// Unmanaged predicates.
284292
Ok(None)
285293
}

‎prusti-viper/src/encoder/high/procedures/inference/unfolding_expressions.rs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -184,6 +184,10 @@ impl ExpressionFallibleFolder for Ensurer {
184184
}
185185
vir_typed::Predicate::OwnedRange(_) => todo!(),
186186
vir_typed::Predicate::OwnedSet(_) => todo!(),
187+
vir_typed::Predicate::UniqueRef(_) => todo!(),
188+
vir_typed::Predicate::UniqueRefRange(_) => todo!(),
189+
vir_typed::Predicate::FracRef(_) => todo!(),
190+
vir_typed::Predicate::FracRefRange(_) => todo!(),
187191
}
188192
} else {
189193
default_fallible_fold_binary_op(self, binary_op)

‎prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs‎

Lines changed: 54 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,8 @@ use vir_crate::{
2727
middle::{
2828
self as vir_mid,
2929
operations::{
30-
ty::Typed, TypedToMiddleExpression, TypedToMiddleStatement, TypedToMiddleType,
30+
ty::Typed, TypedToMiddleExpression, TypedToMiddlePredicate, TypedToMiddleStatement,
31+
TypedToMiddleType,
3132
},
3233
},
3334
typed::{self as vir_typed},
@@ -654,6 +655,58 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
654655
);
655656
self.current_statements.push(encoded_statement);
656657
}
658+
vir_typed::Statement::Havoc(havoc_statement) => {
659+
// The procedure encoder provides only Owned predicates. Based
660+
// on the place and whether the reference is opened or not, we
661+
// produce the actual predicate.
662+
let predicate = match havoc_statement.predicate {
663+
vir_typed::Predicate::LifetimeToken(_) => todo!(),
664+
vir_typed::Predicate::MemoryBlockStack(predicate) => {
665+
vir_mid::Predicate::MemoryBlockStack(
666+
predicate.typed_to_middle_predicate(self.encoder)?,
667+
)
668+
}
669+
vir_typed::Predicate::MemoryBlockStackDrop(_) => todo!(),
670+
vir_typed::Predicate::MemoryBlockHeap(_) => todo!(),
671+
vir_typed::Predicate::MemoryBlockHeapRange(_) => todo!(),
672+
vir_typed::Predicate::MemoryBlockHeapDrop(_) => todo!(),
673+
vir_typed::Predicate::OwnedNonAliased(predicate) => {
674+
// TODO: Take into account whether the reference is opened or not.
675+
if let Some((lifetime, uniqueness)) = predicate.place.get_dereference_kind()
676+
{
677+
let lifetime = lifetime.typed_to_middle_type(self.encoder)?;
678+
let place = predicate.place.typed_to_middle_expression(self.encoder)?;
679+
match uniqueness {
680+
vir_typed::ty::Uniqueness::Unique => {
681+
vir_mid::Predicate::unique_ref(
682+
lifetime,
683+
place,
684+
predicate.position,
685+
)
686+
}
687+
vir_typed::ty::Uniqueness::Shared => vir_mid::Predicate::frac_ref(
688+
lifetime,
689+
place,
690+
predicate.position,
691+
),
692+
}
693+
} else {
694+
vir_mid::Predicate::OwnedNonAliased(
695+
predicate.typed_to_middle_predicate(self.encoder)?,
696+
)
697+
}
698+
}
699+
vir_typed::Predicate::OwnedRange(_) => todo!(),
700+
vir_typed::Predicate::OwnedSet(_) => todo!(),
701+
vir_typed::Predicate::UniqueRef(_) => todo!(),
702+
vir_typed::Predicate::UniqueRefRange(_) => todo!(),
703+
vir_typed::Predicate::FracRef(_) => todo!(),
704+
vir_typed::Predicate::FracRefRange(_) => todo!(),
705+
};
706+
let encoded_statement =
707+
vir_mid::Statement::havoc(predicate, havoc_statement.position);
708+
self.current_statements.push(encoded_statement);
709+
}
657710
_ => {
658711
self.current_statements
659712
.push(statement.typed_to_middle_statement(self.encoder)?);

‎prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ pub(in super::super) struct BuiltinMethodsState {
7777
encoded_duplicate_frac_ref_method: FxHashSet<String>,
7878
encoded_write_address_constant_methods: FxHashSet<String>,
7979
encoded_owned_non_aliased_havoc_methods: FxHashSet<String>,
80+
encoded_unique_ref_havoc_methods: FxHashSet<String>,
8081
encoded_memory_block_copy_methods: FxHashSet<String>,
8182
encoded_memory_block_split_methods: FxHashSet<String>,
8283
encoded_memory_block_range_split_methods: FxHashSet<String>,
@@ -152,6 +153,10 @@ trait Private {
152153
&self,
153154
ty: &vir_mid::Type,
154155
) -> SpannedEncodingResult<String>;
156+
fn encode_havoc_unique_ref_method_name(
157+
&self,
158+
ty: &vir_mid::Type,
159+
) -> SpannedEncodingResult<String>;
155160
fn encode_assign_method(
156161
&mut self,
157162
method_name: &str,
@@ -531,6 +536,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> {
531536
) -> SpannedEncodingResult<String> {
532537
Ok(format!("havoc_owned${}", ty.get_identifier()))
533538
}
539+
fn encode_havoc_unique_ref_method_name(
540+
&self,
541+
ty: &vir_mid::Type,
542+
) -> SpannedEncodingResult<String> {
543+
Ok(format!("havoc_unique_ref${}", ty.get_identifier()))
544+
}
534545
fn encode_assign_method(
535546
&mut self,
536547
method_name: &str,
@@ -1694,6 +1705,7 @@ pub(in super::super) trait BuiltinMethodsInterface {
16941705
&mut self,
16951706
ty: &vir_mid::Type,
16961707
) -> SpannedEncodingResult<()>;
1708+
fn encode_havoc_unique_ref_method(&mut self, ty: &vir_mid::Type) -> SpannedEncodingResult<()>;
16971709
fn encode_havoc_memory_block_method_name(
16981710
&mut self,
16991711
ty: &vir_mid::Type,
@@ -2258,6 +2270,65 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> {
22582270
}
22592271
Ok(())
22602272
}
2273+
fn encode_havoc_unique_ref_method(&mut self, ty: &vir_mid::Type) -> SpannedEncodingResult<()> {
2274+
let ty_identifier = ty.get_identifier();
2275+
if !self
2276+
.builtin_methods_state
2277+
.encoded_unique_ref_havoc_methods
2278+
.contains(&ty_identifier)
2279+
{
2280+
self.builtin_methods_state
2281+
.encoded_unique_ref_havoc_methods
2282+
.insert(ty_identifier);
2283+
use vir_low::macros::*;
2284+
let method_name = self.encode_havoc_unique_ref_method_name(ty)?;
2285+
let type_decl = self.encoder.get_type_decl_mid(ty)?;
2286+
var_decls! {
2287+
place: PlaceOption,
2288+
root_address: Address,
2289+
lifetime: Lifetime,
2290+
fresh_snapshot: {ty.to_snapshot(self)?}
2291+
};
2292+
let position = vir_low::Position::default();
2293+
let validity =
2294+
self.encode_snapshot_valid_call_for_type(fresh_snapshot.clone().into(), ty)?;
2295+
let mut parameters = vec![place.clone(), root_address.clone(), lifetime.clone()];
2296+
parameters.extend(self.create_lifetime_parameters(&type_decl)?);
2297+
let TODO_target_slice_len = None;
2298+
let predicate_in = self.unique_ref_full_vars(
2299+
CallContext::BuiltinMethod,
2300+
ty,
2301+
&type_decl,
2302+
&place,
2303+
&root_address,
2304+
&lifetime,
2305+
TODO_target_slice_len.clone(),
2306+
position,
2307+
)?;
2308+
let predicate_out = self.unique_ref_full_vars_with_current_snapshot(
2309+
CallContext::BuiltinMethod,
2310+
ty,
2311+
&type_decl,
2312+
&place,
2313+
&root_address,
2314+
&fresh_snapshot,
2315+
&lifetime,
2316+
TODO_target_slice_len,
2317+
position,
2318+
)?;
2319+
let method = vir_low::MethodDecl::new(
2320+
method_name,
2321+
vir_low::MethodKind::Havoc,
2322+
parameters,
2323+
vec![fresh_snapshot.clone()],
2324+
vec![predicate_in],
2325+
vec![predicate_out, validity],
2326+
None,
2327+
);
2328+
self.declare_method(method)?;
2329+
}
2330+
Ok(())
2331+
}
22612332
fn encode_memory_block_split_method(
22622333
&mut self,
22632334
ty: &vir_mid::Type,
@@ -2866,6 +2937,35 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> {
28662937
position,
28672938
)?;
28682939
}
2940+
vir_mid::Predicate::UniqueRef(predicate) => {
2941+
let ty = predicate.place.get_type();
2942+
self.encode_havoc_unique_ref_method(ty)?;
2943+
self.mark_unique_ref_as_used(ty)?;
2944+
let lifetime =
2945+
self.encode_lifetime_const_into_procedure_variable(predicate.lifetime)?;
2946+
let place = self.encode_expression_as_place(&predicate.place)?;
2947+
let address = self.encode_expression_as_place_address(&predicate.place)?;
2948+
let snapshot_type = ty.to_snapshot(self)?;
2949+
let fresh_snapshot = self.create_new_temporary_variable(snapshot_type)?;
2950+
let method_name = self.encode_havoc_unique_ref_method_name(ty)?;
2951+
let mut arguments = vec![place, address, lifetime.into()];
2952+
arguments.extend(self.create_lifetime_arguments(CallContext::Procedure, ty)?);
2953+
statements.push(vir_low::Statement::method_call(
2954+
method_name,
2955+
arguments,
2956+
vec![fresh_snapshot.clone().into()],
2957+
position,
2958+
));
2959+
self.encode_snapshot_update(
2960+
statements,
2961+
&predicate.place,
2962+
fresh_snapshot.into(),
2963+
position,
2964+
)?;
2965+
}
2966+
vir_mid::Predicate::FracRef(_) => {
2967+
// Fractional references are immutable, so havoc is a no-op.
2968+
}
28692969
vir_mid::Predicate::MemoryBlockStack(predicate) => {
28702970
let ty = predicate.place.get_type();
28712971
self.encode_havoc_memory_block_method(ty)?;

‎prusti-viper/src/encoder/middle/core_proof/footprint/interface.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,18 @@ impl<'l, 'p, 'v, 'tcx> vir_mid::visitors::ExpressionFolder
148148
vir_mid::Predicate::OwnedSet(predicate) => {
149149
unimplemented!("predicate: {}", predicate);
150150
}
151+
vir_mid::Predicate::UniqueRef(predicate) => {
152+
unimplemented!("predicate: {}", predicate);
153+
}
154+
vir_mid::Predicate::UniqueRefRange(predicate) => {
155+
unimplemented!("predicate: {}", predicate);
156+
}
157+
vir_mid::Predicate::FracRef(predicate) => {
158+
unimplemented!("predicate: {}", predicate);
159+
}
160+
vir_mid::Predicate::FracRefRange(predicate) => {
161+
unimplemented!("predicate: {}", predicate);
162+
}
151163
}
152164
}
153165

‎prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1701,6 +1701,10 @@ impl IntoLow for vir_mid::Predicate {
17011701
}
17021702
Predicate::OwnedRange(_) => todo!(),
17031703
Predicate::OwnedSet(_) => todo!(),
1704+
Predicate::UniqueRef(_) => todo!(),
1705+
Predicate::UniqueRefRange(_) => todo!(),
1706+
Predicate::FracRef(_) => todo!(),
1707+
Predicate::FracRefRange(_) => todo!(),
17041708
};
17051709
Ok(result)
17061710
}

‎prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/constructor.rs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -467,6 +467,10 @@ impl<'a, 'p, 'v: 'p, 'tcx: 'v> IntoSnapshotLowerer<'p, 'v, 'tcx>
467467
));
468468
}
469469
vir_mid::Predicate::OwnedSet(_) => todo!(),
470+
vir_mid::Predicate::UniqueRef(_) => todo!(),
471+
vir_mid::Predicate::UniqueRefRange(_) => todo!(),
472+
vir_mid::Predicate::FracRef(_) => todo!(),
473+
vir_mid::Predicate::FracRefRange(_) => todo!(),
470474
}
471475
Ok(true.into())
472476
}

‎vir/defs/high/ast/predicate.rs‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,10 @@ pub enum Predicate {
1616
OwnedNonAliased(OwnedNonAliased),
1717
OwnedRange(OwnedRange),
1818
OwnedSet(OwnedSet),
19+
UniqueRef(UniqueRef),
20+
UniqueRefRange(UniqueRefRange),
21+
FracRef(FracRef),
22+
FracRefRange(FracRefRange),
1923
}
2024

2125
#[display(fmt = "acc(LifetimeToken({}), {})", lifetime, permission)]
@@ -109,3 +113,53 @@ pub struct OwnedSet {
109113
pub set: Expression,
110114
pub position: Position,
111115
}
116+
117+
/// A unique reference predicate of a specific type.
118+
#[display(fmt = "UniqueRef({}, {})", lifetime, place)]
119+
pub struct UniqueRef {
120+
pub lifetime: LifetimeConst,
121+
pub place: Expression,
122+
pub position: Position,
123+
}
124+
125+
/// A range of unique reference predicates of a specific type. `start_index` is
126+
/// inclusive and `end_index` is exclusive.
127+
#[display(
128+
fmt = "UniqueRefRange({}, {}, {}, {})",
129+
lifetime,
130+
address,
131+
start_index,
132+
end_index
133+
)]
134+
pub struct UniqueRefRange {
135+
pub lifetime: LifetimeConst,
136+
pub address: Expression,
137+
pub start_index: Expression,
138+
pub end_index: Expression,
139+
pub position: Position,
140+
}
141+
142+
/// A shared reference predicate of a specific type.
143+
#[display(fmt = "FracRef({}, {})", lifetime, place)]
144+
pub struct FracRef {
145+
pub lifetime: LifetimeConst,
146+
pub place: Expression,
147+
pub position: Position,
148+
}
149+
150+
/// A range of shared reference predicates of a specific type. `start_index` is
151+
/// inclusive and `end_index` is exclusive.
152+
#[display(
153+
fmt = "FracRefRange({}, {}, {}, {})",
154+
lifetime,
155+
address,
156+
start_index,
157+
end_index
158+
)]
159+
pub struct FracRefRange {
160+
pub lifetime: LifetimeConst,
161+
pub address: Expression,
162+
pub start_index: Expression,
163+
pub end_index: Expression,
164+
pub position: Position,
165+
}

‎vir/defs/high/operations_internal/expression.rs‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1106,6 +1106,18 @@ impl Expression {
11061106
Predicate::OwnedSet(predicate) => {
11071107
unimplemented!("predicate: {}", predicate);
11081108
}
1109+
Predicate::UniqueRef(predicate) => {
1110+
self.owned_places.push(predicate.place.clone());
1111+
}
1112+
Predicate::UniqueRefRange(predicate) => {
1113+
self.owned_range_addresses.push(predicate.address.clone());
1114+
}
1115+
Predicate::FracRef(predicate) => {
1116+
self.owned_places.push(predicate.place.clone());
1117+
}
1118+
Predicate::FracRefRange(predicate) => {
1119+
self.owned_range_addresses.push(predicate.address.clone());
1120+
}
11091121
}
11101122
}
11111123
}
@@ -1144,6 +1156,24 @@ impl Expression {
11441156
Predicate::OwnedSet(predicate) => {
11451157
unimplemented!("predicate: {}", predicate);
11461158
}
1159+
Predicate::UniqueRef(predicate) => {
1160+
self.owned_places.push((
1161+
self.path_condition.iter().cloned().conjoin(),
1162+
predicate.place.clone(),
1163+
));
1164+
}
1165+
Predicate::UniqueRefRange(predicate) => {
1166+
unimplemented!("predicate: {}", predicate);
1167+
}
1168+
Predicate::FracRef(predicate) => {
1169+
self.owned_places.push((
1170+
self.path_condition.iter().cloned().conjoin(),
1171+
predicate.place.clone(),
1172+
));
1173+
}
1174+
Predicate::FracRefRange(predicate) => {
1175+
unimplemented!("predicate: {}", predicate);
1176+
}
11471177
}
11481178
}
11491179
fn walk_binary_op(&mut self, binary_op: &BinaryOp) {

0 commit comments

Comments
 (0)