aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-16 09:13:19 +0200
committerJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-16 09:13:19 +0200
commit31374ebcf4f2cb85adba3f0f861b8bf2addaeb50 (patch)
tree09ff5e3121afc4393ed40d05558ecd471d677722
parentbbe9efbc9b60c5ba0a67077cd06438dc805f0478 (diff)
downloadcompcert-kvx-31374ebcf4f2cb85adba3f0f861b8bf2addaeb50.tar.gz
compcert-kvx-31374ebcf4f2cb85adba3f0f861b8bf2addaeb50.zip
Insert final restoration code at very end of superblock if possible
-rw-r--r--scheduling/MyRTLpathScheduleraux.ml45
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