From 84372020cb71d0b417d8c8cb43f4c34f30c15a94 Mon Sep 17 00:00:00 2001
From: Christophe Garion <tofgarion@runbox.com>
Date: Fri, 24 Mar 2023 10:41:40 +0100
Subject: [PATCH] [optimizations] correct rewritting in conditionals for O3 (LB
patch)
---
src/optimize_machine.ml | 28 +++++++++++++++-------------
1 file changed, 15 insertions(+), 13 deletions(-)
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index bf8b3be3..bb8cab0c 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -1020,10 +1020,12 @@ let add_ghost_assigns_reassigned rasg instrs =
* ns the set of locations where it is written originally in SSA,
* k the equation index where it is originally written,
* b if there is a rewrite *)
-let add_assigned n k v =
+let add_assigned rasg n k v =
VMap.update v (function
| Some (ns, k', b) ->
- if k = k' then Some (IntS.add n ns, k', b)
+ if rasg then
+ Some (ns, k', b || k > k' || not (IntS.mem n ns))
+ else if k = k' then Some (IntS.add n ns, k', b)
else Some (ns, k', b || k > k')
| None ->
Some (IntS.singleton n, k, false))
@@ -1054,19 +1056,19 @@ 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 k (n, asg) instr =
+ let rec asg_instr rasg k (n, asg) instr =
(* k: instruction block index (equation index)
* n: instruction index (absolute) *)
match instr.instr_desc with
| MLocalAssign (i, v) ->
- n + 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 rasg n k i asg
| MStep (il, _, _) ->
- n + 1, List.fold_right (add_assigned n k) il asg
+ n + 1, List.fold_right (add_assigned rasg n k) il asg
| MBranch (_, hl, _) ->
let n, asg =
List.fold_left
(fun (n, asg) (_, il) ->
- let n, asg = List.fold_left (asg_instr k) (n, asg) il in
+ let n, asg = List.fold_left (asg_instr rasg k) (n, asg) il in
n, asg)
(n, asg)
hl
@@ -1075,10 +1077,10 @@ let step_replace_var m reuse step =
| _ ->
n + 1, asg
in
- let assigned asg instrs =
+ let assigned rasg asg instrs =
let _, (_, asg) =
List.fold_left
- (fun (k, acc) i -> k + 1, asg_instr k acc i)
+ (fun (k, acc) i -> k + 1, asg_instr rasg k acc i)
(0, (0, asg))
instrs
in
@@ -1087,20 +1089,20 @@ let step_replace_var m reuse step =
(* 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 (ns, k, ks) = *)
+ let asg = assigned false VMap.empty step_instrs in
+ (* let pp fmt (ns, k, b) = *)
(* Format.( *)
- (* fprintf fmt "[%a]%n{@[%a}@]" *)
+ (* fprintf fmt "[%a]%n:%a" *)
(* (pp_comma_list pp_print_int) (IntS.elements ns) *)
(* k *)
- (* (pp_comma_list pp_print_int) (IntS.elements ks)) *)
+ (* pp_print_bool b) *)
(* in *)
(* Format.printf "AVANT %a@." (VMap.pp pp) asg; *)
(* SSA *)
let step_instrs = instrs_replace_var m fvar step_instrs in
(* update the locations of assignments, consider as reassignments only the
ones appearing *after* the original one *)
- let asg = assigned asg step_instrs in
+ let asg = assigned true asg step_instrs in
let rasg =
VMap.filter_map
(fun _ (ns, _, b) -> if b then Some ns else None)
--
GitLab