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
|
(* *********************************************************************)
(* *)
(* 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 Linux specific printing functions *)
open Printf
open Datatypes
open Camlcoq
open Sections
open Asm
open PrintUtil
module Linux_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 "@sda21"
(* 32-bit relative addressing is supported by the Diab tools but not by
GNU binutils. In the latter case, for testing purposes, we treat
them as absolute addressings. The default base register being GPR0,
this produces correct code, albeit with absolute addresses. *)
| Csymbol_rel_low(s, n) ->
symbol_fragment oc s n "@l"
| Csymbol_rel_high(s, n) ->
symbol_fragment oc s n "@ha"
let ireg oc r =
output_string oc (int_reg_name r)
let freg oc r =
output_string oc (float_reg_name r)
let creg oc r =
fprintf oc "%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 ".section .sdata,\"aw\",@progbits" else "COMM"
| Section_const i ->
if i then ".rodata" else "COMM"
| Section_small_const i ->
if i then ".section .sdata2,\"a\",@progbits" else "COMM"
| Section_string -> ".rodata"
| Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\",\"a%s%s\",@progbits"
s (if wr then "w" else "") (if ex then "x" else "")
let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
let reset_file_line () = Hashtbl.clear filename_num
let print_file_line oc file line =
if !Clflags.option_g && file <> "" then begin
let filenum =
try
Hashtbl.find filename_num file
with Not_found ->
let n = Hashtbl.length filename_num + 1 in
Hashtbl.add filename_num file n;
fprintf oc " .file %d %S\n" n file;
n
in fprintf oc " .loc %d %s\n" filenum line
end
(* Emit .cfi directives *)
let cfi_startproc =
if Configuration.asm_supports_cfi then
(fun oc -> fprintf oc " .cfi_startproc\n")
else
(fun _ -> ())
let cfi_endproc =
if Configuration.asm_supports_cfi then
(fun oc -> fprintf oc " .cfi_endproc\n")
else
(fun _ -> ())
let cfi_adjust =
if Configuration.asm_supports_cfi then
(fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta)
else
(fun _ _ -> ())
let cfi_rel_offset =
if Configuration.asm_supports_cfi then
(fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs)
else
(fun _ _ _ -> ())
let print_prologue oc = ()
let print_epilogue oc = ()
let set_compilation_unit_addrs _ _ = ()
let print_addr_label _ _ = ()
end:SYSTEM)
|
