From 77e37a05de1a7c604f65ec0d544703315ca0363d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Tue, 14 Mar 2023 23:03:57 +0900
Subject: [PATCH] fix a bug where protecting ghost vars were not introduced at
the proper sites
---
src/optimize_machine.ml | 203 ++++++++++++++++++++++++----------------
1 file changed, 120 insertions(+), 83 deletions(-)
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 86445bdf..e2e75fbc 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -794,6 +794,18 @@ let instr_cons instr cont =
| false, _ ->
instr :: cont
+let rec remove_skips_instrs instrs =
+ let aux instr =
+ match instr.instr_desc with
+ | MBranch (e, hl, b) ->
+ let hl = List.map (fun (h, l) -> h, remove_skips_instrs l) hl in
+ { instr with instr_desc = MBranch (e, hl, b) }
+ | _ ->
+ instr
+ in
+ List.fold_left (fun instrs i -> instr_cons (aux i) instrs) [] instrs
+ |> List.rev
+
(* XXX: UNUSED *)
(* let rec instr_remove_skip instr cont =
* match get_instr_desc instr with
@@ -874,8 +886,8 @@ let rec instr_replace_var m fvar instrs instr =
match instr.instr_desc with
| MLocalAssign (i, v) ->
let v = value_replace_var fvar v in
- let i = fvar i in
- MLocalAssign (i, v)
+ let i' = fvar i in
+ MLocalAssign (i', v)
| MStateAssign (i, v) ->
MStateAssign (i, value_replace_var fvar v)
| MStep (il, i, vl) ->
@@ -886,13 +898,10 @@ let rec instr_replace_var m fvar instrs instr =
List.fold_left
(fun hl (h, il) ->
let il = instrs_replace_var m fvar il in
- (* Format.(printf "%s: before %a after %a@." h (IMap.pp
- pp_print_int) asg (IMap.pp pp_print_int) asg''); *)
(h, il) :: hl)
[]
hl
in
- (* Format.(printf "%a@." (IMap.pp pp_print_int) asg); *)
MBranch (value_replace_var fvar g, List.rev hl, e)
| MSetReset _
| MNoReset _
@@ -902,7 +911,7 @@ let rec instr_replace_var m fvar instrs instr =
| MComment _ ->
instr.instr_desc
in
- instr_cons { instr with instr_desc } instrs
+ { instr with instr_desc } :: instrs
and instrs_replace_var m fvar instrs =
let instrs = List.fold_left (instr_replace_var m fvar) [] instrs in
@@ -932,72 +941,82 @@ and add_ghost_assigns fvar = List.map (add_ghost_assign fvar)
let ghost_vd v = { v with var_id = "__" ^ v.var_id }
let add_ghost_assigns_reassigned rasg instrs =
- let _, instrs, _ =
- List.fold_left
- (fun (rasg, instrs, fvar) instr ->
- let rec aux rasg instr fvar =
- match instr.instr_desc with
- | MLocalAssign (i, _) when VSet.mem i rasg ->
- ( VSet.remove i rasg,
- {
- instr with
- instr_spec =
- add_ghost_assign_spec
- (ghost_vd i)
- (vdecl_to_val i)
- instr.instr_spec;
- },
- fun v -> if v = i then ghost_vd i else fvar v )
- | MStep (il, _, _) ->
- let il = List.filter (fun i -> VSet.mem i rasg) il in
- let rasg, instr_spec, fvar =
- List.fold_left
- (fun (rasg, spec, fvar) i ->
- ( VSet.remove i rasg,
- add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec,
- fun v -> if v = i then ghost_vd i else fvar v ))
- (rasg, instr.instr_spec, fvar)
- il
- in
- rasg, { instr with instr_spec }, fvar
- | MBranch (e, hl, b) ->
- let rasg, fvar, hl =
+ 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' ->
+ ( {
+ instr with
+ instr_spec =
+ add_ghost_assign_spec
+ (ghost_vd i)
+ (vdecl_to_val i)
+ instr.instr_spec;
+ },
+ fun v -> if v = i then ghost_vd i else fvar v )
+ | _ ->
+ instr, fvar
+ in
+ n + 1, instr, fvar
+ | MStep (il, _, _) ->
+ let il =
+ List.filter
+ (fun i ->
+ match VMap.find_opt i rasg with Some n' -> n = n' | _ -> false)
+ il
+ in
+ let instr_spec, fvar =
+ List.fold_left
+ (fun (spec, fvar) i ->
+ ( add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec,
+ fun v -> if v = i then ghost_vd i else fvar v ))
+ (instr.instr_spec, fvar)
+ il
+ in
+ n + 1, { instr with instr_spec }, fvar
+ | MBranch (e, hl, b) ->
+ let n, fvar, hl =
+ List.fold_left
+ (fun (n, fvar, hl) (h, l) ->
+ let n, fvar, l =
List.fold_left
- (fun (rasg, fvar, hl) (h, l) ->
- let rasg, fvar, l =
- List.fold_left
- (fun (rasg, fvar, l) i ->
- let rasg, i, fvar = aux rasg i fvar in
- rasg, fvar, i :: l)
- (rasg, fvar, [])
- l
- in
- rasg, fvar, (h, List.rev l) :: hl)
- (rasg, fvar, [])
- hl
+ (fun (n, fvar, l) i ->
+ let n, i, fvar = aux n i fvar in
+ n, fvar, i :: l)
+ (n, fvar, [])
+ l
in
- rasg, { instr with instr_desc = MBranch (e, List.rev hl, b) }, fvar
- | _ ->
- rasg, instr, fvar
- in
- let rasg, instr, fvar = aux rasg instr fvar in
+ n, fvar, (h, List.rev l) :: hl)
+ (n, fvar, [])
+ hl
+ in
+ n, { instr with instr_desc = MBranch (e, List.rev hl, b) }, fvar
+ | _ ->
+ n + 1, instr, fvar
+ in
+ let _, instrs, _ =
+ List.fold_left
+ (fun (n, instrs, fvar) instr ->
+ let n, instr, fvar = aux n instr fvar in
let instr_spec =
List.map (fun (t, b) -> instr_spec_replace fvar t, b) instr.instr_spec
in
- rasg, { instr with instr_spec } :: instrs, fvar)
- (rasg, [], fun v -> v)
+ n, { instr with instr_spec } :: instrs, fvar)
+ (0, [], fun v -> v)
instrs
in
List.rev instrs
module IntS = Set.Make (Int)
-let add_assigned k v =
+let add_assigned n k v =
VMap.update v (function
| Some (n, ks) as b ->
- if k > IntS.max_elt ks then Some (n + 1, IntS.add k ks) else b
+ if k > IntS.max_elt ks then Some (n, IntS.add k ks) else b
| None ->
- Some (1, IntS.singleton k))
+ Some (n, IntS.singleton k))
let silly_asg i v =
match v.value_desc with Var w -> w.var_id = i.var_id | _ -> false
@@ -1025,55 +1044,73 @@ 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 asg instr =
+ let rec asg_instr (n, k, asg) instr =
+ (* k: instruction block index (equation index) n: instruction index
+ (absolute) *)
match instr.instr_desc with
| MLocalAssign (i, v) ->
- if silly_asg i v then asg else add_assigned k i asg
+ n + 1, k + 1, if silly_asg i v then asg else add_assigned n k i asg
| MStep (il, _, _) ->
- List.fold_right (add_assigned k) il asg
+ n + 1, k + 1, List.fold_right (add_assigned n k) il asg
| MBranch (_, hl, _) ->
- List.fold_left
- (fun asg' (_, il) ->
- let asg'' = List.fold_left (asg_instr k) asg il in
- VMap.union (fun _ n1 n2 -> Some (max n1 n2)) asg' asg'')
- VMap.empty
- hl
+ let n, k, 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)
+ hl
+ in
+ n, k + 1, asg
| _ ->
- asg
+ n + 1, k + 1, asg
in
let assigned asg instrs =
- 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 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 *)
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 *)
- (* Format.printf "AVANT %a@." (VMap.pp pp) asg; *)
+ let pp fmt (k, s) =
+ Format.(
+ fprintf fmt "%n{@[%a}@]" k (pp_comma_list pp_print_int) (IntS.elements s))
+ 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
- (* Format.printf "APRES %a@." (VMap.pp pp) asg; *)
let rasg =
- VMap.fold
- (fun v (n, _) rasg -> if n > 1 then VSet.add v rasg else rasg)
+ VMap.filter_map
+ (fun _ (n, ks) -> if IntS.cardinal ks > 1 then Some n else None)
asg
- VSet.empty
+ (* 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 *)
let step_instrs = add_ghost_assigns_reassigned rasg step_instrs in
(* not SSA anymore *)
+ let step_instrs = remove_skips_instrs step_instrs in
{ step with step_checks; step_locals; step_instrs }
let machine_replace_variables reuse m =
--
GitLab