diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-03 18:43:36 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-03 18:43:36 +0100 |
commit | 7cbc68a8056ace840ef187156461a361554d5fef (patch) | |
tree | f9a0e6f4ce4d5b1b6e375df855daefcd389f2ed8 | |
parent | 30dd68d627f68cca0c2addd006d853379ad720cf (diff) | |
download | compcert-7cbc68a8056ace840ef187156461a361554d5fef.tar.gz compcert-7cbc68a8056ace840ef187156461a361554d5fef.zip |
Started moving common backend functions into one file.
-rw-r--r-- | arm/PrintAsm.ml | 65 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 84 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 49 |
3 files changed, 114 insertions, 84 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7f511912..41a815d6 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -19,6 +19,7 @@ open Sections open AST open Memdata open Asm +open PrintAsmaux (* Type for the ABI versions *) type float_abi_type = @@ -45,38 +46,18 @@ module AsmPrinter (Opt: PRINTER_OPTIONS) = let literals_in_code = ref true (* to be turned into a proper option *) -(* 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 label_for_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' - (* Basic printing functions *) -let print_symb oc symb = - fprintf oc "%s" (extern_atom symb) - let print_label oc lbl = - fprintf oc ".L%d" (label_for_label lbl) + fprintf oc ".L%d" (transl_label lbl) let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) let comment = "@" -let print_symb_ofs oc (symb, ofs) = - print_symb oc 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 @@ -254,7 +235,7 @@ let emit_constants oc = Hashtbl.iter (fun (id, ofs) lbl -> fprintf oc ".L%d: .word %a\n" - lbl print_symb_ofs (id, ofs)) + lbl symbol_offset (id, ofs)) symbol_labels; reset_constants () @@ -263,13 +244,13 @@ let emit_constants oc = let loadsymbol oc r id ofs = if !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" - ireg r print_symb_ofs (id, ofs); + ireg r symbol_offset (id, ofs); fprintf oc " movt %a, #:upper16:%a\n" - ireg r print_symb_ofs (id, ofs); 2 + ireg r symbol_offset (id, ofs); 2 end else begin let lbl = label_symbol id ofs in fprintf oc " ldr %a, .L%d @ %a\n" - ireg r lbl print_symb_ofs (id, ofs); 1 + ireg r lbl symbol_offset (id, ofs); 1 end (* Emit instruction sequences that set or offset a register by a constant. *) @@ -483,10 +464,6 @@ let print_builtin_vstore_global oc chunk id ofs args = (* Handling of varargs *) -let current_function_stacksize = ref 0l -let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } - let align n a = (n + a - 1) land (-a) let rec next_arg_location ir ofs = function @@ -761,7 +738,7 @@ let print_instruction oc = function fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 | Pbsymb(id, sg) -> let n = fixup_arguments oc Outgoing sg in - fprintf oc " b %a\n" print_symb id; + fprintf oc " b %a\n" symbol id; n + 1 | Pbreg(r, sg) -> let n = @@ -772,7 +749,7 @@ let print_instruction oc = function n + 1 | Pblsymb(id, sg) -> let n1 = fixup_arguments oc Outgoing sg in - fprintf oc " bl %a\n" print_symb id; + fprintf oc " bl %a\n" symbol id; let n2 = fixup_result oc Incoming sg in n1 + 1 + n2 | Pblreg(r, sg) -> @@ -1084,18 +1061,18 @@ let print_function oc name fn = match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in fprintf oc " .balign %d\n" alignment; if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" print_symb name; + fprintf oc " .global %a\n" symbol name; if !Clflags.option_mthumb then fprintf oc " .thumb_func\n"; - fprintf oc "%a:\n" print_symb name; + fprintf oc "%a:\n" symbol name; print_location oc (C2C.atom_location name); Opt.cfi_startproc oc; ignore (fixup_arguments oc Incoming fn.fn_sig); print_instructions oc fn.fn_code; if !literals_in_code then emit_constants oc; Opt.cfi_endproc oc; - fprintf oc " .type %a, %%function\n" print_symb name; - fprintf oc " .size %a, . - %a\n" print_symb name print_symb name; + fprintf oc " .type %a, %%function\n" symbol name; + fprintf oc " .size %a, . - %a\n" symbol name symbol name; if not !literals_in_code && !size_constants > 0 then begin section oc lit; emit_constants oc @@ -1122,7 +1099,7 @@ let print_init oc = function if Z.gt n Z.zero then fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> - fprintf oc " .word %a\n" print_symb_ofs (symb, ofs) + fprintf oc " .word %a\n" symbol_offset (symb, ofs) let print_init_data oc name id = if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 @@ -1151,18 +1128,18 @@ let print_var oc name v = fprintf oc " %s\n" name_sec; fprintf oc " .balign %d\n" align; if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" print_symb name; - fprintf oc "%a:\n" print_symb name; + fprintf oc " .global %a\n" symbol name; + fprintf oc "%a:\n" symbol name; print_init_data oc name v.gvar_init; - fprintf oc " .type %a, %%object\n" print_symb name; - fprintf oc " .size %a, . - %a\n" print_symb name print_symb name + fprintf oc " .type %a, %%object\n" symbol name; + fprintf oc " .size %a, . - %a\n" symbol name symbol name end else begin let sz = match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in if C2C.atom_is_static name then - fprintf oc " .local %a\n" print_symb name; + fprintf oc " .local %a\n" symbol name; fprintf oc " .comm %a, %s, %d\n" - print_symb name + symbol name (Z.to_string sz) align end diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml new file mode 100644 index 00000000..3493e912 --- /dev/null +++ b/backend/PrintAsmaux.ml @@ -0,0 +1,84 @@ +(* *********************************************************************) +(* *) +(* 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: 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: 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' + + +(* 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 = "#" diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 0c4356ec..6e9e1a4f 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -20,12 +20,12 @@ open Sections open AST open Memdata open Asm +open PrintAsmaux (* Recognition of target ABI and asm syntax *) module type SYSTEM = sig - val comment: string val constant: out_channel -> constant -> unit val ireg: out_channel -> ireg -> unit val freg: out_channel -> freg -> unit @@ -39,15 +39,8 @@ module type SYSTEM = val print_prologue: out_channel -> unit end -let symbol oc symb = - fprintf oc "%s" (extern_atom symb) - -let symbol_offset oc (symb, ofs) = - symbol oc symb; - if ofs <> 0l then fprintf oc " + %ld" ofs - let symbol_fragment oc s n op = - fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op + fprintf oc "(%a)%s" symbol_offset (s, n) op let int_reg_name = function @@ -72,7 +65,6 @@ let float_reg_name = function module Linux_System : SYSTEM = struct - let comment = "#" let constant oc cst = match cst with @@ -155,7 +147,6 @@ module Linux_System : SYSTEM = module Diab_System : SYSTEM = struct - let comment = ";" let constant oc cst = match cst with @@ -224,23 +215,6 @@ module AsmPrinter (Target : SYSTEM) = struct open Target -(* 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' - (* Basic printing functions *) let coqint oc n = @@ -249,7 +223,6 @@ let coqint oc n = let raw_symbol oc s = fprintf oc "%s" s - let label oc lbl = fprintf oc ".L%d" lbl @@ -328,10 +301,6 @@ let short_cond_branch tbl pc lbl_dest = (* Printing of instructions *) -let float_literals : (int * int64) list ref = ref [] -let float32_literals : (int * int32) list ref = ref [] -let jumptables : (int * label list) list ref = ref [] - let print_instruction oc tbl pc fallthrough = function | Padd(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -516,7 +485,7 @@ let print_instruction oc tbl pc fallthrough = function let lbl = new_label() in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); - float_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float_literals; + float64_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float64_literals; | Plfis(r1, c) -> let lbl = new_label() in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; @@ -715,7 +684,7 @@ let print_jumptable oc (lbl, tbl) = let print_function oc name fn = Hashtbl.clear current_function_labels; - float_literals := []; + float64_literals := []; float32_literals := []; jumptables := []; let (text, lit, jmptbl) = @@ -736,12 +705,12 @@ let print_function oc name fn = cfi_endproc oc; fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name; - if !float_literals <> [] || !float32_literals <> [] then begin + if !float64_literals <> [] || !float32_literals <> [] then begin section oc lit; fprintf oc " .balign 8\n"; - List.iter (print_literal64 oc) !float_literals; + List.iter (print_literal64 oc) !float64_literals; List.iter (print_literal32 oc) !float32_literals; - float_literals := []; float32_literals := [] + float64_literals := []; float32_literals := [] end; if !jumptables <> [] then begin section oc jmptbl; @@ -777,7 +746,7 @@ let print_init oc = function fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> fprintf oc " .long %a\n" - symbol_offset (symb, camlint_of_coqint ofs) + symbol_offset (symb, ofs) let print_init_data oc name id = if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 @@ -840,7 +809,7 @@ let print_program oc p = | Linux -> (module Linux_System:SYSTEM) | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in PrintAnnot.reset_filenames(); - PrintAnnot.print_version_and_options oc Target.comment; + PrintAnnot.print_version_and_options oc comment; let module Printer = AsmPrinter(Target) in Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; |