fix introduction of '__' ghost vars in branches

src/optimize_machine.ml

@@ -940,13 +940,15 @@ and add_ghost_assigns fvar = List.map (add_ghost_assign fvar)
 
 let ghost_vd v = { v with var_id = "__" ^ v.var_id }
 
+module IntS = Set.Make (Int)
+
 let add_ghost_assigns_reassigned rasg instrs =
   let rec aux n instr fvar =
     match instr.instr_desc with
     | MLocalAssign (i, _) ->
       let instr, fvar =
         match VMap.find_opt i rasg with
-        | Some n' when n = n' ->
+        | Some ns when IntS.exists (( = ) n) ns ->
           ( {
               instr with
               instr_spec =
@@ -964,7 +966,11 @@ let add_ghost_assigns_reassigned rasg instrs =
       let il =
         List.filter
           (fun i ->
-            match VMap.find_opt i rasg with Some n' -> n = n' | _ -> false)
+            match VMap.find_opt i rasg with
+            | Some ns ->
+              IntS.exists (( = ) n) ns
+            | _ ->
+              false)
           il
       in
       let instr_spec, fvar =
@@ -1009,14 +1015,20 @@ let add_ghost_assigns_reassigned rasg instrs =
   in
   List.rev instrs
 
-module IntS = Set.Make (Int)
-
+(* we build a map v -> (ns, k, ks) where
+ * v is an assigned var,
+ * ns the set of locations where it is written originally in SSA,
+ * k the equation index where it is originally written,
+ * and ks the equation indexes where it is written (rewritten) *)
 let add_assigned n k v =
   VMap.update v (function
-      | Some (n, ks) as b ->
-        if k > IntS.max_elt ks then Some (n, IntS.add k ks) else b
+      | Some (ns, k', ks) as b ->
+        let km = IntS.max_elt ks in
+        if k = k' then Some (IntS.add n ns, k', ks)
+        else if k > km then Some (ns, k', IntS.add k ks)
+        else b
       | None ->
-        Some (n, IntS.singleton k))
+        Some (IntS.singleton n, k, IntS.singleton k))
 
 let silly_asg i v =
   match v.value_desc with Var w -> w.var_id = i.var_id | _ -> false
@@ -1044,52 +1056,47 @@ let step_replace_var m reuse step =
   let step_checks =
     List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks
   in
-  let rec asg_instr (n, k, asg) instr =
-    (* k: instruction block index (equation index) n: instruction index
-       (absolute) *)
+  let rec asg_instr k (n, asg) instr =
+    (* k: instruction block index (equation index)
+     * n: instruction index (absolute) *)
     match instr.instr_desc with
     | MLocalAssign (i, v) ->
-      n + 1, k + 1, if silly_asg i v then asg else add_assigned n k i asg
+      n + 1, if silly_asg i v then asg else add_assigned n k i asg
     | MStep (il, _, _) ->
-      n + 1, k + 1, List.fold_right (add_assigned n k) il asg
+      n + 1, List.fold_right (add_assigned n k) il asg
     | MBranch (_, hl, _) ->
-      let n, k, asg =
+      let n, asg =
         List.fold_left
-          (fun (n, _, asg') (_, il) ->
-            let n, _, asg'' = List.fold_left asg_instr (n, k, asg) il in
-            ( n,
-              k,
-              VMap.union
-                (fun _ ((_, ks1) as x1) ((_, ks2) as x2) ->
-                  if IntS.(cardinal ks1 > cardinal ks2) then Some x1
-                  else Some x2)
-                asg'
-                asg'' ))
-          (n, k, VMap.empty)
+          (fun (n, asg) (_, il) ->
+            let n, asg = List.fold_left (asg_instr k) (n, asg) il in
+            n, asg)
+          (n, asg)
           hl
       in
-      n, k + 1, asg
+      n, asg
     | _ ->
-      n + 1, k + 1, asg
+      n + 1, asg
   in
   let assigned asg instrs =
-    let _, _, asg = List.fold_left asg_instr (0, 0, asg) instrs in
-    (* let asg, _ = *)
-    (*   List.fold_left *)
-    (*     (fun (asg, k) instr -> asg_instr k asg instr, k + 1) *)
-    (*     (asg, 0) *)
-    (*     instrs *)
-    (* in *)
+    let _, (_, asg) =
+      List.fold_left
+        (fun (k, acc) i -> k + 1, asg_instr k acc i)
+        (0, (0, asg))
+        instrs
+    in
     asg
   in
   (* SSA *)
   let step_instrs = add_ghost_assigns fvar step.step_instrs in
   (* register the locations of assignments *)
   let asg = assigned VMap.empty step_instrs in
-  let pp fmt (k, s) =
-    Format.(
-      fprintf fmt "%n{@[%a}@]" k (pp_comma_list pp_print_int) (IntS.elements s))
-  in
+  (* let pp fmt (ns, k, ks) = *)
+  (*   Format.( *)
+  (*     fprintf fmt "[%a]%n{@[%a}@]" *)
+  (*       (pp_comma_list pp_print_int) (IntS.elements ns) *)
+  (*       k *)
+  (*       (pp_comma_list pp_print_int) (IntS.elements ks)) *)
+  (* in *)
   (* Format.printf "AVANT %a@." (VMap.pp pp) asg; *)
   (* SSA *)
   let step_instrs = instrs_replace_var m fvar step_instrs in
@@ -1098,13 +1105,8 @@ let step_replace_var m reuse step =
   let asg = assigned asg step_instrs in
   let rasg =
     VMap.filter_map
-      (fun _ (n, ks) -> if IntS.cardinal ks > 1 then Some n else None)
+      (fun _ (ns, _, ks) -> if IntS.cardinal ks > 1 then Some ns else None)
       asg
-    (* VMap.fold *)
-    (* (fun v (_, ks) rasg -> if IntS.cardinal ks > 1 then VSet.add v rasg else
-       rasg) *)
-    (*   asg *)
-    (*   VSet.empty *)
   in
   (* Format.printf "APRES %a@." (VMap.pp pp) asg; *)
   (* not SSA anymore *)