From 3cb1ac888f0b3522c76eb3128810cea1d1f921a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Tue, 14 Mar 2023 16:35:09 +0900
Subject: [PATCH] apply the same fix to 'reassigned' ghost assignments
---
src/backends/C/c_backend_src.ml | 4 ++
src/optimize_machine.ml | 100 ++++++++++++--------------------
2 files changed, 41 insertions(+), 63 deletions(-)
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 7e3267f4..b03c4c24 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -422,8 +422,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
e
(List.length hl)))
hl
+ | MSpec "" ->
+ ()
| MSpec s ->
fprintf fmt "@[/*@@ %s */@]@ " s
+ | MComment "" ->
+ ()
| MComment s ->
fprintf fmt "/* %s */" s
in
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index cde625bc..86445bdf 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -787,7 +787,8 @@ and instrs_are_skip instrs = List.for_all instr_is_skip instrs
let instr_cons instr cont =
match instr_is_skip instr, cont with
| true, [] ->
- [ { instr with instr_desc = MComment "" } ]
+ if instr.instr_spec = [] then []
+ else [ { instr with instr_desc = MComment "" } ]
| true, i :: cont ->
{ i with instr_spec = i.instr_spec @ instr.instr_spec } :: cont
| false, _ ->
@@ -927,36 +928,6 @@ let rec add_ghost_assign fvar instr =
instr
and add_ghost_assigns fvar = List.map (add_ghost_assign fvar)
-(* let is_reused_def v = Hashtbl.find_opt reuse v.var_id in *)
-(* let add_reused vars i = *)
-(* let v = fvar i in *)
-(* if v.var_id = i.var_id then vars else VMap.add i v vars *)
-(* in *)
-(* let rec is_defining_reused vars instr = *)
-(* match instr.instr_desc with *)
-(* | MLocalAssign (i, _) -> *)
-(* add_reused vars i *)
-(* | MStep (il, _, _) -> *)
-(* List.fold_left add_reused vars il *)
-(* | MBranch (_, hl, _) -> *)
-(* List.fold_left *)
-(* (fun vars (_, instrs) -> List.fold_left is_defining_reused vars instrs) *)
-(* vars *)
-(* hl *)
-(* | _ -> *)
-(* vars *)
-(* in *)
-(* List.map *)
-(* (fun instr -> *)
-(* let vars = is_defining_reused VMap.empty instr in *)
-(* let instr_spec = *)
-(* VMap.fold *)
-(* (fun i v -> add_ghost_assign_spec i (vdecl_to_val v)) *)
-(* vars *)
-(* instr.instr_spec *)
-(* in *)
-(* { instr with instr_spec }) *)
-(* instrs *)
let ghost_vd v = { v with var_id = "__" ^ v.var_id }
@@ -968,47 +939,50 @@ let add_ghost_assigns_reassigned rasg instrs =
match instr.instr_desc with
| MLocalAssign (i, _) when VSet.mem i rasg ->
( VSet.remove i rasg,
- add_ghost_assign_spec
- (ghost_vd i)
- (vdecl_to_val i)
- instr.instr_spec,
+ {
+ 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
- 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
- | MBranch (_, hl, _) ->
- let rasg' =
+ 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 =
List.fold_left
- (fun rasg (_, instrs) ->
- List.fold_left
- (fun rasg instr ->
- let rasg, _, _ = aux rasg instr fvar in
- rasg)
- rasg
- instrs)
- rasg
+ (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
in
- let rasg'' = VSet.diff rasg rasg' in
- ( rasg',
- VSet.fold
- (fun i spec ->
- add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec)
- rasg''
- instr.instr_spec,
- fun v -> if VSet.mem v rasg'' then ghost_vd v else fvar v )
+ rasg, { instr with instr_desc = MBranch (e, List.rev hl, b) }, fvar
| _ ->
- rasg, instr.instr_spec, fvar
+ rasg, instr, fvar
in
- let rasg, instr_spec, fvar = aux rasg instr fvar in
+ let rasg, instr, fvar = aux rasg instr fvar in
let instr_spec =
- List.map (fun (t, b) -> instr_spec_replace fvar t, b) 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)
--
GitLab