blob: aa317a09e0c219f84157bd03ed7b0454e848e6bc (
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
|
(* *********************************************************************)
(* *)
(* 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 PrintAsmaux
open Printf
open Sections
open TargetPrinter
module Target = (val (sel_target ()):TARGET)
let print_location oc loc =
if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
let print_function oc name fn =
Hashtbl.clear current_function_labels;
Target.reset_constants ();
let (text, lit, jmptbl) = Target.get_section_names name in
Target.section oc text;
let alignment =
match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
Target.print_align oc alignment;
if not (C2C.atom_is_static name) then
fprintf oc " .globl %a\n" symbol name;
Target.print_optional_fun_info oc;
fprintf oc "%a:\n" symbol name;
print_location oc (C2C.atom_location name);
Target.cfi_startproc oc;
Target.print_instructions oc fn.fn_code;
Target.cfi_endproc oc;
if Target.print_fun_info then
print_fun_info oc name;
Target.emit_constants oc lit;
Target.print_jumptable oc jmptbl
let print_init_data oc name id =
if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
&& List.for_all (function Init_int8 _ -> true | _ -> false) id
then
fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id)
else
List.iter (Target.print_init oc) id
let print_var oc name v =
match v.gvar_init with
| [] -> ()
| _ ->
let sec =
match C2C.atom_sections name with
| [s] -> s
| _ -> Section_data true
and align =
match C2C.atom_alignof name with
| Some a -> a
| None -> 8 in (* 8-alignment is a safe default *)
let name_sec = Target.name_of_section sec in
if name_sec <> "COMM" then begin
fprintf oc " %s\n" name_sec;
Target.print_align oc align;
if not (C2C.atom_is_static name) then
fprintf oc " .global %a\n" symbol name;
fprintf oc "%a:\n" symbol name;
print_init_data oc name v.gvar_init;
if Target.print_var_info then
print_var_info oc name;
end else
let sz =
match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
Target.print_comm_symb oc sz name align
let print_globdef oc (name,gdef) =
match gdef with
| Gfun (Internal code) -> print_function oc name code
| Gfun (External ef) -> ()
| Gvar v -> print_var oc name v
let print_program oc p =
PrintAnnot.reset_filenames ();
PrintAnnot.print_version_and_options oc Target.comment;
Target.print_prologue oc;
List.iter (print_globdef oc) p.prog_defs;
Target.print_epilogue oc;
PrintAnnot.close_filenames ()
|
