Added an interface file for DebugInformation.

The interface hides the implementation details, like the huge
number of Hashtbls from the rest of the implementatio.
Bug 18394

5 files changed, 183 insertions, 43 deletions

diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index e8f1703a..828759a7 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -10,7 +10,6 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open AST
 open BinNums
 open C
 open Camlcoq
@@ -47,6 +46,10 @@ let add_file file =
 (* All types encountered *)
 let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7
 
+let get_type = Hashtbl.find types
+
+let fold_types f a = Hashtbl.fold f types a
+
 (* Lookup table for types *)
 let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7
 
@@ -213,6 +216,8 @@ let replace_typedef id f =
 (* All global definitions encountered *)
 let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7
 
+let fold_definitions f a  = Hashtbl.fold f definitions a
+
 (* Mapping from stamp to debug id *)
 let stamp_to_definition: (int,int) Hashtbl.t = Hashtbl.create 7
 
@@ -255,6 +260,8 @@ let replace_fun id f =
 (* All local variables *)
 let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7
 
+let get_local_variable id = Hashtbl.find local_variables id
+
 (* Mapping from stamp to the debug id of the local variable *)
 let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7
 
@@ -516,29 +523,18 @@ let enter_scope f_id p_id id =
   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 * atom,var_location) Hashtbl.t = Hashtbl.create 7
 
+let variable_location var f = Hashtbl.find var_locations (var,f)
+
 let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7
 
+let get_scope_ranges = Hashtbl.find scope_ranges
+
 let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7
 
+let translate_label f l = Hashtbl.find label_translation (f,l)
+
 let add_label atom p i =
   Hashtbl.add label_translation (atom,p) i
 
@@ -589,8 +585,18 @@ 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 section_start n = Hashtbl.find compilation_section_start n
+
+let fold_section_start f a =  Hashtbl.fold f compilation_section_start a
+
+let section_end n = Hashtbl.find compilation_section_end n
+
 let diab_additional: (string,int * int * section_name) Hashtbl.t = Hashtbl.create 7
 
+let diab_additional_section s =
+  let line_start,debug_start,_ = Hashtbl.find diab_additional s in
+  line_start,debug_start
+
 let section_to_string = function
   | Section_user (n,_,_) -> n
   | _ -> ".text"
@@ -622,6 +628,8 @@ let exists_section sec =
 
 let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7
 
+let diab_file_loc f l = Hashtbl.find filenum (f,l)
+
 let compute_diab_file_enum end_label entry_label line_end =
   Hashtbl.iter (fun sec (_,_,secname) ->
     Hashtbl.add compilation_section_end sec (end_label secname);
@@ -633,8 +641,12 @@ let compute_diab_file_enum end_label entry_label line_end =
 let compute_gnu_file_enum f =
   StringSet.iter f !all_files
 
+let all_files_iter f = StringSet.iter f !all_files
+
 let printed_vars: StringSet.t ref = ref StringSet.empty
 
+let is_variable_printed id = StringSet.mem id !printed_vars
+
 let variable_printed id =
   printed_vars := StringSet.add id !printed_vars
 
diff --git a/debug/DebugInformation.mli b/debug/DebugInformation.mli
new file mode 100644
index 00000000..66c4cd11
--- /dev/null
+++ b/debug/DebugInformation.mli
@@ -0,0 +1,106 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open BinNums
+open !C
+open Camlcoq
+open DebugTypes
+open Sections
+
+val typ_to_string: C.typ -> string
+
+val next_id: unit -> int
+
+val get_type: int -> debug_types
+
+val fold_types: (int -> debug_types -> 'a -> 'a) -> 'a -> 'a
+
+val is_variable_printed: string -> bool
+
+val variable_location: atom -> atom -> var_location
+
+val translate_label: atom -> positive -> int
+
+val get_scope_ranges: int -> scope_range list
+
+val get_local_variable: int -> local_information
+
+val diab_file_loc: string -> string -> int
+
+val section_start: string -> int
+
+val fold_section_start: (string -> int -> 'a -> 'a) -> 'a -> 'a
+
+val section_end: string -> int
+
+val diab_additional_section: string -> int * int
+
+val file_name: string ref
+
+val fold_definitions: (int -> definition_type -> 'a -> 'a) -> 'a -> 'a
+
+val atom_global: ident -> atom -> unit
+
+val set_composite_size: ident -> struct_or_union -> int option -> unit
+
+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 diab_add_fun_addr: atom -> section_name -> (int * int) -> unit
+
+val gnu_add_fun_addr: atom -> section_name -> (int * int) -> unit
+
+val all_files_iter: (string -> unit) -> unit
+
+val insert_local_declaration: storage -> ident -> typ -> location -> unit
+
+val atom_local_variable: ident -> atom -> unit
+
+val enter_scope: int -> int -> int -> unit
+
+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 * atom) -> positive -> (int * int builtin_arg) -> unit
+
+val end_live_range: (atom * atom) -> positive -> unit
+
+val stack_variable: (atom * atom) -> int * int builtin_arg -> unit
+
+val add_label: atom -> positive -> int -> unit
+
+val atom_parameter: ident -> ident -> atom -> 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: section_name -> bool
+
+val remove_unused: ident -> unit
+
+val remove_unused_function: ident -> unit
+
+val variable_printed: string -> unit
+
+val add_diab_info: section_name ->  int -> int  -> int -> unit
+
+val init: string -> unit
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index 24712b27..462ca2d3 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -22,7 +22,7 @@ let default_debug =
    insert_global_declaration = DebugInformation.insert_global_declaration;
    add_fun_addr = (fun _ _ _ -> ());
    generate_debug_info = (fun _ _  -> None);
-   all_files_iter = (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files);
+   all_files_iter = DebugInformation.all_files_iter;
    insert_local_declaration = DebugInformation.insert_local_declaration;
    atom_local_variable = DebugInformation.atom_local_variable;
    enter_scope = DebugInformation.enter_scope;
diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli
index 53a39665..25c7390f 100644
--- a/debug/DebugTypes.mli
+++ b/debug/DebugTypes.mli
@@ -10,6 +10,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open AST
+open BinNums
 open C
 open Camlcoq
 
@@ -158,3 +160,21 @@ type scope_information =
 type local_information =
   | LocalVariable of local_variable_information
   | Scope of scope_information
+
+
+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 *)
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index fe0764e8..f1a8ce3e 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -21,6 +21,8 @@ open DwarfUtil
 
 (* Generate the dwarf DIE's from the information collected in DebugInformation *)
 
+module StringSet = Set.Make(String)
+
 (* Helper function to get values that must be set. *)
 let get_opt_val = function
   | Some a -> a
@@ -270,7 +272,7 @@ module Dwarfgenaux (Target: TARGET) =
           IntSet.add id d,true
         else
           d,false in
-      let t = Hashtbl.find types id in
+      let t = get_type id in
       match t with
       | IntegerType _
       | FloatType _
@@ -308,15 +310,15 @@ module Dwarfgenaux (Target: TARGET) =
         else
           d in
       let typs = aux needed in
-      List.rev (Hashtbl.fold (fun id t acc ->
+      List.rev (fold_types (fun id t acc ->
         if IntSet.mem id typs then
           (infotype_to_entry id t)::acc
         else
-          acc) types [])
+          acc) [])
 
     let global_variable_to_entry acc id v =
       let loc = match v.gvar_atom with
-      | Some a when StringSet.mem (extern_atom a) !printed_vars ->
+      | Some a when is_variable_printed (extern_atom a) ->
           Some (LocSymbol a)
       | _ -> None in
       let var = {
@@ -369,15 +371,15 @@ module Dwarfgenaux (Target: TARGET) =
       if !Clflags.option_gdepth > 2 then
         try
           begin
-            match (Hashtbl.find var_locations (f_id,atom)) with
+            match variable_location f_id atom with
             | FunctionLoc (a,r) ->
                 translate_function_loc a r
             | RangeLoc l ->
                 let l = List.rev_map (fun i ->
                   let hi = get_opt_val i.range_start
                   and lo = get_opt_val i.range_end in
-                  let hi = Hashtbl.find label_translation (f_id,hi)
-                  and lo = Hashtbl.find label_translation (f_id,lo) in
+                  let hi = translate_label f_id hi
+                  and lo = translate_label f_id lo in
                   hi,lo,range_entry_loc i.var_loc) l in
                 let id = next_id () in
                 Some (LocRef id),[{loc = l;loc_id = id;}]
@@ -402,11 +404,11 @@ module Dwarfgenaux (Target: TARGET) =
 
     let scope_range f_id id (o,dwr) =
       try
-        let r = Hashtbl.find scope_ranges id in
+        let r = get_scope_ranges id in
         let lbl l h = match l,h with
         | Some l,Some h->
-            let l = (Hashtbl.find label_translation (f_id,l))
-            and h = (Hashtbl.find label_translation (f_id,h)) in
+            let l = translate_label f_id l
+            and h = translate_label f_id h in
             l,h
         | _ -> raise Not_found in
         begin
@@ -451,7 +453,7 @@ module Dwarfgenaux (Target: TARGET) =
       add_children entry vars,(acc >>= dwr)
 
     and local_to_entry f_id acc id =
-      match Hashtbl.find local_variables id with
+      match get_local_variable id with
       | LocalVariable v -> local_variable_to_entry f_id acc v id
       | Scope v -> let s,acc = (scope_to_entry f_id acc v id) in
         Some s,acc
@@ -460,7 +462,7 @@ module Dwarfgenaux (Target: TARGET) =
       match id with
       | None -> [],acc
       | Some id ->
-          let sc = Hashtbl.find local_variables id in
+          let sc = get_local_variable id in
           (match sc with
           | Scope sc -> mmap_opt (local_to_entry f_id) acc sc.scope_variables
           | _ -> assert false)
@@ -499,7 +501,7 @@ module Dwarfgenaux (Target: TARGET) =
 module StringMap = Map.Make(String)
 
 let diab_file_loc sec (f,l)  =
-  Diab_file_loc (Hashtbl.find filenum (sec,f),l)
+  Diab_file_loc ((diab_file_loc sec f),l)
 
 let prod_name =
   let version_string =
@@ -518,9 +520,9 @@ let diab_gen_compilation_section s defs acc =
   let defs,accu = List.fold_left (fun (acc,bcc) (id,t) ->
     let t,bcc = Gen.definition_to_entry bcc id t in
     t::acc,bcc) ([],empty_accu) defs in
-  let low_pc = Hashtbl.find compilation_section_start s
-  and line_start,debug_start,_ = Hashtbl.find diab_additional s
-  and high_pc = Hashtbl.find compilation_section_end s in
+  let low_pc = section_start s
+  and line_start,debug_start = diab_additional_section s
+  and high_pc = section_end s in
   let cp = {
     compile_unit_name = Simple_string !file_name;
     compile_unit_range = Pc_pair (low_pc,high_pc);
@@ -538,12 +540,12 @@ let diab_gen_compilation_section s defs acc =
   }::acc
 
 let gen_diab_debug_info sec_name var_section : debug_entries =
-  let defs = Hashtbl.fold (fun id t acc ->
+  let defs = fold_definitions (fun id t acc ->
     let s = match t with
     | GlobalVariable _ -> var_section
     | Function f -> sec_name (get_opt_val f.fun_atom) in
     let old = try StringMap.find s acc with Not_found -> [] in
-    StringMap.add s ((id,t)::old) acc) definitions StringMap.empty in
+    StringMap.add s ((id,t)::old) acc) StringMap.empty in
   let entries = StringMap.fold diab_gen_compilation_section defs [] in
   Diab entries
 
@@ -567,15 +569,15 @@ let gnu_string_entry s =
 let gen_gnu_debug_info sec_name var_section : debug_entries =
   let r,dwr,low_pc =
     try if !Clflags.option_gdwarf > 3 then
-        let pcs  = Hashtbl.fold (fun s low acc ->
-          (low,Hashtbl.find compilation_section_end s)::acc) compilation_section_start [] in
+        let pcs  = fold_section_start (fun s low acc ->
+          (low,section_end s)::acc) [] in
         match pcs with
         | [] ->  Empty,(0,[]),None
         | [(l,h)] ->   Pc_pair (l,h),(0,[]),Some l
         | _ -> Offset 0,(2 + 4 * (List.length pcs),[pcs]),None
     else
-        let l = Hashtbl.find compilation_section_start ".text"
-        and h = Hashtbl.find compilation_section_end ".text" in
+        let l = section_start ".text"
+        and h = section_end ".text" in
         Pc_pair(l,h),(0,[]),Some l
     with Not_found ->  Empty,(0,[]),None in
   let accu = empty_accu >>= dwr in
@@ -583,12 +585,12 @@ let gen_gnu_debug_info sec_name var_section : debug_entries =
     let file_loc = gnu_file_loc
     let string_entry = gnu_string_entry
   end) in
-  let defs,accu,sec = Hashtbl.fold (fun  id t (acc,bcc,sec) ->
+  let defs,accu,sec = fold_definitions (fun  id t (acc,bcc,sec) ->
     let s = match t with
     | GlobalVariable _ -> var_section
     | Function f -> sec_name (get_opt_val f.fun_atom) in
     let t,bcc = Gen.definition_to_entry bcc id t in
-    t::acc,bcc,StringSet.add s sec) definitions ([],accu,StringSet.empty) in
+    t::acc,bcc,StringSet.add s sec) ([],accu,StringSet.empty) in
   let types = Gen.gen_types accu.typs in
   let cp = {
     compile_unit_name = gnu_string_entry !file_name;