diff options
-rw-r--r-- | debug/DebugInformation.ml | 147 | ||||
-rw-r--r-- | debug/DebugTypes.mli | 160 | ||||
-rw-r--r-- | debug/Dwarfgen.ml | 2 |
3 files changed, 163 insertions, 146 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 1fe1a805..40cc4060 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -15,6 +15,7 @@ open BinNums open C open Camlcoq open Cutil +open DebugTypes (* This implements an interface for the collection of debugging information. *) @@ -42,96 +43,6 @@ let all_files : StringSet.t ref = ref StringSet.empty let add_file file = all_files := StringSet.add file !all_files -(* Types for the information of type info *) -type composite_field = - { - cfd_name: string; - cfd_typ: int; - cfd_bit_size: int option; - cfd_bit_offset: int option; - cfd_byte_offset: int option; - cfd_byte_size: int option; - cfd_bitfield: string option; - } - -type composite_type = - { - ct_name: string; - ct_sou: struct_or_union; - ct_file_loc: location option; - ct_members: composite_field list; - ct_sizeof: int option; - ct_declaration: bool; - } - -type ptr_type = { - pts: int - } - -type const_type = { - cst_type: int - } - -type volatile_type = { - vol_type: int - } - - -type array_type = { - arr_type: int; - arr_size: int64 option list; - } - -type typedef = { - typedef_file_loc: location option; - typedef_name: string; - typ: int option; - } - -type enumerator = { - enumerator_name: string; - enumerator_const: int64; - } - -type enum_type = { - enum_name: string; - enum_byte_size: int option; - enum_file_loc: location option; - enum_enumerators: enumerator list; - } - -type int_type = { - int_kind: ikind; - } - -type float_type = { - float_kind: fkind; - } - -type parameter_type = { - param_type: int; - param_name: string; - } - -type function_type = { - fun_return_type: int option; - fun_prototyped: bool; - fun_params: parameter_type list; - } - -type debug_types = - | IntegerType of int_type - | FloatType of float_type - | PointerType of ptr_type - | ArrayType of array_type - | CompositeType of composite_type - | EnumType of enum_type - | FunctionType of function_type - | Typedef of typedef - | ConstType of const_type - | VolatileType of volatile_type - | Void - (* All types encountered *) let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7 @@ -343,43 +254,6 @@ let replace_typedef id f = if typ <> typ' then Hashtbl.replace types id (Typedef typ') | _ -> assert false (* This should never happen *) -(* Types for global definitions *) - -(* Information for a global variable *) -type global_variable_information = { - gvar_name: string; - gvar_atom: atom option; - gvar_file_loc: location; - gvar_declaration: bool; - gvar_external: bool; - gvar_type: int; - } - -type parameter_information = - { - parameter_name: string; - parameter_ident: int; - parameter_atom: atom option; - parameter_type: int; -} - -type function_information = { - fun_name: string; - fun_atom: atom option; - fun_file_loc: location; - fun_external: bool; - fun_return_type: int option; (* Again the special case of void functions *) - fun_vararg: bool; - fun_parameter: parameter_information list; - fun_low_pc: int option; - fun_high_pc: int option; - fun_scope: int option; - } - -type definition_type = - | GlobalVariable of global_variable_information - | Function of function_information - (* All global definitions encountered *) let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7 @@ -422,25 +296,6 @@ let replace_fun id f = let f = Function f in Hashtbl.replace definitions id f - -(* Information for local variables *) -type local_variable_information = { - lvar_name: string; - lvar_atom: atom option; - lvar_file_loc:location; - lvar_type: int; - lvar_static: bool; (* Static variable are mapped to symbols *) - } - -type scope_information = - { - scope_variables: int list; (* Variable and Scope ids *) - } - -type local_information = - | LocalVariable of local_variable_information - | Scope of scope_information - (* All local variables *) let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7 diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli new file mode 100644 index 00000000..6a4f619c --- /dev/null +++ b/debug/DebugTypes.mli @@ -0,0 +1,160 @@ +(* *********************************************************************) +(* *) +(* 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 C +open Camlcoq + +(* Types for the information of type info *) +type composite_field = + { + cfd_name: string; + cfd_typ: int; + cfd_bit_size: int option; + cfd_bit_offset: int option; + cfd_byte_offset: int option; + cfd_byte_size: int option; + cfd_bitfield: string option; + } + +type composite_type = + { + ct_name: string; + ct_sou: struct_or_union; + ct_file_loc: location option; + ct_members: composite_field list; + ct_sizeof: int option; + ct_declaration: bool; + } + +type ptr_type = { + pts: int + } + +type const_type = { + cst_type: int + } + +type volatile_type = { + vol_type: int + } + + +type array_type = { + arr_type: int; + arr_size: int64 option list; + } + +type typedef = { + typedef_file_loc: location option; + typedef_name: string; + typ: int option; + } + +type enumerator = { + enumerator_name: string; + enumerator_const: int64; + } + +type enum_type = { + enum_name: string; + enum_byte_size: int option; + enum_file_loc: location option; + enum_enumerators: enumerator list; + } + +type int_type = { + int_kind: ikind; + } + +type float_type = { + float_kind: fkind; + } + +type parameter_type = { + param_type: int; + param_name: string; + } + +type function_type = { + fun_return_type: int option; + fun_prototyped: bool; + fun_params: parameter_type list; + } + +type debug_types = + | IntegerType of int_type + | FloatType of float_type + | PointerType of ptr_type + | ArrayType of array_type + | CompositeType of composite_type + | EnumType of enum_type + | FunctionType of function_type + | Typedef of typedef + | ConstType of const_type + | VolatileType of volatile_type + | Void + +(* Types for global definitions *) + +(* Information for a global variable *) +type global_variable_information = { + gvar_name: string; + gvar_atom: atom option; + gvar_file_loc: location; + gvar_declaration: bool; + gvar_external: bool; + gvar_type: int; + } + +type parameter_information = + { + parameter_name: string; + parameter_ident: int; + parameter_atom: atom option; + parameter_type: int; +} + +type function_information = { + fun_name: string; + fun_atom: atom option; + fun_file_loc: location; + fun_external: bool; + fun_return_type: int option; (* Again the special case of void functions *) + fun_vararg: bool; + fun_parameter: parameter_information list; + fun_low_pc: int option; + fun_high_pc: int option; + fun_scope: int option; + } + +type definition_type = + | GlobalVariable of global_variable_information + | Function of function_information + + +(* Information for local variables *) +type local_variable_information = { + lvar_name: string; + lvar_atom: atom option; + lvar_file_loc:location; + lvar_type: int; + lvar_static: bool; (* Static variable are mapped to symbols *) + } + +type scope_information = + { + scope_variables: int list; (* Variable and Scope ids *) + } + +type local_information = + | LocalVariable of local_variable_information + | Scope of scope_information diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 6c79ce0c..1ef00c31 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -15,8 +15,10 @@ open C open Camlcoq open Cutil open DebugInformation +open DebugTypes open DwarfTypes open DwarfUtil + (* Generate the dwarf DIE's from the information collected in DebugInformation *) (* Helper function to get values that must be set. *) |