diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-11 11:40:04 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-11 11:40:04 +0200 |
commit | 511fd79173174df1f9c19a37751ebe7967c052c9 (patch) | |
tree | c165a940088d4b6ba95f703a7a97b4b26e89bea6 | |
parent | 9e076df6b14e019b569e3a1c3c2e90ef797fe9d2 (diff) | |
download | compcert-kvx-511fd79173174df1f9c19a37751ebe7967c052c9.tar.gz compcert-kvx-511fd79173174df1f9c19a37751ebe7967c052c9.zip |
Add missing dependency for restoration_instructions'
-rw-r--r-- | scheduling/MyRTLpathScheduleraux.ml | 24 |
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 |