diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | debug/DwarfTypes.ml | 277 | ||||
| -rw-r--r-- | debug/DwarfUtil.ml | 71 |
3 files changed, 349 insertions, 1 deletions
@@ -15,7 +15,7 @@ include Makefile.config -DIRS=lib common $(ARCH) backend cfrontend driver \ +DIRS=lib common $(ARCH) backend cfrontend driver debug\ flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ cparser cparser/validator diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml new file mode 100644 index 00000000..70d31ef8 --- /dev/null +++ b/debug/DwarfTypes.ml @@ -0,0 +1,277 @@ +(* *********************************************************************) +(* *) +(* 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 identifier_case = + | DW_ID_case_sensitive + | DW_ID_up_case + | DW_ID_down_case + | DW_ID_case_insensitive + +type address = int + +type language = + | DW_LANG_C + | DW_LANG_C89 + +type block = string (* Used as bitvector *) + +type calling_convention = + | DW_CC_normal + | DW_CC_program + | DW_CC_nocall + | DW_CC_lo_user + | DW_CC_hi_user + +type inline = + | DW_INL_not_inlined + | DW_INL_inlined + | DW_INL_declared_not_inlined + | DW_INL_declared_inlined + +type const_value = + | String of string + | Const of constant + | Block of block + +type location_value = + | Const of constant + | Block of block + +type data_location_value = + | Block of block + | Ref of reference + +type bound_value = + | Const of constant + | Ref of reference + +(* Types representing the attribute information per tag value *) + +type dw_tag_array_type = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_type: reference; + } + +type dw_tag_base_type = + { + dw_at_byte_size: constant; + dw_at_encoding: encoding; + dw_at_name: string; + } + +type dw_tag_compile_unit = + { + dw_at_base_types: reference option; + dw_at_comp_dir: string; + dw_at_identifier_case: identifier_case option; + dw_at_high_pc: address; + dw_at_language: language; + dw_at_low_pc: address; + dw_at_macro_info: constant option; + dw_at_name: string; + dw_at_producer: string; + dw_at_stmt_list: constant option; + } + +type dw_tag_const_type = + { + dw_at_type: reference; + } + +type dw_tag_enumeration_type = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_byte_size: constant; + dw_at_declaration: flag option; + dw_at_name: string; + dw_at_start_scope: constant option; + } + +type dw_tag_enumerator = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_const_value: constant; + dw_at_name: string; + } + +type dw_tag_formal_parameter = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_artificial: flag option; + dw_at_location: location_value option; + dw_at_name: string; + dw_at_segment: location_value option; + dw_at_type: reference; + dw_at_variable_parameter: flag option; + } + +type dw_tag_label = + { + dw_at_low_pc: address; + dw_at_name: string; + } + +type dw_tag_lexical_block = + { + dw_at_high_pc: address; + dw_at_low_pc: address; + } + +type dw_tag_member = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_byte_size: constant option; + dw_at_bit_offset: constant option; + dw_at_bit_size: constant option; + dw_at_data_member_location: data_location_value option; + dw_at_declaration: flag option; + dw_at_name: string; + dw_at_type: reference; + } + +type dw_tag_pointer_type = + { + dw_at_type: reference; + } + +type dw_tag_structure_type = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_byte_size: constant; + dw_at_declaration: flag option; + dw_at_name: string; + } + +type dw_tag_subprogram = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_external: flag option; + dw_at_frame_base: location_value option; + dw_at_high_pc: address; + dw_at_inline: inline option; + dw_at_low_pc: address; + dw_at_name: string; + dw_at_prototyped: flag; + dw_at_type: reference; + } + +type dw_tag_subrange_type = + { + dw_at_type: reference option; + dw_at_upper_bound: bound_value; + } + +type dw_tag_subroutine_type = + { + dw_at_prototyped: flag; + } + +type dw_tag_typedef = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_name: string; + dw_at_type: reference; + } + +type dw_tag_union_type = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_byte_size: constant; + dw_at_name: string; + } + +type dw_tag_unspecified_parameter = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_artificial: flag option; + } + +type dw_tag_variable = + { + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; + dw_at_declaration: flag option; + dw_at_external: flag option; + dw_at_location: location_value option; + dw_at_name: string; + dw_at_segment: location_value option; + dw_at_type: reference; + } + +type dw_tag_volatile_type = + { + dw_at_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_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; + } + + diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml new file mode 100644 index 00000000..ec5495c1 --- /dev/null +++ b/debug/DwarfUtil.ml @@ -0,0 +1,71 @@ +(* *********************************************************************) +(* *) +(* 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 + +(* 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;} + + +(* Iter over the tree in prefix order *) +let rec entry_iter f entry = + f entry.tag; + List.iter (entry_iter f) entry.children + +(* Iter over the tree in prefix order with passing additional reference to next sibling *) +let entry_iter_sibling f acc entry = + f None entry.tag; + let rec aux = (function + | [] -> () + | [last] -> f None last.tag + | a::b::rest -> f (Some b.id) a.tag; aux (b::rest)) in + aux entry.children + + +(* 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 + +(* Fold over the tree in prefix order with passing additional reference to next sibling *) +let entry_fold_sibling f acc entry = + let acc = f acc None entry.tag in + let rec aux acc = (function + | [] -> acc + | [last] -> f acc None last.tag + | a::b::rest -> aux (f acc (Some b.id) a.tag) (b::rest)) in + aux acc entry.children |