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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
open Maps
open RTL
open BTL
open Registers
open DebugPrint
open PrintRTL
open PrintBTL
(* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
This should be accessible everywhere. *)
let get_some = function
| None -> failwith "Got None instead of Some _"
| Some thing -> thing
let successors_inst = function
| Inop n
| Iop (_, _, _, n)
| Iload (_, _, _, _, _, n)
| Istore (_, _, _, _, n)
| Icall (_, _, _, _, n)
| Ibuiltin (_, _, _, n) ->
[ n ]
| Icond (_, _, n1, n2, _) -> [ n1; n2 ]
| Ijumptable (_, l) -> l
| Itailcall _ | Ireturn _ -> []
let predicted_successor = function
| Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
->
Some n
| Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
| Icond (_, _, n1, n2, p) -> (
match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
| Ijumptable _ | Itailcall _ | Ireturn _ -> None
(* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
let non_predicted_successors i = function
| None -> successors_inst i
| Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
(* adapted from Linearizeaux.get_join_points *)
let get_join_points code entry =
let reached = ref (PTree.map (fun n i -> false) code) in
let reached_twice = ref (PTree.map (fun n i -> false) code) in
let rec traverse pc =
if get_some @@ PTree.get pc !reached then (
if not (get_some @@ PTree.get pc !reached_twice) then
reached_twice := PTree.set pc true !reached_twice)
else (
reached := PTree.set pc true !reached;
traverse_succs (successors_inst @@ get_some @@ PTree.get pc code))
and traverse_succs = function
| [] -> ()
| [ pc ] -> traverse pc
| pc :: l ->
traverse pc;
traverse_succs l
in
traverse entry;
!reached_twice
let encaps_final inst osucc =
match inst with
| BF _ | Bcond _ -> inst
| _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
let translate_inst inst is_final =
let osucc = ref None in
let btli =
match inst with
| Inop s ->
osucc := Some s;
Bnop
| Iop (op, lr, rd, s) ->
osucc := Some s;
Bop (op, lr, rd)
| Iload (trap, chk, addr, lr, rd, s) ->
osucc := Some s;
Bload (trap, chk, addr, lr, rd)
| Istore (chk, addr, lr, rd, s) ->
osucc := Some s;
Bstore (chk, addr, lr, rd)
| Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s))
| Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr))
| Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s))
| Icond (cond, lr, ifso, ifnot, info) ->
(* TODO gourdinl remove this *)
assert (info = None);
Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info)
| Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
| Ireturn oreg -> BF (Breturn oreg)
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
(* 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
debug "Inst is : ";
print_instruction stderr (0, inst);
debug "\n";
let psucc = predicted_successor inst 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)
| _ -> Bseq (translate_inst inst false, build_btl_block s))
| None ->
debug "BLOCK END.\n";
next_nodes := !next_nodes @ successors_inst inst;
translate_inst 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,ib) ->*)
(*debug "%d:" (P.to_int n);*)
(*print_iblock stderr false ib.entry)*)
(*(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 "RTL Code: ";
print_code code;
debug "BTL Code: ";
print_btl_code stderr btl true;
debug "Join points: ";
print_true_nodes join_points;
debug "\n";
(*print_dm dm;*)
debug_flag := false;
((btl, entry), dm)
|
