From aff813685455559f6d6a88158dd3d605893ba3a3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 25 Sep 2015 16:43:18 +0200 Subject: Added support for the locations of stack allocated local variables. This commit adds furher support for location information for local variables and starts with the implementation of the debug_loc section. --- debug/Debug.ml | 16 +++++++-- debug/Debug.mli | 8 +++-- debug/DebugInformation.ml | 88 +++++++++++++++++++++++++++++++++++++++++++---- debug/DwarfPrinter.ml | 75 +++++++++++++++++++++++++++++++--------- debug/DwarfPrinter.mli | 2 +- debug/DwarfTypes.mli | 26 +++++++++----- debug/DwarfUtil.ml | 9 ++++- debug/Dwarfgen.ml | 61 ++++++++++++++++++++++++-------- 8 files changed, 232 insertions(+), 53 deletions(-) (limited to 'debug') diff --git a/debug/Debug.ml b/debug/Debug.ml index fba921e1..7155ae0f 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -30,7 +30,7 @@ type implem = mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit; mutable insert_global_declaration: Env.t -> globdecl -> unit; mutable add_fun_addr: atom -> (int * int) -> unit; - mutable generate_debug_info: unit -> dw_entry option; + mutable generate_debug_info: unit -> (dw_entry * dw_locations) option; mutable all_files_iter: (string -> unit) -> unit; mutable insert_local_declaration: storage -> ident -> typ -> location -> unit; mutable atom_local_variable: ident -> atom -> unit; @@ -39,9 +39,11 @@ type implem = mutable add_lvar_scope: int -> ident -> int -> unit; mutable open_scope: atom -> int -> positive -> unit; mutable close_scope: atom -> int -> positive -> unit; - mutable start_live_range: atom -> positive -> string builtin_arg -> unit; + mutable start_live_range: atom -> positive -> int * int builtin_arg -> unit; mutable end_live_range: atom -> positive -> unit; - mutable stack_variable: atom -> string builtin_arg -> unit + mutable stack_variable: atom -> int * int builtin_arg -> unit; + mutable function_end: atom -> positive -> unit; + mutable add_label: atom -> positive -> int -> unit; } let implem = @@ -66,6 +68,8 @@ let implem = start_live_range = (fun _ _ _ -> ()); end_live_range = (fun _ _ -> ()); stack_variable = (fun _ _ -> ()); + function_end = (fun _ _ -> ()); + add_label = (fun _ _ _ -> ()); } let init () = @@ -90,6 +94,8 @@ let init () = implem.start_live_range <- DebugInformation.start_live_range; implem.end_live_range <- DebugInformation.end_live_range; implem.stack_variable <- DebugInformation.stack_variable; + implem.function_end <- DebugInformation.function_end; + implem.add_label <- DebugInformation.add_label; end else begin implem.init <- (fun _ -> ()); implem.atom_function <- (fun _ _ -> ()); @@ -111,6 +117,8 @@ let init () = implem.start_live_range <- (fun _ _ _ -> ()); implem.end_live_range <- (fun _ _ -> ()); implem.stack_variable <- (fun _ _ -> ()); + implem.function_end <- (fun _ _ -> ()); + implem.add_label <- (fun _ _ _ -> ()); end let init_compile_unit name = implem.init name @@ -133,3 +141,5 @@ let close_scope atom id lbl = implem.close_scope atom id lbl let start_live_range atom lbl loc = implem.start_live_range atom lbl loc let end_live_range atom lbl = implem.end_live_range atom lbl let stack_variable atom loc = implem.stack_variable atom loc +let function_end atom loc = implem.function_end atom loc +let add_label atom p lbl = implem.add_label atom p lbl diff --git a/debug/Debug.mli b/debug/Debug.mli index 42a0cee7..2954c300 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -26,7 +26,6 @@ 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 add_fun_addr: atom -> (int * int) -> unit -val generate_debug_info: unit -> dw_entry option val all_files_iter: (string -> unit) -> unit val insert_local_declaration: storage -> ident -> typ -> location -> unit val atom_local_variable: ident -> atom -> unit @@ -35,6 +34,9 @@ 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 -> positive -> string builtin_arg -> unit +val start_live_range: atom -> positive -> (int * int builtin_arg) -> unit val end_live_range: atom -> positive -> unit -val stack_variable: atom -> string builtin_arg -> unit +val stack_variable: atom -> int * int builtin_arg -> unit +val function_end: atom -> positive -> unit +val add_label: atom -> positive -> int -> unit +val generate_debug_info: unit -> (dw_entry * dw_locations) option diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index f12853c9..459c4e9d 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -10,6 +10,8 @@ (* *) (* *********************************************************************) +open AST +open BinNums open C open Camlcoq open Cutil @@ -659,20 +661,94 @@ let enter_scope f_id p_id id = replace_scope p_id' ({scope_variables = id'::scope.scope_variables;}) 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,var_location) Hashtbl.t = Hashtbl.create 7 + +let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7 + +let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7 + +let add_label atom p i = + Hashtbl.add label_translation (atom,p) i + +(* Auxiliary data structures and functions *) +module IntSet = Set.Make(struct + type t = int + let compare (x:int) (y:int) = compare x y +end) + +let open_scopes: IntSet.t ref = ref IntSet.empty + let open_scope atom s_id lbl = - () + try + let s_id = Hashtbl.find atom_to_scope (atom,s_id) in + let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in + let n_scop = { start_addr = Some lbl; end_addr = None;} in + open_scopes := IntSet.add s_id !open_scopes; + Hashtbl.replace scope_ranges s_id (n_scop::old_r) + with Not_found -> () let close_scope atom s_id lbl = - () + try + let s_id = Hashtbl.find atom_to_scope (atom,s_id) in + let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in + let last_r,rest = + begin + match old_r with + | a::rest -> a,rest + | _ -> assert false (* We must have an opening scope *) + end in + let new_r = ({last_r with end_addr = Some lbl;})::rest in + open_scopes := IntSet.remove s_id !open_scopes; + Hashtbl.replace scope_ranges s_id new_r + with Not_found -> () let start_live_range atom lbl loc = - () + try + let old_r = Hashtbl.find var_locations atom in + match old_r with + | RangeLoc old_r -> + let n_r = { range_start = Some lbl; range_end = None; var_loc = loc } in + Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r)) + | _ -> assert false + with Not_found -> () + let end_live_range atom lbl = - () + try + let old_r = Hashtbl.find var_locations atom in + match old_r with + | RangeLoc (n_r::old_r) -> + let n_r = {n_r with range_end = Some lbl} in + Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r)) + | _ -> assert false + with Not_found -> () + + +let stack_variable atom (sp,loc) = + Hashtbl.add var_locations atom (FunctionLoc (sp,loc)) + +let function_end atom loc = + IntSet.iter (fun id -> close_scope atom id loc) !open_scopes; + open_scopes := IntSet.empty -let stack_variable atom loc = - () let init name = id := 0; diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index f3cfdc6e..5f459a57 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -21,7 +21,7 @@ open Sections (* The printer is parameterized over target specific functions and a set of dwarf type constants *) module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): sig - val print_debug: out_channel -> dw_entry -> unit + val print_debug: out_channel -> dw_entry -> dw_locations -> unit end = struct @@ -36,6 +36,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_label oc lbl = fprintf oc "%a:\n" label lbl + (* Print a positive label *) + let print_plabel oc lbl = + print_label oc (transl_label lbl) + (* Helper functions for abbreviation printing *) let add_byte buf value = Buffer.add_string buf (string_of_byte value) @@ -69,9 +73,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let add_location loc buf = match loc with | None -> () - | Some (LocSymbol _) ->add_abbr_entry (0x2,location_block_type_abbr) buf - | Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf - | Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf + | Some (LocRef _) -> add_abbr_entry (0x2,location_ref_type_abbr) buf + | Some (LocList _ ) + | Some (LocSymbol _) + | Some (LocSimple _) -> add_abbr_entry (0x2,location_block_type_abbr) buf (* Dwarf entity to string function *) let abbrev_string_of_entity entity has_sibling = @@ -101,8 +106,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): | DW_TAG_compile_unit e -> prologue 0x11; add_abbr_entry (0x1b,comp_dir_type_abbr) buf; - add_high_pc buf; add_low_pc buf; + add_high_pc buf; add_abbr_entry (0x13,language_type_abbr) buf; add_name buf; add_abbr_entry (0x25,producer_type_abbr) buf; @@ -288,20 +293,43 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_byte oc b = fprintf oc " .byte 0x%X\n" b + + let size_of_loc_expr = function + | DW_OP_bregx _ -> 3 + | DW_OP_plus_uconst _ -> 2 + | DW_OP_piece _ -> 2 + + let print_loc_expr oc = function + | DW_OP_bregx (a,b) -> + print_byte oc dw_op_bregx; + print_uleb128 oc a; + fprintf oc " .sleb128 %ld\n" b + | DW_OP_plus_uconst i -> + print_byte oc dw_op_plus_uconst; + print_byte oc i + | DW_OP_piece i -> + print_byte oc dw_op_piece; + print_uleb128 oc i + let print_loc oc loc = match loc with | LocSymbol s -> - fprintf oc " .sleb128 5\n"; - fprintf oc " .byte 3\n"; + print_sleb128 oc 5; + print_byte oc dw_op_addr; fprintf oc " .4byte %a\n" symbol s + | LocSimple e -> + print_sleb128 oc (size_of_loc_expr e); + print_loc_expr oc e + | LocList e -> + let size = List.fold_left (fun acc a -> acc + size_of_loc_expr a) 0 e in + print_sleb128 oc size; + List.iter (print_loc_expr oc) e | _ -> () let print_data_location oc dl = match dl with - | DataLocBlock [DW_OP_plus_uconst i] -> - fprintf oc " .sleb128 2\n"; - fprintf oc " .byte 0x23\n"; - fprintf oc " .byte %d\n" i + | DataLocBlock e -> + print_loc_expr oc e | _ -> () let print_ref oc r = @@ -340,8 +368,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_compilation_unit oc tag = let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in print_string oc (Sys.getcwd ()); - print_addr oc (get_end_addr ()); print_addr oc (get_start_addr ()); + print_addr oc (get_end_addr ()); print_uleb128 oc 1; print_string oc tag.compile_unit_name; print_string oc prod_name; @@ -372,9 +400,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_ref oc tl.label_low_pc; print_string oc tl.label_name + let print_lexical_block oc lb = - print_opt_value oc lb.lexical_block_high_pc print_ref; - print_opt_value oc lb.lexical_block_low_pc print_ref + print_opt_value oc lb.lexical_block_high_pc print_addr; + print_opt_value oc lb.lexical_block_low_pc print_addr let print_member oc mb = print_file_loc oc mb.member_file_loc; @@ -504,10 +533,24 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_sleb128 oc 0; print_label oc debug_end (* End of the debug section *) + let print_location_entry oc l = + let c_low = get_start_addr () in + print_label oc (entry_to_label l.loc_id); + List.iter (fun (b,e,loc) -> + fprintf oc " .4byte %a-%a\n" label b label c_low; + fprintf oc " .4byte %a-%a\n" label e label c_low; + print_loc oc loc) l.loc; + fprintf oc " .4byte 0\n"; + fprintf oc " .4byte 0\n" + + let print_location_list oc l = + List.iter (print_location_entry oc) l (* Print the debug info and abbrev section *) - let print_debug oc entry = + let print_debug oc entry loc = print_debug_abbrev oc entry; - print_debug_info oc entry + print_debug_info oc entry; + print_location_list oc loc + end diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli index 9e0e6693..ab9ab264 100644 --- a/debug/DwarfPrinter.mli +++ b/debug/DwarfPrinter.mli @@ -14,5 +14,5 @@ open DwarfTypes module DwarfPrinter: functor (Target: DWARF_TARGET) -> functor (DwarfAbbrevs: DWARF_ABBREVS) -> sig - val print_debug: out_channel -> dw_entry -> unit + val print_debug: out_channel -> dw_entry -> dw_locations -> unit end diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index 1d41403b..f01e550a 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -12,8 +12,9 @@ (* Types used for writing dwarf debug information *) -open Sections +open BinNums open Camlcoq +open Sections (* Basic types for the value of attributes *) @@ -39,16 +40,17 @@ type block = string type location_expression = | DW_OP_plus_uconst of constant - | DW_OP - + | DW_OP_bregx of int * int32 + | DW_OP_piece of int type location_value = | LocSymbol of atom - | LocConst of constant - | LocBlock of block - + | LocRef of address + | LocSimple of location_expression + | LocList of location_expression list + type data_location_value = - | DataLocBlock of location_expression list + | DataLocBlock of location_expression | DataLocRef of reference type bound_value = @@ -233,6 +235,14 @@ type dw_entry = id: reference; } +(* The type for the location list. *) +type location_entry = + { + loc: (int * int * location_value) list; + loc_id: reference; + } +type dw_locations = location_entry list + (* Module type for a matching from type to dwarf encoding *) module type DWARF_ABBREVS = sig @@ -257,7 +267,7 @@ module type DWARF_ABBREVS = 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_ref_type_abbr: int val location_block_type_abbr: int val data_location_block_type_abbr: int val data_location_ref_type_abbr: int diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index 4cd838b6..954324f1 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -76,6 +76,13 @@ let dw_form_ref8 = 0x14 let dw_ref_udata = 0x15 let dw_ref_indirect = 0x16 +(* Operation encoding *) +let dw_op_addr = 0x3 +let dw_op_plus_uconst = 0x23 +let dw_op_bregx = 0x92 +let dw_op_piece = 0x93 + + (* Default corresponding encoding for the different abbreviations *) module DefaultAbbrevs = struct @@ -100,7 +107,7 @@ module DefaultAbbrevs = 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_ref_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 diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 6c10b362..7b155419 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -10,7 +10,9 @@ (* *) (* *********************************************************************) +open AST open C +open Camlcoq open Cutil open DebugInformation open DwarfTypes @@ -162,7 +164,7 @@ let member_to_entry mem = member_data_member_location = (match mem.cfd_byte_offset with | None -> None - | Some s -> Some (DataLocBlock [DW_OP_plus_uconst s])); + | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s))); member_declaration = None; member_name = Some (mem.cfd_name); member_type = mem.cfd_typ; @@ -280,38 +282,66 @@ let function_parameter_to_entry acc p = } in new_entry (next_id ()) (DW_TAG_formal_parameter p),IntSet.add p.formal_parameter_type acc -let rec local_variable_to_entry acc v id = +let rec local_variable_to_entry f_id acc v id = + let loc = try + begin + match (Hashtbl.find var_locations (get_opt_val v.lvar_atom)) with + | FunctionLoc (a,BA_addrstack (ofs)) -> + let ofs = camlint_of_coqint ofs in + Some (LocSimple (DW_OP_bregx (a,ofs))) + | FunctionLoc (a,BA_splitlong ((BA_addrstack hi),(BA_addrstack lo))) -> + let hi = camlint_of_coqint hi + and lo = camlint_of_coqint lo in + if lo = Int32.add hi 4l then + Some (LocSimple (DW_OP_bregx (a,hi))) + else + Some (LocList [DW_OP_bregx (a,hi);DW_OP_piece 4;DW_OP_bregx (a,lo);DW_OP_piece 4]) + | _ -> None + end + with Not_found -> None in let var = { variable_file_loc = v.lvar_file_loc; variable_declaration = None; variable_external = None; variable_name = v.lvar_name; variable_type = v.lvar_type; - variable_location = None; + variable_location = loc; } in new_entry id (DW_TAG_variable var),IntSet.add v.lvar_type acc -and scope_to_entry acc sc id = +and scope_to_entry f_id acc sc id = + let l_pc,h_pc = try + let r = Hashtbl.find scope_ranges id in + let lbl l = match l with + | Some l -> Some (Hashtbl.find label_translation (f_id,l)) + | None -> None in + begin + match r with + | [] -> None,None + | [a] -> lbl a.start_addr, lbl a.end_addr + | a::rest -> lbl (List.hd (List.rev rest)).start_addr,lbl a.end_addr + end + with Not_found -> None,None in let scope = { - lexical_block_high_pc = None; - lexical_block_low_pc = None; + lexical_block_high_pc = h_pc; + lexical_block_low_pc = l_pc; } in - let vars,acc = mmap local_to_entry acc sc.scope_variables in + let vars,acc = mmap (local_to_entry f_id) acc sc.scope_variables in let entry = new_entry id (DW_TAG_lexical_block scope) in add_children entry vars,acc -and local_to_entry acc id = +and local_to_entry f_id acc id = match Hashtbl.find local_variables id with - | LocalVariable v -> local_variable_to_entry acc v id - | Scope v -> scope_to_entry acc v id + | LocalVariable v -> local_variable_to_entry f_id acc v id + | Scope v -> scope_to_entry f_id acc v id -let fun_scope_to_entries acc id = +let fun_scope_to_entries f_id acc id = match id with | None -> [],acc | Some id -> let sc = Hashtbl.find local_variables id in (match sc with - | Scope sc ->mmap local_to_entry acc sc.scope_variables + | Scope sc ->mmap (local_to_entry f_id) acc sc.scope_variables | _ -> assert false) let function_to_entry acc id f = @@ -324,10 +354,11 @@ let function_to_entry acc id f = subprogram_high_pc = f.fun_high_pc; subprogram_low_pc = f.fun_low_pc; } in + let f_id = get_opt_val f.fun_atom in let acc = match f.fun_return_type with Some s -> IntSet.add s acc | None -> acc in let f_entry = new_entry id (DW_TAG_subprogram f_tag) in let params,acc = mmap function_parameter_to_entry acc f.fun_parameter in - let vars,acc = fun_scope_to_entries acc f.fun_scope in + let vars,acc = fun_scope_to_entries f_id acc f.fun_scope in add_children f_entry (params@vars),acc let definition_to_entry acc id t = @@ -340,10 +371,10 @@ let gen_defs () = t::acc,bcc) definitions ([],IntSet.empty) in List.rev defs,typ -let gen_debug_info () = +let gen_debug_info () : dw_entry * dw_locations= let cp = { compile_unit_name = !file_name; } in let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in let defs,ty = gen_defs () in - add_children cp ((gen_types ty) @ defs) + add_children cp ((gen_types ty) @ defs),[] -- cgit