diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 11:44:11 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 11:44:11 +0200 |
| commit | 05b24fdb11414100b9b04867e6e2d3a1a9054162 (patch) | |
| tree | 6ae4a50a2f311c6b2786e64de12d4d5f7755f865 /scheduling/RTLtoBTLaux.ml | |
| parent | 56901933d110adef341312e1c7630b672827b41d (diff) | |
| download | compcert-kvx-05b24fdb11414100b9b04867e6e2d3a1a9054162.tar.gz compcert-kvx-05b24fdb11414100b9b04867e6e2d3a1a9054162.zip | |
Improvements in scheduling and renumbering BTL code
Diffstat (limited to 'scheduling/RTLtoBTLaux.ml')
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 056fe213..d04326ea 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -10,7 +10,7 @@ open BTLScheduleraux let encaps_final inst osucc = match inst with - | BF _ | Bcond _ -> inst + | BF _ -> inst | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ())) let translate_inst (iinfo : BTL.inst_info) inst is_final = @@ -33,12 +33,13 @@ let translate_inst (iinfo : BTL.inst_info) inst is_final = | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo) | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo) | Icond (cond, lr, ifso, ifnot, info) -> + osucc := Some ifnot; iinfo.pcond <- info; Bcond ( cond, lr, BF (Bgoto ifso, def_iinfo ()), - BF (Bgoto ifnot, def_iinfo ()), + Bnop None, iinfo ) | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo) | Ireturn oreg -> BF (Breturn oreg, iinfo) |