aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLtoBTLaux.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-24 17:39:44 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-24 17:39:44 +0200
commita6006df63f0d03cc223d13834e81a71651513fbe (patch)
tree7ce509e87f659159dc9e9669290e3f2f5000f5e0 /scheduling/RTLtoBTLaux.ml
parent0efe7783c50d72858352fda93d30e0f52792d658 (diff)
downloadcompcert-kvx-a6006df63f0d03cc223d13834e81a71651513fbe.tar.gz
compcert-kvx-a6006df63f0d03cc223d13834e81a71651513fbe.zip
a draft frontend for prepass
Diffstat (limited to 'scheduling/RTLtoBTLaux.ml')
-rw-r--r--scheduling/RTLtoBTLaux.ml19
1 files changed, 7 insertions, 12 deletions
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 07e7a9d9..e932d766 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -1,11 +1,11 @@
open Maps
open RTL
open BTL
-open Registers
open PrintBTL
open RTLcommonaux
open DebugPrint
open BTLaux
+open BTLScheduleraux
let undef_node = -1
@@ -13,7 +13,7 @@ let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond }
let def_iinfo = { inumb = undef_node; pcond = None }
-let mk_binfo _bnumb _output_regs = { bnumb = _bnumb; visited = false; output_regs = _output_regs }
+let mk_binfo _bnumb = { bnumb = _bnumb; visited = false }
let encaps_final inst osucc =
match inst with
@@ -33,9 +33,9 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final =
| Iload (trap, chk, addr, lr, rd, s) ->
osucc := Some s;
Bload (trap, chk, addr, lr, rd, iinfo)
- | Istore (chk, addr, lr, rd, s) ->
+ | Istore (chk, addr, lr, src, s) ->
osucc := Some s;
- Bstore (chk, addr, lr, rd, iinfo)
+ Bstore (chk, addr, lr, src, iinfo)
| Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo)
| Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo)
| Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo)
@@ -60,7 +60,6 @@ let translate_function code entry join_points liveness =
else (
reached := PTree.set e true !reached;
let next_nodes = ref [] in
- let last = ref None in
let rec build_btl_block n =
let inst = get_some @@ PTree.get n code in
let psucc = predicted_successor inst in
@@ -91,7 +90,6 @@ let translate_function code entry join_points liveness =
| _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
| None ->
debug "BLOCK END.\n";
- last := Some inst;
next_nodes := !next_nodes @ successors_inst inst;
translate_inst iinfo inst true
in
@@ -99,12 +97,7 @@ let translate_function code entry join_points liveness =
let succs = !next_nodes in
let inputs = get_some @@ PTree.get e liveness in
- let blk_last_successors = successors_inst (get_some @@ !last) in
- let list_input_regs = List.map (
- fun n -> get_some @@ PTree.get n liveness
- ) blk_last_successors in
- let outputs = List.fold_left Regset.union Regset.empty list_input_regs in
- let bi = mk_binfo (p2i e) outputs in
+ let bi = mk_binfo (p2i e) in
let ibf = { entry = ib; input_regs = inputs; binfo = bi } in
btl_code := PTree.set e ibf !btl_code;
List.iter build_btl_tree succs)
@@ -119,6 +112,8 @@ let rtl2btl (f : RTL.coq_function) =
let liveness = analyze f in
let btl = translate_function code entry join_points liveness in
let dm = PTree.map (fun n i -> n) btl in
+ (* TODO gourdinl move elsewhere *)
+ btl_scheduler btl entry;
debug "Entry %d\n" (p2i entry);
debug "RTL Code: ";
print_code code;