diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-16 09:13:19 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-16 09:13:19 +0200 |
commit | 31374ebcf4f2cb85adba3f0f861b8bf2addaeb50 (patch) | |
tree | 09ff5e3121afc4393ed40d05558ecd471d677722 | |
parent | bbe9efbc9b60c5ba0a67077cd06438dc805f0478 (diff) | |
download | compcert-kvx-31374ebcf4f2cb85adba3f0f861b8bf2addaeb50.tar.gz compcert-kvx-31374ebcf4f2cb85adba3f0f861b8bf2addaeb50.zip |
Insert final restoration code at very end of superblock if possible
-rw-r--r-- | scheduling/MyRTLpathScheduleraux.ml | 45 |
1 files changed, 23 insertions, 22 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml index c1caf6c0..4c8be5f2 100644 --- a/scheduling/MyRTLpathScheduleraux.ml +++ b/scheduling/MyRTLpathScheduleraux.ml @@ -392,29 +392,30 @@ let final_restoration_code sb code live_renames = | Icond _ -> false | _ -> true in - let open Either in - let to_insert = - PTree.fold - (fun to_insert side_exit_pc renames -> - let live_regs_opt = PTree.get side_exit_pc sb.liveins in - let (above, below) = - ListLabels.partition_map renames - ~f:(fun {old_name; new_name} -> - let inst = Iop (Op.Omove, [new_name], old_name, Camlcoq.P.one) in - match last_inst_is_basic, live_regs_opt with - | true, _ -> Right inst - | false, None -> Left inst - | false, Some live_regs -> - if Regset.mem old_name live_regs then - Left inst - else Right inst) - in - InsertPositionMap.add (InsertPosition.Above side_exit_pc) above to_insert - |> InsertPositionMap.add (InsertPosition.Below side_exit_pc) below) - live_renames - InsertPositionMap.empty + let final_renames = ptree_get_or_default live_renames last_inst_pc [] in + let live_regs_opt = PTree.get last_inst_pc sb.liveins in + let (above, below) = let open Either in + ListLabels.partition_map final_renames + ~f:(fun {old_name; new_name} -> + let inst = Iop (Op.Omove, [new_name], old_name, Camlcoq.P.one) in + match last_inst_is_basic, live_regs_opt with + | true, _ -> + (* Printf.eprintf "Putting %d below basic inst\n" (Camlcoq.P.to_int old_name); *) + Right inst + | false, None -> + (* Printf.eprintf "Putting %d above unpredicted icond.\n" (Camlcoq.P.to_int old_name); *) + Left inst + | false, Some live_regs -> + if Regset.mem old_name live_regs then ( + (* Printf.eprintf "Putting %d above icond\n" (Camlcoq.P.to_int old_name); *) + Left inst + ) else ( + (* Printf.eprintf "Putting %d below icond\n" (Camlcoq.P.to_int old_name); *) + Right inst)) in - to_insert + InsertPositionMap.empty + |> InsertPositionMap.add (InsertPosition.Above last_inst_pc) above + |> InsertPositionMap.add (InsertPosition.Below last_inst_pc) below let used_before_redefinition sb code ~offset ~reg = let length = Array.length sb.instructions in |