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
|
open Maps
open BTL
open RTL
open Camlcoq
open AuxTools
open DebugPrint
open PrintBTL
let is_atom = function
| Bseq (_, _) | Bcond (_, _, _, _, _, _) -> false
| _ -> true
let rec get_nn = function
| Bnop ni
| Bop (_, _, _, ni)
| Bload (_, _, _, _, _, ni)
| Bstore (_, _, _, _, ni)
| Bcond (_, _, _, _, _, ni)
| BF (Breturn (_, ni))
| BF (Bcall (_, _, _, _, _, ni))
| BF (Btailcall (_, _, _, ni))
| BF (Bbuiltin (_, _, _, _, ni))
| BF (Bjumptable (_, _, ni)) ->
ni
| BF (Bgoto s) -> s
| Bseq (ib1, _) -> get_nn ib1
let translate_function code entry =
let reached = ref (PTree.map (fun n i -> false) code) in
let rtl_code = ref PTree.empty in
let rec build_rtl_tree e =
if get_some @@ PTree.get e !reached then ()
else (
reached := PTree.set e true !reached;
let next_nodes = ref [] in
let ib = (get_some @@ PTree.get e code).entry in
let rec translate_btl_block ib k =
print_btl_inst stderr ib;
let rtli =
match ib with
| Bcond (cond, lr, BF (Bgoto s1), BF (Bgoto s2), info, ni) ->
next_nodes := s1 :: s2 :: !next_nodes;
Some (Icond (cond, lr, s1, s2, info), ni)
| Bcond (cond, lr, BF (Bgoto s1), ib2, info, ni) ->
assert (info = Some false);
next_nodes := s1 :: !next_nodes;
translate_btl_block ib2 None;
Some (Icond (cond, lr, s1, get_nn ib2, info), ni)
(* TODO gourdinl remove dynamic check *)
| Bcond (_, _, _, _, _, _) ->
failwith "translate_function: invalid Bcond"
| Bseq (ib1, ib2) ->
(* TODO gourdinl remove dynamic check *)
assert (is_atom ib1);
translate_btl_block ib1 (Some ib2);
translate_btl_block ib2 None;
None
| Bnop ni -> Some (Inop (get_nn (get_some k)), ni)
| Bop (op, lr, rd, ni) ->
Some (Iop (op, lr, rd, get_nn (get_some k)), ni)
| Bload (trap, chk, addr, lr, rd, ni) ->
Some (Iload (trap, chk, addr, lr, rd, get_nn (get_some k)), ni)
| Bstore (chk, addr, lr, rd, ni) ->
Some (Istore (chk, addr, lr, rd, get_nn (get_some k)), ni)
| BF (Bcall (sign, fn, lr, rd, s, ni)) ->
next_nodes := s :: !next_nodes;
Some (Icall (sign, fn, lr, rd, s), ni)
| BF (Btailcall (sign, fn, lr, ni)) ->
Some (Itailcall (sign, fn, lr), ni)
| BF (Bbuiltin (ef, lr, rd, s, ni)) ->
next_nodes := s :: !next_nodes;
Some (Ibuiltin (ef, lr, rd, s), ni)
| BF (Bjumptable (arg, tbl, ni)) -> Some (Ijumptable (arg, tbl), ni)
| BF (Breturn (oreg, ni)) -> Some (Ireturn oreg, ni)
| BF (Bgoto s) ->
next_nodes := s :: !next_nodes;
None
in
match rtli with
| Some (inst, ni) -> rtl_code := PTree.set ni inst !rtl_code
| None -> ()
in
translate_btl_block ib None;
let succs = !next_nodes in
List.iter build_rtl_tree succs)
in
build_rtl_tree entry;
!rtl_code
let btl2rtl (f : BTL.coq_function) =
debug_flag := true;
let code = f.fn_code in
let entry = f.fn_entrypoint in
let rtl = translate_function code entry in
let dm = PTree.map (fun n i -> n) code in
debug "Entry %d\n" (P.to_int entry);
debug "RTL Code: ";
print_code rtl;
debug "Dupmap:\n";
print_ptree print_pint dm;
debug "\n";
debug_flag := false;
((rtl, entry), dm)
|
