Handle Unconstrained Lifetimes in Loops

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<Region> = 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<Region> {

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
+}

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<i32> = WrapperIterator::new(&mut ve);
-    for x in &mut v {}
+// fn test1() {
+//     let mut ve = Vec::new();
+//     let mut v: WrapperIterator<i32> = WrapperIterator::new(&mut ve);
+//     for x in &mut v {}
+// }
+// fn test1_assert_false() {
+//     let mut ve = Vec::new();
+//     let mut v: WrapperIterator<i32> = 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<i32> = 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<i32> = 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<X> = WrapperIterator::new(&mut ve);
+// }
+// fn test3_assert_false() {
+//     let mut ve = Vec::new();
+//     let mut v: WrapperIterator<X> = WrapperIterator::new(&mut ve);
+//     assert!(false);      //~ ERROR: the asserted expression might not hold
+// }
+fn test4() {
     let mut ve = Vec::new();
-    let mut v: WrapperIterator<i32> = WrapperIterator::new(&mut ve);
+    let mut v: WrapperIterator<X> = 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<i32> = 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<i32> = 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<X> = WrapperIterator::new(&mut ve);
+//     for x in &mut v {}
+//     assert!(false);      //~ ERROR: the asserted expression might not hold
+// }

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> {

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::*;
 

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<usize>,
     encoded_lifetime_included_intersect_axiom: FxHashSet<usize>,
 }
@@ -41,6 +42,7 @@ pub(in super::super) trait LifetimesInterface {
     ) -> SpannedEncodingResult<Vec<vir_low::Expression>>;
     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,