diff options
-rw-r--r-- | arm/TargetPrinter.ml | 6 | ||||
-rw-r--r-- | backend/PrintAsm.ml | 8 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 3 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 10 | ||||
-rw-r--r-- | debug/CtoDwarf.ml | 13 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 25 | ||||
-rw-r--r-- | debug/DwarfTypes.mli | 14 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 6 | ||||
-rw-r--r-- | lib/Camlcoq.ml | 7 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 9 |
10 files changed, 74 insertions, 27 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index f8d72836..33071a9a 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -923,6 +923,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let new_label = new_label let print_file_loc _ _ = () (* Dummy function *) + + let get_location _ = None (* Dummy function *) + + let get_segment_location _ = None (* Dummy function *) + + let add_var_location _ = () (* Dummy function *) end let sel_target () = diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index f3c80f3e..29409b32 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -78,6 +78,7 @@ module Printer(Target:TARGET) = List.iter (Target.print_init oc) id let print_var oc name v = + if !Clflags.option_g && Configuration.advanced_debug then Target.add_var_location name; match v.gvar_init with | [] -> () | _ -> @@ -102,8 +103,7 @@ module Printer(Target:TARGET) = let sz = match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in Target.print_comm_symb oc sz name align - - + let print_globdef oc (name,gdef) = match gdef with | Gfun (Internal code) -> print_function oc name code @@ -120,6 +120,10 @@ module Printer(Target:TARGET) = let get_stmt_list_addr = Target.get_stmt_list_addr let name_of_section = Target.name_of_section let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None + let get_location a = try (Target.get_location (stamp_atom a)) with Not_found -> None + let get_segment_location a = try (Target.get_segment_location (stamp_atom a)) with Not_found -> None + let get_frame_base a = None + let symbol = Target.symbol end module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs) diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index b54188ca..efc8030f 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -51,6 +51,9 @@ module type TARGET = val new_label: unit -> int val label: out_channel -> int -> unit val print_file_loc: out_channel -> file_loc -> unit + val get_location: P.t -> location_value option + val get_segment_location: P.t -> location_value option + val add_var_location: P.t -> unit module DwarfAbbrevs: DWARF_ABBREVS end diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index b919c1d4..f1c8ec8e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1038,7 +1038,9 @@ let convertFundef loc env fd = let params = List.map (fun (id, ty) -> - (intern_string id.name, convertTyp env ty)) + let id' = intern_string id.name in + add_stamp id.stamp id'; + (id', convertTyp env ty)) fd.fd_params in let vars = List.map @@ -1047,7 +1049,9 @@ let convertFundef loc env fd = unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; - (intern_string id.name, convertTyp env ty)) + let id' = intern_string id.name in + add_stamp id.stamp id'; + (id', convertTyp env ty)) fd.fd_locals in let body' = convertStmt loc env fd.fd_body in let id' = intern_string fd.fd_name.name in @@ -1075,6 +1079,7 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in + add_stamp id.stamp id'; let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else @@ -1116,6 +1121,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in + add_stamp id.stamp id'; let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml index c5f1142c..063b0823 100644 --- a/debug/CtoDwarf.ml +++ b/debug/CtoDwarf.ml @@ -164,15 +164,14 @@ and fun_to_dwarf_tag rt args = false,[u],[] | Some [] -> true,[],[] | Some l -> - let c,e = mmap (fun acc (_,t) -> + let c,e = mmap (fun acc (i,t) -> let t,e = type_to_dwarf t in let fp = { + formal_parameter_id = i.stamp; formal_parameter_file_loc = None; formal_parameter_artificial = None; - formal_parameter_location = None; formal_parameter_name = None; - formal_parameter_segment = None; formal_parameter_type = t; formal_parameter_variable_parameter = None; } in @@ -312,12 +311,11 @@ let glob_var_to_dwarf (s,n,t,_) gloc = | Storage_static -> false | _ -> true) in let decl = { + variable_id = n.stamp; variable_file_loc = (Some gloc); variable_declaration = Some at_decl; variable_external = Some ext; - variable_location = None; variable_name = n.name; - variable_segment = None; variable_type = i; } in let decl = new_entry (DW_TAG_variable decl) in @@ -333,9 +331,9 @@ let fundef_to_dwarf f gloc = | Storage_static -> false | _ -> true) in let fdef = { + subprogram_id = f.fd_name.stamp; subprogram_file_loc = (Some gloc); subprogram_external = Some ext; - subprogram_frame_base = None; subprogram_name = f.fd_name.name; subprogram_prototyped = true; subprogram_type = ret; @@ -344,11 +342,10 @@ let fundef_to_dwarf f gloc = let t,e = type_to_dwarf t in let fp = { + formal_parameter_id = p.stamp; formal_parameter_file_loc = None; formal_parameter_artificial = None; - formal_parameter_location = None; formal_parameter_name = (Some p.name); - formal_parameter_segment = None; formal_parameter_type = t; formal_parameter_variable_parameter = None; } in diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 7f1caaf6..cd888a80 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -127,9 +127,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): prologue 0x5; add_attr_some e.formal_parameter_file_loc add_file_loc; add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr)); - add_location e.formal_parameter_location buf; + add_location (get_location e.formal_parameter_id) buf; add_attr_some e.formal_parameter_name add_name; - add_location e.formal_parameter_segment buf; + add_location (get_segment_location e.formal_parameter_id) buf; add_type buf; add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr)) | DW_TAG_label _ -> @@ -202,9 +202,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): add_attr_some e.variable_file_loc add_file_loc; add_attr_some e.variable_declaration add_declaration; add_attr_some e.variable_external (add_abbr_entry (0x3f,external_type_abbr)); - add_location e.variable_location buf; + add_location (get_location e.variable_id) buf; add_name buf; - add_location e.variable_segment buf; + add_location (get_segment_location e.variable_id) buf; add_type buf | DW_TAG_volatile_type _ -> prologue 0x35; @@ -294,7 +294,12 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): fprintf oc " .byte 0x%X\n" b let print_loc oc loc = - () + match loc with + | LocSymbol s -> + fprintf oc " .sleb128 5\n"; + fprintf oc " .byte 3\n"; + fprintf oc " .4byte %a\n" symbol s + | _ -> () let print_data_location oc dl = () @@ -359,9 +364,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_formal_parameter oc fp = print_file_loc oc fp.formal_parameter_file_loc; print_opt_value oc fp.formal_parameter_artificial print_flag; - print_opt_value oc fp.formal_parameter_location print_loc; + print_opt_value oc (get_location fp.formal_parameter_id) print_loc; print_opt_value oc fp.formal_parameter_name print_string; - print_opt_value oc fp.formal_parameter_segment print_loc; + print_opt_value oc (get_segment_location fp.formal_parameter_id) print_loc; print_ref oc fp.formal_parameter_type; print_opt_value oc fp.formal_parameter_variable_parameter print_flag @@ -400,7 +405,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let addr = get_fun_addr sp.subprogram_name in print_file_loc oc sp.subprogram_file_loc; print_opt_value oc sp.subprogram_external print_flag; - print_opt_value oc sp.subprogram_frame_base print_loc; + print_opt_value oc (get_frame_base sp.subprogram_id) print_loc; print_opt_value oc addr print_subprogram_addr; print_string oc sp.subprogram_name; print_flag oc sp.subprogram_prototyped; @@ -433,9 +438,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_file_loc oc var.variable_file_loc; print_opt_value oc var.variable_declaration print_flag; print_opt_value oc var.variable_external print_flag; - print_opt_value oc var.variable_location print_loc; + print_opt_value oc (get_location var.variable_id) print_loc; print_string oc var.variable_name; - print_opt_value oc var.variable_segment print_loc; + print_opt_value oc (get_segment_location var.variable_id) print_loc; print_ref oc var.variable_type let print_volatile_type oc vt = diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index d6592bd9..174f2403 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -13,6 +13,7 @@ (* Types used for writing dwarf debug information *) open Sections +open Camlcoq (* Basic types for the value of attributes *) @@ -37,6 +38,7 @@ type address = int type block = string type location_value = + | LocSymbol of atom | LocConst of constant | LocBlock of block @@ -92,11 +94,10 @@ type dw_tag_enumerator = type dw_tag_formal_parameter = { + formal_parameter_id: int; formal_parameter_file_loc: file_loc option; formal_parameter_artificial: flag option; - formal_parameter_location: location_value option; formal_parameter_name: string option; - formal_parameter_segment: location_value option; formal_parameter_type: reference; formal_parameter_variable_parameter: flag option; } @@ -140,9 +141,9 @@ type dw_tag_structure_type = type dw_tag_subprogram = { + subprogram_id: int; subprogram_file_loc: file_loc option; subprogram_external: flag option; - subprogram_frame_base: location_value option; subprogram_name: string; subprogram_prototyped: flag; subprogram_type: reference option; @@ -183,12 +184,11 @@ type dw_tag_unspecified_parameter = type dw_tag_variable = { + variable_id: int; variable_file_loc: file_loc option; variable_declaration: flag option; variable_external: flag option; - variable_location: location_value option; variable_name: string; - variable_segment: location_value option; variable_type: reference; } @@ -269,4 +269,8 @@ module type DWARF_TARGET= val get_stmt_list_addr: unit -> int val name_of_section: section_name -> string val get_fun_addr: string -> (int * int) option + val get_location: int -> location_value option + val get_segment_location: int -> location_value option + val get_frame_base: int -> location_value option + val symbol: out_channel -> atom -> unit end diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 13bc6826..992c97e2 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -789,6 +789,12 @@ module Target(System: SYSTEM):TARGET = let new_label = new_label let print_file_loc _ _ = () (* Dummy function *) + + let get_location _ = None (* Dummy function *) + + let get_segment_location _ = None (* Dummy function *) + + let add_var_location _ = () (* Dummy function *) end diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 68c095f0..5eb52e88 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -284,6 +284,7 @@ let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64 type atom = positive let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t) +let atom_of_stamp = (Hashtbl.create 17: (int, atom) Hashtbl.t) let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t) let next_atom = ref Coq_xH @@ -297,6 +298,12 @@ let intern_string s = Hashtbl.add string_of_atom a s; a +let add_stamp s a = + Hashtbl.add atom_of_stamp s a + +let stamp_atom s = + Hashtbl.find atom_of_stamp s + let extern_atom a = try Hashtbl.find string_of_atom a diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 8610f750..1e78f038 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -854,7 +854,16 @@ module Target (System : SYSTEM):TARGET = let section oc sec = section oc sec; debug_section oc sec + + let locations = (Hashtbl.create 17 : (atom,DwarfTypes.location_value) Hashtbl.t) + let get_location a = try Some (Hashtbl.find locations a) with Not_found -> None + + let get_segment_location _ = None + + let add_var_location a = + if !Clflags.option_g && Configuration.advanced_debug then + Hashtbl.add locations a (DwarfTypes.LocSymbol a); end let sel_target () = |