From a6bb01f79d1ec6c3bc485d65677314e87ddd7bb9 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 8 Oct 2014 17:53:38 +0200 Subject: Refactored the code of powerpc/PrintAsm.ml by moving the function depending on the target system in a seperate module. --- powerpc/PrintAsm.ml | 436 ++++++++++++++++++++++++++++------------------------ 1 file changed, 236 insertions(+), 200 deletions(-) (limited to 'powerpc') diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index d2ec5613..587dfccf 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -23,13 +23,227 @@ open Asm (* Recognition of target ABI and asm syntax *) -type target = Linux | Diab +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 + val creg: out_channel -> int -> unit + val name_of_section: section_name -> string + val print_file_line: out_channel -> string -> string -> unit + val reset_file_line: unit -> unit + val cfi_startproc: out_channel -> unit + val cfi_endproc: out_channel -> unit + val cfi_adjust: out_channel -> int32 -> unit + val cfi_rel_offset: out_channel -> string -> int32 -> unit + 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 -let target = - match Configuration.system with - | "linux" -> Linux - | "diab" -> Diab - | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") + +let int_reg_name = function + | GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3" + | GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7" + | GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11" + | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15" + | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19" + | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23" + | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27" + | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31" + +let float_reg_name = function + | FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3" + | FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7" + | FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11" + | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15" + | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19" + | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23" + | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" + | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" + +module Linux_System = + (struct + let comment = "#" + + let constant oc cst = + match cst with + | Cint n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Csymbol_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_high(s, n) -> + symbol_fragment oc s n "@ha" + | Csymbol_sda(s, n) -> + symbol_fragment oc s n "@sda21" + (* 32-bit relative addressing is supported by the Diab tools but not by + GNU binutils. In the latter case, for testing purposes, we treat + them as absolute addressings. The default base register being GPR0, + this produces correct code, albeit with absolute addresses. *) + | Csymbol_rel_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_rel_high(s, n) -> + symbol_fragment oc s n "@ha" + + let ireg oc r = + output_string oc (int_reg_name r) + + let freg oc r = + output_string oc (float_reg_name r) + + let creg oc r = + fprintf oc "%d" r + + let name_of_section = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else "COMM" + | Section_small_data i -> + if i + then ".section .sdata,\"aw\",@progbits" + else ".section .sbss,\"aw\",@progbits" + | Section_const -> ".rodata" + | Section_small_const -> ".section .sdata2,\"a\",@progbits" + | Section_string -> ".rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + + let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7 + let reset_file_line () = Hashtbl.clear filename_num + let print_file_line oc file line = + if !Clflags.option_g && file <> "" then begin + let filenum = + try + Hashtbl.find filename_num file + with Not_found -> + let n = Hashtbl.length filename_num + 1 in + Hashtbl.add filename_num file n; + fprintf oc " .file %d %S\n" n file; + n + in fprintf oc " .loc %d %s\n" filenum line + end + + (* 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 _ _ _ -> ()) + + + let print_prologue oc = () + + end:SYSTEM) + +module Diab_System = + (struct + let comment = ";" + + let constant oc cst = + match cst with + | Cint n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Csymbol_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_high(s, n) -> + symbol_fragment oc s n "@ha" + | Csymbol_sda(s, n) -> + symbol_fragment oc s n "@sdarx" + | Csymbol_rel_low(s, n) -> + symbol_fragment oc s n "@sdax@l" + | Csymbol_rel_high(s, n) -> + symbol_fragment oc s n "@sdarx@ha" + + let ireg oc r = + output_char oc 'r'; + output_string oc (int_reg_name r) + + let freg oc r = + output_char oc 'f'; + output_string oc (float_reg_name r) + + let creg oc r = + fprintf oc "cr%d" r + + let name_of_section = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else ".bss" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const -> ".text" + | Section_small_const -> ".sdata2" + | Section_string -> ".text" + | Section_literal -> ".text" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",,%c" + s + (match wr, ex with + | true, true -> 'm' (* text+data *) + | true, false -> 'd' (* data *) + | false, true -> 'c' (* text *) + | false, false -> 'r') (* const *) + + let last_file = ref "" + let reset_file_line () = last_file := "" + let print_file_line oc file line = + if !Clflags.option_g && file <> "" then begin + if file <> !last_file then begin + fprintf oc " .d1file %S\n" file; + last_file := file + end; + fprintf oc " .d1line %s\n" line + end + + (* Emit .cfi directives *) + let cfi_startproc oc = () + + let cfi_endproc oc = () + + let cfi_adjust oc delta = () + + let cfi_rel_offset oc reg ofs = () + + + let print_prologue oc = + fprintf oc " .xopt align-fill-text=0x60000000\n"; + if !Clflags.option_g then + fprintf oc " .xopt asm-debug-on\n" + + end:SYSTEM) + +module AsmPrinter (Target : SYSTEM) = + (struct + open Target (* On-the-fly label renaming *) @@ -56,12 +270,6 @@ let coqint oc n = let raw_symbol oc s = fprintf oc "%s" s -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 label oc lbl = fprintf oc ".L%d" lbl @@ -72,35 +280,6 @@ let label_low oc lbl = let label_high oc lbl = fprintf oc ".L%d@ha" lbl -let comment = - match target with - | Linux -> "#" - | Diab -> ";" - -let symbol_fragment oc s n op = - fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op - -let constant oc cst = - match cst with - | Cint n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Csymbol_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_high(s, n) -> - symbol_fragment oc s n "@ha" - | Csymbol_sda(s, n) -> - symbol_fragment oc s n - (match target with Linux -> "@sda21" | Diab -> "@sdarx") - (* 32-bit relative addressing is supported by the Diab tools but not by - GNU binutils. In the latter case, for testing purposes, we treat - them as absolute addressings. The default base register being GPR0, - this produces correct code, albeit with absolute addresses. *) - | Csymbol_rel_low(s, n) -> - symbol_fragment oc s n - (match target with Linux -> "@l" | Diab -> "@sdax@l") - | Csymbol_rel_high(s, n) -> - symbol_fragment oc s n - (match target with Linux -> "@ha" | Diab -> "@sdarx@ha") let num_crbit = function | CRbit_0 -> 0 @@ -112,170 +291,23 @@ let num_crbit = function let crbit oc bit = fprintf oc "%d" (num_crbit bit) -let int_reg_name = function - | GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3" - | GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7" - | GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11" - | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15" - | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19" - | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23" - | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27" - | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31" - -let float_reg_name = function - | FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3" - | FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7" - | FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11" - | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15" - | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19" - | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23" - | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" - | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" - -let ireg oc r = - begin match target with - | Diab -> output_char oc 'r' - | Linux -> () - end; - output_string oc (int_reg_name r) - let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r -let freg oc r = - begin match target with - | Diab -> output_char oc 'f' - | Linux -> () - end; - output_string oc (float_reg_name r) - -let creg oc r = - match target with - | Diab -> fprintf oc "cr%d" r - | Linux -> fprintf oc "%d" r - let preg oc = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false -(* Names of sections *) - -let name_of_section_Linux = function - | Section_text -> ".text" - | Section_data i -> if i then ".data" else "COMM" - | Section_small_data i -> - if i - then ".section .sdata,\"aw\",@progbits" - else ".section .sbss,\"aw\",@progbits" - | Section_const -> ".rodata" - | Section_small_const -> ".section .sdata2,\"a\",@progbits" - | Section_string -> ".rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" - s (if wr then "w" else "") (if ex then "x" else "") - -let name_of_section_Diab = function - | Section_text -> ".text" - | Section_data i -> if i then ".data" else ".bss" - | Section_small_data i -> if i then ".sdata" else ".sbss" - | Section_const -> ".text" - | Section_small_const -> ".sdata2" - | Section_string -> ".text" - | Section_literal -> ".text" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",,%c" - s - (match wr, ex with - | true, true -> 'm' (* text+data *) - | true, false -> 'd' (* data *) - | false, true -> 'c' (* text *) - | false, false -> 'r') (* const *) - -let name_of_section = - match target with - | Linux -> name_of_section_Linux - | Diab -> name_of_section_Diab - let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); fprintf oc " %s\n" name -(* Emit .file / .loc debugging directives *) - -module DebugLinux = struct - let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7 - let reset () = Hashtbl.clear filename_num - let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - let filenum = - try - Hashtbl.find filename_num file - with Not_found -> - let n = Hashtbl.length filename_num + 1 in - Hashtbl.add filename_num file n; - fprintf oc " .file %d %S\n" n file; - n - in fprintf oc " .loc %d %s\n" filenum line - end -end - -module DebugDiab = struct - let last_file = ref "" - let reset () = last_file := "" - let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - if file <> !last_file then begin - fprintf oc " .d1file %S\n" file; - last_file := file - end; - fprintf oc " .d1line %s\n" line - end -end - -let print_file_line = - match target with - | Linux -> DebugLinux.print_file_line - | Diab -> DebugDiab.print_file_line - let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (string_of_int (snd loc)) -let reset_file_line = - match target with - | Linux -> DebugLinux.reset - | Diab -> DebugDiab.reset - -(* Emit .cfi directives *) - -let cfi_startproc oc = - if Configuration.asm_supports_cfi then - match target with - | Linux -> fprintf oc " .cfi_startproc\n" - | Diab -> () - -let cfi_endproc oc = - if Configuration.asm_supports_cfi then - match target with - | Linux -> fprintf oc " .cfi_endproc\n" - | Diab -> () - -let cfi_adjust oc delta = - if Configuration.asm_supports_cfi then - match target with - | Linux -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta - | Diab -> () - -let cfi_rel_offset oc reg ofs = - if Configuration.asm_supports_cfi then - match target with - | Linux -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs - | Diab -> () (* Encoding masks for rlwinm instructions *) @@ -824,18 +856,22 @@ let print_globdef oc (name, gdef) = | Gfun f -> print_fundef oc name f | Gvar v -> print_var oc name v -let print_prologue oc = - match target with - | Linux -> - () - | Diab -> - fprintf oc " .xopt align-fill-text=0x60000000\n"; - if !Clflags.option_g then - fprintf oc " .xopt asm-debug-on\n" + end) + +type target = Linux | Diab let print_program oc p = - reset_file_line(); - PrintAnnot.print_version_and_options oc comment; - print_prologue oc; - List.iter (print_globdef oc) p.prog_defs + let target = + (match Configuration.system with + | "linux" -> Linux + | "diab" -> Diab + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) in + let module Target = (val (match target with + | Linux -> (module Linux_System:SYSTEM) + | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in + Target.reset_file_line(); + PrintAnnot.print_version_and_options oc Target.comment; + let module Printer = AsmPrinter(Target) in + Target.print_prologue oc; + List.iter (Printer.print_globdef oc) p.prog_defs -- cgit