blob: 64db2cb0f88f25b096f099ab3d38ba97bfda9687 (
plain)
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
open AST
open Asm
open Camlcoq
open Datatypes
open Printf
open Sections
(** Auxiliary functions for printing of asm *)
module type TARGET =
sig
val print_prologue: out_channel -> unit
val print_epilogue: out_channel -> unit
val print_align: out_channel -> int -> unit
val print_comm_symb: out_channel -> Z.t -> P.t -> int -> unit
val print_var_info: out_channel -> P.t -> unit
val print_fun_info: out_channel -> P.t -> unit
val print_init: out_channel -> init_data -> unit
val reset_constants: unit -> unit
val get_section_names: P.t -> section_name * section_name * section_name
val print_file_line: out_channel -> string -> int -> unit
val print_optional_fun_info: out_channel -> unit
val cfi_startproc: out_channel -> unit
val print_instructions: out_channel -> coq_function -> unit
val cfi_endproc: out_channel -> unit
val emit_constants: out_channel -> section_name -> unit
val print_jumptable: out_channel -> section_name -> unit
val section: out_channel -> section_name -> unit
val name_of_section: section_name -> string
val comment: string
val symbol: out_channel -> P.t -> unit
val default_falignment: int
end
(* On-the-fly label renaming *)
let next_label = ref 100
let new_label () =
let lbl = !next_label in incr next_label; lbl
let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
let transl_label lbl =
try
Hashtbl.find current_function_labels lbl
with Not_found ->
let lbl' = new_label() in
Hashtbl.add current_function_labels lbl lbl';
lbl'
let elf_label oc lbl =
fprintf oc ".L%d" lbl
(* List of literals and jumptables used in the code *)
let float64_literals : (int * int64) list ref = ref []
let float32_literals : (int * int32) list ref = ref []
let jumptables : (int * label list) list ref = ref []
let reset_constants () =
float64_literals := [];
float32_literals := [];
jumptables := []
(* Variables used for the handling of varargs *)
let current_function_stacksize = ref 0l
let current_function_sig =
ref { sig_args = []; sig_res = None; sig_cc = cc_default }
(* Functions for printing of symbol names *)
let elf_symbol oc symb =
fprintf oc "%s" (extern_atom symb)
let elf_symbol_offset oc (symb, ofs) =
elf_symbol oc symb;
let ofs = camlint_of_coqint ofs in
if ofs <> 0l then fprintf oc " + %ld" ofs
(* Functions for fun and var info *)
let elf_print_fun_info oc name =
fprintf oc " .type %a, @function\n" elf_symbol name;
fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name
let elf_print_var_info oc name =
fprintf oc " .type %a, @object\n" elf_symbol name;
fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name
(* 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 _ _ _ -> ())
(* For handling of annotations *)
let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
(* Basic printing functions *)
let coqint oc n =
fprintf oc "%ld" (camlint_of_coqint n)
|
