diff options
| -rw-r--r-- | debug/Debug.ml | 13 | ||||
| -rw-r--r-- | debug/Debug.mli | 21 | ||||
| -rw-r--r-- | debug/DebugInformation.ml | 16 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 13 |
4 files changed, 37 insertions, 26 deletions
diff --git a/debug/Debug.ml b/debug/Debug.ml index 806ebb08..14176d3b 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -16,6 +16,7 @@ open C open Camlcoq open Dwarfgen open DwarfTypes +open Sections (* Interface for generating and printing debug information *) @@ -43,14 +44,14 @@ type implem = stack_variable: (atom * atom) -> int * int builtin_arg -> unit; add_label: atom -> positive -> int -> unit; atom_parameter: ident -> ident -> atom -> unit; - add_compilation_section_start: string -> int -> unit; - add_compilation_section_end: string -> int -> unit; - compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit; + add_compilation_section_start: section_name -> int -> unit; + add_compilation_section_end: section_name -> int -> unit; + compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit; compute_gnu_file_enum: (string -> unit) -> unit; - exists_section: string -> bool; + exists_section: section_name -> bool; remove_unused: ident -> unit; variable_printed: string -> unit; - add_diab_info: string -> (int * int * string) -> unit; + add_diab_info: section_name -> int -> int -> unit; } let default_implem = @@ -83,7 +84,7 @@ let default_implem = exists_section = (fun _ -> true); remove_unused = (fun _ -> ()); variable_printed = (fun _ -> ()); - add_diab_info = (fun _ _ -> ()); + add_diab_info = (fun _ _ _ -> ()); } let implem = ref default_implem diff --git a/debug/Debug.mli b/debug/Debug.mli index 145927f4..83d5703b 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -15,6 +15,7 @@ open C open Camlcoq open DwarfTypes open BinNums +open Sections (* Record used for stroring references to the actual implementation functions *) @@ -41,14 +42,14 @@ type implem = stack_variable: (atom * atom) -> int * int builtin_arg -> unit; add_label: atom -> positive -> int -> unit; atom_parameter: ident -> ident -> atom -> unit; - add_compilation_section_start: string -> int -> unit; - add_compilation_section_end: string -> int -> unit; - compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit; + add_compilation_section_start: section_name -> int -> unit; + add_compilation_section_end: section_name -> int -> unit; + compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit; compute_gnu_file_enum: (string -> unit) -> unit; - exists_section: string -> bool; + exists_section: section_name -> bool; remove_unused: ident -> unit; variable_printed: string -> unit; - add_diab_info: string -> (int * int * string) -> unit; + add_diab_info: section_name -> int -> int -> unit; } val default_implem: implem @@ -76,11 +77,11 @@ val stack_variable: (atom * atom) -> int * int builtin_arg -> unit val add_label: atom -> positive -> int -> unit val generate_debug_info: (atom -> string) -> string -> debug_entries option val atom_parameter: ident -> ident -> atom -> unit -val add_compilation_section_start: string -> int -> unit -val add_compilation_section_end: string -> int -> unit -val compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit +val add_compilation_section_start: section_name -> int -> unit +val add_compilation_section_end: section_name -> int -> 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: string -> bool +val exists_section: section_name -> bool val remove_unused: ident -> unit val variable_printed: string -> unit -val add_diab_info: string -> (int * int * string) -> unit +val add_diab_info: section_name -> int -> int -> unit diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 55d49e72..95f34b1d 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -16,6 +16,7 @@ open C open Camlcoq open Cutil open DebugTypes +open Sections (* This implements an interface for the collection of debugging information. *) @@ -578,19 +579,26 @@ 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 diab_additional: (string,int * int * string) Hashtbl.t = Hashtbl.create 7 +let diab_additional: (string,int * int * section_name) Hashtbl.t = Hashtbl.create 7 + +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 addr = - Hashtbl.add diab_additional sec addr +let add_diab_info sec addr1 add2 = + let sec' = section_to_string sec in + Hashtbl.add diab_additional sec' (addr1,add2,sec) let exists_section sec = - Hashtbl.mem compilation_section_start sec + Hashtbl.mem compilation_section_start (section_to_string sec) let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7 diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 10d89d54..aed6e2bf 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -152,7 +152,7 @@ module Linux_System : SYSTEM = if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in - Debug.add_compilation_section_start ".text" low_pc; + Debug.add_compilation_section_start Section_text low_pc; fprintf oc "%a:\n" label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end @@ -161,7 +161,7 @@ module Linux_System : SYSTEM = if !Clflags.option_g then begin let high_pc = new_label () in - Debug.add_compilation_section_end ".text" high_pc; + Debug.add_compilation_section_end Section_text high_pc; Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; fprintf oc "%a:\n" label high_pc @@ -256,17 +256,18 @@ module Diab_System : SYSTEM = match sec with | Section_debug_abbrev | Section_debug_info _ + | Section_debug_str | Section_debug_loc -> () | sec -> let name = match sec with | Section_user (name,_,_) -> name | _ -> name_of_section sec in - if not (Debug.exists_section name) then + if not (Debug.exists_section sec) then let line_start = new_label () and low_pc = new_label () and debug_info = new_label () in - Debug.add_diab_info name (line_start,debug_info,name_of_section sec); - Debug.add_compilation_section_start name low_pc; + Debug.add_diab_info sec line_start debug_info; + Debug.add_compilation_section_start sec low_pc; let line_name = ".debug_line" ^(if name <> ".text" then name else "") in section oc (Section_debug_line (if name <> ".text" then Some name else None)); fprintf oc " .section %s,,n\n" line_name; @@ -287,7 +288,7 @@ module Diab_System : SYSTEM = let print_epilogue oc = let end_label sec = fprintf oc "\n"; - fprintf oc " %s\n" sec; + section oc sec; let label_end = new_label () in fprintf oc "%a:\n" label label_end; label_end |