diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-14 10:10:19 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-14 15:45:54 +0200 |
commit | ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec (patch) | |
tree | 3412177948c85f853aef3996bebedc83c8100309 /debug | |
parent | f5bb397acd12292f6b41438778f2df7391d6f2fe (diff) | |
download | compcert-kvx-ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec.tar.gz compcert-kvx-ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec.zip |
Reworked the section interface for the debug information.
Instead of pushing strings around use the actual section. However
the string is still used in the Hashtbl.
Bug 17392.
Diffstat (limited to 'debug')
-rw-r--r-- | debug/Debug.ml | 13 | ||||
-rw-r--r-- | debug/Debug.mli | 21 | ||||
-rw-r--r-- | debug/DebugInformation.ml | 16 |
3 files changed, 30 insertions, 20 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 |