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 /debug | |
parent | 803eb70bbbbc5749882efd2a3af339a7e05f1f62 (diff) | |
download | compcert-8aae10b50b321cfcbde86582cdd7ce1df8960628.tar.gz compcert-8aae10b50b321cfcbde86582cdd7ce1df8960628.zip |
Starting to remove the seperate printers for each backend.
Diffstat (limited to 'debug')
-rw-r--r-- | debug/DwarfDiab.ml | 55 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml (renamed from debug/DwarfAbbrvPrinter.ml) | 58 |
2 files changed, 105 insertions, 8 deletions
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) |