diff options
Diffstat (limited to 'powerpc/PrintAsm.ml')
| -rw-r--r-- | powerpc/PrintAsm.ml | 319 |
1 files changed, 9 insertions, 310 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index f058cde5..97b57c0e 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -20,256 +20,16 @@ open Sections open AST open Memdata open Asm - -(* 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 - val creg: out_channel -> int -> unit - val name_of_section: section_name -> string - val print_file_line: out_channel -> string -> int -> 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 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 : 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 "COMM" - | Section_const i -> - if i then ".rodata" else "COMM" - | Section_small_const i -> - if i then ".section .sdata2,\"a\",@progbits" else "COMM" - | 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 print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line - - (* 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 - -module Diab_System : 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 "COMM" - | 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 print_file_line oc file line = - PrintAnnot.print_file_line_d1 oc comment file line - - (* 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 +open PrintUtil +open PrintLinux +open PrintDiab 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' + include Target (* Basic printing functions *) -let coqint oc n = - fprintf oc "%ld" (camlint_of_coqint n) - -let raw_symbol oc s = - fprintf oc "%s" s - - -let label oc lbl = - fprintf oc ".L%d" lbl - -let label_low oc lbl = - fprintf oc ".L%d@l" lbl - -let label_high oc lbl = - fprintf oc ".L%d@ha" lbl - - -let num_crbit = function - | CRbit_0 -> 0 - | CRbit_1 -> 1 - | CRbit_2 -> 2 - | CRbit_3 -> 3 - | CRbit_6 -> 6 - -let crbit oc bit = - fprintf oc "%d" (num_crbit bit) - let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r @@ -286,29 +46,8 @@ let section oc sec = let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) -(* Encoding masks for rlwinm instructions *) - -let rolm_mask n = - let mb = ref 0 (* location of last 0->1 transition *) - and me = ref 32 (* location of last 1->0 transition *) - and last = ref ((Int32.logand n 1l) <> 0l) (* last bit seen *) - and count = ref 0 (* number of transitions *) - and mask = ref 0x8000_0000l in - for mx = 0 to 31 do - if Int32.logand n !mask <> 0l then - if !last then () else (incr count; mb := mx; last := true) - else - if !last then (incr count; me := mx; last := false) else (); - mask := Int32.shift_right_logical !mask 1 - done; - if !me = 0 then me := 32; - assert (!count = 2 || (!count = 0 && !last)); - (!mb, !me-1) - (* Handling of annotations *) -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - let print_annot_stmt oc txt targs args = if Str.string_match re_file_line txt 0 then begin print_file_line oc (Str.matched_group 1 txt) @@ -318,14 +57,6 @@ let print_annot_stmt oc txt targs args = PrintAnnot.print_annot_stmt preg "R1" oc txt targs args end -(* Determine if the displacement of a conditional branch fits the short form *) - -let short_cond_branch tbl pc lbl_dest = - match PTree.get lbl_dest tbl with - | None -> assert false - | Some pc_dest -> - let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000 - (* Printing of instructions *) let float_literals : (int * int64) list ref = ref [] @@ -657,37 +388,6 @@ let print_instruction oc tbl pc fallthrough = function | Pcfi_rel_offset n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) -(* Determine if an instruction falls through *) - -let instr_fall_through = function - | Pb _ -> false - | Pbctr _ -> false - | Pbs _ -> false - | Pblr -> false - | _ -> true - -(* Estimate the size of an Asm instruction encoding, in number of actual - PowerPC instructions. We can over-approximate. *) - -let instr_size = function - | Pbf(bit, lbl) -> 2 - | Pbt(bit, lbl) -> 2 - | Pbtbl(r, tbl) -> 5 - | Plfi(r1, c) -> 2 - | Plfis(r1, c) -> 2 - | Plabel lbl -> 0 - | Pbuiltin(ef, args, res) -> 0 - | Pannot(ef, args) -> 0 - | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 - | _ -> 1 - -(* Build a table label -> estimated position in generated code. - Used to predict if relative conditional branches can use the short form. *) - -let rec label_positions tbl pc = function - | [] -> tbl - | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c - | i :: c -> label_positions tbl (pc + instr_size i) c (* Emit a sequence of instructions *) @@ -847,11 +547,10 @@ let print_program oc p = let module Target = (val (match target with | Linux -> (module Linux_System:SYSTEM) | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in - PrintAnnot.reset_filenames(); - PrintAnnot.print_version_and_options oc Target.comment; let module Printer = AsmPrinter(Target) in - Target.print_prologue oc; + Printer.set_compilation_unit_addrs 1 2; (* TODO This is dummy code *) + PrintAnnot.reset_filenames(); + PrintAnnot.print_version_and_options oc Printer.comment; + Printer.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; - PrintAnnot.close_filenames() - - + Printer.print_epilogue oc |