diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-17 14:44:12 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-17 14:44:12 +0200 |
commit | 3a3649930a96412eae3a51ca329aee76581ee72c (patch) | |
tree | 7039e0a04aee55951bc1215b168b1b5490ad85b0 | |
parent | 0170983b100074c615600afb934b0813aaa761eb (diff) | |
download | compcert-kvx-3a3649930a96412eae3a51ca329aee76581ee72c.tar.gz compcert-kvx-3a3649930a96412eae3a51ca329aee76581ee72c.zip |
Work-around for prepass-past-side-exits error.
Before, downward scheduling would sometimes give an unverifiable result
because instructions are duplicated before restoration instructions and
aliasing are applied. If for example a loop increment was moved below
multiple side-exits, the restoration code would still mess up the
correct duplication of the instruction because the aliasing logic for
later side exits would overwrite this change.
As a work-around, this commit ensures that the aliasing logic for
side-exits is applied in-order. This may leave aliasing code that is
utterly useless, which should be cleaned up by DCE.
-rw-r--r-- | scheduling/MyRTLpathScheduleraux.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml index 63e362ad..df5e476f 100644 --- a/scheduling/MyRTLpathScheduleraux.ml +++ b/scheduling/MyRTLpathScheduleraux.ml @@ -1251,7 +1251,7 @@ let apply_aliases sb code name_map ~offset = let name_map = ref name_map in let length = Array.length sb.instructions in - (* TODO: prepferably there was an early exit condition when there is nothing left to do *) + (* TODO: preferably there was an early exit condition when there is nothing left to do *) for i = offset to length - 1 do let pc = sb.instructions.(i) in let inst = get_some @@ PTree.get pc !code in @@ -1261,10 +1261,13 @@ let apply_aliases sb code name_map ~offset = (match RTL.instr_defs inst with | None -> !name_map | Some r -> - if Option.is_some @@ PTree.get r !name_map then + if Option.is_some @@ PTree.get r !name_map then ( (* The restoration code, is no longer incorrectly applicable *) - PTree.remove r !name_map - else + if not !Clflags.option_fpoormansssa then + PTree.remove r !name_map + else + !name_map + ) else !name_map) ; done; @@ -1516,13 +1519,16 @@ let scheduler f = PTree.empty in let (to_insert_restoration, to_rename, next_free_reg) = restoration_instructions' sb code live_renames ~next_free_reg in - let code = PTree.fold - (fun code side_exit_pc aliases -> - let idx = apply_map' pc_to_idx side_exit_pc in - let code = apply_aliases sb code aliases ~offset:idx in - code) - to_rename - code + let side_exit_pcs = side_exit_pcs sb code in + let code = ListLabels.fold_left side_exit_pcs + ~init:code + ~f:(fun code side_exit_pc -> + match PTree.get side_exit_pc to_rename with + | None -> code + | Some aliases -> + let idx = apply_map' pc_to_idx side_exit_pc in + let code = apply_aliases sb code aliases ~offset:idx in + code) in let (sb, code, pm, next_free_pc, _fwmap) = insert_code sb code pm to_insert_restoration ~next_free_pc in (sb::sbs, code, pm, next_free_pc, next_free_reg) ) |