Merge #1093

1093: Add Lifetimes Support for LoopInvariant r=vakaras a=pascal-huber

Add Lifetime relations to loop invariants


Co-authored-by: Pascal Huber <[email protected]>

prusti-interface/src/environment/mir_body/borrowck/lifetimes/mod.rs

@@ -54,6 +54,13 @@ impl Lifetimes {
             .collect()
     }
 
+    pub fn get_loan_live_at_mid(&self, location: mir::Location) -> BTreeSet<String> {
+        let info = self.get_loan_live_at(RichLocation::Mid(location));
+        info.into_iter()
+            .map(|x| opaque_lifetime_string(x.index()))
+            .collect()
+    }
+
     pub fn get_origin_contains_loan_at_start(
         &self,
         location: mir::Location,

prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/enums.rs

@@ -7,20 +7,24 @@ enum Enum1 {
     A(i32),
     B(i32),
 }
+
 fn test1() {
     let x = Enum1::A(4);
     let y = &x;
 }
+
 fn test1_assert_false() {
     let x = Enum1::A(4);
     let y = &x;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+
 fn test2() {
     let mut x = Enum1::A(4);
     let mut y = &mut x;
     let z = &mut y;
 }
+
 fn test2_assert_false() {
     let mut x = Enum1::A(4);
     let mut y = &mut x;
@@ -32,44 +36,52 @@ enum Enum2<'a> {
     A(&'a mut i32),
     B(&'a i32)
 }
+
 fn test3() {
     let mut n = 4;
     let x = Enum2::A(&mut n);
     let y = &x;
 }
+
 fn test3_assert_false() {
     let mut n = 4;
     let x = Enum2::A(&mut n);
     let y = &x;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+
 fn test4() {
     let n = 4;
     let x = Enum2::B(&n);
     let y = &x;
 }
+
 fn test4_assert_false() {
     let n = 4;
     let x = Enum2::B(&n);
     let y = &x;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+
 fn test5() {
     let mut n = 4;
     let mut x = Enum2::A(&mut n);
     let y = &mut x;
 }
+
 fn test5_assert_false() {
     let mut n = 4;
     let mut x = Enum2::A(&mut n);
     let y = &mut x;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+
 fn test6() {
     let n = 4;
     let mut x = Enum2::B(&n);
     let y = &mut x;
 }
+
 fn test6_assert_false() {
     let n = 4;
     let mut x = Enum2::B(&n);
@@ -139,3 +151,18 @@ fn test9_assert_false(){
     let r = &mut e;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+fn test10(){
+    let n = 5;
+    let mut a = D{ x: &n };
+    let mut b = &mut a;
+    let mut c = &mut b;
+    let mut _d = &mut c;
+}
+fn test10_assert_false(){
+    let n = 5;
+    let mut a = D{ x: &n };
+    let mut b = &mut a;
+    let mut c = &mut b;
+    let mut _d = &mut c;
+    assert!(false);      //~ ERROR: the asserted expression might not hold
+}

prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/loops.rs

@@ -25,15 +25,35 @@ impl<'a, T> Iterator for WrapperIterator<'a, T> {
 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 {
-        // *x = 4;
+        s = x;
     }
+    *s = 4;
+    assert!(*s == 4);
 }
-fn test1_assert_false() {
+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 {
-        // *x = 4;
+        s = x;
     }
-    assert!(false) //~ ERROR
+    assert!(*s == 4);      //~ ERROR: the asserted expression might not hold
+    *s = 4;
 }

prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/simple.rs

@@ -59,6 +59,20 @@ pub fn shared_reborrow_assert_false() {
     assert!(*z == 5);      //~ ERROR: the asserted expression might not hold
 }
 
+pub fn simple_references() {
+    let mut a = 4;
+    let mut b = &mut a;
+    let mut c = &mut b;
+    let mut d = &mut c;
+}
+pub fn simple_references_assert_false() {
+    let mut a = 4;
+    let mut b = &mut a;
+    let mut c = &mut b;
+    let mut d = &mut c;
+    assert!(false);      //~ ERROR: the asserted expression might not hold
+}
+
 // FIXME: Fix overlapping shared references
 // pub fn shared_borrow() {
 //     let mut a = 4;

prusti-tests/tests/verify_overflow/fail/unsafe_core_proof/structs.rs

@@ -46,6 +46,21 @@ fn struct_with_mut_reference_assert_false () {
     let u = &t;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+fn struct_shared_references(){
+    let mut n = 4;
+    let s1 = S2{ x: &mut n};
+    let s2 = &s1;
+    let s3 = &s2;
+    let _s4 = &s3;
+}
+fn struct_shared_references_assert_false(){
+    let mut n = 4;
+    let s1 = S2{ x: &mut n};
+    let s2 = &s1;
+    let s3 = &s2;
+    let _s4 = &s3;
+    assert!(false);      //~ ERROR: the asserted expression might not hold
+}
 
 struct S3<'a> {
     x: &'a u32,
@@ -63,6 +78,20 @@ fn struct_with_shared_reference_assert_false () {
     let u = &mut t2;
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
+fn struct_mut_references(){
+    let n = 4;
+    let mut s1 = S3{ x: &n};
+    let mut s2 = &mut s1;
+    let mut s3 = &mut s2;
+    let mut s4 = &mut s3;
+}
+fn struct_mut_references_assert_false(){
+    let n = 4;
+    let mut s1 = S3{ x: &n};
+    let mut s2 = &mut s1;
+    let mut s3 = &mut s2;
+    let mut _s4 = &mut s3;
+}
 
 struct S4I<'a> {
     x: &'a mut u32,
@@ -127,6 +156,29 @@ fn struct_with_subset_lifetime_assert_false() {
     assert!(false);      //~ ERROR: the asserted expression might not hold
 }
 
+struct S7_1<'a> {
+    x: &'a mut u32,
+}
+struct S7_2<'a, 'b> {
+    x: &'b mut S7_1<'a>,
+}
+struct S7_3<'a, 'b, 'c> {
+    x: &'c mut S7_2<'a, 'b>,
+}
+fn test_deeply_nested(){
+    let mut n = 4;
+    let mut s1 = S7_1{ x: &mut n };
+    let mut s2 = S7_2{ x: &mut s1 };
+    let mut s3 = S7_3{ x: &mut s2 };
+}
+fn test_deeply_nested_assert_false(){
+    let mut n = 4;
+    let mut s1 = S7_1{ x: &mut n };
+    let mut s2 = S7_2{ x: &mut s1 };
+    let mut s3 = S7_3{ x: &mut s2 };
+    assert!(false);      //~ ERROR: the asserted expression might not hold
+}
+
 // FIXME: Nested structs with "shared" lifetimes don't work due to "lifetime extension"
 // struct S6I<'a> {
 //     x: &'a u32,

prusti-viper/src/encoder/mir/procedures/encoder/loops.rs

@@ -86,6 +86,39 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> {
             }
         }
 
+        // Encode Lifetime Relations
+        let derived_lifetimes = self
+            .lifetimes
+            .get_origin_contains_loan_at_mid(invariant_location);
+        for (derived_lifetime, derived_from) in derived_lifetimes {
+            let derived_from_args: Vec<vir_high::Expression> = derived_from
+                .iter()
+                .map(|x| {
+                    vir_high::VariableDecl {
+                        name: x.clone(),
+                        ty: vir_high::Type::Lifetime,
+                    }
+                    .into()
+                })
+                .collect();
+            let intersect_expr = vir_high::Expression::builtin_func_app_no_pos(
+                vir_high::BuiltinFunc::LifetimeIntersect,
+                vec![], // NOTE: we ignore argument_types for LifetimeItersect
+                derived_from_args,
+                vir_high::ty::Type::Lifetime,
+            );
+            let equality_expr = vir_high::Expression::binary_op_no_pos(
+                vir_high::BinaryOpKind::EqCmp,
+                vir_high::VariableDecl {
+                    name: derived_lifetime,
+                    ty: vir_high::ty::Type::Lifetime,
+                }
+                .into(),
+                intersect_expr,
+            );
+            encoded_specs.push(equality_expr);
+        }
+
         // Construct the info.
         let loop_invariant = vir_high::Statement::loop_invariant_no_pos(
             self.encode_basic_block_label(loop_head),

prusti-viper/src/encoder/mir/procedures/passes/loop_desugaring.rs

@@ -52,6 +52,11 @@ pub(in super::super) fn desugar_loops<'v, 'tcx: 'v>(
             .unwrap()
             .unwrap_loop_invariant();
 
+        invariant_block
+            .statements
+            .push(vir_high::Statement::comment(
+                "Loop Invariant Functional Specifications".to_string(),
+            ));
         for assertion in &loop_invariant.functional_specifications {
             let statement = encoder.set_surrounding_error_context_for_statement(
                 vir_high::Statement::assert_no_pos(assertion.clone()),
@@ -64,6 +69,12 @@ pub(in super::super) fn desugar_loops<'v, 'tcx: 'v>(
         // Note: It is important for soundness that we havoc here everything
         // that could potentially be mutated in the loop body. This means that
         // we should always fully havoc all aliased memory.
+
+        invariant_block
+            .statements
+            .push(vir_high::Statement::comment(
+                "Loop Invariant Maybe Modified Places".to_string(),
+            ));
         for predicate in loop_invariant.maybe_modified_places {
             let statement = encoder.set_surrounding_error_context_for_statement(
                 vir_high::Statement::havoc_no_pos(predicate),