1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
open Maps
open RTL
open BTL
open Registers
open DebugPrint
open PrintBTL
open Camlcoq
open AuxTools
let mk_ni n = n
let encaps_final inst osucc =
match inst with
| BF _ | Bcond _ -> inst
| _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
let translate_inst ni inst is_final =
let osucc = ref None in
let btli =
match inst with
| Inop s ->
osucc := Some s;
Bnop ni
| Iop (op, lr, rd, s) ->
osucc := Some s;
Bop (op, lr, rd, ni)
| Iload (trap, chk, addr, lr, rd, s) ->
osucc := Some s;
Bload (trap, chk, addr, lr, rd, ni)
| Istore (chk, addr, lr, rd, s) ->
osucc := Some s;
Bstore (chk, addr, lr, rd, ni)
| Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s, ni))
| Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr, ni))
| Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s, ni))
| Icond (cond, lr, ifso, ifnot, info) ->
Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info, ni)
| Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl, ni))
| Ireturn oreg -> BF (Breturn (oreg, ni))
in
if is_final then encaps_final btli !osucc else btli
let translate_function code entry join_points =
let reached = ref (PTree.map (fun n i -> false) code) in
let btl_code = ref PTree.empty in
(* TODO gourdinl SEPARATE IN A BETTER WAY!! *)
let rec build_btl_tree e =
if get_some @@ PTree.get e !reached then ()
else (
reached := PTree.set e true !reached;
let next_nodes = ref [] in
let rec build_btl_block n =
let inst = get_some @@ PTree.get n code in
let psucc = predicted_successor inst in
let ni = mk_ni n in
let succ =
match psucc with
| Some ps ->
if get_some @@ PTree.get ps join_points then (
debug "IS JOIN PT\n";
None)
else Some ps
| None -> None
in
match succ with
| Some s -> (
debug "BLOCK CONTINUE\n";
match inst with
| Icond (cond, lr, ifso, ifnot, info) ->
(* TODO gourdinl remove this *)
assert (s = ifnot);
next_nodes := !next_nodes @ non_predicted_successors inst psucc;
Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info, ni)
| _ -> Bseq (translate_inst ni inst false, build_btl_block s))
| None ->
debug "BLOCK END.\n";
next_nodes := !next_nodes @ successors_inst inst;
translate_inst ni inst true
in
let ib = build_btl_block e in
let succs = !next_nodes in
let ibf = { entry = ib; input_regs = Regset.empty } in
btl_code := PTree.set e ibf !btl_code;
List.iter build_btl_tree succs)
in
build_btl_tree entry;
!btl_code
let print_dm dm =
List.iter
(fun (n, n') ->
debug "%d -> %d" (P.to_int n) (P.to_int n');
(*print_btl_inst stderr ib.entry;*)
debug "\n")
(PTree.elements dm)
let rtl2btl (f : RTL.coq_function) =
debug_flag := true;
let code = f.fn_code in
let entry = f.fn_entrypoint in
let join_points = get_join_points code entry in
let btl = translate_function code entry join_points in
let dm = PTree.map (fun n i -> n) btl in
debug "Entry %d\n" (P.to_int entry);
debug "RTL Code: ";
print_code code;
debug_flag := false;
debug "BTL Code: ";
print_btl_code stderr btl true;
debug "Dupmap:\n";
print_ptree print_pint dm;
debug "Join points: ";
print_true_nodes join_points;
debug "\n";
((btl, entry), dm)
|
