diff options
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DebugInformation.ml | 48 | ||||
| -rw-r--r-- | debug/DebugInformation.mli | 106 | ||||
| -rw-r--r-- | debug/DebugInit.ml | 2 | ||||
| -rw-r--r-- | debug/DebugTypes.mli | 20 | ||||
| -rw-r--r-- | debug/Dwarfgen.ml | 50 |
5 files changed, 183 insertions, 43 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index e8f1703a..828759a7 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -10,7 +10,6 @@ (* *) (* *********************************************************************) -open AST open BinNums open C open Camlcoq @@ -47,6 +46,10 @@ let add_file file = (* All types encountered *) let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7 +let get_type = Hashtbl.find types + +let fold_types f a = Hashtbl.fold f types a + (* Lookup table for types *) let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7 @@ -213,6 +216,8 @@ let replace_typedef id f = (* All global definitions encountered *) let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7 +let fold_definitions f a = Hashtbl.fold f definitions a + (* Mapping from stamp to debug id *) let stamp_to_definition: (int,int) Hashtbl.t = Hashtbl.create 7 @@ -255,6 +260,8 @@ let replace_fun id f = (* All local variables *) let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7 +let get_local_variable id = Hashtbl.find local_variables id + (* Mapping from stamp to the debug id of the local variable *) let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7 @@ -516,29 +523,18 @@ let enter_scope f_id p_id id = with Not_found -> () -type scope_range = - { - start_addr: positive option; - end_addr: positive option; - } - -type var_range = - { - range_start: positive option; - range_end: positive option; - var_loc: int * int builtin_arg; - } - -type var_location = - | RangeLoc of var_range list - | FunctionLoc of int * int builtin_arg (* Stack allocated variables *) - let var_locations: (atom * atom,var_location) Hashtbl.t = Hashtbl.create 7 +let variable_location var f = Hashtbl.find var_locations (var,f) + let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7 +let get_scope_ranges = Hashtbl.find scope_ranges + let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7 +let translate_label f l = Hashtbl.find label_translation (f,l) + let add_label atom p i = Hashtbl.add label_translation (atom,p) i @@ -589,8 +585,18 @@ let stack_variable (f,v) (sp,loc) = let compilation_section_start: (string,int) Hashtbl.t = Hashtbl.create 7 let compilation_section_end: (string,int) Hashtbl.t = Hashtbl.create 7 +let section_start n = Hashtbl.find compilation_section_start n + +let fold_section_start f a = Hashtbl.fold f compilation_section_start a + +let section_end n = Hashtbl.find compilation_section_end n + let diab_additional: (string,int * int * section_name) Hashtbl.t = Hashtbl.create 7 +let diab_additional_section s = + let line_start,debug_start,_ = Hashtbl.find diab_additional s in + line_start,debug_start + let section_to_string = function | Section_user (n,_,_) -> n | _ -> ".text" @@ -622,6 +628,8 @@ let exists_section sec = let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7 +let diab_file_loc f l = Hashtbl.find filenum (f,l) + let compute_diab_file_enum end_label entry_label line_end = Hashtbl.iter (fun sec (_,_,secname) -> Hashtbl.add compilation_section_end sec (end_label secname); @@ -633,8 +641,12 @@ let compute_diab_file_enum end_label entry_label line_end = let compute_gnu_file_enum f = StringSet.iter f !all_files +let all_files_iter f = StringSet.iter f !all_files + let printed_vars: StringSet.t ref = ref StringSet.empty +let is_variable_printed id = StringSet.mem id !printed_vars + let variable_printed id = printed_vars := StringSet.add id !printed_vars diff --git a/debug/DebugInformation.mli b/debug/DebugInformation.mli new file mode 100644 index 00000000..66c4cd11 --- /dev/null +++ b/debug/DebugInformation.mli @@ -0,0 +1,106 @@ +(* *********************************************************************) +(* *) +(* 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 AST +open BinNums +open !C +open Camlcoq +open DebugTypes +open Sections + +val typ_to_string: C.typ -> string + +val next_id: unit -> int + +val get_type: int -> debug_types + +val fold_types: (int -> debug_types -> 'a -> 'a) -> 'a -> 'a + +val is_variable_printed: string -> bool + +val variable_location: atom -> atom -> var_location + +val translate_label: atom -> positive -> int + +val get_scope_ranges: int -> scope_range list + +val get_local_variable: int -> local_information + +val diab_file_loc: string -> string -> int + +val section_start: string -> int + +val fold_section_start: (string -> int -> 'a -> 'a) -> 'a -> 'a + +val section_end: string -> int + +val diab_additional_section: string -> int * int + +val file_name: string ref + +val fold_definitions: (int -> definition_type -> 'a -> 'a) -> 'a -> 'a + +val atom_global: ident -> atom -> unit + +val set_composite_size: ident -> struct_or_union -> int option -> unit + +val set_member_offset: ident -> string -> int -> unit + +val set_bitfield_offset: ident -> string -> int -> string -> int -> unit + +val insert_global_declaration: Env.t -> globdecl -> unit + +val diab_add_fun_addr: atom -> section_name -> (int * int) -> unit + +val gnu_add_fun_addr: atom -> section_name -> (int * int) -> unit + +val all_files_iter: (string -> unit) -> unit + +val insert_local_declaration: storage -> ident -> typ -> location -> unit + +val atom_local_variable: ident -> atom -> unit + +val enter_scope: int -> int -> int -> unit + +val enter_function_scope: int -> int -> unit + +val add_lvar_scope: int -> ident -> int -> unit + +val open_scope: atom -> int -> positive -> unit + +val close_scope: atom -> int -> positive -> unit + +val start_live_range: (atom * atom) -> positive -> (int * int builtin_arg) -> unit + +val end_live_range: (atom * atom) -> positive -> unit + +val stack_variable: (atom * atom) -> int * int builtin_arg -> unit + +val add_label: atom -> positive -> int -> unit + +val atom_parameter: ident -> ident -> atom -> unit + +val compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit + +val compute_gnu_file_enum: (string -> unit) -> unit + +val exists_section: section_name -> bool + +val remove_unused: ident -> unit + +val remove_unused_function: ident -> unit + +val variable_printed: string -> unit + +val add_diab_info: section_name -> int -> int -> int -> unit + +val init: string -> unit diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 24712b27..462ca2d3 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -22,7 +22,7 @@ let default_debug = insert_global_declaration = DebugInformation.insert_global_declaration; add_fun_addr = (fun _ _ _ -> ()); generate_debug_info = (fun _ _ -> None); - all_files_iter = (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files); + all_files_iter = DebugInformation.all_files_iter; insert_local_declaration = DebugInformation.insert_local_declaration; atom_local_variable = DebugInformation.atom_local_variable; enter_scope = DebugInformation.enter_scope; diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli index 53a39665..25c7390f 100644 --- a/debug/DebugTypes.mli +++ b/debug/DebugTypes.mli @@ -10,6 +10,8 @@ (* *) (* *********************************************************************) +open AST +open BinNums open C open Camlcoq @@ -158,3 +160,21 @@ type scope_information = type local_information = | LocalVariable of local_variable_information | Scope of scope_information + + +type scope_range = + { + start_addr: positive option; + end_addr: positive option; + } + +type var_range = + { + range_start: positive option; + range_end: positive option; + var_loc: int * int builtin_arg; + } + +type var_location = + | RangeLoc of var_range list + | FunctionLoc of int * int builtin_arg (* Stack allocated variables *) diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index fe0764e8..f1a8ce3e 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -21,6 +21,8 @@ open DwarfUtil (* Generate the dwarf DIE's from the information collected in DebugInformation *) +module StringSet = Set.Make(String) + (* Helper function to get values that must be set. *) let get_opt_val = function | Some a -> a @@ -270,7 +272,7 @@ module Dwarfgenaux (Target: TARGET) = IntSet.add id d,true else d,false in - let t = Hashtbl.find types id in + let t = get_type id in match t with | IntegerType _ | FloatType _ @@ -308,15 +310,15 @@ module Dwarfgenaux (Target: TARGET) = else d in let typs = aux needed in - List.rev (Hashtbl.fold (fun id t acc -> + List.rev (fold_types (fun id t acc -> if IntSet.mem id typs then (infotype_to_entry id t)::acc else - acc) types []) + acc) []) let global_variable_to_entry acc id v = let loc = match v.gvar_atom with - | Some a when StringSet.mem (extern_atom a) !printed_vars -> + | Some a when is_variable_printed (extern_atom a) -> Some (LocSymbol a) | _ -> None in let var = { @@ -369,15 +371,15 @@ module Dwarfgenaux (Target: TARGET) = if !Clflags.option_gdepth > 2 then try begin - match (Hashtbl.find var_locations (f_id,atom)) with + match variable_location f_id atom with | FunctionLoc (a,r) -> translate_function_loc a r | RangeLoc l -> let l = List.rev_map (fun i -> let hi = get_opt_val i.range_start and lo = get_opt_val i.range_end in - let hi = Hashtbl.find label_translation (f_id,hi) - and lo = Hashtbl.find label_translation (f_id,lo) in + let hi = translate_label f_id hi + and lo = translate_label f_id lo in hi,lo,range_entry_loc i.var_loc) l in let id = next_id () in Some (LocRef id),[{loc = l;loc_id = id;}] @@ -402,11 +404,11 @@ module Dwarfgenaux (Target: TARGET) = let scope_range f_id id (o,dwr) = try - let r = Hashtbl.find scope_ranges id in + let r = get_scope_ranges id in let lbl l h = match l,h with | Some l,Some h-> - let l = (Hashtbl.find label_translation (f_id,l)) - and h = (Hashtbl.find label_translation (f_id,h)) in + let l = translate_label f_id l + and h = translate_label f_id h in l,h | _ -> raise Not_found in begin @@ -451,7 +453,7 @@ module Dwarfgenaux (Target: TARGET) = add_children entry vars,(acc >>= dwr) and local_to_entry f_id acc id = - match Hashtbl.find local_variables id with + match get_local_variable id with | LocalVariable v -> local_variable_to_entry f_id acc v id | Scope v -> let s,acc = (scope_to_entry f_id acc v id) in Some s,acc @@ -460,7 +462,7 @@ module Dwarfgenaux (Target: TARGET) = match id with | None -> [],acc | Some id -> - let sc = Hashtbl.find local_variables id in + let sc = get_local_variable id in (match sc with | Scope sc -> mmap_opt (local_to_entry f_id) acc sc.scope_variables | _ -> assert false) @@ -499,7 +501,7 @@ module Dwarfgenaux (Target: TARGET) = module StringMap = Map.Make(String) let diab_file_loc sec (f,l) = - Diab_file_loc (Hashtbl.find filenum (sec,f),l) + Diab_file_loc ((diab_file_loc sec f),l) let prod_name = let version_string = @@ -518,9 +520,9 @@ let diab_gen_compilation_section s defs acc = let defs,accu = List.fold_left (fun (acc,bcc) (id,t) -> let t,bcc = Gen.definition_to_entry bcc id t in t::acc,bcc) ([],empty_accu) defs in - let low_pc = Hashtbl.find compilation_section_start s - and line_start,debug_start,_ = Hashtbl.find diab_additional s - and high_pc = Hashtbl.find compilation_section_end s in + let low_pc = section_start s + and line_start,debug_start = diab_additional_section s + and high_pc = section_end s in let cp = { compile_unit_name = Simple_string !file_name; compile_unit_range = Pc_pair (low_pc,high_pc); @@ -538,12 +540,12 @@ let diab_gen_compilation_section s defs acc = }::acc let gen_diab_debug_info sec_name var_section : debug_entries = - let defs = Hashtbl.fold (fun id t acc -> + let defs = fold_definitions (fun id t acc -> let s = match t with | GlobalVariable _ -> var_section | Function f -> sec_name (get_opt_val f.fun_atom) in let old = try StringMap.find s acc with Not_found -> [] in - StringMap.add s ((id,t)::old) acc) definitions StringMap.empty in + StringMap.add s ((id,t)::old) acc) StringMap.empty in let entries = StringMap.fold diab_gen_compilation_section defs [] in Diab entries @@ -567,15 +569,15 @@ let gnu_string_entry s = let gen_gnu_debug_info sec_name var_section : debug_entries = let r,dwr,low_pc = try if !Clflags.option_gdwarf > 3 then - let pcs = Hashtbl.fold (fun s low acc -> - (low,Hashtbl.find compilation_section_end s)::acc) compilation_section_start [] in + let pcs = fold_section_start (fun s low acc -> + (low,section_end s)::acc) [] in match pcs with | [] -> Empty,(0,[]),None | [(l,h)] -> Pc_pair (l,h),(0,[]),Some l | _ -> Offset 0,(2 + 4 * (List.length pcs),[pcs]),None else - let l = Hashtbl.find compilation_section_start ".text" - and h = Hashtbl.find compilation_section_end ".text" in + let l = section_start ".text" + and h = section_end ".text" in Pc_pair(l,h),(0,[]),Some l with Not_found -> Empty,(0,[]),None in let accu = empty_accu >>= dwr in @@ -583,12 +585,12 @@ let gen_gnu_debug_info sec_name var_section : debug_entries = let file_loc = gnu_file_loc let string_entry = gnu_string_entry end) in - let defs,accu,sec = Hashtbl.fold (fun id t (acc,bcc,sec) -> + let defs,accu,sec = fold_definitions (fun id t (acc,bcc,sec) -> let s = match t with | GlobalVariable _ -> var_section | Function f -> sec_name (get_opt_val f.fun_atom) in let t,bcc = Gen.definition_to_entry bcc id t in - t::acc,bcc,StringSet.add s sec) definitions ([],accu,StringSet.empty) in + t::acc,bcc,StringSet.add s sec) ([],accu,StringSet.empty) in let types = Gen.gen_types accu.typs in let cp = { compile_unit_name = gnu_string_entry !file_name; |