Update checker with new fpcs

viperproject · Oct 25, 2023 · 348623d · 348623d
1 parent 741284e
commit 348623d
Showing 1 changed file with 24 additions and 4 deletions.
diff --git a/mir-state-analysis/src/coupling_graph/check/checker.rs b/mir-state-analysis/src/coupling_graph/check/checker.rs
@@ -58,6 +58,7 @@ pub(crate) fn check<'tcx>(mut cg: CgAnalysis<'_, '_, 'tcx>, mut fpcs_cursor: Fre
         fpcs_cursor.set_bound_non_empty();
         let mut fpcs = Fpcs {
             summary: fpcs_cursor.initial_state().clone(),
+            apply_pre_effect: false,
             bottom: false,
             repackings: Vec::new(),
             repacker: rp,
@@ -89,16 +90,25 @@ pub(crate) fn check<'tcx>(mut cg: CgAnalysis<'_, '_, 'tcx>, mut fpcs_cursor: Fre
         fpcs_cursor.unset_bound();
 
         // Repacks
-        for op in fpcs_after.repacks {
+        for op in fpcs_after.repacks_middle {
             op.update_free(&mut fpcs.summary, false, rp);
         }
         // Couplings bound set
         let bound: Box<dyn Fn(Place<'tcx>) -> CapabilityKind> = Box::new(cg_state.mk_capability_upper_bound());
         fpcs.bound.borrow_mut().0 = Some(unsafe { std::mem::transmute(bound) });
         // Consistency
         fpcs.summary.consistency_check(rp);
-        // Statement
+        // Statement pre
+        assert!(fpcs.repackings.is_empty());
+        fpcs.apply_pre_effect = true;
+        fpcs.visit_terminator(data.terminator(), loc);
+        // Repacks
+        for op in fpcs_after.repacks {
+            op.update_free(&mut fpcs.summary, false, rp);
+        }
+        // Statement post
         assert!(fpcs.repackings.is_empty());
+        fpcs.apply_pre_effect = false;
         fpcs.visit_terminator(data.terminator(), loc);
         assert!(fpcs.repackings.is_empty());
         // Consistency
@@ -169,16 +179,26 @@ impl<'a, 'tcx> CouplingState<'a, 'tcx> {
         fpcs_cursor.unset_bound();
 
         // Repacks
-        for op in fpcs_after.repacks {
+        for op in fpcs_after.repacks_middle {
             op.update_free(&mut fpcs.summary, false, rp);
         }
         // Couplings bound set
         let bound: Box<dyn Fn(Place<'tcx>) -> CapabilityKind> = Box::new(self.mk_capability_upper_bound());
         fpcs.bound.borrow_mut().0 = Some(unsafe { std::mem::transmute(bound) }); // Extend lifetimes (safe since we unset it later)
         // Consistency
         fpcs.summary.consistency_check(rp);
-        // Statement
+        // Statement pre
+        assert!(fpcs.repackings.is_empty());
+        fpcs.apply_pre_effect = true;
+        fpcs.visit_statement(stmt, loc);
+        assert!(fpcs.repackings.is_empty());
+        // Repacks
+        for op in fpcs_after.repacks {
+            op.update_free(&mut fpcs.summary, false, rp);
+        }
+        // Statement post
         assert!(fpcs.repackings.is_empty());
+        fpcs.apply_pre_effect = false;
         fpcs.visit_statement(stmt, loc);
         assert!(fpcs.repackings.is_empty());
         // Consistency