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
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* The Diab specific printing functions *)
open Printf
open Datatypes
open DwarfTypes
open DwarfUtil
open DwarfAbbrvPrinter
open Camlcoq
open Sections
open Asm
open PrintUtil
module Diab_System =
(struct
let comment = ";"
let constant oc cst =
match cst with
| Cint n ->
fprintf oc "%ld" (camlint_of_coqint n)
| Csymbol_low(s, n) ->
symbol_fragment oc s n "@l"
| Csymbol_high(s, n) ->
symbol_fragment oc s n "@ha"
| Csymbol_sda(s, n) ->
symbol_fragment oc s n "@sdarx"
| Csymbol_rel_low(s, n) ->
symbol_fragment oc s n "@sdax@l"
| Csymbol_rel_high(s, n) ->
symbol_fragment oc s n "@sdarx@ha"
let ireg oc r =
output_char oc 'r';
output_string oc (int_reg_name r)
let freg oc r =
output_char oc 'f';
output_string oc (float_reg_name r)
let creg oc r =
fprintf oc "cr%d" r
let name_of_section = function
| Section_text -> ".text"
| Section_data i -> if i then ".data" else "COMM"
| Section_small_data i -> if i then ".sdata" else ".sbss"
| Section_const _ -> ".text"
| Section_small_const _ -> ".sdata2"
| Section_string -> ".text"
| Section_literal -> ".text"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\",,%c"
s
(match wr, ex with
| true, true -> 'm' (* text+data *)
| true, false -> 'd' (* data *)
| false, true -> 'c' (* text *)
| false, false -> 'r') (* const *)
let filenum : (string, int) Hashtbl.t = Hashtbl.create 7
let print_file_line oc file line =
PrintAnnot.print_file_line_d2 oc comment file line;
if !Clflags.option_g && file <> "" && not (Hashtbl.mem filenum file) then
Hashtbl.add filenum file (new_label ())
(* Emit .cfi directives *)
let cfi_startproc oc = ()
let cfi_endproc oc = ()
let cfi_adjust oc delta = ()
let cfi_rel_offset oc reg ofs = ()
let debug_line_start = ref (-1)
let compilation_unit_start_addr = ref (-1)
let compilation_unit_end_addr = ref (-1)
(* Mapping from debug addresses to labels *)
let addr_label_map: (int,int) Hashtbl.t = Hashtbl.create 7
let set_compilation_unit_addrs cu_start cu_end =
compilation_unit_start_addr := cu_start;
compilation_unit_end_addr := cu_end
let debug_info_start = ref (-1)
let print_addr_label oc addr =
let lbl = try
Hashtbl.find addr_label_map addr
with Not_found ->
let lbl = new_label () in
Hashtbl.add addr_label_map addr lbl;
lbl in
fprintf oc "%a:\n" label lbl
let register_addr_label = Hashtbl.add addr_label_map
let print_prologue oc =
fprintf oc " .xopt align-fill-text=0x60000000\n";
if !Clflags.option_g then
begin
fprintf oc " .text\n";
fprintf oc " .section .debug_line,,n\n";
let label_debug_line = new_label () in
debug_line_start := label_debug_line;
fprintf oc "%a:\n" label label_debug_line;
fprintf oc " .text\n";
print_addr_label oc !compilation_unit_start_addr;
let label_debug_info = new_label () in
debug_info_start := label_debug_info;
fprintf oc " .0byte %a\n" label label_debug_info;
fprintf oc " .d2_line_start .debug_line\n";
fprintf oc " .text\n";
fprintf oc " .align 2\n"
end
let print_epilogue oc =
if !Clflags.option_g then
begin
(* Everthink available for printing of the compilation unit *)
fprintf oc " .text\n";
(* End Address of the compilation unit *)
print_addr_label oc !compilation_unit_end_addr;
(* Print the filenum which is used for the location expressions *)
Hashtbl.iter (fun name lbl ->
fprintf oc "%a: .d2filenum \"%s\"\n" label lbl name) filenum;
(* The end of the debug line info *)
fprintf oc " .d2_line_end\n";
end
module AbbrvPrinter = DwarfAbbrvPrinter(struct
let string_of_byte value =
Printf.sprintf " .byte %s\n" (if value then "0x1" else "0x2")
let string_of_abbrv_entry v =
Printf.sprintf " .uleb128 %d\n" v
let abbrv_start_addr = ref (-1)
let get_abbrv_start_addr () = !abbrv_start_addr
let sibling_type_abbr = dw_form_ref4
let decl_file_type_abbr = dw_form_data4
let decl_line_type_abbr = dw_form_udata
let type_abbr = dw_form_ref_addr
let name_type_abbr = dw_form_string
let encoding_type_abbr = dw_form_data1
let byte_size_type_abbr = dw_form_data1
let high_pc_type_abbr = dw_form_addr
let low_pc_type_abbr = dw_form_addr
let stmt_list_type_abbr = dw_form_data4
let declaration_type_abbr = dw_form_flag
let external_type_abbr = dw_form_flag
let prototyped_type_abbr = dw_form_flag
let bit_offset_type_abbr = dw_form_data1
let comp_dir_type_abbr = dw_form_string
let language_type_abbr = dw_form_udata
let producer_type_abbr = dw_form_string
let value_type_abbr = dw_form_sdata
let artificial_type_abbr = dw_form_flag
let variable_parameter_type_abbr = dw_form_flag
let bit_size_type_abbr = dw_form_data1
let location_const_type_abbr = dw_form_data4
let location_block_type_abbr = dw_form_block
let data_location_block_type_abbr = dw_form_block
let data_location_ref_type_abbr = dw_form_ref4
let bound_const_type_abbr = dw_form_udata
let bound_ref_type_abbr=dw_form_ref4
let abbrv_section_start oc =
fprintf oc " .section .debug_abbrev,,n\n";
let lbl = new_label () in
abbrv_start_addr := lbl;
fprintf oc "%a:\n" label lbl
let abbrv_section_end oc =
fprintf oc " .section .debug_abbrev,,n\n";
fprintf oc " .sleb128 0\n"
let abbrv_prologue oc id =
fprintf oc " .section .debug_abbrev,,n\n";
fprintf oc " .uleb128 %d\n" id
let abbrv_epilogue oc =
fprintf oc " .uleb128 0\n";
fprintf oc " .uleb128 0\n"
end)
let rec print_entry oc entry has_sibling =
()
let print_debug_info oc entry =
AbbrvPrinter.print_debug_abbrv oc entry;
let abbrv_start = AbbrvPrinter.get_abbrv_start_addr () in
let debug_start = new_label () in
let print_info () =
fprintf oc" .section .debug_info,,n\n" in
print_info ();
fprintf oc "%a\n" label debug_start;
let debug_length_start = new_label () in (* Address used for length calculation *)
let debug_end = new_label () in
fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start;
fprintf oc "%a\n" label debug_length_start;
fprintf oc " .2byte 0x2\n"; (* Dwarf version *)
fprintf oc " .4byte %a\n" label abbrv_start; (* Offset into the abbreviation *)
fprintf oc " .byte %X\n" !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *)
print_entry oc entry false;
fprintf oc "%a\n" label debug_end; (* End of the debug section *)
fprintf oc " .sleb128 0\n"
end:SYSTEM)
|
