From ac33d0914303798dfe1d86e2b5a2710106276748 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Wed, 15 Mar 2023 04:12:04 +0900
Subject: [PATCH] fix introduction of '__' ghost vars in branches
---
src/optimize_machine.ml | 88 +++++++++++++++++++++--------------------
1 file changed, 45 insertions(+), 43 deletions(-)
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index c24567ad..15704783 100644
--- a/src/optimize_machine.ml
+++ b/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 *)
--
GitLab