aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-16 09:12:08 +0200
committerJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-16 09:12:08 +0200
commitbbe9efbc9b60c5ba0a67077cd06438dc805f0478 (patch)
tree2087d28a10846c1019808e9fb65d3bbf6b07637f
parent6c90b08a1451e212d48f96d2fdd23c0c85f40bab (diff)
downloadcompcert-kvx-bbe9efbc9b60c5ba0a67077cd06438dc805f0478.tar.gz
compcert-kvx-bbe9efbc9b60c5ba0a67077cd06438dc805f0478.zip
More appropriate name for function
-rw-r--r--scheduling/MyRTLpathScheduleraux.ml7
1 files changed, 2 insertions, 5 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml
index 547019a9..c1caf6c0 100644
--- a/scheduling/MyRTLpathScheduleraux.ml
+++ b/scheduling/MyRTLpathScheduleraux.ml
@@ -380,7 +380,7 @@ let local_single_assignment sb code liveatentry ~next_free_reg =
debug_flag := old_debug_flag;
(code, live_renames, next_free_reg)
-let restoration_instructions sb code live_renames =
+let final_restoration_code sb code live_renames =
let last_inst_pc = sb.instructions.(Array.length sb.instructions - 1) in
let last_inst = get_some @@ PTree.get last_inst_pc code in
let last_inst_is_basic = match last_inst with
@@ -1381,10 +1381,7 @@ let scheduler f =
let (sb_renamings, code, pm, next_free_pc) = ListLabels.fold_left sb_renamings
~init:([], code, pm, next_free_pc)
~f:(fun (sbs, code, pm, next_free_pc) (sb, live_renames) ->
- let nr_instr = Array.length sb.instructions in
- let last_pc = sb.instructions.(nr_instr - 1) in
- let final_renames = PTree.map (fun pc renames -> if Camlcoq.P.eq pc last_pc then renames else []) live_renames in
- let final_restoration = restoration_instructions final_renames in
+ let final_restoration = final_restoration_code sb code live_renames in
let (sb, code, pm, next_free_pc, fwmap) = insert_code sb code pm final_restoration ~next_free_pc in
let live_renames =
PTree.fold