1 files changed, 37 insertions, 89 deletions

diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 9c5a92ba..51fbfde9 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. *)
@@ -60,53 +61,7 @@ let typ_to_string (ty: typ) =
   Buffer.contents buf
 
 (* Helper functions for the attributes *)
-let strip_attributes typ =
-  let strip =  List.filter (fun a -> a = AConst || a = AVolatile) in
-  match typ with
-  | TVoid at -> TVoid (strip at)
-  | TInt (k,at) ->  TInt (k,strip at)
-  | TFloat (k,at) -> TFloat(k,strip at)
-  | TPtr (t,at) -> TPtr(t,strip at)
-  | TArray (t,s,at) -> TArray(t,s,strip at)
-  | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at)
-  | TNamed (n,at) -> TNamed(n,strip at)
-  | TStruct (n,at) -> TStruct(n,strip at)
-  | TUnion (n,at) -> TUnion(n,strip at)
-  | TEnum (n,at) -> TEnum(n,strip at)
-
-let strip_last_attribute typ  =
-  let rec hd_opt l = match l with
-    [] -> None,[]
-  | AConst::rest -> Some AConst,rest
-  | AVolatile::rest -> Some AVolatile,rest
-  | _::rest -> hd_opt rest in
-  match typ with
-  | TVoid at -> let l,r = hd_opt at in
-    l,TVoid r
-  | TInt (k,at) -> let l,r = hd_opt at in
-    l,TInt (k,r)
-  | TFloat (k,at) -> let l,r = hd_opt at in
-    l,TFloat (k,r)
-  | TPtr (t,at) -> let l,r = hd_opt at in
-    l,TPtr(t,r)
-  | TArray (t,s,at) -> let l,r = hd_opt at in
-    l,TArray(t,s,r)
-  | TFun (t,arg,v,at) -> let l,r = hd_opt at in
-    l,TFun(t,arg,v,r)
-  | TNamed (n,at) -> let l,r = hd_opt at in
-    l,TNamed(n,r)
-  | TStruct (n,at) -> let l,r = hd_opt at in
-    l,TStruct(n,r)
-  | TUnion (n,at) -> let l,r = hd_opt at in
-    l,TUnion(n,r)
-  | TEnum (n,at) -> let l,r = hd_opt at in
-    l,TEnum(n,r)
-
-(* Does the type already exist? *)
-let exist_type (ty: typ) =
-  (* We are only interrested in Const and Volatile *)
-  let ty = strip_attributes ty in
-  Hashtbl.mem lookup_types (typ_to_string ty)
+let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile]
 
 (* Find the type id to an type *)
 let find_type (ty: typ) =
@@ -267,6 +222,7 @@ let name_to_definition: (string,int) Hashtbl.t = Hashtbl.create 7
 (* Mapping from atom to debug id *)
 let atom_to_definition: (atom, int) Hashtbl.t = Hashtbl.create 7
 
+(* Various lookup functions for defintions *)
 let find_gvar_stamp id =
   let id = (Hashtbl.find stamp_to_definition id) in
   let var = Hashtbl.find definitions id in
@@ -302,9 +258,6 @@ let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7
 (* Mapping from stampt to the debug id of the local variable *)
 let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7
 
-(* Mapping form atom to the debug id of the local variable *)
-let atom_to_local: (atom, int) Hashtbl.t = Hashtbl.create 7
-
 (* Map from scope id + function id to debug id *)
 let scope_to_local: (int * int,int) Hashtbl.t = Hashtbl.create 7
 
@@ -476,20 +429,18 @@ let set_bitfield_offset str field offset underlying size =
         comp.ct_members in
     {comp with ct_members = members;})
 
-let atom_global_variable id atom =
-  try
-    let id,var = find_gvar_stamp id.stamp in
-    replace_var id ({var with gvar_atom = Some atom;});
-    Hashtbl.add atom_to_definition atom id
-  with Not_found -> ()
-
-let atom_function id atom =
+let atom_global id atom =
   try
-    let id',f = find_fun_stamp id.stamp in
-    replace_fun id' ({f with fun_atom = Some atom;});
-    Hashtbl.add atom_to_definition atom id';
-    Hashtbl.iter (fun (fid,sid) tid -> if fid = id.stamp then
-      Hashtbl.add atom_to_scope (atom,sid) tid) scope_to_local
+    let id' = (Hashtbl.find stamp_to_definition id.stamp) in
+    let g = Hashtbl.find definitions id' in
+    match g with
+    | Function f ->
+        replace_fun id' ({f with fun_atom = Some atom;});
+        Hashtbl.add atom_to_definition atom id';
+        Hashtbl.iter (fun (fid,sid) tid -> if fid = id.stamp then
+          Hashtbl.add atom_to_scope (atom,sid) tid) scope_to_local
+    | GlobalVariable var ->
+        replace_var id' ({var with gvar_atom = Some atom;})
   with Not_found -> ()
 
 let atom_parameter fid id atom =
@@ -509,8 +460,7 @@ let add_fun_addr atom (high,low) =
 let atom_local_variable id atom =
   try
     let id,var = find_lvar_stamp id.stamp in
-    replace_lvar id ({var with lvar_atom = Some atom;});
-    Hashtbl.add atom_to_local atom id
+    replace_lvar id ({var with lvar_atom = Some atom;})
   with Not_found -> ()
 
 let add_lvar_scope f_id var_id s_id =
@@ -582,21 +532,11 @@ 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_vars: atom list ref = ref []
-
 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 -> ()
 
@@ -611,7 +551,6 @@ let close_scope atom s_id lbl =
         | _ -> 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 -> ()
 
@@ -620,7 +559,6 @@ let start_live_range (f,v) lbl loc =
   match old_r with
   | RangeLoc old_r ->
       let n_r = { range_start = Some lbl; range_end = None; var_loc = loc } in
-      open_vars := v::!open_vars;
       Hashtbl.replace var_locations (f,v) (RangeLoc (n_r::old_r))
   | _ -> () (* Parameter that is passed as variable *)
 
@@ -638,28 +576,39 @@ let end_live_range (f,v) lbl =
 let stack_variable (f,v) (sp,loc) =
   Hashtbl.add var_locations (f,v) (FunctionLoc (sp,loc))
 
-let function_end atom loc =
-  IntSet.iter (fun id -> close_scope atom id loc) !open_scopes;
-  open_scopes := IntSet.empty;
-  List.iter (fun id-> end_live_range (atom,id) loc) !open_vars;
-  open_vars:= []
-
 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 addr3 =
+  let sec' = section_to_string sec in
+  Hashtbl.add compilation_section_start sec' addr3;
+  Hashtbl.add diab_additional sec' (addr1,add2,sec)
+
+let diab_add_fun_addr name _ addr = add_fun_addr name addr
+
+let gnu_add_fun_addr name sec (high,low) =
+  let sec = section_to_string sec in
+  if not (Hashtbl.mem compilation_section_start sec) then
+    Hashtbl.add compilation_section_start sec low;
+  Hashtbl.replace compilation_section_end sec high;
+  add_fun_addr name (high,low)
 
 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
 
@@ -690,7 +639,6 @@ let init name =
   Hashtbl.reset atom_to_definition;
   Hashtbl.reset local_variables;
   Hashtbl.reset stamp_to_local;
-  Hashtbl.reset atom_to_local;
   Hashtbl.reset scope_to_local;
   Hashtbl.reset atom_to_scope;
   Hashtbl.reset compilation_section_start;
@@ -701,4 +649,4 @@ let init name =
   Hashtbl.reset scope_ranges;
   Hashtbl.reset label_translation;
   all_files := StringSet.singleton name;
-  printed_vars := StringSet.empty;
+  printed_vars := StringSet.empty