aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-11 11:40:04 +0200
committerJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-11 11:40:04 +0200
commit511fd79173174df1f9c19a37751ebe7967c052c9 (patch)
treec165a940088d4b6ba95f703a7a97b4b26e89bea6
parent9e076df6b14e019b569e3a1c3c2e90ef797fe9d2 (diff)
downloadcompcert-kvx-511fd79173174df1f9c19a37751ebe7967c052c9.tar.gz
compcert-kvx-511fd79173174df1f9c19a37751ebe7967c052c9.zip
Add missing dependency for restoration_instructions'
-rw-r--r--scheduling/MyRTLpathScheduleraux.ml24
1 files changed, 24 insertions, 0 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml
index 293faccf..212867f4 100644
--- a/scheduling/MyRTLpathScheduleraux.ml
+++ b/scheduling/MyRTLpathScheduleraux.ml
@@ -410,6 +410,30 @@ let restoration_instructions sb code live_renames =
in
to_insert
+let used_before_redefinition sb code ~offset ~reg =
+ let length = Array.length sb.instructions in
+ if not (offset < length) then
+ raise (Invalid_argument (Printf.sprintf "offset must be less than the superblock's length: %d is not less than %d" offset length))
+ ;
+ let finished = ref false in
+ let i = ref offset in
+ let res = ref false in
+ while (!i < length && not !finished) do
+ let inst = get_some @@ PTree.get sb.instructions.(!i) code in
+ if List.mem reg (RTL.instr_uses inst) then (
+ res := true;
+ finished := true;
+ ) else
+ ()
+ ;
+ let defined_reg = RTL.instr_defs inst in
+ (match defined_reg with
+ | None -> ()
+ | Some r -> if r = reg then finished := true else ());
+ i := !i + 1;
+ done;
+ !res
+
type restoration_actions =
| Just_restore of renamed
| Restore_and_alias of renamed