diff --git a/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs b/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs index e63766bc9c7..da1d8f12d73 100644 --- a/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs +++ b/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs @@ -223,7 +223,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> { self.process_actions(actions)?; state.remove_permissions(&consumed_permissions)?; state.insert_permissions(produced_permissions)?; - match &statement { + match statement { vir_typed::Statement::ObtainMutRef(_) => { // The requirements already performed the needed changes. } @@ -261,7 +261,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> { .push(statement.typed_to_middle_statement(self.encoder)?); } vir_typed::Statement::Pack(pack_statement) => { - state.remove_manually_managed(&pack_statement.place)?; + // state.remove_manually_managed(&pack_statement.place)?; let position = pack_statement.position(); let place = pack_statement .place @@ -271,7 +271,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> { self.current_statements.push(encoded_statement); } vir_typed::Statement::Unpack(unpack_statement) => { - state.insert_manually_managed(unpack_statement.place.clone())?; + // state.insert_manually_managed(unpack_statement.place.clone())?; let position = unpack_statement.position(); let place = unpack_statement .place @@ -297,7 +297,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> { self.current_statements.push(encoded_statement); } vir_typed::Statement::ForgetInitialization(forget_statement) => { - state.insert_manually_managed(forget_statement.place.clone())?; + // state.insert_manually_managed(forget_statement.place.clone())?; let position = forget_statement.position(); let place = forget_statement .place diff --git a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs index 958b1d27508..e2428f4fa2b 100644 --- a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs @@ -2315,13 +2315,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> { source_snapshot.clone(), source_permission_amount, )?]; - let new_snapshot = self.new_snapshot_variable_version(&target.get_base(), position)?; - self.encode_snapshot_update_with_new_snapshot( + let new_snapshot = self.encode_snapshot_update_with_new_snapshot( &mut copy_place_statements, &target, source_snapshot, position, - Some(new_snapshot.clone()), + // Some(new_snapshot.clone()), )?; if let Some(conditions) = value.use_field { let mut disjuncts = Vec::new(); @@ -2329,12 +2328,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> { disjuncts.push(self.lower_block_marker_condition(condition)?); } let mut else_branch = vec![assign_statement]; - self.encode_snapshot_update_with_new_snapshot( + let new_snapshot_else_branch = self.encode_snapshot_update_with_new_snapshot( &mut else_branch, &target, result_value.into(), position, - Some(new_snapshot), + // Some(new_snapshot), )?; statements.push(vir_low::Statement::conditional( disjuncts.into_iter().disjoin(), @@ -2342,6 +2341,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> { else_branch, position, )); + statements.push(vir_low::Statement::assume( + vir_low::Expression::equals( + new_snapshot, + new_snapshot_else_branch, + ), + position, + )); } else { // Use field unconditionally. statements.extend(copy_place_statements); diff --git a/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs b/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs index 9de92cca773..3649c4da729 100644 --- a/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs +++ b/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs @@ -639,7 +639,6 @@ impl IntoLow for vir_mid::Statement { &mut statements, union_place, statement.position, - None, )?; let snapshot = union_place.to_procedure_snapshot(lowerer)?; let discriminant = lowerer.obtain_enum_discriminant( diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/variables/interface.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/variables/interface.rs index a12cb1ffef5..aa0272c6bcd 100644 --- a/prusti-viper/src/encoder/middle/core_proof/snapshots/variables/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/snapshots/variables/interface.rs @@ -38,6 +38,8 @@ trait Private { version: u64, ) -> SpannedEncodingResult; #[allow(clippy::ptr_arg)] // Clippy false positive. + /// Note: if `new_snapshot_root` is `Some`, the current encoding assumes + /// that the `place` is not behind a raw pointer. fn snapshot_copy_except( &mut self, statements: &mut Vec, @@ -380,7 +382,7 @@ pub(in super::super::super) trait SnapshotVariablesInterface { statements: &mut Vec, target: &vir_mid::Expression, position: vir_low::Position, - new_snapshot: Option, + // new_snapshot: Option, ) -> SpannedEncodingResult; fn encode_snapshot_update_with_new_snapshot( &mut self, @@ -388,8 +390,8 @@ pub(in super::super::super) trait SnapshotVariablesInterface { target: &vir_mid::Expression, value: vir_low::Expression, position: vir_low::Position, - new_snapshot: Option, - ) -> SpannedEncodingResult<()>; + // new_snapshot: Option, + ) -> SpannedEncodingResult; #[allow(clippy::ptr_arg)] // Clippy false positive. fn encode_snapshot_update( &mut self, @@ -562,7 +564,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotVariablesInterface for Lowerer<'p, 'v, 'tcx> statements: &mut Vec, target: &vir_mid::Expression, position: vir_low::Position, - new_snapshot: Option, + // new_snapshot_root: Option, ) -> SpannedEncodingResult { // let base = target.get_base(); // self.ensure_type_definition(&base.ty)?; @@ -614,21 +616,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotVariablesInterface for Lowerer<'p, 'v, 'tcx> Ok(new_snapshot) // } } + /// `new_snapshot_root` is used when we want to use a specific variable + /// version as the root of the new snapshot. fn encode_snapshot_update_with_new_snapshot( &mut self, statements: &mut Vec, target: &vir_mid::Expression, value: vir_low::Expression, position: vir_low::Position, - new_snapshot: Option, - ) -> SpannedEncodingResult<()> { + // new_snapshot_root: Option, + ) -> SpannedEncodingResult { use vir_low::macros::*; // self.encode_snapshot_havoc(statements, target, position, new_snapshot)?; // statements // .push(stmtp! { position => assume ([target.to_procedure_snapshot(self)?] == [value]) }); let new_snapshot = self.encode_snapshot_havoc(statements, target, position)?; - statements.push(stmtp! { position => assume ([new_snapshot] == [value]) }); - Ok(()) + statements.push(stmtp! { position => assume ([new_snapshot.clone()] == [value]) }); + Ok(new_snapshot) } fn encode_snapshot_update( &mut self, @@ -637,7 +641,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotVariablesInterface for Lowerer<'p, 'v, 'tcx> value: vir_low::Expression, position: vir_low::Position, ) -> SpannedEncodingResult<()> { - self.encode_snapshot_update_with_new_snapshot(statements, target, value, position, None) + self.encode_snapshot_update_with_new_snapshot(statements, target, value, position)?; + Ok(()) } /// `basic_block_edges` are statements to be executed then going from one /// block to another. diff --git a/prusti-viper/src/encoder/mir/types/encoder.rs b/prusti-viper/src/encoder/mir/types/encoder.rs index b2b34745e9d..fc91d447d0f 100644 --- a/prusti-viper/src/encoder/mir/types/encoder.rs +++ b/prusti-viper/src/encoder/mir/types/encoder.rs @@ -200,7 +200,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { // .unwrap(); // (array_len.into(), &[]) // }; - let array_len: usize = self.compute_array_len(*size).try_into().unwrap(); + let array_len: usize = self.compute_array_len(*size).with_span(self.get_definition_span())?.try_into().unwrap(); let lifetimes = self.encoder.get_lifetimes_from_type_high(*elem_ty)?; vir::Type::array( vir::ty::ConstGenericArgument::new(Some(Box::new(array_len.into()))), diff --git a/vir/defs/middle/ast/rvalue.rs b/vir/defs/middle/ast/rvalue.rs index 2c4e57c1256..1bb242eafa1 100644 --- a/vir/defs/middle/ast/rvalue.rs +++ b/vir/defs/middle/ast/rvalue.rs @@ -17,7 +17,7 @@ pub enum Rvalue { // ThreadLocalRef(ThreadLocalRef), AddressOf(AddressOf), Len(Len), - // Cast(Cast), + Cast(Cast), BinaryOp(BinaryOp), CheckedBinaryOp(CheckedBinaryOp), // NullaryOp(NullaryOp), @@ -67,6 +67,13 @@ pub struct Len { pub place: Expression, } +#[display(fmt = "cast({} -> {})", operand, ty)] +pub struct Cast { + // TODO: kind: CastKind, + pub operand: Operand, + pub ty: Type, +} + #[display(fmt = "{}({}, {})", kind, left, right)] pub struct BinaryOp { pub kind: BinaryOpKind,