blob: 75ecfa40e3a315550fa3da61b5ccbea30570c247 (
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
|
(* *********************************************************************)
(* *)
(* 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 -> P.t -> int -> unit
val print_var_info: bool
val print_fun_info: bool
val print_init: out_channel -> init_data -> unit
val reset_constants: unit -> unit
val get_section_names: unit -> 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 -> code -> 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
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 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 []
(* 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 symbol oc symb =
fprintf oc "%s" (extern_atom symb)
let symbol_offset oc (symb, ofs) =
symbol oc symb;
let ofs = camlint_of_coqint ofs in
if ofs <> 0l then fprintf oc " + %ld" ofs
(* The comment deliminiter *)
let comment = "#"
(* Functions for fun and var info *)
let print_fun_info oc name =
fprintf oc " .type %a, @function\n" symbol name;
fprintf oc " .size %a, . - %a\n" symbol name symbol name
let print_var_info oc name =
fprintf oc " .type %a, @object\n" symbol name;
fprintf oc " .size %a, . - %a\n" symbol name 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)
|
