fix: handle RevisitPlacement in symbolic revisit checks

Author: SaharRamezani

traceforge/src/exec_graph.rs

@@ -839,6 +839,30 @@ impl ExecutionGraph {
         }
     }
 
+    /// Change the rf of `pos` according to a revisit placement, dispatching to
+    /// `change_rf` for a single send or `change_inbox_rfs` for a whole inbox
+    /// send set. Used both for in-place revisits and for the symbolic what-if
+    /// checks that operate on a copied graph.
+    pub(crate) fn change_rf_placement(&mut self, pos: Event, placement: &RevisitPlacement) {
+        match placement {
+            RevisitPlacement::Default(send) => {
+                // Standard recv revisit: single rf edge.
+                self.change_rf(pos, Some(*send));
+            }
+            RevisitPlacement::Inbox(sends) => {
+                // Inbox revisit: whole set of chosen sends.
+                if sends.is_empty() {
+                    self.change_inbox_rfs(pos, None);
+                } else {
+                    let mut sorted = sends.clone();
+                    // Keep a canonical order for deterministic comparisons/printing.
+                    sorted.sort();
+                    self.change_inbox_rfs(pos, Some(sorted));
+                }
+            }
+        }
+    }
+
     fn check_spawn_invariants(&self) {
         // This function checks the consistency of the information about which thread spawned
         // which, and at what event number.

traceforge/src/must.rs

@@ -1043,6 +1043,7 @@ impl Must {
         solver
     }
 
+    // TODO: This code is never run. Change it in the future.
     #[cfg(feature = "symbolic")]
     fn symbolic_backward_revisit_is_sat(&self, rev: &Revisit) -> bool {
         if !self.config.symbolic {
@@ -1051,7 +1052,7 @@ impl Must {
 
         let view = self.current.graph.revisit_view(rev);
         let mut g = self.current.graph.copy_to_view(&view);
-        g.change_rf(rev.pos, Some(rev.rev));
+        g.change_rf_placement(rev.pos, &rev.rev);
 
         self.symbolic_solver_for_graph(&g).is_sat()
     }
@@ -1060,7 +1061,7 @@ impl Must {
     fn is_maximal_constraint(&self, c: &ConstraintEval, rev: &Revisit) -> bool {
         let view = self.current.graph.revisit_view(rev);
         let mut g = self.current.graph.copy_to_view(&view);
-        g.change_rf(rev.pos, Some(rev.rev));
+        g.change_rf_placement(rev.pos, &rev.rev);
 
         let solver = self.symbolic_solver_for_graph(&g);
 
@@ -2157,25 +2158,7 @@ impl Must {
 
     /// Change an rf according to the revisit
     fn change_rf(&mut self, rev: &Revisit) {
-        match &rev.rev {
-            RevisitPlacement::Default(vv) => {
-                // Standard recv revisit: single rf edge.
-                self.current.graph.change_rf(rev.pos, Some(*vv));
-            }
-            RevisitPlacement::Inbox(vv) => {
-                // Inbox revisit: whole set of chosen sends.
-                if vv.is_empty() {
-                    self.current.graph.change_inbox_rfs(rev.pos, None);
-                } else {
-                    let mut vv_sorted = vv.clone();
-                    // Keep a canonical order for deterministic comparisons/printing.
-                    vv_sorted.sort();
-                    self.current
-                        .graph
-                        .change_inbox_rfs(rev.pos, Some(vv_sorted));
-                }
-            }
-        }
+        self.current.graph.change_rf_placement(rev.pos, &rev.rev);
     }
 
     fn pick_revisit(&mut self, revs: Vec<Event>, pos: Event) {