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
|
open Maps
open BTL
open RTL
open Camlcoq
open RTLcommonaux
open DebugPrint
open PrintBTL
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 rec translate_btl_block ib k =
debug "Entering translate_btl_block...\n";
print_btl_inst stderr ib;
let rtli =
match ib with
| Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) ->
Some
( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.opt_info),
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) ->
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) ->
Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
| BF (Bjumptable (arg, tbl), iinfo) ->
Some (Ijumptable (arg, tbl), get_inumb iinfo)
| BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
| BF (Bgoto s, iinfo) -> None
in
match rtli with
| Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code
| None -> ()
in
List.iter
(fun (n, ibf) ->
ibf.binfo.visited <- true;
let ib = ibf.entry in
translate_btl_block ib None)
(PTree.elements btl);
!rtl_code
let btl2rtl (f : BTL.coq_function) =
(*debug_flag := true;*)
let btl = f.fn_code in
let entry = f.fn_entrypoint in
let obne, dm = renumber btl entry in
let ordered_btl, new_entry = obne in
let rtl = translate_function ordered_btl new_entry in
debug "Entry %d\n" (p2i new_entry);
debug "BTL Code:\n";
print_btl_code stderr ordered_btl;
debug "RTL Code: ";
print_code rtl;
debug "Dupmap:\n";
print_ptree print_pint dm;
debug "\n";
(*debug_flag := false;*)
((rtl, new_entry), dm)
|
