Problems with Dwarf ranges (#159)

Merge of branch dwarf-ranges

9 files changed, 96 insertions, 56 deletions

diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 92d465d5..dd428808 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -40,6 +40,7 @@ module Printer(Target:TARGET) =
 
     let print_function oc name fn =
       Hashtbl.clear current_function_labels;
+      Debug.symbol_printed (extern_atom name);
       let (text, lit, jmptbl) = Target.get_section_names name in
       Target.section oc text;
       let alignment =
@@ -117,7 +118,7 @@ module Printer(Target:TARGET) =
       match v.gvar_init with
       | [] -> ()
       | _  ->
-          Debug.variable_printed (extern_atom name);
+          Debug.symbol_printed (extern_atom name);
           let sec =
             match C2C.atom_sections name with
             | [s] -> s
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index da8049a5..66b497cc 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -340,7 +340,6 @@ and unblock_block env ctx ploc = function
 
 let unblock_fundef env f =
   local_variables := [];
-  next_scope_id := 0;
   curr_fun_id:= f.fd_name.stamp;
   (* TODO: register the parameters as being declared in function scope *)
   let body = unblock_stmt env [] no_loc f.fd_body in
@@ -398,5 +397,6 @@ let rec unblock_glob env accu = function
 (* Entry point *)
 
 let program p =
+  next_scope_id := 0;
   {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
   unblock_glob (Builtins.environment()) [] p
diff --git a/debug/Debug.ml b/debug/Debug.ml
index 168df5a0..812f57cc 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -47,7 +47,7 @@ type implem =
       exists_section: section_name -> bool;
       remove_unused: ident -> unit;
       remove_unused_function: ident -> unit;
-      variable_printed: string -> unit;
+      symbol_printed: string -> unit;
       add_diab_info: section_name -> int -> int -> int -> unit;
    }
 
@@ -79,7 +79,7 @@ let default_implem =
    exists_section = (fun _ -> true);
    remove_unused = (fun _ -> ());
    remove_unused_function = (fun _ -> ());
-   variable_printed = (fun _ -> ());
+   symbol_printed = (fun _ -> ());
    add_diab_info = (fun _ _ _ _ -> ());
 }
 
@@ -111,5 +111,5 @@ let compute_diab_file_enum end_l entry_l line_e = !implem.compute_diab_file_enum
 let compute_gnu_file_enum f = !implem.compute_gnu_file_enum f
 let remove_unused ident = !implem.remove_unused ident
 let remove_unused_function ident = !implem.remove_unused_function ident
-let variable_printed ident = !implem.variable_printed ident
+let symbol_printed ident = !implem.symbol_printed ident
 let add_diab_info sec line_start debug_info low_pc = !implem.add_diab_info sec line_start debug_info low_pc
diff --git a/debug/Debug.mli b/debug/Debug.mli
index 3869a056..60e2f9bc 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -46,7 +46,7 @@ type implem =
      exists_section: section_name -> bool;
      remove_unused: ident -> unit;
      remove_unused_function: ident -> unit;
-     variable_printed: string -> unit;
+     symbol_printed: string -> unit;
      add_diab_info: section_name ->  int -> int -> int -> unit;
    }
 
@@ -80,5 +80,5 @@ 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 symbol_printed: string -> unit
 val add_diab_info: section_name ->  int -> int  -> int -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index e3f5d98e..21c2ad19 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -553,7 +553,10 @@ let close_scope atom s_id lbl =
         | a::rest -> a,rest
         | _ -> assert false (* We must have an opening scope *)
       end in
-    let new_r = ({last_r with end_addr = Some lbl;})::rest in
+    let new_r = if last_r.start_addr = Some lbl then
+        rest
+      else
+        ({last_r with end_addr = Some lbl;})::rest in
     Hashtbl.replace scope_ranges s_id new_r
   with Not_found -> ()
 
@@ -632,12 +635,12 @@ let compute_gnu_file_enum f =
 
 let all_files_iter f = StringSet.iter f !all_files
 
-let printed_vars: StringSet.t ref = ref StringSet.empty
+let printed_symbols: StringSet.t ref = ref StringSet.empty
 
-let is_variable_printed id = StringSet.mem id !printed_vars
+let is_symbol_printed id = StringSet.mem id !printed_symbols
 
-let variable_printed id =
-  printed_vars := StringSet.add id !printed_vars
+let symbol_printed id =
+  printed_symbols := StringSet.add id !printed_symbols
 
 let init name =
   id := 0;
@@ -660,7 +663,7 @@ let init name =
   Hashtbl.reset scope_ranges;
   Hashtbl.reset label_translation;
   all_files := StringSet.singleton name;
-  printed_vars := StringSet.empty
+  printed_symbols := StringSet.empty
 
 let default_debug =
   {
@@ -690,6 +693,6 @@ let default_debug =
    exists_section = exists_section;
    remove_unused = remove_unused;
    remove_unused_function = remove_unused_function;
-   variable_printed = variable_printed;
+   symbol_printed = symbol_printed;
    add_diab_info = (fun _ _ _ _ -> ());
  }
diff --git a/debug/DebugInformation.mli b/debug/DebugInformation.mli
index 8905d8bf..0cf34756 100644
--- a/debug/DebugInformation.mli
+++ b/debug/DebugInformation.mli
@@ -23,7 +23,7 @@ val get_type: int -> debug_types
 
 val fold_types: (int -> debug_types -> 'a -> 'a) -> 'a -> 'a
 
-val is_variable_printed: string -> bool
+val is_symbol_printed: string -> bool
 
 val variable_location: atom -> atom -> var_location
 
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index a45fff0c..c5df5637 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -244,6 +244,9 @@ module DwarfPrinter(Target: DWARF_TARGET):
     (* Mapping from abbreviation string to abbreviaton id *)
     let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7
 
+    (* Mapping from abbreviation range id to label *)
+    let range_labels : (int, int) Hashtbl.t = Hashtbl.create 7
+
     (* Look up the id of the abbreviation and add it if it is missing *)
     let get_abbrev entity has_sibling =
       let abbrev_string = abbrev_string_of_entity entity has_sibling in
@@ -439,8 +442,11 @@ module DwarfPrinter(Target: DWARF_TARGET):
       | Pc_pair (l,h) ->
           print_addr oc "DW_AT_low_pc" l;
           print_addr oc "DW_AT_high_pc" h
-      | Offset i -> fprintf oc "	.4byte		%a+0x%d%a\n"
-            label !debug_ranges_addr i print_comment "DW_AT_ranges"
+      | Offset i ->
+        let lbl = new_label () in
+        Hashtbl.add range_labels i lbl;
+        fprintf oc "	.4byte		%a%a\n"
+          label lbl print_comment "DW_AT_ranges"
       | _ -> ()
 
     let print_compilation_unit oc tag =
@@ -641,14 +647,23 @@ module DwarfPrinter(Target: DWARF_TARGET):
       end
 
     let print_ranges oc r =
+      let print_range_entry = function
+        | AddressRange l ->
+          List.iter (fun (b,e) ->
+              fprintf oc "	%s		%a\n" address label b;
+              fprintf oc "	%s		%a\n" address label e) l;
+        | OffsetRange (start, l) ->
+          List.iter (fun (b,e) ->
+              fprintf oc "	%s		%a-%a\n" address label b label start;
+              fprintf oc "	%s		%a-%a\n" address label e label start) l
+      in
       section oc Section_debug_ranges;
       print_label oc !debug_ranges_addr;
-      List.iter (fun l ->
-        List.iter (fun (b,e) ->
-          fprintf oc "	%s		%a\n" address label b;
-          fprintf oc "	%s		%a\n" address label e) l;
-        fprintf oc "	%s	0\n" address;
-        fprintf oc "	%s	0\n" address) r
+      List.iter (fun (lbl,l) ->
+          print_label oc (Hashtbl.find range_labels lbl);
+          print_range_entry l;
+          fprintf oc "	%s	0\n" address;
+          fprintf oc "	%s	0\n" address)  r
 
     let print_gnu_entries oc cp (lpc,loc) s r =
       compute_abbrev cp;
@@ -679,6 +694,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
     (* Print the debug info and abbrev section *)
     let print_debug oc debug =
       Hashtbl.clear abbrev_mapping;
+      Hashtbl.clear range_labels;
       Hashtbl.clear loc_labels;
       match debug with
       | Diab entries -> print_diab_entries oc entries
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 23aba448..5a2bce3b 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -272,9 +272,11 @@ type location_entry =
    }
 type dw_locations = constant option * location_entry list
 
-type range_entry = (address * address) list
+type range_entry =
+  | AddressRange  of (address * address) list
+  | OffsetRange of reference * (address * address) list
 
-type dw_ranges = range_entry list
+type dw_ranges = (int * range_entry) list
 
 type dw_string = (int * string) list
 
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index ee568042..50063df8 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -72,7 +72,9 @@ let up_locs acc loc =
   {acc with locs = loc@acc.locs;}
 
 let up_ranges acc r =
-  {acc with ranges = r;}
+  let off, old_r = acc.ranges in
+  let new_r = (off +1 ), (off, r):: old_r in
+  (Offset off), {acc with ranges = new_r;}
 
 let empty_accu =
   {
@@ -90,6 +92,8 @@ module Dwarfgenaux (Target: TARGET) =
 
     let subrange_type : int option ref = ref None
 
+    let current_section_start : int option ref = ref None
+
     let encoding_of_ikind = function
       | IBool -> DW_ATE_boolean
       | IChar ->
@@ -340,7 +344,7 @@ module Dwarfgenaux (Target: TARGET) =
 
     let global_variable_to_entry acc id v =
       let loc = match v.gvar_atom with
-      | Some a when is_variable_printed (extern_atom a) ->
+      | Some a when is_symbol_printed (extern_atom a) ->
           Some (LocSymbol a)
       | _ -> None in
       let var = {
@@ -424,7 +428,7 @@ module Dwarfgenaux (Target: TARGET) =
       let acc = up_locs (up_typs acc p.formal_parameter_type) loc_list in
       new_entry (next_id ()) (DW_TAG_formal_parameter p),acc
 
-    let scope_range f_id id (o,dwr) =
+    let scope_range f_id id acc =
       try
         let r = get_scope_ranges id in
         let lbl l h = match l,h with
@@ -435,19 +439,22 @@ module Dwarfgenaux (Target: TARGET) =
         | _ -> raise Not_found in
         begin
           match r with
-          | [] -> Empty,(o,dwr)
+          | [] -> Empty,acc
           | [a] ->
               let l,h = lbl a.start_addr a.end_addr in
-              Pc_pair (l,h),(o,dwr)
+              Pc_pair (l,h), acc
           | a::rest ->
               if !Clflags.option_gdwarf > 2 then
                 let r = List.map (fun e -> lbl e.start_addr e.end_addr) r in
-                (Offset o), (o + 2 + 4 * (List.length r),r::dwr)
-              else
+                let r = match !current_section_start with
+                  | None -> AddressRange r
+                  | Some s -> OffsetRange (s, r) in
+                up_ranges acc r
+             else
                 let l,h = lbl (List.hd (List.rev rest)).start_addr a.end_addr in
-                Pc_pair (l,h),(o,dwr)
+                Pc_pair (l,h), acc
         end
-      with Not_found -> Empty,(o,dwr)
+      with Not_found -> Empty, acc
 
     let rec local_variable_to_entry f_id acc v id =
       match v.lvar_atom with
@@ -466,11 +473,10 @@ module Dwarfgenaux (Target: TARGET) =
           Some (new_entry id (DW_TAG_variable var)),acc
 
     and scope_to_entry f_id acc sc id =
-      let r,dwr = scope_range f_id id acc.ranges in
+      let r, acc = scope_range f_id id acc in
       let scope = {
         lexical_block_range = r;
       } in
-      let acc = up_ranges acc dwr in
       let vars,acc = mmap_opt (local_to_entry  f_id) acc sc.scope_variables in
       let entry = new_entry id (DW_TAG_lexical_block scope) in
       add_children entry vars,acc
@@ -490,7 +496,7 @@ module Dwarfgenaux (Target: TARGET) =
           | Scope sc -> mmap_opt (local_to_entry f_id) acc sc.scope_variables
           | _ -> assert false)
 
-    let function_to_entry acc id f =
+    let function_to_entry sec_name acc id f =
       let r = match f.fun_low_pc, f.fun_high_pc with
       | Some l,Some h -> Pc_pair (l,h)
       | _ -> Empty in
@@ -503,8 +509,13 @@ module Dwarfgenaux (Target: TARGET) =
         subprogram_range = r;
       } in
       let f_id = get_opt_val f.fun_atom in
+      let start_sec =
+        try
+          Some (section_start (sec_name f_id))
+        with Not_found -> None in
+      current_section_start := start_sec;
       let acc = match f.fun_return_type with Some s -> up_typs acc s | None -> acc in
-      let f_entry =  new_entry id (DW_TAG_subprogram f_tag) in
+      let f_entry = new_entry id (DW_TAG_subprogram f_tag) in
       let children,acc =
         if !Clflags.option_gdepth > 1 then
           let params,acc = mmap (function_parameter_to_entry f_id) acc f.fun_parameter in
@@ -514,10 +525,14 @@ module Dwarfgenaux (Target: TARGET) =
           [],acc in
       add_children f_entry (children),acc
 
-    let definition_to_entry acc id t =
+    let definition_to_entry sec_name acc id t =
       match t with
-      | GlobalVariable g -> global_variable_to_entry acc id g
-      | Function f -> function_to_entry acc id f
+      | GlobalVariable g -> Some (global_variable_to_entry acc id g)
+      | Function f ->
+        if is_symbol_printed f.fun_name then
+          Some (function_to_entry sec_name acc id f)
+        else
+          None
 
   end
 
@@ -535,14 +550,15 @@ let prod_name =
   Printf.sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:(%s,%s,%s,%s)"
     version_string Configuration.arch Configuration.system Configuration.abi Configuration.model
 
-let diab_gen_compilation_section s defs acc =
+let diab_gen_compilation_section sec_name s defs acc =
   let module Gen = Dwarfgenaux(struct
     let file_loc = diab_file_loc s
     let string_entry s =  Simple_string s
   end) in
   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
+      match Gen.definition_to_entry sec_name bcc id t with
+      | Some (t,bcc) -> t::acc,bcc
+      | None -> acc,bcc) ([],empty_accu) defs in
   let low_pc = section_start s
   and line_start,debug_start = diab_additional_section s
   and high_pc = section_end s in
@@ -569,7 +585,7 @@ let gen_diab_debug_info sec_name var_section : debug_entries =
     | 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) StringMap.empty in
-  let entries = StringMap.fold diab_gen_compilation_section defs [] in
+  let entries = StringMap.fold (diab_gen_compilation_section sec_name) defs [] in
   Diab entries
 
 let gnu_file_loc (f,l) =
@@ -592,30 +608,32 @@ let gnu_string_entry s =
 
 let gen_gnu_debug_info sec_name var_section : debug_entries =
   Hashtbl.clear string_table;
-  let r,dwr,low_pc =
-    try if !Clflags.option_gdwarf > 3 then
+  let r,accu,low_pc =
+    try if !Clflags.option_gdwarf > 2 then
         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
+        | [] ->  Empty, empty_accu, None
+        | [(l,h)] ->   Pc_pair (l,h), empty_accu, Some l
+        | _ ->
+          let off, acc = up_ranges empty_accu (AddressRange pcs) in
+          off, acc, None
     else
         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 = up_ranges empty_accu dwr in
+        Pc_pair(l,h), empty_accu,Some l
+    with Not_found ->  Empty ,empty_accu, None in
   let module Gen = Dwarfgenaux (struct
     let file_loc = gnu_file_loc
     let string_entry = gnu_string_entry
   end) in
-  let defs,accu,sec = fold_definitions (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) ([],accu,StringSet.empty) in
+    match Gen.definition_to_entry sec_name bcc id t with
+    | Some (t,bcc) -> t::acc,bcc,StringSet.add s sec
+    | None -> acc, bcc, sec) ([],accu,StringSet.empty) in
   let types = Gen.gen_types accu.typs in
   let cp = {
     compile_unit_name = gnu_string_entry !file_name;