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
|
(* *********************************************************************)
(* *)
(* 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 DwarfPrinter
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 ".bss"
| 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 last_file = ref ""
let reset_file_line () = last_file := ""
let print_file_line oc file line =
if !Clflags.option_g && file <> "" then begin
if file <> !last_file then begin
fprintf oc " .d1file %S\n" file;
last_file := file
end;
fprintf oc " .d1line %s\n" line
end
(* Emit .cfi directives *)
let cfi_startproc oc = ()
let cfi_endproc oc = ()
let cfi_adjust oc delta = ()
let cfi_rel_offset oc reg ofs = ()
let print_prologue oc =
fprintf oc " .xopt align-fill-text=0x60000000\n";
if !Clflags.option_g then
fprintf oc " .xopt asm-debug-on\n"
module DwarfDefs =
(struct
let string_of_byte value =
if value then
" .byte 0x1\n"
else
" .byte 0x0\n"
let string_of_abbrv_entry v =
Printf.sprintf " .uleb128 %d\n" v
let abbrv_start_addr = ref (-1)
let debug_end_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"
let info_section_start oc =
fprintf oc " .section .debug_info,,n\n";
let debug_start = new_label ()
and debug_end = new_label () in
debug_end_addr:= debug_end;
fprintf oc " .4byte %a-%a\n" label debug_end label debug_start;
fprintf oc "%a:\n" label debug_start;
fprintf oc " .2byte 0x2\n";
fprintf oc " .4byte %a\n" label !abbrv_start_addr;
fprintf oc " .1byte %d\n" !Machine.config.Machine.sizeof_ptr
let info_section_end oc =
fprintf oc "%a\n" label !debug_end_addr
let print_entry oc entry abbrv =
()
end:DWARF_DEFS)
end:SYSTEM)
|
