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 BTL
open RTL
open Camlcoq
open AuxTools
open DebugPrint
open BTLaux
let is_atom = function
| Bseq (_, _) | Bcond (_, _, _, _, _) -> false
| _ -> true
let get_inumb iinfo = P.of_int iinfo.inumb
let rec get_ib_num = function
| BF (Bgoto s, _) -> s
| Bnop iinfo
| Bop (_, _, _, iinfo)
| Bload (_, _, _, _, _, iinfo)
| Bstore (_, _, _, _, iinfo)
| Bcond (_, _, _, _, iinfo)
| BF (_, iinfo) ->
get_inumb iinfo
| Bseq (ib1, _) -> get_ib_num ib1
let translate_function code entry =
let rtl_code = ref PTree.empty in
let code =
PTree.map
(fun n ibf ->
ibf.binfo.visited <- false;
ibf)
code
in
let rec build_rtl_tree e =
let ibf = get_some @@ PTree.get e code in
if ibf.binfo.visited then ()
else (
ibf.binfo.visited <- true;
let ib = ibf.entry in
let next_nodes = ref [] in
let rec translate_btl_block ib k =
let rtli =
match ib with
| Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) ->
next_nodes := s1 :: s2 :: !next_nodes;
Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo)
| Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) ->
assert (iinfo.pcond = Some false);
next_nodes := s1 :: !next_nodes;
translate_btl_block ib2 None;
Some
( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond),
get_inumb iinfo )
(* 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 iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
| Bop (op, lr, rd, iinfo) ->
Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo)
| Bload (trap, chk, addr, lr, rd, iinfo) ->
Some
( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)),
get_inumb iinfo )
| Bstore (chk, addr, lr, rd, iinfo) ->
Some
( Istore (chk, addr, lr, rd, get_ib_num (get_some k)),
get_inumb iinfo )
| BF (Bcall (sign, fn, lr, rd, s), iinfo) ->
next_nodes := s :: !next_nodes;
Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo)
| BF (Btailcall (sign, fn, lr), iinfo) ->
Some (Itailcall (sign, fn, lr), get_inumb iinfo)
| BF (Bbuiltin (ef, lr, rd, s), iinfo) ->
next_nodes := s :: !next_nodes;
Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
| BF (Bjumptable (arg, tbl), iinfo) ->
next_nodes := !next_nodes @ tbl;
Some (Ijumptable (arg, tbl), get_inumb iinfo)
| BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
| BF (Bgoto s, iinfo) ->
next_nodes := s :: !next_nodes;
None
in
match rtli with
| Some (inst, inumb) -> rtl_code := PTree.set inumb 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" (p2i entry);
debug "RTL Code: ";
(*print_code rtl;*)
debug "Dupmap:\n";
print_ptree print_pint dm;
debug "\n";
(*debug_flag := false;*)
((rtl, entry), dm)
|
