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
|
(* *********************************************************************)
(* *)
(* 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 "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
end:SYSTEM)
|
