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
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Common functions for the AsmPrinter *)
open Printf
open Maps
open Camlcoq
open Sections
open Asm
(* Recognition of target ABI and asm syntax *)
module type SYSTEM =
sig
val comment: string
val constant: out_channel -> constant -> unit
val ireg: out_channel -> ireg -> unit
val freg: out_channel -> freg -> unit
val creg: out_channel -> int -> unit
val name_of_section: section_name -> string
val print_file_line: out_channel -> string -> string -> unit
val reset_file_line: unit -> unit
val cfi_startproc: out_channel -> unit
val cfi_endproc: out_channel -> unit
val cfi_adjust: out_channel -> int32 -> unit
val cfi_rel_offset: out_channel -> string -> int32 -> unit
val print_prologue: out_channel -> unit
val print_epilogue: out_channel -> unit
val print_addr_label: out_channel -> int -> unit
val set_compilation_unit_addrs: int -> int -> unit
end
let symbol oc symb =
fprintf oc "%s" (extern_atom symb)
let symbol_offset oc (symb, ofs) =
symbol oc symb;
if ofs <> 0l then fprintf oc " + %ld" ofs
let symbol_fragment oc s n op =
fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op
let int_reg_name = function
| GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3"
| GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7"
| GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11"
| GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15"
| GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19"
| GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23"
| GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27"
| GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31"
let float_reg_name = function
| FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3"
| FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7"
| FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11"
| FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15"
| FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19"
| FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23"
| FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27"
| FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31"
(* On-the-fly label renaming *)
let next_label = ref 100
let new_label() =
let lbl = !next_label in incr next_label; lbl
let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
let transl_label lbl =
try
Hashtbl.find current_function_labels lbl
with Not_found ->
let lbl' = new_label() in
Hashtbl.add current_function_labels lbl lbl';
lbl'
(* Basic printing functions *)
let coqint oc n =
fprintf oc "%ld" (camlint_of_coqint n)
let raw_symbol oc s =
fprintf oc "%s" s
let label oc lbl =
fprintf oc ".L%d" lbl
let label_low oc lbl =
fprintf oc ".L%d@l" lbl
let label_high oc lbl =
fprintf oc ".L%d@ha" lbl
let num_crbit = function
| CRbit_0 -> 0
| CRbit_1 -> 1
| CRbit_2 -> 2
| CRbit_3 -> 3
| CRbit_6 -> 6
let crbit oc bit =
fprintf oc "%d" (num_crbit bit)
(* Encoding masks for rlwinm instructions *)
let rolm_mask n =
let mb = ref 0 (* location of last 0->1 transition *)
and me = ref 32 (* location of last 1->0 transition *)
and last = ref ((Int32.logand n 1l) <> 0l) (* last bit seen *)
and count = ref 0 (* number of transitions *)
and mask = ref 0x8000_0000l in
for mx = 0 to 31 do
if Int32.logand n !mask <> 0l then
if !last then () else (incr count; mb := mx; last := true)
else
if !last then (incr count; me := mx; last := false) else ();
mask := Int32.shift_right_logical !mask 1
done;
if !me = 0 then me := 32;
assert (!count = 2 || (!count = 0 && !last));
(!mb, !me-1)
(* Handling of annotations *)
let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
(* Determine if the displacement of a conditional branch fits the short form *)
let short_cond_branch tbl pc lbl_dest =
match PTree.get lbl_dest tbl with
| None -> assert false
| Some pc_dest ->
let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000
(* Determine if an instruction falls through *)
let instr_fall_through = function
| Pb _ -> false
| Pbctr _ -> false
| Pbs _ -> false
| Pblr -> false
| _ -> true
(* Estimate the size of an Asm instruction encoding, in number of actual
PowerPC instructions. We can over-approximate. *)
let instr_size = function
| Pbf(bit, lbl) -> 2
| Pbt(bit, lbl) -> 2
| Pbtbl(r, tbl) -> 5
| Plfi(r1, c) -> 2
| Plfis(r1, c) -> 2
| Plabel lbl -> 0
| Pbuiltin(ef, args, res) -> 0
| Pannot(ef, args) -> 0
| Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
| _ -> 1
(* Build a table label -> estimated position in generated code.
Used to predict if relative conditional branches can use the short form. *)
let rec label_positions tbl pc = function
| [] -> tbl
| Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c
| i :: c -> label_positions tbl (pc + instr_size i) c
|
