diff options
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/Debug.ml | 5 | ||||
| -rw-r--r-- | debug/Debug.mli | 2 | ||||
| -rw-r--r-- | debug/DebugInformation.ml | 66 | ||||
| -rw-r--r-- | debug/DebugInformation.mli | 106 | ||||
| -rw-r--r-- | debug/DebugInit.ml | 8 | ||||
| -rw-r--r-- | debug/DebugTypes.mli | 20 | ||||
| -rw-r--r-- | debug/DwarfPrinter.ml | 11 | ||||
| -rw-r--r-- | debug/DwarfTypes.mli | 3 | ||||
| -rw-r--r-- | debug/Dwarfgen.ml | 52 |
9 files changed, 195 insertions, 78 deletions
diff --git a/debug/Debug.ml b/debug/Debug.ml index 775a0903..7403d7c2 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -12,9 +12,8 @@ open AST open BinNums -open C +open !C open Camlcoq -open Dwarfgen open DwarfTypes open Sections @@ -32,7 +31,7 @@ type implem = add_fun_addr: atom -> section_name -> (int * int) -> unit; generate_debug_info: (atom -> string) -> string -> debug_entries option; all_files_iter: (string -> unit) -> unit; - insert_local_declaration: storage -> ident -> typ -> location -> unit; + insert_local_declaration: storage -> ident -> C.typ -> location -> unit; atom_local_variable: ident -> atom -> unit; enter_scope: int -> int -> int -> unit; enter_function_scope: int -> int -> unit; diff --git a/debug/Debug.mli b/debug/Debug.mli index 387491c2..f044b1ad 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -11,7 +11,7 @@ (* *********************************************************************) open AST -open C +open !C open Camlcoq open DwarfTypes open BinNums diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 105b6aad..471318af 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -10,7 +10,6 @@ (* *) (* *********************************************************************) -open AST open BinNums open C open Camlcoq @@ -28,8 +27,6 @@ let next_id () = let nid = !id in incr id; nid -let reset_id () = - id := 0 (* Auximilary functions *) let list_replace c f l = @@ -47,11 +44,15 @@ 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 (* Translate a C.typ to a string needed for hashing *) -let typ_to_string (ty: typ) = +let typ_to_string ty = let buf = Buffer.create 7 in let chan = Format.formatter_of_buffer buf in Cprint.print_debug_idents := true; @@ -64,13 +65,13 @@ let typ_to_string (ty: typ) = let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile] (* Find the type id to an type *) -let find_type (ty: typ) = +let find_type ty = (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in Hashtbl.find lookup_types (typ_to_string ty) (* Add type and information *) -let insert_type (ty: typ) = +let insert_type ty = let insert d_ty ty = let id = next_id () and name = typ_to_string ty in @@ -104,7 +105,7 @@ let insert_type (ty: typ) = arr_size= s; } in ArrayType arr - | TFun (t,param,va,_) -> + | TFun (t,param,_,_) -> let param,prot = (match param with | None -> [],false | Some p -> List.map (fun (i,t) -> let t = attr_aux t in @@ -213,6 +214,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 +258,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 +521,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,20 +583,22 @@ 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" -let add_compilation_section_start sec addr = - let sec = section_to_string sec in - Hashtbl.add compilation_section_start sec addr - -let add_compilation_section_end sec addr = - let sec = section_to_string sec in - Hashtbl.add compilation_section_end sec addr - let add_diab_info sec addr1 add2 addr3 = let sec' = section_to_string sec in Hashtbl.add compilation_section_start sec' addr3; @@ -622,6 +618,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 +631,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 17a90536..462ca2d3 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -10,12 +10,6 @@ (* *) (* *********************************************************************) -open AST -open BinNums -open C -open Camlcoq -open Dwarfgen -open DwarfTypes open Debug let default_debug = @@ -28,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/DwarfPrinter.ml b/debug/DwarfPrinter.ml index ef44a2d5..9313b6c5 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -33,9 +33,6 @@ module DwarfPrinter(Target: DWARF_TARGET): let string_of_comment s = sprintf " %s %s" comment s - let add_comment buf s = - Buffer.add_string buf (sprintf " %s %s" comment s) - (* Byte value to string *) let string_of_byte value ct = sprintf " .byte %s%s\n" (if value then "0x1" else "0x0") (string_of_comment ct) @@ -67,8 +64,6 @@ module DwarfPrinter(Target: DWARF_TARGET): let add_member_size = add_abbr_entry (0x0b,"DW_AT_byte_size",DW_FORM_udata) - let add_high_pc = add_abbr_entry (0x12,"DW_AT_high_pc",DW_FORM_addr) - let add_low_pc = add_abbr_entry (0x11,"DW_AT_low_pc",DW_FORM_addr) let add_declaration = add_abbr_entry (0x3c,"DW_AT_declaration",DW_FORM_flag) @@ -115,7 +110,7 @@ module DwarfPrinter(Target: DWARF_TARGET): if has_sibling then add_abbr_entry (0x1,"DW_AT_sibling",DW_FORM_ref4) buf; in (match entity.tag with - | DW_TAG_array_type e -> + | DW_TAG_array_type _ -> prologue 0x1 "DW_TAG_array_type"; add_type buf | DW_TAG_base_type b -> @@ -623,9 +618,9 @@ module DwarfPrinter(Target: DWARF_TARGET): let name = if e.section_name <> ".text" then Some e.section_name else None in section oc (Section_debug_info name); print_debug_info oc e.start_label e.line_label e.entry) entries; - if List.exists (fun e -> match e.locs with _,[] -> false | _,_ -> true) entries then begin + if List.exists (fun e -> match e.dlocs with _,[] -> false | _,_ -> true) entries then begin section oc Section_debug_loc; - List.iter (fun e -> print_location_list oc e.locs) entries + List.iter (fun e -> print_location_list oc e.dlocs) entries end let print_ranges oc r = diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index 2af64c0b..f6074cf3 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -12,7 +12,6 @@ (* Types used for writing dwarf debug information *) -open BinNums open Camlcoq open Sections @@ -285,7 +284,7 @@ type diab_entry = start_label: int; line_label: int; entry: dw_entry; - locs: dw_locations; + dlocs: dw_locations; } type diab_entries = diab_entry list diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index d070e3a9..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); @@ -534,16 +536,16 @@ let diab_gen_compilation_section s defs acc = start_label = debug_start; line_label = line_start; entry = cp; - locs = Some low_pc,accu.locs; + dlocs = Some low_pc,accu.locs; }::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; |