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. --- arm/TargetPrinter.ml | 1 + backend/PrintAsm.ml | 8 ++-- common/Sections.ml | 1 + common/Sections.mli | 1 + 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 ++++++++++++++++++------- ia32/TargetPrinter.ml | 1 + powerpc/AsmToJSON.ml | 3 +- powerpc/Asmexpand.ml | 112 +++++++++++++++++++++++++++++----------------- powerpc/TargetPrinter.ml | 4 +- 16 files changed, 318 insertions(+), 98 deletions(-) diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 5f16fc9e..30166215 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -153,6 +153,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = sprintf ".section \"%s\",\"a%s%s\",%%progbits" s (if wr then "w" else "") (if ex then "x" else "") | Section_debug_info + | Section_debug_loc | Section_debug_abbrev -> "" (* Dummy value *) let section oc sec = diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 9ffe3aa5..104440c6 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -66,7 +66,9 @@ module Printer(Target:TARGET) = print_debug_label oc e; Target.print_fun_info oc name; Target.emit_constants oc lit; - Target.print_jumptable oc jmptbl + Target.print_jumptable oc jmptbl; + if !Clflags.option_g then + Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels let print_init_data oc name id = if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 @@ -141,6 +143,6 @@ let print_program oc p db = begin match Debug.generate_debug_info () with | None -> () - | Some db -> - Printer.DebugPrinter.print_debug oc db + | Some (db,loc) -> + Printer.DebugPrinter.print_debug oc db loc end diff --git a/common/Sections.ml b/common/Sections.ml index c0c95848..8e569389 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -29,6 +29,7 @@ type section_name = | Section_user of string * bool (*writable*) * bool (*executable*) | Section_debug_info | Section_debug_abbrev + | Section_debug_loc type access_mode = | Access_default diff --git a/common/Sections.mli b/common/Sections.mli index e878b9e5..eca9a993 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -28,6 +28,7 @@ type section_name = | Section_user of string * bool (*writable*) * bool (*executable*) | Section_debug_info | Section_debug_abbrev + | Section_debug_loc type access_mode = | Access_default 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),[] diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index b06f6f97..215eb4b8 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -102,6 +102,7 @@ module Cygwin_System : SYSTEM = sprintf ".section \"%s\", \"%s\"\n" s (if ex then "xr" else if wr then "d" else "dr") | Section_debug_info + | Section_debug_loc | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index a7e66701..136c9e41 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -331,7 +331,8 @@ let p_section oc = function | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e | Section_debug_info - | Section_debug_abbrev -> () (* There should be no info in the debug sections *) + | Section_debug_abbrev + | Section_debug_loc -> () (* There should be no info in the debug sections *) let p_int_opt oc = function | None -> fprintf oc "0" diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index d4675e5f..d44f709e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -586,36 +586,57 @@ let expand_instruction_simple instr = | _ -> emit instr -let preg_to_string p = - "" - -let rec translate_annot a = - match a with - | BA x -> BA (preg_to_string x) - | BA_int n -> BA_int n - | BA_long n -> BA_long n - | BA_float n -> BA_float n - | BA_single n -> BA_single n - | BA_loadstack (chunk,ofs) -> BA_loadstack (chunk,ofs) - | BA_addrstack ofs -> BA_addrstack ofs - | BA_loadglobal (chunk,id,ofs) -> BA_loadglobal (chunk,id,ofs) - | BA_addrglobal (id,ofs) -> BA_addrglobal (id,ofs) - | BA_splitlong (hi,lo) -> BA_splitlong (translate_annot hi,translate_annot lo) - -let expand_stack_loc txt = function - | [a] -> Debug.stack_variable txt (translate_annot a) - | _ -> assert false - -let expand_start_live_range txt lbl = function - | [a] -> Debug.start_live_range txt lbl (translate_annot a) - | _ -> assert false - -let expand_end_live_range = - Debug.end_live_range +(* Translate to the integer identifier of the register as + the EABI specifies *) + +let int_reg_to_dwarf = function + | GPR0 -> 0 | GPR1 -> 1 | GPR2 -> 2 | GPR3 -> 3 + | GPR4 -> 4 | GPR5 -> 5 | GPR6 -> 6 | GPR7 -> 7 + | GPR8 -> 8 | GPR9 -> 9 | GPR10 -> 10 | GPR11 -> 11 + | GPR12 -> 12 | GPR13 -> 13 | GPR14 -> 14 | GPR15 -> 15 + | GPR16 -> 16 | GPR17 -> 17 | GPR18 -> 18 | GPR19 -> 19 + | GPR20 -> 20 | GPR21 -> 21 | GPR22 -> 22 | GPR23 -> 23 + | GPR24 -> 24 | GPR25 -> 25 | GPR26 -> 26 | GPR27 -> 27 + | GPR28 -> 28 | GPR29 -> 29 | GPR30 -> 30 | GPR31 -> 31 + +let float_reg_to_dwarf = function + | FPR0 -> 32 | FPR1 -> 33 | FPR2 -> 34 | FPR3 -> 35 + | FPR4 -> 36 | FPR5 -> 37 | FPR6 -> 38 | FPR7 -> 39 + | FPR8 -> 40 | FPR9 -> 41 | FPR10 -> 42 | FPR11 -> 43 + | FPR12 -> 44 | FPR13 -> 45 | FPR14 -> 46 | FPR15 -> 47 + | FPR16 -> 48 | FPR17 -> 49 | FPR18 -> 50 | FPR19 -> 51 + | FPR20 -> 52 | FPR21 -> 53 | FPR22 -> 54| FPR23 -> 55 + | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59 + | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63 + +let preg_to_dwarf_int = function + | IR r -> int_reg_to_dwarf r + | FR r -> float_reg_to_dwarf r + | _ -> assert false + + +let translate_annot a = + let rec aux = function + | BA x -> Some (BA (preg_to_dwarf_int x)) + | BA_int _ + | BA_long _ + | BA_float _ + | BA_single _ + | BA_loadglobal _ + | BA_addrglobal _ + | BA_loadstack _ -> None + | BA_addrstack ofs -> Some (BA_addrstack ofs) + | BA_splitlong (hi,lo) -> + begin + match (aux hi,aux lo) with + | Some hi ,Some lo -> Some (BA_splitlong (hi,lo)) + | _,_ -> None + end in + aux (List.hd a) let expand_scope id lbl oldscopes newscopes = - let opening = List.filter (fun a -> List.mem a oldscopes) newscopes - and closing = List.filter (fun a -> List.mem a newscopes) oldscopes in + let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes + and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in List.iter (fun i -> Debug.open_scope id i lbl) opening; List.iter (fun i -> Debug.close_scope id i lbl) closing @@ -627,31 +648,42 @@ let expand_instruction id l = lbl | Some lbl -> lbl in let rec aux lbl scopes = function - | [] -> () + | [] -> let lbl = get_lbl lbl in + Debug.function_end id lbl | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> let kind = (P.to_int kind) in begin match kind with - | 1 -> - emit i; aux lbl scopes rest + | 1-> + aux lbl scopes rest | 2 -> aux lbl scopes rest | 3 -> - let lbl = get_lbl lbl in - expand_start_live_range txt lbl args; - aux (Some lbl) scopes rest + begin + match translate_annot args with + | Some a -> + let lbl = get_lbl lbl in + Debug.start_live_range txt lbl (1,a); + aux (Some lbl) scopes rest + | None -> aux lbl scopes rest + end | 4 -> let lbl = get_lbl lbl in - expand_end_live_range txt lbl; + Debug.end_live_range txt lbl; aux (Some lbl) scopes rest - | 5 -> - expand_stack_loc txt args; - aux lbl scopes rest - | 6 -> + | 5 -> + begin + match translate_annot args with + | Some a-> + Debug.stack_variable txt (1,a); + aux lbl scopes rest + | _ -> aux lbl scopes rest + end + | 6 -> let lbl = get_lbl lbl in let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in expand_scope id lbl scopes scopes'; - aux (Some lbl) scopes' rest + emit i;aux (Some lbl) scopes' rest | _ -> emit i; aux None scopes rest end diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 21181215..e53f56a9 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -133,7 +133,8 @@ module Linux_System : SYSTEM = s (if wr then "w" else "") (if ex then "x" else "") | Section_debug_info -> ".debug_info,\"\",@progbits" | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits" - + | Section_debug_loc -> ".debug_loc,\"\",@progbits" + let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); @@ -211,6 +212,7 @@ module Diab_System : SYSTEM = | false, false -> 'r') (* const *) | Section_debug_info -> ".debug_info,,n" | Section_debug_abbrev -> ".debug_abbrev,,n" + | Section_debug_loc -> ".debug_loc,,n" let section oc sec = let name = name_of_section sec in -- cgit