diff options
Diffstat (limited to 'scheduling/RTLtoBTLaux.ml')
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index d544e87f..3c06f4cb 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -45,7 +45,7 @@ let translate_inst (iinfo : BTL.inst_info) inst is_final = in if is_final then encaps_final btli !osucc else btli -let translate_function code entry join_points liveness = +let translate_function code entry join_points liveness (typing : RTLtyping.regenv) = let reached = ref (PTree.map (fun n i -> false) code) in let btl_code = ref PTree.empty in let rec build_btl_tree e = @@ -53,6 +53,7 @@ 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 @@ -78,13 +79,16 @@ let translate_function code entry join_points liveness = | None -> debug "BLOCK END.\n"; next_nodes := !next_nodes @ successors_inst inst; + last := Some inst; translate_inst iinfo inst true in let ib = build_btl_block e in let succs = !next_nodes in let inputs = get_some @@ PTree.get e liveness in - let bi = mk_binfo (p2i e) in + let soutput = get_outputs liveness e (get_some @@ !last) in + + let bi = mk_binfo (p2i e) soutput typing 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) @@ -97,7 +101,8 @@ let rtl2btl (f : RTL.coq_function) = let entry = f.fn_entrypoint in let join_points = get_join_points code entry in let liveness = analyze f in - let btl = translate_function code entry join_points liveness in + let typing = get_ok @@ RTLtyping.type_function f in + let btl = translate_function code entry join_points liveness typing in let dm = PTree.map (fun n i -> n) btl in (*debug_flag := true;*) debug "Entry %d\n" (p2i entry); |