diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-03-10 14:30:00 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-03-10 14:30:00 +0100 |
commit | 337dddf6ea7c69c06c883ce4287ddf3d92b63c05 (patch) | |
tree | 92ceb94ef94aff3fe22ce11bb21452341f2dd717 /backend | |
parent | 3e01154d693e1c457e1e974f5e9ebaa4601050aa (diff) | |
parent | 5a027c08f3fed3e52061978e1757ffb255422333 (diff) | |
download | compcert-337dddf6ea7c69c06c883ce4287ddf3d92b63c05.tar.gz compcert-337dddf6ea7c69c06c883ce4287ddf3d92b63c05.zip |
Merge pull request #21 from AbsInt/backend_printer
Re-factoring of the asm printers.
Diffstat (limited to 'backend')
-rw-r--r-- | backend/PrintAsm.ml | 101 | ||||
-rw-r--r-- | backend/PrintAsm.mli | 16 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 134 |
3 files changed, 251 insertions, 0 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml new file mode 100644 index 00000000..a6883339 --- /dev/null +++ b/backend/PrintAsm.ml @@ -0,0 +1,101 @@ +(* *********************************************************************) +(* *) +(* 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 Printer(Target:TARGET) = + struct + + 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 -> Target.default_falignment in + Target.print_align oc alignment; + if not (C2C.atom_is_static name) then + fprintf oc " .globl %a\n" Target.symbol name; + Target.print_optional_fun_info oc; + fprintf oc "%a:\n" Target.symbol name; + print_location oc (C2C.atom_location name); + Target.cfi_startproc oc; + Target.print_instructions oc fn; + Target.cfi_endproc oc; + Target.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" Target.symbol name; + fprintf oc "%a:\n" Target.symbol name; + print_init_data oc name v.gvar_init; + Target.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 + + end + +let print_program oc p = + let module Target = (val (sel_target ()):TARGET) in + let module Printer = Printer(Target) in + PrintAnnot.reset_filenames (); + PrintAnnot.print_version_and_options oc Target.comment; + Target.print_prologue oc; + List.iter (Printer.print_globdef oc) p.prog_defs; + Target.print_epilogue oc; + PrintAnnot.close_filenames () diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli new file mode 100644 index 00000000..eb63f1be --- /dev/null +++ b/backend/PrintAsm.mli @@ -0,0 +1,16 @@ +(* *********************************************************************) +(* *) +(* 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 PrintAsmaux + +val print_program: out_channel -> Asm.program -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml new file mode 100644 index 00000000..64db2cb0 --- /dev/null +++ b/backend/PrintAsmaux.ml @@ -0,0 +1,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) |