diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-02 09:14:10 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-02 09:14:10 +0100 |
commit | 8aae10b50b321cfcbde86582cdd7ce1df8960628 (patch) | |
tree | 4e76f4d98f1bf97783c1f55fc5adcba415abfc41 | |
parent | 803eb70bbbbc5749882efd2a3af339a7e05f1f62 (diff) | |
download | compcert-8aae10b50b321cfcbde86582cdd7ce1df8960628.tar.gz compcert-8aae10b50b321cfcbde86582cdd7ce1df8960628.zip |
Starting to remove the seperate printers for each backend.
-rw-r--r-- | arm/PrintAsm.ml | 2 | ||||
-rw-r--r-- | common/Sections.ml | 2 | ||||
-rw-r--r-- | common/Sections.mli | 2 | ||||
-rw-r--r-- | debug/DwarfDiab.ml | 55 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml (renamed from debug/DwarfAbbrvPrinter.ml) | 58 | ||||
-rw-r--r-- | ia32/PrintAsm.ml | 7 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 317 | ||||
-rw-r--r-- | powerpc/PrintDiab.ml | 85 | ||||
-rw-r--r-- | powerpc/PrintUtil.ml | 180 |
9 files changed, 432 insertions, 276 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7f511912..582b70e7 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -177,6 +177,8 @@ let name_of_section = function | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",%%progbits" s (if wr then "w" else "") (if ex then "x" else "") + | Section_debug -> sprintf ".section .debug_info,\"\",@progbits" + | Section_debug_abbrev -> sprintf ".section .debug_abbrev,\"\",@progbits" let section oc sec = fprintf oc " %s\n" (name_of_section sec) diff --git a/common/Sections.ml b/common/Sections.ml index c6d4c4c2..086c860e 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -27,6 +27,8 @@ type section_name = | Section_literal | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) + | Section_debug + | Section_debug_abbrev type access_mode = | Access_default diff --git a/common/Sections.mli b/common/Sections.mli index 38b99db0..be716e48 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -26,6 +26,8 @@ type section_name = | Section_literal | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) + | Section_debug + | Section_debug_abbrev type access_mode = | Access_default diff --git a/debug/DwarfDiab.ml b/debug/DwarfDiab.ml new file mode 100644 index 00000000..a852053f --- /dev/null +++ b/debug/DwarfDiab.ml @@ -0,0 +1,55 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open Printf +open DwarfPrinter +open DwarfTypes +open DwarfUtil + +module AbbrvPrinter = DwarfPrinter(struct + let string_of_byte value = + Printf.sprintf " .byte %s\n" (if value then "0x1" else "0x2") + + let string_of_abbrv_entry v = + Printf.sprintf " .uleb128 %d\n" v + + let sibling_type_abbr = dw_form_ref4 + let decl_file_type_abbr = dw_form_data4 + let decl_line_type_abbr = dw_form_udata + let type_abbr = dw_form_ref_addr + let name_type_abbr = dw_form_string + let encoding_type_abbr = dw_form_data1 + let byte_size_type_abbr = dw_form_data1 + let high_pc_type_abbr = dw_form_addr + let low_pc_type_abbr = dw_form_addr + let stmt_list_type_abbr = dw_form_data4 + let declaration_type_abbr = dw_form_flag + let external_type_abbr = dw_form_flag + let prototyped_type_abbr = dw_form_flag + let bit_offset_type_abbr = dw_form_data1 + let comp_dir_type_abbr = dw_form_string + let language_type_abbr = dw_form_udata + let producer_type_abbr = dw_form_string + let value_type_abbr = dw_form_sdata + let artificial_type_abbr = dw_form_flag + let variable_parameter_type_abbr = dw_form_flag + let bit_size_type_abbr = dw_form_data1 + let location_const_type_abbr = dw_form_data4 + let location_block_type_abbr = dw_form_block + let data_location_block_type_abbr = dw_form_block + let data_location_ref_type_abbr = dw_form_ref4 + let bound_const_type_abbr = dw_form_udata + let bound_ref_type_abbr=dw_form_ref4 + + + +end) diff --git a/debug/DwarfAbbrvPrinter.ml b/debug/DwarfPrinter.ml index 214484b6..81f36a24 100644 --- a/debug/DwarfAbbrvPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -14,15 +14,11 @@ open DwarfTypes open DwarfUtil -module type DWARF_ABBRV_DEFS = +module type DWARF_DEFS = sig (* Functions used for the printing of the dwarf abbreviations *) val string_of_byte: bool -> string val string_of_abbrv_entry: int -> string - val abbrv_section_start: out_channel -> unit - val abbrv_section_end: out_channel -> unit - val abbrv_prologue: out_channel -> int -> unit - val abbrv_epilogue: out_channel -> unit val get_abbrv_start_addr: unit -> int (* The form constants of the types *) val sibling_type_abbr: int @@ -54,9 +50,9 @@ module type DWARF_ABBRV_DEFS = val bound_ref_type_abbr: int end -module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) : +module DwarfPrinter(Defs:DWARF_DEFS) : sig - val print_debug_abbrv: out_channel -> dw_entry -> unit + val print_debug: out_channel -> dw_entry -> unit val get_abbrv: dw_entry -> bool -> int val get_abbrv_start_addr: unit -> int end = @@ -295,6 +291,25 @@ module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) : | None -> false | Some _ -> true in ignore (get_abbrv entry has_sib)) entry + + let abbrv_section_start oc = + fprintf oc " .section .debug_abbrev,,n\n"(* ; *) + (* let lbl = new_label () in *) + (* abbrv_start_addr := lbl; *) + (* fprintf oc "%a:\n" label lbl *) + + let abbrv_section_end oc = + fprintf oc " .section .debug_abbrev,,n\n"; + fprintf oc " .sleb128 0\n" + + let abbrv_prologue oc id = + fprintf oc " .section .debug_abbrev,,n\n"; + fprintf oc " .uleb128 %d\n" id + + let abbrv_epilogue oc = + fprintf oc " .uleb128 0\n"; + fprintf oc " .uleb128 0\n" + let print_abbrv oc = let abbrvs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) !abbrvs in @@ -305,10 +320,37 @@ module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) : Defs.abbrv_epilogue oc) abbrvs; Defs.abbrv_section_end oc + + let rec print_entry oc entry has_sibling = + () + let print_debug_abbrv oc entry = compute_abbrv entry; print_abbrv oc - let get_abbrv_start_addr = Defs.get_abbrv_start_addr + let print_debug_info oc entry = + print_debug_abbrv oc entry; + let abbrv_start = DwarfDiab.AbbrvPrinter.get_abbrv_start_addr () in + let debug_start = new_label () in + let print_info () = + fprintf oc" .section .debug_info,,n\n" in + print_info (); + fprintf oc "%a\n" label debug_start; + let debug_length_start = new_label () in (* Address used for length calculation *) + let debug_end = new_label () in + fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start; + fprintf oc "%a\n" label debug_length_start; + fprintf oc " .2byte 0x2\n"; (* Dwarf version *) + fprintf oc " .4byte %a\n" label abbrv_start; (* Offset into the abbreviation *) + fprintf oc " .byte %X\n" !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *) + print_entry oc entry false; + fprintf oc "%a\n" label debug_end; (* End of the debug section *) + fprintf oc " .sleb128 0\n" + + + let abbrv_start_addr = ref (-1) + + let get_abbrv_start_addr () = !abbrv_start_addr + end) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index b0ef0180..c77347da 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -98,6 +98,8 @@ module Cygwin_System = | Section_user(s, wr, ex) -> sprintf ".section \"%s\", \"%s\"\n" s (if ex then "xr" else if wr then "d" else "dr") + | Section_debug -> ".section .debug_info,\"\"" + | Section_debug_abbrev -> ".section .debug_abbrev,\"\"" let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -147,7 +149,10 @@ module ELF_System = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") + | Section_debug -> sprintf ".section .debug_info,\"\",@progbits" + | Section_debug_abbrev -> sprintf ".section .debug_abbrev,\"\",@progbits" + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) let print_align oc n = @@ -201,6 +206,8 @@ module MacOS_System = sprintf ".section \"%s\", %s, %s" (if wr then "__DATA" else "__TEXT") s (if ex then "regular, pure_instructions" else "regular") + | Section_debug -> ".section __DWARF,__debug_info,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" let stack_alignment = 16 (* mandatory *) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 8a064d52..77eb2378 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -20,16 +20,263 @@ open Sections open AST open Memdata open Asm -open PrintUtil -open PrintLinux -open PrintDiab + +(* 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 + (* val print_epilogue: out_channel -> unit *) + (* val print_addr_label: out_channel -> int -> unit *) + (* val set_compilation_unit_addrs: int -> int -> 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 "") + | Section_debug -> sprintf ".section .debug_info,\"\",@progbits" + | Section_debug_abbrev -> sprintf ".section .debug_abbrev,\"\",@progbits" + + 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 *) + | Section_debug -> ".section .debug_info,,n" + | Section_debug_abbrev -> ".section .debug_abbrev,,n" + + let print_file_line oc file line = + PrintAnnot.print_file_line_d2 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 module AsmPrinter (Target : SYSTEM) = struct include 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 = + 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 @@ -46,8 +293,29 @@ 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) @@ -57,6 +325,14 @@ 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 [] @@ -388,6 +664,37 @@ 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 *) @@ -540,9 +847,9 @@ let print_program oc p = | Linux -> (module Linux_System:SYSTEM) | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in let module Printer = AsmPrinter(Target) in - Printer.set_compilation_unit_addrs 1 2; (* TODO This is dummy code *) + (* 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; - Printer.print_epilogue oc + (* Printer.print_epilogue oc *) diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml index e431a8c7..61a4eff9 100644 --- a/powerpc/PrintDiab.ml +++ b/powerpc/PrintDiab.ml @@ -16,7 +16,7 @@ open Printf open Datatypes open DwarfTypes open DwarfUtil -open DwarfAbbrvPrinter +open DwarfPrinter open Camlcoq open Sections open Asm @@ -145,87 +145,6 @@ module Diab_System = fprintf oc " .d2_line_end\n"; end - module AbbrvPrinter = DwarfAbbrvPrinter(struct - let string_of_byte value = - Printf.sprintf " .byte %s\n" (if value then "0x1" else "0x2") - - let string_of_abbrv_entry v = - Printf.sprintf " .uleb128 %d\n" v - - let abbrv_start_addr = ref (-1) - - let get_abbrv_start_addr () = !abbrv_start_addr - - let sibling_type_abbr = dw_form_ref4 - let decl_file_type_abbr = dw_form_data4 - let decl_line_type_abbr = dw_form_udata - let type_abbr = dw_form_ref_addr - let name_type_abbr = dw_form_string - let encoding_type_abbr = dw_form_data1 - let byte_size_type_abbr = dw_form_data1 - let high_pc_type_abbr = dw_form_addr - let low_pc_type_abbr = dw_form_addr - let stmt_list_type_abbr = dw_form_data4 - let declaration_type_abbr = dw_form_flag - let external_type_abbr = dw_form_flag - let prototyped_type_abbr = dw_form_flag - let bit_offset_type_abbr = dw_form_data1 - let comp_dir_type_abbr = dw_form_string - let language_type_abbr = dw_form_udata - let producer_type_abbr = dw_form_string - let value_type_abbr = dw_form_sdata - let artificial_type_abbr = dw_form_flag - let variable_parameter_type_abbr = dw_form_flag - let bit_size_type_abbr = dw_form_data1 - let location_const_type_abbr = dw_form_data4 - let location_block_type_abbr = dw_form_block - let data_location_block_type_abbr = dw_form_block - let data_location_ref_type_abbr = dw_form_ref4 - let bound_const_type_abbr = dw_form_udata - let bound_ref_type_abbr=dw_form_ref4 - - - let abbrv_section_start oc = - fprintf oc " .section .debug_abbrev,,n\n"; - let lbl = new_label () in - abbrv_start_addr := lbl; - fprintf oc "%a:\n" label lbl - - let abbrv_section_end oc = - fprintf oc " .section .debug_abbrev,,n\n"; - fprintf oc " .sleb128 0\n" - - let abbrv_prologue oc id = - fprintf oc " .section .debug_abbrev,,n\n"; - fprintf oc " .uleb128 %d\n" id - - let abbrv_epilogue oc = - fprintf oc " .uleb128 0\n"; - fprintf oc " .uleb128 0\n" - - end) - - let rec print_entry oc entry has_sibling = - () - - let print_debug_info oc entry = - AbbrvPrinter.print_debug_abbrv oc entry; - let abbrv_start = AbbrvPrinter.get_abbrv_start_addr () in - let debug_start = new_label () in - let print_info () = - fprintf oc" .section .debug_info,,n\n" in - print_info (); - fprintf oc "%a\n" label debug_start; - let debug_length_start = new_label () in (* Address used for length calculation *) - let debug_end = new_label () in - fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start; - fprintf oc "%a\n" label debug_length_start; - fprintf oc " .2byte 0x2\n"; (* Dwarf version *) - fprintf oc " .4byte %a\n" label abbrv_start; (* Offset into the abbreviation *) - fprintf oc " .byte %X\n" !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *) - print_entry oc entry false; - fprintf oc "%a\n" label debug_end; (* End of the debug section *) - fprintf oc " .sleb128 0\n" - + end:SYSTEM) diff --git a/powerpc/PrintUtil.ml b/powerpc/PrintUtil.ml deleted file mode 100644 index e007b273..00000000 --- a/powerpc/PrintUtil.ml +++ /dev/null @@ -1,180 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Common functions for the AsmPrinter *) - -open Printf -open Maps -open Camlcoq -open Sections -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 - val print_epilogue: out_channel -> unit - val print_addr_label: out_channel -> int -> unit - val set_compilation_unit_addrs: int -> int -> 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" - -(* 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 = - 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) - - -(* 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]*\\)$" - -(* 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 - -(* 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 |