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..c61d9c4399c 100644 --- a/prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs +++ b/prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs @@ -47,6 +47,18 @@ impl Lifetimes { } } + pub fn get_static_lifetime(&self) -> String { + "bw6".to_string() + // let opaque_lifetimes: BTreeMap> = + // self.get_opaque_lifetimes_with_inclusions_names(); + // for (lifetime, derived_from) in opaque_lifetimes { + // if derived_from.is_empty() { + // return lifetime.to_text(); + // } + // } + // unreachable!("There must be a static lifetime everywhere"); + } + pub fn get_loan_live_at_start(&self, location: mir::Location) -> BTreeSet { let info = self.get_loan_live_at(RichLocation::Start(location)); info.into_iter() @@ -92,6 +104,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 +197,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-interface/src/environment/procedure.rs b/prusti-interface/src/environment/procedure.rs index 8b0169006ee..82613469dcc 100644 --- a/prusti-interface/src/environment/procedure.rs +++ b/prusti-interface/src/environment/procedure.rs @@ -77,6 +77,24 @@ impl<'tcx> Procedure<'tcx> { } + pub fn get_ty_of_var(&self, var: mir::Local) -> Option>{ + let mir = self.get_mir(); + for local in mir.vars_and_temps_iter() { + if local == var { + return Some(mir.local_decls[local].ty); + // dbg!(&ty_kind); + // if let prusti_rustc_interface::middle::ty::TyKind::Ref(region, _ty, _mutability) = ty_kind { + // dbg!(&_ty); + // return Some(region.to_text()); + // } + // if let Some(lifetime) = get_lifetime_if_matches(local, var, mir) { + // return Some(lifetime); + // } + } + } + None + } + pub fn get_lifetime_of_var(&self, var: mir::Local) -> Option{ fn get_lifetime_if_matches(local: mir::Local, var: mir::Local, mir: &Mir) -> Option{ if local == var { 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..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 @@ -166,3 +166,23 @@ 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; +} +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/middle/core_proof/lowerer/mod.rs b/prusti-viper/src/encoder/middle/core_proof/lowerer/mod.rs index 7bf4c5852c3..4258586f94b 100644 --- a/prusti-viper/src/encoder/middle/core_proof/lowerer/mod.rs +++ b/prusti-viper/src/encoder/middle/core_proof/lowerer/mod.rs @@ -130,7 +130,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> Lowerer<'p, 'v, 'tcx> { )?), ]; for statement in basic_block.statements { - statements.extend(statement.into_low(&mut self)?); + let statement_low = statement.into_low(&mut self)?; + // dbg!(&statement_low); + statements.extend(statement_low); } let successor = basic_block.successor.into_low(&mut self)?; basic_blocks_map.insert(label.clone(), (statements, successor)); diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs b/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs index e881c0cc89e..e81cc53e1f4 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs @@ -3,6 +3,7 @@ use crate::encoder::{ mir::{ errors::ErrorInterface, procedures::encoder::{scc::*, ProcedureEncoder}, + types::*, }, }; use prusti_interface::environment::{ @@ -19,6 +20,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 +29,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 +61,10 @@ 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)>, + statement: Option<&mir::Statement<'tcx>>, + set_static: bool, shorten_lifetime_takes: bool, new_reborrow_lifetime_to_remove: Option, reborrow_lifetimes: Option<(String, BTreeSet)>, @@ -89,6 +96,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 +155,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 +204,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 +245,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 +255,17 @@ 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, + statement, + false, false, new_reborrow_lifetime_to_ignore, None, @@ -241,6 +279,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 +289,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 +298,10 @@ 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, + statement, + true, false, new_reborrow_lifetime_to_ignore, reborrow_lifetimes, @@ -326,12 +370,19 @@ 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, + None, // TODO: add statement? + false, true, None, None, @@ -366,12 +417,19 @@ 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, + None, // TODO: add statement? + false, true, None, None, @@ -401,6 +459,10 @@ 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)>, + statement: Option<&mir::Statement<'tcx>>, + set_static: bool, shorten_lifetimes: bool, new_reborrow_lifetime_to_remove: Option, reborrow_lifetimes: Option<(String, BTreeSet)>, @@ -459,6 +521,56 @@ 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, + // )?; + + // Create Lifetimes which are not in derived lifetimes + if set_static { + let lifetimes_required_for_statement: Vec = if let Some(statement) = statement { + match statement.kind { + mir::StatementKind::StorageLive(local) => { + let ty = self.procedure.get_ty_of_var(local); + if let Some(ty) = ty { + self.encoder.get_lifetimes_high(&ty)?.iter().map(|x| x.name.clone()).collect() + } else { + unreachable!() + } + }, + _ => vec![] + } + } else { + vec![] + }; + let static_lifetime = self.lifetimes.get_static_lifetime(); + println!("--------------------------------"); + dbg!(&statement); + // dbg!(&static_lifetime); + for required_lifetime in &lifetimes_required_for_statement { + if !new_derived_lifetimes.contains_key(required_lifetime) { + println!("---- we need"); + dbg!(&required_lifetime); + + + let encoded_required_lifetime = self.encode_lft_variable(required_lifetime.clone())?; + block_builder.add_statement(self.set_statement_error( + location, + ErrorCtxt::LifetimeEncoding, + vir_high::Statement::lifetime_take_no_pos( + encoded_required_lifetime, + vec![self.encode_lft_variable(static_lifetime.clone())?], + self.lifetime_token_fractional_permission(self.lifetime_count), + ), + )?); + } else { + println!("---- no need"); + dbg!(&required_lifetime); + } + } + } *old_original_lifetimes = new_original_lifetimes.clone(); *old_derived_lifetimes = new_derived_lifetimes.clone(); @@ -534,6 +646,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, @@ -606,6 +767,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' location: mir::Location, lifetime_backups: &BTreeMap, ) -> SpannedEncodingResult<()> { + // let static_lifetime = self.encode_lft_variable(self.lifetimes.get_static_lifetime())?; for (lifetime, (backup_var_name, _object)) in lifetime_backups { let lifetime_var = vir_high::VariableDecl::new(lifetime, vir_high::ty::Type::Lifetime); let backup_var = @@ -615,7 +777,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' ErrorCtxt::LifetimeEncoding, vir_high::Statement::lifetime_take_no_pos( backup_var, - vec![lifetime_var], + vec![ + lifetime_var, + // static_lifetime.clone(), + ], self.lifetime_token_fractional_permission(self.lifetime_count), ), )?); @@ -669,12 +834,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' ) -> SpannedEncodingResult<()> { let lifetimes_to_return = self.lifetimes_to_return(old_derived_lifetimes, new_derived_lifetimes); + let static_lifetime = self.encode_lft_variable(self.lifetimes.get_static_lifetime())?; for (lifetime, derived_from) in lifetimes_to_return { let encoded_target = self.encode_lft_variable(lifetime.clone())?; let mut lifetimes: Vec = Vec::new(); for lifetime_name in &derived_from { lifetimes.push(self.encode_lft_variable(lifetime_name.to_string())?); } + lifetimes.push(static_lifetime.clone()); self.derived_lifetimes_yet_to_kill .insert(lifetime.clone(), derived_from.clone()); block_builder.add_statement(self.set_statement_error( @@ -700,6 +867,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' ) -> SpannedEncodingResult<()> { let lifetimes_to_take = self.lifetimes_to_take(old_derived_lifetimes, new_derived_lifetimes); + let static_lifetime = self.encode_lft_variable(self.lifetimes.get_static_lifetime())?; for (lifetime, derived_from) in lifetimes_to_take { let encoded_target = self.encode_lft_variable(lifetime.clone())?; let mut lifetimes: Vec = Vec::new(); @@ -707,6 +875,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' for lifetime_name in derived_from { lifetimes.push(self.encode_lft_variable(lifetime_name)?); } + lifetimes.push(static_lifetime.clone()); self.derived_lifetimes_yet_to_kill.remove(&lifetime[..]); block_builder.add_statement(self.set_statement_error( location, @@ -719,7 +888,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' )?); } if let Some((value_lifetime, lifetimes)) = reborrow_lifetimes { - let existing_lifetime = [self.encode_lft_variable(value_lifetime.clone())?].to_vec(); + let existing_lifetime = vec![ + self.encode_lft_variable(value_lifetime.clone())?, + static_lifetime, + ]; for lifetime in lifetimes { if !new_derived_lifetimes.contains_key(lifetime) { let encoded_target = self.encode_lft_variable(lifetime.clone())?; @@ -792,6 +964,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, @@ -974,6 +1217,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, ' for lifetime_name in opaque { lifetimes.push(self.encode_lft_variable(lifetime_name.clone())?); } + let static_lifetime = self.encode_lft_variable(self.lifetimes.get_static_lifetime())?; + lifetimes.push(static_lifetime); preconditions.push(self.encoder.set_statement_error_ctxt( vir_high::Statement::lifetime_take_no_pos( encoded_target, @@ -1020,6 +1265,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/prusti-viper/src/encoder/mir/types/interface.rs b/prusti-viper/src/encoder/mir/types/interface.rs index 87eafda3ff0..d12ed81d79e 100644 --- a/prusti-viper/src/encoder/mir/types/interface.rs +++ b/prusti-viper/src/encoder/mir/types/interface.rs @@ -218,11 +218,18 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode | ty::TyKind::Opaque(_, substs) | ty::TyKind::FnDef(_, substs) => self.get_lifetimes_substs(substs)?, ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) => self.get_lifetimes_high(ty)?, - ty::TyKind::Dynamic(_, region) | ty::TyKind::Ref(region, _, _) => { + ty::TyKind::Dynamic(_, region) => { vec![vir_high::ty::LifetimeConst { name: region.to_text(), }] } + ty::TyKind::Ref(region, ty, _) => { + let mut lifetimes = vec![vir_high::ty::LifetimeConst { + name: region.to_text(), + }]; + lifetimes.extend(self.get_lifetimes_high(ty)?); + lifetimes + } ty::TyKind::Tuple(ty_list) => { let mut lifetimes = vec![]; for item_ty in ty_list.iter() { diff --git a/vir/defs/high/operations_internal/lifetimes.rs b/vir/defs/high/operations_internal/lifetimes.rs index b9a457d4054..152f3e74912 100644 --- a/vir/defs/high/operations_internal/lifetimes.rs +++ b/vir/defs/high/operations_internal/lifetimes.rs @@ -4,6 +4,7 @@ use super::{ default_fold_expression, default_fold_quantifier, default_walk_expression, ExpressionFolder, ExpressionWalker, }, + statement::*, position::Position, rvalue::*, ty::{self, LifetimeConst}, @@ -15,20 +16,84 @@ pub trait WithLifetimes { fn get_lifetimes(&self) -> Vec; } +fn get_lifetimes_with_arguments( + lifetimes: &[ty::LifetimeConst], + arguments: &Vec, +) -> Vec { + let mut all_lifetimes = lifetimes.to_owned(); + for ty in arguments { + for lifetime in ty.get_lifetimes() { + if !all_lifetimes.contains(&lifetime) { + all_lifetimes.push(lifetime); + } + } + } + all_lifetimes +} + +// impl WithLifetimes for mir::Statement { +// fn get_lifetimes(&self) -> Vec { +// match self.kind() { +// _ => vec![] +// } +// } +// } + +// impl WithLifetimes for Statement { +// fn get_lifetimes(&self) -> Vec { +// match self { +// Self::LifetimeTake(lifetime_take) => lifetime_take.get_lifetimes(), +// _ => vec![] +// } +// } +// } +// +// impl WithLifetimes for LifetimeTake { +// fn get_lifetimes(&self) -> Vec { +// let mut lifetimes = vec![ LifetimeConst{ name: self.target.name.clone() }]; +// for value in &self.value { +// lifetimes.push( +// LifetimeConst{ name: value.name.clone() } +// ); +// } +// 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![], } }