aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
Diffstat (limited to 'debug')
-rw-r--r--debug/DwarfPrinter.ml452
-rw-r--r--debug/DwarfTypes.ml258
-rw-r--r--debug/DwarfUtil.ml118
3 files changed, 828 insertions, 0 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
new file mode 100644
index 00000000..4f79584f
--- /dev/null
+++ b/debug/DwarfPrinter.ml
@@ -0,0 +1,452 @@
+(* *********************************************************************)
+(* *)
+(* 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 DwarfTypes
+open DwarfUtil
+open Printf
+open PrintAsmaux
+open Sections
+
+module DwarfPrinter(Target: TARGET) :
+ sig
+ val print_debug: out_channel -> dw_entry -> unit
+ end =
+ struct
+
+ open Target
+
+ let string_of_byte value =
+ sprintf " .byte %s\n" (if value then "0x1" else "0x0")
+
+ let print_label oc lbl =
+ fprintf oc "%a:\n" label lbl
+
+ let curr_abbrev = ref 1
+
+ let next_abbrev =
+ let abbrev = !curr_abbrev in
+ incr curr_abbrev;abbrev
+
+ let abbrevs: (string * int) list ref = ref []
+
+ let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7
+
+ let add_byte buf value =
+ Buffer.add_string buf (string_of_byte value)
+
+ let add_abbr_uleb v buf =
+ Buffer.add_string buf (Printf.sprintf " .uleb128 %d\n" v)
+
+ let add_abbr_entry (v1,v2) buf =
+ add_abbr_uleb v1 buf;
+ add_abbr_uleb v2 buf
+
+ let add_sibling = add_abbr_entry (0x1,DwarfAbbrevs.sibling_type_abbr)
+
+ let add_file_loc buf =
+ let file,line = DwarfAbbrevs.file_loc_type_abbr in
+ add_abbr_entry (0x3a,file) buf;
+ add_abbr_entry (0x3b,line) buf
+
+ let add_type = add_abbr_entry (0x49,DwarfAbbrevs.type_abbr)
+
+ let add_name = add_abbr_entry (0x3,DwarfAbbrevs.name_type_abbr)
+
+ let add_encoding = add_abbr_entry (0x3e,DwarfAbbrevs.encoding_type_abbr)
+
+ let add_byte_size = add_abbr_entry (0xb,DwarfAbbrevs.byte_size_type_abbr)
+
+ let add_high_pc = add_abbr_entry (0x12,DwarfAbbrevs.high_pc_type_abbr)
+
+ let add_low_pc = add_abbr_entry (0x11,DwarfAbbrevs.low_pc_type_abbr)
+
+ let add_stmt_list = add_abbr_entry (0x10,DwarfAbbrevs.stmt_list_type_abbr)
+
+ let add_declaration = add_abbr_entry (0x3c,DwarfAbbrevs.declaration_type_abbr)
+
+ let add_external = add_abbr_entry (0x3f,DwarfAbbrevs.external_type_abbr)
+
+ let add_prototyped = add_abbr_entry (0x27,DwarfAbbrevs.prototyped_type_abbr)
+
+ let add_bit_offset = add_abbr_entry (0xd,DwarfAbbrevs.bit_offset_type_abbr)
+
+ let add_comp_dir = add_abbr_entry (0x1b,DwarfAbbrevs.comp_dir_type_abbr)
+
+ let add_language = add_abbr_entry (0x13,DwarfAbbrevs.language_type_abbr)
+
+ let add_producer = add_abbr_entry (0x25,DwarfAbbrevs.producer_type_abbr)
+
+ let add_value = add_abbr_entry (0x1c,DwarfAbbrevs.value_type_abbr)
+
+ let add_artificial = add_abbr_entry (0x34,DwarfAbbrevs.artificial_type_abbr)
+
+ let add_variable_parameter = add_abbr_entry (0x4b,DwarfAbbrevs.variable_parameter_type_abbr)
+
+ let add_bit_size = add_abbr_entry (0xc,DwarfAbbrevs.bit_size_type_abbr)
+
+ let add_location loc buf =
+ match loc with
+ | None -> ()
+ | Some (LocConst _) -> add_abbr_entry (0x2,DwarfAbbrevs.location_const_type_abbr) buf
+ | Some (LocBlock _) -> add_abbr_entry (0x2,DwarfAbbrevs.location_block_type_abbr) buf
+
+ let add_data_location loc buf =
+ match loc with
+ | None -> ()
+ | Some (DataLocBlock __) -> add_abbr_entry (0x38,DwarfAbbrevs.data_location_block_type_abbr) buf
+ | Some (DataLocRef _) -> add_abbr_entry (0x38,DwarfAbbrevs.data_location_ref_type_abbr) buf
+
+ let add_bound_value bound =
+ match bound with
+ | BoundConst _ -> add_abbr_entry (0x2f,DwarfAbbrevs.bound_const_type_abbr)
+ | BoundRef _ -> add_abbr_entry (0x2f,DwarfAbbrevs.bound_ref_type_abbr)
+
+ let abbrev_string_of_entity entity has_sibling =
+ let buf = Buffer.create 12 in
+ let add_attr_some v f =
+ match v with
+ | None -> ()
+ | Some _ -> f buf in
+ let prologue id =
+ let has_child = match entity.children with
+ | [] -> false
+ | _ -> true in
+ add_abbr_uleb id buf;
+ add_byte buf has_child;
+ if has_sibling then add_sibling buf;
+ in
+ (match entity.tag with
+ | DW_TAG_array_type e ->
+ prologue 0x1;
+ add_attr_some e.array_type_file_loc add_file_loc;
+ add_type buf
+ | DW_TAG_base_type _ ->
+ prologue 0x24;
+ add_encoding buf;
+ add_byte_size buf;
+ add_name buf
+ | DW_TAG_compile_unit e ->
+ prologue 0x11;
+ add_comp_dir buf;
+ add_high_pc buf;
+ add_low_pc buf;
+ add_language buf;
+ add_name buf;
+ add_producer buf;
+ add_stmt_list buf;
+ | DW_TAG_const_type _ ->
+ prologue 0x26;
+ add_type buf
+ | DW_TAG_enumeration_type e ->
+ prologue 0x4;
+ add_attr_some e.enumeration_file_loc add_file_loc;
+ add_byte_size buf;
+ add_name buf;
+ add_attr_some e.enumeration_declaration add_declaration
+ | DW_TAG_enumerator e ->
+ prologue 0x28;
+ add_attr_some e.enumerator_file_loc add_file_loc;
+ add_value buf;
+ add_name buf
+ | DW_TAG_formal_parameter e ->
+ prologue 0x34;
+ add_attr_some e.formal_parameter_file_loc add_file_loc;
+ add_attr_some e.formal_parameter_artificial add_artificial;
+ add_location e.formal_parameter_location buf;
+ add_name buf;
+ add_location e.formal_parameter_segment buf;
+ add_type buf;
+ add_attr_some e.formal_parameter_variable_parameter add_variable_parameter
+ | DW_TAG_label _ ->
+ prologue 0xa;
+ add_low_pc buf;
+ add_name buf;
+ | DW_TAG_lexical_block _ ->
+ prologue 0xb;
+ add_high_pc buf;
+ add_low_pc buf
+ | DW_TAG_member e ->
+ prologue 0xd;
+ add_attr_some e.member_file_loc add_file_loc;
+ add_attr_some e.member_byte_size add_byte_size;
+ add_attr_some e.member_bit_offset add_bit_offset;
+ add_attr_some e.member_bit_size add_bit_size;
+ add_data_location e.member_data_member_location buf;
+ add_attr_some e.member_declaration add_declaration;
+ add_name buf;
+ add_type buf
+ | DW_TAG_pointer_type _ ->
+ prologue 0xf;
+ add_type buf
+ | DW_TAG_structure_type e ->
+ prologue 0x13;
+ add_attr_some e.structure_file_loc add_file_loc;
+ add_byte_size buf;
+ add_attr_some e.structure_declaration add_declaration;
+ add_name buf
+ | DW_TAG_subprogram e ->
+ prologue 0x2e;
+ add_attr_some e.subprogram_file_loc add_file_loc;
+ add_attr_some e.subprogram_external add_external;
+ add_high_pc buf;
+ add_low_pc buf;
+ add_name buf;
+ add_prototyped buf;
+ add_type buf
+ | DW_TAG_subrange_type e ->
+ prologue 0x21;
+ add_attr_some e.subrange_type add_type;
+ add_bound_value e.subrange_upper_bound buf
+ | DW_TAG_subroutine_type _ ->
+ prologue 0x15;
+ add_prototyped buf
+ | DW_TAG_typedef e ->
+ prologue 0x16;
+ add_attr_some e.typedef_file_loc add_file_loc;
+ add_name buf;
+ add_type buf
+ | DW_TAG_union_type e ->
+ prologue 0x17;
+ add_attr_some e.union_file_loc add_file_loc;
+ add_byte_size buf;
+ add_name buf
+ | DW_TAG_unspecified_parameter e ->
+ prologue 0x18;
+ add_attr_some e.unspecified_parameter_file_loc add_file_loc;
+ add_attr_some e.unspecified_parameter_artificial add_artificial
+ | DW_TAG_variable e ->
+ prologue 0x34;
+ add_attr_some e.variable_file_loc add_file_loc;
+ add_attr_some e.variable_declaration add_declaration;
+ add_attr_some e.variable_external add_external;
+ add_location e.variable_location buf;
+ add_name buf;
+ add_location e.variable_segment buf;
+ add_type buf
+ | DW_TAG_volatile_type _ ->
+ prologue 0x35;
+ add_type buf);
+ Buffer.contents buf
+
+ let get_abbrev entity has_sibling =
+ let abbrev_string = abbrev_string_of_entity entity has_sibling in
+ (try
+ Hashtbl.find abbrev_mapping abbrev_string
+ with Not_found ->
+ let id = next_abbrev in
+ abbrevs:=(abbrev_string,id)::!abbrevs;
+ Hashtbl.add abbrev_mapping abbrev_string id;
+ id)
+
+ let compute_abbrev entry =
+ entry_iter_sib (fun sib entry ->
+ let has_sib = match sib with
+ | None -> false
+ | Some _ -> true in
+ ignore (get_abbrev entry has_sib)) entry
+
+ let abbrev_start_addr = ref (-1)
+
+ let abbrev_section_start oc =
+ fprintf oc " .section %s\n" (name_of_section Section_debug_abbrev);
+ let lbl = new_label () in
+ abbrev_start_addr := lbl;
+ print_label oc lbl
+
+ let abbrev_section_end oc =
+ fprintf oc " .sleb128 0\n"
+
+ let abbrev_prologue oc id =
+ fprintf oc " .uleb128 %d\n" id
+
+ let abbrev_epilogue oc =
+ fprintf oc " .uleb128 0\n";
+ fprintf oc " .uleb128 0\n"
+
+
+ let print_abbrev oc =
+ let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) !abbrevs in
+ abbrev_section_start oc;
+ List.iter (fun (s,id) ->
+ abbrev_prologue oc id;
+ output_string oc s;
+ abbrev_epilogue oc) abbrevs;
+ abbrev_section_end oc
+
+ let debug_start_addr = ref (-1)
+
+ let entry_labels: (int,int) Hashtbl.t = Hashtbl.create 7
+
+ let entry_to_label id =
+ try
+ Hashtbl.find entry_labels id
+ with Not_found ->
+ let label = new_label () in
+ Hashtbl.add entry_labels id label;
+ label
+
+ let print_opt_value oc o f =
+ match o with
+ | None -> ()
+ | Some o -> f oc o
+
+ let print_file_loc oc f =
+ print_opt_value oc f print_file_loc
+
+ let print_flag oc b =
+ output_string oc (string_of_byte b)
+
+ let print_string oc s =
+ fprintf oc " .asciz \"%s\"\n" s
+
+ let print_uleb128 oc d =
+ fprintf oc " .uleb128 %d\n" d
+
+ let print_sleb128 oc d =
+ fprintf oc " .sleb128 %d\n" d
+
+ let print_byte oc b =
+ fprintf oc " .byte 0x%X\n" b
+
+ let print_loc oc loc =
+ ()
+
+ let print_data_location oc dl =
+ ()
+
+ let print_ref oc r =
+ print_label oc (entry_to_label r)
+
+ let print_array_type oc at =
+ print_file_loc oc at.array_type_file_loc;
+ print_label oc (entry_to_label at.array_type)
+
+ let print_base_type oc bt =
+ print_byte oc bt.base_type_byte_size;
+ let encoding = match bt.base_type_encoding with
+ | DW_ATE_address -> 0x1
+ | DW_ATE_boolean -> 0x2
+ | DW_ATE_complex_float -> 0x3
+ | DW_ATE_float -> 0x4
+ | DW_ATE_signed -> 0x5
+ | DW_ATE_signed_char -> 0x6
+ | DW_ATE_unsigned -> 0x7
+ | DW_ATE_unsigned_char -> 0x8
+ in
+ print_byte oc encoding;
+ print_string oc bt.base_type_name
+
+ let print_compilation_unit oc tag =
+ print_string oc (Sys.getcwd ());
+ print_label oc (get_start_addr ());
+ print_label oc (get_end_addr ());
+ print_uleb128 oc 1;
+ print_string oc tag.compile_unit_name;
+ print_string oc ("CompCert "^Configuration.version);
+ print_label oc (get_stmt_list_addr ())
+
+ let print_const_type oc ct =
+ print_ref oc ct.const_type
+
+ let print_enumeration_type oc et =
+ print_file_loc oc et.enumeration_file_loc;
+ print_uleb128 oc et.enumeration_byte_size;
+ print_opt_value oc et.enumeration_declaration print_flag;
+ print_string oc et.enumeration_name
+
+ let print_enumerator oc en =
+ print_file_loc oc en.enumerator_file_loc;
+ print_sleb128 oc en.enumerator_value;
+ print_string oc en.enumerator_name
+
+ let print_formal_parameter oc fp =
+ print_file_loc oc fp.formal_parameter_file_loc;
+ print_opt_value oc fp.formal_parameter_artificial print_flag;
+ print_opt_value oc fp.formal_parameter_location print_loc;
+ print_string oc fp.formal_parameter_name;
+ print_opt_value oc fp.formal_parameter_segment print_loc;
+ print_ref oc fp.formal_parameter_type;
+ print_opt_value oc fp.formal_parameter_variable_parameter print_flag
+
+ let print_tag_label oc tl =
+ print_ref oc tl.label_low_pc;
+ print_string oc tl.label_name
+
+ let print_lexical_block oc lb =
+ print_ref oc lb.lexical_block_high_pc;
+ print_ref oc lb.lexical_block_low_pc
+
+ let print_member oc mb =
+ print_file_loc oc mb.member_file_loc;
+ print_opt_value oc mb.member_byte_size print_byte;
+ print_opt_value oc mb.member_bit_offset print_byte;
+ print_opt_value oc mb.member_bit_size print_byte;
+ print_opt_value oc mb.member_data_member_location print_data_location;
+ print_opt_value oc mb.member_declaration print_flag;
+ print_string oc mb.member_name;
+ print_ref oc mb.member_type
+
+ let print_pointer oc pt =
+ print_ref oc pt.pointer_type
+
+ let print_structure oc st =
+ print_file_loc oc st.structure_file_loc;
+ print_uleb128 oc st.structure_byte_size;
+ print_opt_value oc st.structure_declaration print_flag;
+ print_string oc st.structure_name
+
+ let print_entry oc entry =
+ entry_iter_sib (fun sib entry ->
+ print_ref oc entry.id;
+ let has_sib = match sib with
+ | None -> false
+ | Some _ -> true in
+ let id = get_abbrev entry has_sib in
+ print_sleb128 oc id;
+ (match sib with
+ | None -> ()
+ | Some s -> let lbl = entry_to_label s in
+ fprintf oc " .4byte %a-%a\n" label lbl label !debug_start_addr);
+ begin
+ match entry.tag with
+ | DW_TAG_array_type arr_type -> print_array_type oc arr_type
+ | DW_TAG_compile_unit comp -> print_compilation_unit oc comp
+ | DW_TAG_base_type bt -> print_base_type oc bt
+ | DW_TAG_const_type ct -> print_const_type oc ct
+ | _ -> ()
+ end;
+ if entry.children = [] then
+ print_sleb128 oc 0) entry
+
+ let print_debug_abbrev oc entry =
+ compute_abbrev entry;
+ print_abbrev oc
+
+ let print_debug oc entry =
+ print_debug_abbrev oc entry;
+ let debug_start = new_label () in
+ debug_start_addr:= debug_start;
+ fprintf oc" .section %s\n" (name_of_section Section_debug_info);
+ print_label oc debug_start;
+ let debug_length_start = new_label () (* Address used for length calculation *)
+ and debug_end = new_label () in
+ fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start;
+ print_label oc debug_length_start;
+ fprintf oc " .2byte 0x2\n"; (* Dwarf version *)
+ fprintf oc " .4byte %a\n" label !abbrev_start_addr; (* Offset into the abbreviation *)
+ print_byte oc !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *)
+ print_entry oc entry;
+ print_sleb128 oc 0;
+ print_label oc debug_end (* End of the debug section *)
+
+ end
diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml
new file mode 100644
index 00000000..81c4b858
--- /dev/null
+++ b/debug/DwarfTypes.ml
@@ -0,0 +1,258 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Types used for writing dwarf debug information *)
+
+(* Basic types for the value of attributes *)
+
+type constant = int
+
+type flag = bool
+
+type reference = int
+
+type encoding =
+ | DW_ATE_address
+ | DW_ATE_boolean
+ | DW_ATE_complex_float
+ | DW_ATE_float
+ | DW_ATE_signed
+ | DW_ATE_signed_char
+ | DW_ATE_unsigned
+ | DW_ATE_unsigned_char
+
+type address = int
+
+type block = string
+
+type location_value =
+ | LocConst of constant
+ | LocBlock of block
+
+type data_location_value =
+ | DataLocBlock of block
+ | DataLocRef of reference
+
+type bound_value =
+ | BoundConst of constant
+ | BoundRef of reference
+
+(* Types representing the attribute information per tag value *)
+
+type file_loc = string * constant
+
+type dw_tag_array_type =
+ {
+ array_type_file_loc: file_loc option;
+ array_type: reference;
+ }
+
+type dw_tag_base_type =
+ {
+ base_type_byte_size: constant;
+ base_type_encoding: encoding;
+ base_type_name: string;
+ }
+
+type dw_tag_compile_unit =
+ {
+ compile_unit_name: string;
+ }
+
+type dw_tag_const_type =
+ {
+ const_type: reference;
+ }
+
+type dw_tag_enumeration_type =
+ {
+ enumeration_file_loc: file_loc option;
+ enumeration_byte_size: constant;
+ enumeration_declaration: flag option;
+ enumeration_name: string;
+ }
+
+type dw_tag_enumerator =
+ {
+ enumerator_file_loc: file_loc option;
+ enumerator_value: constant;
+ enumerator_name: string;
+ }
+
+type dw_tag_formal_parameter =
+ {
+ formal_parameter_file_loc: file_loc option;
+ formal_parameter_artificial: flag option;
+ formal_parameter_location: location_value option;
+ formal_parameter_name: string;
+ formal_parameter_segment: location_value option;
+ formal_parameter_type: reference;
+ formal_parameter_variable_parameter: flag option;
+ }
+
+type dw_tag_label =
+ {
+ label_low_pc: address;
+ label_name: string;
+ }
+
+type dw_tag_lexical_block =
+ {
+ lexical_block_high_pc: address;
+ lexical_block_low_pc: address;
+ }
+
+type dw_tag_member =
+ {
+ member_file_loc: file_loc option;
+ member_byte_size: constant option;
+ member_bit_offset: constant option;
+ member_bit_size: constant option;
+ member_data_member_location: data_location_value option;
+ member_declaration: flag option;
+ member_name: string;
+ member_type: reference;
+ }
+
+type dw_tag_pointer_type =
+ {
+ pointer_type: reference;
+ }
+
+type dw_tag_structure_type =
+ {
+ structure_file_loc: file_loc option;
+ structure_byte_size: constant;
+ structure_declaration: flag option;
+ structure_name: string;
+ }
+
+type dw_tag_subprogram =
+ {
+ subprogram_file_loc: file_loc option;
+ subprogram_external: flag option;
+ subprogram_frame_base: location_value option;
+ subprogram_high_pc: address;
+ subprogram_low_pc: address;
+ subprogram_name: string;
+ subprogram_prototyped: flag;
+ subprogram_type: reference;
+ }
+
+type dw_tag_subrange_type =
+ {
+ subrange_type: reference option;
+ subrange_upper_bound: bound_value;
+ }
+
+type dw_tag_subroutine_type =
+ {
+ subroutine_prototyped: flag;
+ }
+
+type dw_tag_typedef =
+ {
+ typedef_file_loc: file_loc option;
+ typedef_name: string;
+ typedef_type: reference;
+ }
+
+type dw_tag_union_type =
+ {
+ union_file_loc: file_loc option;
+ union_byte_size: constant;
+ union_name: string;
+ }
+
+type dw_tag_unspecified_parameter =
+ {
+ unspecified_parameter_file_loc: file_loc option;
+ unspecified_parameter_artificial: flag option;
+ }
+
+type dw_tag_variable =
+ {
+ variable_file_loc: file_loc option;
+ variable_declaration: flag option;
+ variable_external: flag option;
+ variable_location: location_value option;
+ variable_name: string;
+ variable_segment: location_value option;
+ variable_type: reference;
+ }
+
+type dw_tag_volatile_type =
+ {
+ volatile_type: reference;
+ }
+
+type dw_tag =
+ | DW_TAG_array_type of dw_tag_array_type
+ | DW_TAG_base_type of dw_tag_base_type
+ | DW_TAG_compile_unit of dw_tag_compile_unit
+ | DW_TAG_const_type of dw_tag_const_type
+ | DW_TAG_enumeration_type of dw_tag_enumeration_type
+ | DW_TAG_enumerator of dw_tag_enumerator
+ | DW_TAG_formal_parameter of dw_tag_formal_parameter
+ | DW_TAG_label of dw_tag_label
+ | DW_TAG_lexical_block of dw_tag_lexical_block
+ | DW_TAG_member of dw_tag_member
+ | DW_TAG_pointer_type of dw_tag_pointer_type
+ | DW_TAG_structure_type of dw_tag_structure_type
+ | DW_TAG_subprogram of dw_tag_subprogram
+ | DW_TAG_subrange_type of dw_tag_subrange_type
+ | DW_TAG_subroutine_type of dw_tag_subroutine_type
+ | DW_TAG_typedef of dw_tag_typedef
+ | DW_TAG_union_type of dw_tag_union_type
+ | DW_TAG_unspecified_parameter of dw_tag_unspecified_parameter
+ | DW_TAG_variable of dw_tag_variable
+ | DW_TAG_volatile_type of dw_tag_volatile_type
+
+(* The type of the entries. *)
+
+type dw_entry =
+ {
+ tag: dw_tag;
+ children: dw_entry list;
+ id: reference;
+ }
+
+
+module type DWARF_ABBREVS =
+ sig
+ val sibling_type_abbr: int
+ val file_loc_type_abbr: int * int
+ val type_abbr: int
+ val name_type_abbr: int
+ val encoding_type_abbr: int
+ val byte_size_type_abbr: int
+ val high_pc_type_abbr: int
+ val low_pc_type_abbr: int
+ val stmt_list_type_abbr: int
+ val declaration_type_abbr: int
+ val external_type_abbr: int
+ val prototyped_type_abbr: int
+ val bit_offset_type_abbr: int
+ val comp_dir_type_abbr: int
+ val language_type_abbr: int
+ val producer_type_abbr: int
+ val value_type_abbr: int
+ val artificial_type_abbr: int
+ val variable_parameter_type_abbr: int
+ val bit_size_type_abbr: int
+ val location_const_type_abbr: int
+ val location_block_type_abbr: int
+ val data_location_block_type_abbr: int
+ val data_location_ref_type_abbr: int
+ val bound_const_type_abbr: int
+ val bound_ref_type_abbr: int
+ end
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
new file mode 100644
index 00000000..b3cef748
--- /dev/null
+++ b/debug/DwarfUtil.ml
@@ -0,0 +1,118 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Utility functions for the dwarf debuging type *)
+
+open DwarfTypes
+
+let id = ref 0
+
+let next_id () =
+ let nid = !id in
+ incr id; nid
+
+let reset_id () =
+ id := 0
+
+(* Hashtable to from type name to entry id *)
+let type_table: (string, int) Hashtbl.t = Hashtbl.create 7
+
+(* Clear the type map *)
+let reset_type_table () =
+ Hashtbl.clear type_table
+
+(* Generate a new entry from a given tag *)
+let new_entry tag =
+ let id = next_id () in
+ {
+ tag = tag;
+ children = [];
+ id = id;
+ }
+
+(* Add an entry as child to another entry *)
+let add_children entry child =
+ {entry with children = child::entry.children;}
+
+
+let list_iter_with_next f list =
+ let rec aux = (function
+ | [] -> ()
+ | [a] -> f None a
+ | a::b::rest -> f (Some b.id) a; aux (b::rest)) in
+ aux list
+
+(* Iter over the tree and pass the sibling id *)
+let entry_iter_sib f entry =
+ let rec aux sib entry =
+ f sib entry;
+ list_iter_with_next aux entry.children in
+ aux None entry
+
+
+(* Fold over the tree in prefix order *)
+let rec entry_fold f acc entry =
+ let acc = f acc entry.tag in
+ List.fold_left (entry_fold f) acc entry.children
+
+(* Attribute form encoding *)
+let dw_form_addr = 0x01
+let dw_form_block2 = 0x03
+let dw_form_block4 = 0x04
+let dw_form_data2 = 0x05
+let dw_form_data4 = 0x06
+let dw_form_data8 = 0x07
+let dw_form_string = 0x08
+let dw_form_block = 0x09
+let dw_form_block1 = 0x0a
+let dw_form_data1 = 0x0b
+let dw_form_flag = 0x0c
+let dw_form_sdata = 0x0d
+let dw_form_strp = 0x0e
+let dw_form_udata = 0x0f
+let dw_form_ref_addr = 0x10
+let dw_form_ref1 = 0x11
+let dw_form_ref2 = 0x12
+let dw_form_ref4 = 0x13
+let dw_form_ref8 = 0x14
+let dw_ref_udata = 0x15
+let dw_ref_indirect = 0x16
+
+module DefaultAbbrevs =
+ struct
+ let sibling_type_abbr = dw_form_ref4
+ let file_loc_type_abbr = dw_form_data4,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
generated by cgit (git 2.34.1) at 2024-07-18 07:23:28 +0000