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
|
(* *********************************************************************)
(* *)
(* 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 print_file_line oc file line =
PrintAnnot.print_file_line oc comment file line
(* 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)
|
