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
|
open Maps
open BTL
open RTL
open Camlcoq
open RTLcommonaux
open DebugPrint
open BTLcommonaux
open BTLtypes
open BTLRenumber
let get_inumb iinfo = P.of_int iinfo.inumb
let get_ib_num ib = P.of_int (get_inumb_or_next ib)
let translate_function btl entry =
let rtl_code = ref PTree.empty in
let btl = reset_visited_ibf btl in
let rec build_rtl_tree e =
let ibf = get_some @@ PTree.get e btl 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 =
(* TODO gourdinl remove assertions *)
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, _), Bnop None, iinfo) ->
assert (iinfo.pcond = Some false);
next_nodes := s1 :: !next_nodes;
Some
( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond),
get_inumb iinfo )
| Bcond (_, _, _, _, _) ->
failwith "translate_function: unsupported Bcond"
| Bseq (ib1, ib2) ->
translate_btl_block ib1 (Some ib2);
translate_btl_block ib2 None;
None
| Bnop (Some iinfo) ->
Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
| Bnop None ->
failwith
"translate_function: Bnop None can only be in the right child \
of Bcond"
| 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, src, iinfo) ->
Some
( Istore (chk, addr, lr, src, 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 := tbl @ !next_nodes;
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 btl = f.fn_code in
let entry = f.fn_entrypoint in
let ordered_btl, new_entry = renumber btl entry in
let rtl = translate_function ordered_btl new_entry in
let dm = PTree.map (fun n i -> n) btl 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)
|
