From 70d78a7662b585677d38b6009b161d112b6f8763 Mon Sep 17 00:00:00 2001 From: Pascal Huber Date: Tue, 19 Jul 2022 08:52:16 +0200 Subject: [PATCH 1/2] Handle Generic Argument Lifetimes --- .../fail/unsafe_core_proof/enums.rs | 12 +++++ .../high/operations_internal/lifetimes.rs | 49 ++++++++++++++++--- 2 files changed, 54 insertions(+), 7 deletions(-) diff --git a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs index d960b2295ac..3a1d15445a0 100644 --- a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs +++ b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs @@ -166,3 +166,15 @@ fn test10_assert_false(){ let mut _d = &mut c; assert!(false); //~ ERROR: the asserted expression might not hold } + +enum Enum5<'a, T> { + A(&'a mut T), + B(&'a mut T), +} +fn test11(){ + let mut n = 4; + let mut c = C{ x: &mut n}; + let mut e = Enum5::A(&mut c); + let mut f = &mut e; + let mut g = &mut f; +} \ No newline at end of file diff --git a/vir/defs/high/operations_internal/lifetimes.rs b/vir/defs/high/operations_internal/lifetimes.rs index b9a457d4054..4cc5a63a426 100644 --- a/vir/defs/high/operations_internal/lifetimes.rs +++ b/vir/defs/high/operations_internal/lifetimes.rs @@ -15,20 +15,55 @@ pub trait WithLifetimes { fn get_lifetimes(&self) -> Vec; } +fn get_lifetimes_with_arguments( + lifetimes: &Vec, + arguments: &Vec, +) -> Vec { + let mut all_lifetimes = lifetimes.clone(); + for ty in arguments { + for lifetime in ty.get_lifetimes() { + if !all_lifetimes.contains(&lifetime) { + all_lifetimes.push(lifetime); + } + } + } + all_lifetimes +} + impl WithLifetimes for ty::Type { fn get_lifetimes(&self) -> Vec { match self { ty::Type::Reference(reference) => reference.get_lifetimes(), - ty::Type::Tuple(ty::Tuple { lifetimes, .. }) - | ty::Type::Struct(ty::Struct { lifetimes, .. }) - | ty::Type::Sequence(ty::Sequence { lifetimes, .. }) + ty::Type::Tuple(ty::Tuple { + arguments, + lifetimes, + .. + }) + | ty::Type::Union(ty::Union { + arguments, + lifetimes, + .. + }) + | ty::Type::Projection(ty::Projection { + arguments, + lifetimes, + .. + }) + | ty::Type::Enum(ty::Enum { + arguments, + lifetimes, + .. + }) + | ty::Type::Struct(ty::Struct { + arguments, + lifetimes, + .. + }) => get_lifetimes_with_arguments(lifetimes, arguments), + ty::Type::Sequence(ty::Sequence { lifetimes, .. }) | ty::Type::Map(ty::Map { lifetimes, .. }) - | ty::Type::Enum(ty::Enum { lifetimes, .. }) | ty::Type::Array(ty::Array { lifetimes, .. }) | ty::Type::Slice(ty::Slice { lifetimes, .. }) - | ty::Type::Projection(ty::Projection { lifetimes, .. }) - | ty::Type::Trusted(ty::Trusted { lifetimes, .. }) - | ty::Type::Union(ty::Union { lifetimes, .. }) => lifetimes.clone(), + | ty::Type::Trusted(ty::Trusted { lifetimes, .. }) => lifetimes.clone(), _ => vec![], } } From f50bf4d820697066f0c2ac7781486d2c53ccf7eb Mon Sep 17 00:00:00 2001 From: Pascal Huber Date: Wed, 20 Jul 2022 11:41:23 +0200 Subject: [PATCH 2/2] Attempt to add subset-base lifetimes --- .../mir_body/borrowck/lifetimes/mod.rs | 17 +- .../fail/unsafe_core_proof/enums.rs | 10 +- .../fail/unsafe_core_proof/loops.rs | 86 ++++--- .../fail/unsafe_core_proof/structs.rs | 1 + .../core_proof/builtin_methods/interface.rs | 1 + .../middle/core_proof/lifetimes/interface.rs | 41 ++++ .../mir/procedures/encoder/lifetimes.rs | 220 ++++++++++++++++++ .../src/encoder/mir/procedures/encoder/mod.rs | 12 +- .../high/operations_internal/lifetimes.rs | 4 +- 9 files changed, 350 insertions(+), 42 deletions(-) diff --git a/prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs b/prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs index 0a25acf86cd..3f25b7104dd 100644 --- a/prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs +++ b/prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs @@ -92,6 +92,13 @@ impl Lifetimes { .collect() } + // pub fn get_subset_base_at_mid( + // &self, + // location: mir::Location, + // ) -> BTreeSet<(String, String)> { + // self.get_subset_base(RichLocation::Mid(location)).map(|(x,y)| (x.to_text(), y.to_text())).collect() + // } + pub fn lifetime_count(&self) -> usize { let original_lifetimes_count = self.get_original_lifetimes().len(); let subset_lifetimes: BTreeSet = self @@ -178,14 +185,20 @@ impl Lifetimes { .collect() } - pub fn get_subset_base_at_start(&self, location: mir::Location) -> Vec<(Region, Region)> { + pub fn get_subset_base_at_start(&self, location: mir::Location) -> BTreeSet<(String, String)> { let rich_location = RichLocation::Start(location); self.get_subset_base(rich_location) + .iter() + .map(|(x, y)| (x.to_text(), y.to_text())) + .collect() } - pub fn get_subset_base_at_mid(&self, location: mir::Location) -> Vec<(Region, Region)> { + pub fn get_subset_base_at_mid(&self, location: mir::Location) -> BTreeSet<(String, String)> { let rich_location = RichLocation::Mid(location); self.get_subset_base(rich_location) + .iter() + .map(|(x, y)| (x.to_text(), y.to_text())) + .collect() } pub fn get_lifetimes_dead_on_edge(&self, from: RichLocation, to: RichLocation) -> Vec { diff --git a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs index 3a1d15445a0..55cd56c8294 100644 --- a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs +++ b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs @@ -177,4 +177,12 @@ fn test11(){ let mut e = Enum5::A(&mut c); let mut f = &mut e; let mut g = &mut f; -} \ No newline at end of file +} +fn test11_assert_false(){ + let mut n = 4; + let mut c = C{ x: &mut n}; + let mut e = Enum5::A(&mut c); + let mut f = &mut e; + let mut g = &mut f; + assert!(false); //~ ERROR: the asserted expression might not hold +} diff --git a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/loops.rs b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/loops.rs index b8c7c310e33..243756d9911 100644 --- a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/loops.rs +++ b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/loops.rs @@ -22,38 +22,62 @@ impl<'a, T> Iterator for WrapperIterator<'a, T> { self.iter_mut.next() } } -fn test1() { - let mut ve = Vec::new(); - let mut v: WrapperIterator = WrapperIterator::new(&mut ve); - for x in &mut v {} +// fn test1() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// for x in &mut v {} +// } +// fn test1_assert_false() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// for x in &mut v {} +// assert!(false); //~ ERROR: the asserted expression might not hold +// } +// fn test2() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// let mut n = 4; +// let mut s = &mut n; +// assert!(*s == 4); +// for x in &mut v { +// s = x; +// } +// *s = 4; +// assert!(*s == 4); +// } +// fn test2_assert_false() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// let mut n = 4; +// let mut s = &mut n; +// assert!(*s == 4); +// for x in &mut v { +// s = x; +// } +// assert!(*s == 4); //~ ERROR: the asserted expression might not hold +// *s = 4; +// } + +struct X<'a>{ + x: &'a mut i32, } -fn test1_assert_false() { +// fn test3() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// } +// fn test3_assert_false() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// assert!(false); //~ ERROR: the asserted expression might not hold +// } +fn test4() { let mut ve = Vec::new(); - let mut v: WrapperIterator = WrapperIterator::new(&mut ve); + let mut v: WrapperIterator = WrapperIterator::new(&mut ve); for x in &mut v {} - assert!(false); //~ ERROR: the asserted expression might not hold -} -fn test2() { - let mut ve = Vec::new(); - let mut v: WrapperIterator = WrapperIterator::new(&mut ve); - let mut n = 4; - let mut s = &mut n; - assert!(*s == 4); - for x in &mut v { - s = x; - } - *s = 4; - assert!(*s == 4); -} -fn test2_assert_false() { - let mut ve = Vec::new(); - let mut v: WrapperIterator = WrapperIterator::new(&mut ve); - let mut n = 4; - let mut s = &mut n; - assert!(*s == 4); - for x in &mut v { - s = x; - } - assert!(*s == 4); //~ ERROR: the asserted expression might not hold - *s = 4; } +// fn test3_assert_false() { +// let mut ve = Vec::new(); +// let mut v: WrapperIterator = WrapperIterator::new(&mut ve); +// for x in &mut v {} +// assert!(false); //~ ERROR: the asserted expression might not hold +// } diff --git a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/structs.rs b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/structs.rs index a426660e43d..3ce9d51001e 100644 --- a/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/structs.rs +++ b/prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/structs.rs @@ -91,6 +91,7 @@ fn struct_mut_references_assert_false(){ let mut s2 = &mut s1; let mut s3 = &mut s2; let mut _s4 = &mut s3; + assert!(false); //~ ERROR: the asserted expression might not hold } struct S4I<'a> { 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 4c969d2b056..c9bd128823c 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 @@ -2915,6 +2915,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> { self.encode_lifetime_token_predicate()?; self.encode_lifetime_included()?; self.encode_lifetime_intersect(lft_count)?; + self.encode_lifetime_included_id_axiom()?; self.encode_lifetime_included_intersect_axiom(lft_count)?; use vir_low::macros::*; diff --git a/prusti-viper/src/encoder/middle/core_proof/lifetimes/interface.rs b/prusti-viper/src/encoder/middle/core_proof/lifetimes/interface.rs index d9790ae5609..4b13756505b 100644 --- a/prusti-viper/src/encoder/middle/core_proof/lifetimes/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/lifetimes/interface.rs @@ -17,6 +17,7 @@ use vir_crate::{ pub(in super::super) struct LifetimesState { is_lifetime_token_encoded: bool, is_lifetime_included_encoded: bool, + encoded_lifetime_included_id_axiom: bool, encoded_lifetime_intersect: FxHashSet, encoded_lifetime_included_intersect_axiom: FxHashSet, } @@ -41,6 +42,7 @@ pub(in super::super) trait LifetimesInterface { ) -> SpannedEncodingResult>; fn encode_lifetime_intersect(&mut self, lft_count: usize) -> SpannedEncodingResult<()>; fn encode_lifetime_included(&mut self) -> SpannedEncodingResult<()>; + fn encode_lifetime_included_id_axiom(&mut self) -> SpannedEncodingResult<()>; fn encode_lifetime_included_in_itself_axiom(&mut self) -> SpannedEncodingResult<()>; fn encode_lifetime_included_intersect_axiom( &mut self, @@ -153,6 +155,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesInterface for Lowerer<'p, 'v, 'tcx> { vir_low::ty::Type::Bool, Default::default(), )?; + self.encode_lifetime_included_id_axiom()?; self.encode_lifetime_included_in_itself_axiom()?; } Ok(()) @@ -176,6 +179,44 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesInterface for Lowerer<'p, 'v, 'tcx> { Ok(()) } + fn encode_lifetime_included_id_axiom(&mut self) -> SpannedEncodingResult<()> { + if !self.lifetimes_state.encoded_lifetime_included_id_axiom { + self.lifetimes_state.encoded_lifetime_included_id_axiom = true; + use vir_low::macros::*; + var_decls! { + lft_1: Lifetime, + lft_2: Lifetime + } + let included_1 = self.create_domain_func_app( + "Lifetime", + "included", + vec![lft_1.clone().into(), lft_2.clone().into()], + vir_low::ty::Type::Bool, + Default::default(), + )?; + let included_2 = self.create_domain_func_app( + "Lifetime", + "included", + vec![lft_2.clone().into(), lft_1.clone().into()], + vir_low::ty::Type::Bool, + Default::default(), + )?; + let condition = expr! { + [included_1] && [included_2] + }; + let equality = expr! { + [ lft_1.clone().into() ] == [ lft_2.clone().into() ] + }; + let quantifier_body = expr! { [condition] ==> [equality]}; + let axiom = vir_low::DomainAxiomDecl { + name: "included_id$".to_string(), + body: QuantifierHelpers::forall(vec![lft_1, lft_2], vec![], quantifier_body), + }; + self.declare_axiom("Lifetime", axiom)?; + } + Ok(()) + } + fn encode_lifetime_included_intersect_axiom( &mut self, lft_count: usize, diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs b/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs index e881c0cc89e..b93356cf223 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs @@ -19,6 +19,7 @@ pub(super) trait LifetimesEncoder<'tcx> { location: mir::Location, original_lifetimes: &mut BTreeSet, derived_lifetimes: &mut BTreeMap>, + subset_base_created: &mut BTreeSet<(String, String)>, statement: Option<&mir::Statement<'tcx>>, ) -> SpannedEncodingResult<()>; fn encode_lft_for_statement_mid( @@ -27,6 +28,7 @@ pub(super) trait LifetimesEncoder<'tcx> { location: mir::Location, original_lifetimes: &mut BTreeSet, derived_lifetimes: &mut BTreeMap>, + subset_base_created: &mut BTreeSet<(String, String)>, statement: Option<&mir::Statement<'tcx>>, ) -> SpannedEncodingResult<()>; fn reborrow_lifetimes( @@ -58,6 +60,8 @@ pub(super) trait LifetimesEncoder<'tcx> { old_original_lifetimes: &mut BTreeSet, old_derived_lifetimes: &mut BTreeMap>, new_derived_lifetimes: &mut BTreeMap>, + subset_base_created: &mut BTreeSet<(String, String)>, + new_subset_base: &mut BTreeSet<(String, String)>, shorten_lifetime_takes: bool, new_reborrow_lifetime_to_remove: Option, reborrow_lifetimes: Option<(String, BTreeSet)>, @@ -89,6 +93,13 @@ pub(super) trait LifetimesEncoder<'tcx> { location: mir::Location, lifetime_backups: &BTreeMap, ) -> SpannedEncodingResult<()>; + fn encode_subset_base_assumptions( + &mut self, + block_builder: &mut BasicBlockBuilder, + location: mir::Location, + subset_base_created: &mut BTreeSet<(String, String)>, + new_subset_base: &mut BTreeSet<(String, String)>, + ) -> SpannedEncodingResult<()>; fn encode_bor_shorten( &mut self, block_builder: &mut BasicBlockBuilder, @@ -141,6 +152,20 @@ pub(super) trait LifetimesEncoder<'tcx> { from: RichLocation, to: RichLocation, ) -> SpannedEncodingResult<()>; + fn encode_lft_assume_equal( + &mut self, + block_builder: &mut BasicBlockBuilder, + location: mir::Location, + lifetime_1: String, + lifetime_2: String, + ) -> SpannedEncodingResult<()>; + fn encode_lft_assume_subset( + &mut self, + block_builder: &mut BasicBlockBuilder, + location: mir::Location, + lifetime_lhs: String, + lifetime_rhs: String, + ) -> SpannedEncodingResult<()>; fn encode_lft_assert_subset( &mut self, block_builder: &mut BasicBlockBuilder, @@ -176,6 +201,10 @@ pub(super) trait LifetimesEncoder<'tcx> { fn encode_lifetime_specifications( &mut self, ) -> SpannedEncodingResult<(Vec, Vec)>; + fn identical_lifetimes( + &mut self, + relations: BTreeSet<(String, String)>, + ) -> BTreeSet>; fn identical_lifetimes_map( &mut self, existing_lifetimes: BTreeSet, @@ -213,6 +242,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' location: mir::Location, original_lifetimes: &mut BTreeSet, derived_lifetimes: &mut BTreeMap>, + subset_base_created: &mut BTreeSet<(String, String)>, statement: Option<&mir::Statement<'tcx>>, ) -> SpannedEncodingResult<()> { let mut new_derived_lifetimes = self.lifetimes.get_origin_contains_loan_at_start(location); @@ -222,12 +252,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' )); let new_reborrow_lifetime_to_ignore: Option = self.reborrow_operand_lifetime(statement); + let mut new_subset_base = self.lifetimes.get_subset_base_at_mid(location); self.encode_lft( block_builder, location, original_lifetimes, derived_lifetimes, &mut new_derived_lifetimes, + subset_base_created, + &mut new_subset_base, false, new_reborrow_lifetime_to_ignore, None, @@ -241,6 +274,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' location: mir::Location, original_lifetimes: &mut BTreeSet, derived_lifetimes: &mut BTreeMap>, + subset_base_created: &mut BTreeSet<(String, String)>, statement: Option<&mir::Statement<'tcx>>, ) -> SpannedEncodingResult<()> { let mut new_derived_lifetimes = self.lifetimes.get_origin_contains_loan_at_mid(location); @@ -250,6 +284,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' )); let new_reborrow_lifetime_to_ignore: Option = self.reborrow_operand_lifetime(statement); + let mut new_subset_base = self.lifetimes.get_subset_base_at_mid(location); // FIXME: The lifetimes read via the reborrow statement are currently not killed. let reborrow_lifetimes = self.reborrow_lifetimes(statement)?; self.encode_lft( @@ -258,6 +293,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' original_lifetimes, derived_lifetimes, &mut new_derived_lifetimes, + subset_base_created, + &mut new_subset_base, false, new_reborrow_lifetime_to_ignore, reborrow_lifetimes, @@ -326,12 +363,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' self.lifetimes.get_origin_contains_loan_at_mid(location); let mut current_original_lifetimes = self.lifetimes.get_loan_live_at_start(location); block_builder.add_comment(format!("Prepare lifetimes for block {:?}", target)); + // FIXME: this is nasty + let mut s1 = BTreeSet::new(); + let mut s2 = BTreeSet::new(); self.encode_lft( block_builder, location, &mut current_original_lifetimes, &mut current_derived_lifetimes, &mut needed_derived_lifetimes, + &mut s1, + &mut s2, true, None, None, @@ -366,12 +408,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' let mut intermediate_block_builder = block_builder.create_basic_block_builder(fresh_destination_label.clone()); intermediate_block_builder.add_comment(format!("Prepare lifetimes for block {:?}", target)); + // FIXME: this is nasty + let mut s1 = BTreeSet::new(); + let mut s2 = BTreeSet::new(); self.encode_lft( &mut intermediate_block_builder, location, &mut current_original_lifetimes, &mut current_derived_lifetimes, &mut needed_derived_lifetimes, + &mut s1, + &mut s2, true, None, None, @@ -401,6 +448,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' old_original_lifetimes: &mut BTreeSet, old_derived_lifetimes: &mut BTreeMap>, new_derived_lifetimes: &mut BTreeMap>, + subset_base_created: &mut BTreeSet<(String, String)>, + new_subset_base: &mut BTreeSet<(String, String)>, shorten_lifetimes: bool, new_reborrow_lifetime_to_remove: Option, reborrow_lifetimes: Option<(String, BTreeSet)>, @@ -459,6 +508,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' &reborrow_lifetimes, )?; self.encode_bor_shorten(block_builder, location, &lifetime_backups)?; + self.encode_subset_base_assumptions( + block_builder, + location, + subset_base_created, + new_subset_base, + )?; *old_original_lifetimes = new_original_lifetimes.clone(); *old_derived_lifetimes = new_derived_lifetimes.clone(); @@ -534,6 +589,55 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' .collect(); } + fn encode_subset_base_assumptions( + &mut self, + block_builder: &mut BasicBlockBuilder, + location: mir::Location, + subset_base_created: &mut BTreeSet<(String, String)>, + new_subset_base: &mut BTreeSet<(String, String)>, + ) -> SpannedEncodingResult<()> { + // println!("------ {:?}", location); + // let identical_lifetimes = self.identical_lifetimes(new_subset_base.clone()); + // dbg!(&identical_lifetimes); + // dbg!(&new_subset_base); + // for identical_lifetimes_set in identical_lifetimes { + // let mut iter = identical_lifetimes_set.iter(); + // let mut current = iter.next().unwrap().clone(); + // let first = current.clone(); + // let mut last = current.clone(); + // while let Some(next) = iter.next() { + // self.encode_lft_assume_equal( + // block_builder, + // location, + // current.clone(), + // next.clone(), + // )?; + // current = next.clone(); + // last = next.clone(); + // } + // if first != last { + // self.encode_lft_assume_equal( + // block_builder, + // location, + // first.clone(), + // last.clone(), + // )?; + // } + // } + for (lft_1, lft_2) in new_subset_base.iter() { + if !subset_base_created.contains(&(lft_1.clone(), lft_2.clone())) { + subset_base_created.insert((lft_1.clone(), lft_2.clone())); + self.encode_lft_assume_subset( + block_builder, + location, + lft_1.clone(), + lft_2.clone(), + )?; + } + } + Ok(()) + } + fn encode_bor_shorten( &mut self, block_builder: &mut BasicBlockBuilder, @@ -792,6 +896,77 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' Ok(()) } + fn encode_lft_assume_equal( + &mut self, + block_builder: &mut BasicBlockBuilder, + location: mir::Location, + lifetime_1: String, + lifetime_2: String, + ) -> SpannedEncodingResult<()> { + let assume_statement = self.encoder.set_statement_error_ctxt( + vir_high::Statement::assume_no_pos(vir_high::Expression::binary_op_no_pos( + vir_high::BinaryOpKind::EqCmp, + vir_high::VariableDecl { + name: lifetime_1, + ty: vir_high::ty::Type::Lifetime, + } + .into(), + vir_high::VariableDecl { + name: lifetime_2, + ty: vir_high::ty::Type::Lifetime, + } + .into(), + )), + self.mir.span, + ErrorCtxt::LifetimeEncoding, + self.def_id, + )?; + + block_builder.add_statement(self.set_statement_error( + location, + ErrorCtxt::LifetimeEncoding, + assume_statement, + )?); + Ok(()) + } + + fn encode_lft_assume_subset( + &mut self, + block_builder: &mut BasicBlockBuilder, + location: mir::Location, + lifetime_lhs: String, + lifetime_rhs: String, + ) -> SpannedEncodingResult<()> { + let assert_statement = self.encoder.set_statement_error_ctxt( + vir_high::Statement::assume_no_pos(vir_high::Expression::builtin_func_app_no_pos( + vir_high::BuiltinFunc::LifetimeIncluded, + vec![], // NOTE: we ignore argument_types for LifetimeIncluded + vec![ + vir_high::VariableDecl { + name: lifetime_lhs, + ty: vir_high::ty::Type::Lifetime, + } + .into(), + vir_high::VariableDecl { + name: lifetime_rhs, + ty: vir_high::ty::Type::Lifetime, + } + .into(), + ], + vir_high::ty::Type::Bool, + )), + self.mir.span, + ErrorCtxt::LifetimeEncoding, + self.def_id, + )?; + block_builder.add_statement(self.set_statement_error( + location, + ErrorCtxt::LifetimeEncoding, + assert_statement, + )?); + Ok(()) + } + fn encode_lft_assert_subset( &mut self, block_builder: &mut BasicBlockBuilder, @@ -1020,6 +1195,51 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' Ok((preconditions, postconditions)) } + // FIXME: remove redundancy with identical_lifetimes_map + fn identical_lifetimes( + &mut self, + relations: BTreeSet<(String, String)>, + ) -> BTreeSet> { + let unique_lifetimes: BTreeSet = relations + .iter() + .flat_map(|(x, y)| [x, y]) + .cloned() + .collect(); + let n = unique_lifetimes.len(); + let mut lft_enumarate: BTreeMap = BTreeMap::new(); + let mut lft_enumarate_rev: BTreeMap = BTreeMap::new(); + + for (i, e) in unique_lifetimes.iter().enumerate() { + lft_enumarate.insert(e.to_string(), i); + lft_enumarate_rev.insert(i, e.to_string()); + } + + let graph = { + let mut g = Graph::new(n); + for (k, v) in relations { + g.add_edge( + *lft_enumarate.get(&k[..]).unwrap(), + *lft_enumarate.get(&v[..]).unwrap(), + ); + } + g + }; + + // compute strongly connected components + let mut identical_lifetimes: BTreeSet> = BTreeSet::new(); + for component in Tarjan::walk(&graph) { + identical_lifetimes.insert( + component + .iter() + .map(|x| lft_enumarate_rev.get(x).unwrap()) + .cloned() + .collect(), + ); + } + + identical_lifetimes + } + fn identical_lifetimes_map( &mut self, existing_lifetimes: BTreeSet, diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs index 6db3624f974..7c6ad274ca2 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs @@ -461,12 +461,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { self.lifetimes.get_loan_live_at_start(location); let mut derived_lifetimes: BTreeMap> = self.lifetimes.get_origin_contains_loan_at_start(location); + let mut subset_base_created: BTreeSet<(String, String)> = BTreeSet::new(); while location.statement_index < terminator_index { self.encode_lft_for_statement_mid( &mut block_builder, location, &mut original_lifetimes, &mut derived_lifetimes, + &mut subset_base_created, Some(&statements[location.statement_index]), )?; self.encode_lifetimes_dead_on_edge( @@ -494,6 +496,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { location, &mut original_lifetimes, &mut derived_lifetimes, + &mut subset_base_created, Some(&statements[location.statement_index]), )?; } @@ -504,6 +507,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { location, &mut original_lifetimes, &mut derived_lifetimes, + &mut subset_base_created, None, )?; let terminator = &terminator.kind; @@ -1485,12 +1489,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // FIXME: Ideally, before a function call, assert *exactly* what is assumed in the function. // In this case, that is the opaque lifetimes conditions. Finding the right lifetimes // which correspond to the the lifetimes in the function seems to be hard. - let subset_base: Vec<(String, String)> = self - .lifetimes - .get_subset_base_at_mid(location) - .iter() - .map(|(x, y)| (x.to_text(), y.to_text())) - .collect(); + let subset_base: BTreeSet<(String, String)> = + self.lifetimes.get_subset_base_at_mid(location); for (lifetime_lhs, lifetime_rhs) in subset_base { if lifetimes_to_exhale_inhale.contains(&lifetime_lhs) || lifetimes_to_exhale_inhale.contains(&lifetime_rhs) diff --git a/vir/defs/high/operations_internal/lifetimes.rs b/vir/defs/high/operations_internal/lifetimes.rs index 4cc5a63a426..77dc7e59263 100644 --- a/vir/defs/high/operations_internal/lifetimes.rs +++ b/vir/defs/high/operations_internal/lifetimes.rs @@ -16,10 +16,10 @@ pub trait WithLifetimes { } fn get_lifetimes_with_arguments( - lifetimes: &Vec, + lifetimes: &[ty::LifetimeConst], arguments: &Vec, ) -> Vec { - let mut all_lifetimes = lifetimes.clone(); + let mut all_lifetimes = lifetimes.to_owned(); for ty in arguments { for lifetime in ty.get_lifetimes() { if !all_lifetimes.contains(&lifetime) {