fix(constraints): apply assign to sync-split states before join

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/9fbe3c8e-0b5b-4c06-af38-fee7944ab663

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

Author: Copilot

src/analyses/mCP.ml

@@ -173,13 +173,13 @@ struct
     in
     iter (uncurry side_one) @@ group_assoc_eq V.equal xs
 
-  let rec do_splits ?(local_tf=Fun.id) man pv (xs:(int * (Obj.t * Events.t list)) list) emits =
+  let rec do_splits man pv (xs:(int * (Obj.t * Events.t list)) list) emits =
     let split_one n (d,emits') =
       let nv = assoc_replace (n,d) pv in
       (* Do split-specific emits before general emits.
          [emits] and [do_emits] are in reverse order.
          [emits'] is in normal order. *)
-      man.split (local_tf (do_emits man (emits @ List.rev emits') nv false)) []
+      man.split (do_emits man (emits @ List.rev emits') nv false) []
     in
     iter (uncurry split_one) xs
 
@@ -510,7 +510,7 @@ struct
     let d = do_emits man !emits d q in
     if q then raise Deadcode else d
 
-  let rec sync_with_split_tf transform_splits (man:(D.t, G.t, C.t, V.t) man) reason =
+  let sync (man:(D.t, G.t, C.t, V.t) man) reason =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
@@ -523,19 +523,10 @@ struct
     let d, q = map_deadcode f @@ spec_list man.local in
     do_sideg man !sides;
     do_spawns man !spawns;
-    let local_tf =
-      if transform_splits then
-        fun d -> sync_with_split_tf false {man with local = d} reason
-      else
-        Fun.id
-    in
-    do_splits ~local_tf man d !splits !emits;
+    do_splits man d !splits !emits;
     let d = do_emits man !emits d q in
     if q then raise Deadcode else d
 
-  and sync (man:(D.t, G.t, C.t, V.t) man) reason =
-    sync_with_split_tf true man reason
-
   let enter (man:(D.t, G.t, C.t, V.t) man) r f a =
     let spawns = ref [] in
     let sides  = ref [] in

src/framework/constraints.ml

@@ -140,10 +140,27 @@ struct
 
   let common_joins man ds splits spawns = common_join man (bigsqcup ds) splits spawns
 
+  let man_with_local (man: (D.t, S.G.t, S.C.t, S.V.t) man) (local: D.t) : (D.t, S.G.t, S.C.t, S.V.t) man =
+    let rec man' =
+      { man with
+        ask = (fun (type a) (q: a Queries.t) -> S.query man' q);
+        local;
+      }
+    in
+    man'
+
   let tf_assign var edge prev_node lv e getl sidel demandl getg sideg d =
     let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
+    let sync_splits = !r in
+    r := [];
     let d = S.assign man lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
-    common_join man d !r !spawns
+    let ds =
+      List.filter_map (fun split_d ->
+          try Some (S.assign (man_with_local man split_d) lv e)
+          with Deadcode -> None
+        ) sync_splits
+    in
+    common_joins man (d :: ds) !r !spawns
 
   let tf_vdecl var edge prev_node v getl sidel demandl getg sideg d =
     let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in