Started integrating the debug printing in the common backend_printer.

10 files changed, 169 insertions, 160 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 62dd2bc2..7c8c373c 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -1122,6 +1122,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
     let print_epilogue oc = ()
 
     let default_falignment = 4
+
+    let get_start_addr () = -1 (* Dummy constant *)
+
+    let get_end_addr () = -1 (* Dummy constant *)
+
+    let get_stmt_list_addr () = -1 (* Dummy constant *)
   end
 
 let sel_target () = 
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index a6883339..a48bd910 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -15,6 +15,7 @@ open AST
 open Asm
 open Camlcoq
 open Datatypes
+open DwarfPrinter
 open PrintAsmaux
 open Printf
 open Sections
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 64db2cb0..aa0f4214 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -43,6 +43,9 @@ module type TARGET =
       val comment: string
       val symbol: out_channel -> P.t -> unit
       val default_falignment: int
+      val get_start_addr: unit -> int
+      val get_end_addr: unit -> int
+      val get_stmt_list_addr: unit -> int
     end
 
 (* On-the-fly label renaming *)
diff --git a/common/Sections.ml b/common/Sections.ml
index 086c860e..c0c95848 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -27,7 +27,7 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
-  | Section_debug
+  | Section_debug_info
   | Section_debug_abbrev
 
 type access_mode =
diff --git a/common/Sections.mli b/common/Sections.mli
index be716e48..e878b9e5 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -26,7 +26,7 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
-  | Section_debug
+  | Section_debug_info
   | Section_debug_abbrev
 
 type access_mode =
diff --git a/debug/DwarfDiab.ml b/debug/DwarfDiab.ml
deleted file mode 100644
index a852053f..00000000
--- a/debug/DwarfDiab.ml
+++ /dev/null
@@ -1,55 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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 Printf
-open DwarfPrinter
-open DwarfTypes
-open DwarfUtil
-
-module AbbrvPrinter = DwarfPrinter(struct
-  let string_of_byte value =
-    Printf.sprintf "	.byte	%s\n" (if value then "0x1" else "0x2")
-      
-  let string_of_abbrv_entry v =
-    Printf.sprintf "	.uleb128	%d\n" v
-
-  let sibling_type_abbr = dw_form_ref4
-  let decl_file_type_abbr = dw_form_data4
-  let decl_line_type_abbr = dw_form_udata
-  let type_abbr = dw_form_ref_addr
-  let name_type_abbr = dw_form_string
-  let encoding_type_abbr = dw_form_data1
-  let byte_size_type_abbr = dw_form_data1
-  let high_pc_type_abbr = dw_form_addr
-  let low_pc_type_abbr = dw_form_addr
-  let stmt_list_type_abbr = dw_form_data4
-  let declaration_type_abbr = dw_form_flag
-  let external_type_abbr = dw_form_flag
-  let prototyped_type_abbr = dw_form_flag
-  let bit_offset_type_abbr = dw_form_data1
-  let comp_dir_type_abbr = dw_form_string
-  let language_type_abbr = dw_form_udata
-  let producer_type_abbr = dw_form_string
-  let value_type_abbr = dw_form_sdata
-  let artificial_type_abbr = dw_form_flag
-  let variable_parameter_type_abbr = dw_form_flag
-  let bit_size_type_abbr = dw_form_data1
-  let location_const_type_abbr = dw_form_data4
-  let location_block_type_abbr = dw_form_block
-  let data_location_block_type_abbr = dw_form_block
-  let data_location_ref_type_abbr = dw_form_ref4
-  let bound_const_type_abbr = dw_form_udata
-  let bound_ref_type_abbr=dw_form_ref4
-      
-
-      
-end)
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 81f36a24..b3d554dc 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -13,81 +13,53 @@
 
 open DwarfTypes
 open DwarfUtil
+open Printf
 
-module type DWARF_DEFS =
-    sig
-      (* Functions used for the printing of the dwarf abbreviations *)
-      val string_of_byte: bool -> string
-      val string_of_abbrv_entry: int -> string
-      val get_abbrv_start_addr: unit -> int
-      (* The form constants of the types *)
-      val sibling_type_abbr: int
-      val decl_file_type_abbr: int
-      val decl_line_type_abbr: int
-      val type_abbr: int
-      val name_type_abbr: int
-      val encoding_type_abbr: int
-      val byte_size_type_abbr: int
-      val high_pc_type_abbr: int
-      val low_pc_type_abbr: int
-      val stmt_list_type_abbr: int
-      val declaration_type_abbr: int
-      val external_type_abbr: int
-      val prototyped_type_abbr: int
-      val bit_offset_type_abbr: int
-      val comp_dir_type_abbr: int
-      val language_type_abbr: int
-      val producer_type_abbr: int
-      val value_type_abbr: int
-      val artificial_type_abbr: int
-      val variable_parameter_type_abbr: int
-      val bit_size_type_abbr: int
-      val location_const_type_abbr: int
-      val location_block_type_abbr: int
-      val data_location_block_type_abbr: int
-      val data_location_ref_type_abbr: int
-      val bound_const_type_abbr: int
-      val bound_ref_type_abbr: int
-    end
-
-module DwarfPrinter(Defs:DWARF_DEFS) :
+module DwarfPrinter :
     sig
       val print_debug: out_channel -> dw_entry -> unit
-      val get_abbrv: dw_entry -> bool -> int
-      val get_abbrv_start_addr: unit -> int
     end =
-  (struct
-    
+  struct
+
+
+    module Defs = DefaultAbbrevs
+
+    let string_of_abbrv_entry v =
+      Printf.sprintf "	.uleb128	%d\n" v
+
+    let string_of_byte value =
+      Printf.sprintf "	.byte	%s\n" (if value then "0x1" else "0x2")
+
     let curr_abbrv = ref 0
 
     let next_abbrv =
       let abbrv = !curr_abbrv in
       incr curr_abbrv;abbrv
 
-    let abbrvs: (string * int) list ref = ref []
+    let abbrevs: (string * int) list ref = ref []
 
     let abbrv_mapping: (string,int) Hashtbl.t = Hashtbl.create 7
 
     let add_byte buf value =
-      Buffer.add_string buf (Defs.string_of_byte value)
+      Buffer.add_string buf (string_of_byte value)
 
     let add_abbr_uleb v buf =
-      Buffer.add_string buf (Defs.string_of_abbrv_entry v) 
+      Buffer.add_string buf (string_of_abbrv_entry v)
 
     let add_abbr_entry (v1,v2) buf =
       add_abbr_uleb v1 buf;
       add_abbr_uleb v2 buf
- 
+
     let add_sibling = add_abbr_entry (0x1,Defs.sibling_type_abbr)
-       
+
     let add_decl_file = add_abbr_entry (0x3a,Defs.decl_file_type_abbr)
- 
+
     let add_decl_line = add_abbr_entry (0x3b,Defs.decl_line_type_abbr)
-        
+
     let add_type = add_abbr_entry (0x49,Defs.type_abbr)
-   
+
     let add_name = add_abbr_entry (0x3,Defs.name_type_abbr)
-        
+
     let add_encoding = add_abbr_entry (0x3e,Defs.encoding_type_abbr)
 
     let add_byte_size = add_abbr_entry (0xb,Defs.byte_size_type_abbr)
@@ -97,7 +69,7 @@ module DwarfPrinter(Defs:DWARF_DEFS) :
     let add_low_pc = add_abbr_entry (0x11,Defs.low_pc_type_abbr)
 
     let add_stmt_list = add_abbr_entry (0x10,Defs.stmt_list_type_abbr)
-        
+
     let add_declaration = add_abbr_entry (0x3c,Defs.declaration_type_abbr)
 
     let add_external = add_abbr_entry (0x3f,Defs.external_type_abbr)
@@ -120,13 +92,13 @@ module DwarfPrinter(Defs:DWARF_DEFS) :
 
     let add_bit_size = add_abbr_entry (0xc,Defs.bit_size_type_abbr)
 
-    let add_location loc buf = 
+    let add_location loc buf =
       match loc with
       | None -> ()
       | Some (LocConst _) -> add_abbr_entry (0x2,Defs.location_const_type_abbr) buf
       | Some (LocBlock _) -> add_abbr_entry (0x2,Defs.location_block_type_abbr) buf
 
-    let add_data_location loc buf = 
+    let add_data_location loc buf =
       match loc with
       | None -> ()
       | Some (DataLocBlock __) -> add_abbr_entry (0x38,Defs.data_location_block_type_abbr) buf
@@ -149,10 +121,10 @@ module DwarfPrinter(Defs:DWARF_DEFS) :
         | _ -> true in
         add_abbr_uleb id buf;
         add_byte buf has_child;
-        if has_sibling then add_sibling buf; 
-      in     
+        if has_sibling then add_sibling buf;
+      in
       (match entity.tag with
-      | DW_TAG_array_type e -> 
+      | DW_TAG_array_type e ->
           prologue 0x1;
           add_attr_some e.array_type_decl_file add_decl_file;
           add_attr_some e.array_type_decl_line add_decl_line;
@@ -281,44 +253,45 @@ module DwarfPrinter(Defs:DWARF_DEFS) :
         Hashtbl.find abbrv_mapping abbrv_string
       with Not_found ->
         let id = next_abbrv in
-        abbrvs:=(abbrv_string,id)::!abbrvs;
+        abbrevs:=(abbrv_string,id)::!abbrevs;
         Hashtbl.add abbrv_mapping abbrv_string id;
         id)
 
     let compute_abbrv entry =
       entry_iter_sib (fun sib entry ->
-        let has_sib = match sib with 
+        let has_sib = match sib with
         | None -> false
         | Some _ -> true in
         ignore (get_abbrv entry has_sib)) entry
-      
-    let abbrv_section_start oc = 
+
+    let abbrv_section_start oc =
       fprintf oc "	.section	.debug_abbrev,,n\n"(* ; *)
         (* let lbl = new_label () in *)
         (* abbrv_start_addr := lbl; *)
         (* fprintf oc "%a:\n" label lbl *)
-        
-    let abbrv_section_end oc = 
+
+    let abbrv_section_end oc =
       fprintf oc "	.section	.debug_abbrev,,n\n";
       fprintf oc "	.sleb128	0\n"
-        
-    let abbrv_prologue oc id = 
+
+    let abbrv_prologue oc id =
       fprintf oc "	.section	.debug_abbrev,,n\n";
       fprintf oc "	.uleb128	%d\n" id
-        
-    let abbrv_epilogue oc = 
+
+    let abbrv_epilogue oc =
       fprintf oc "	.uleb128	0\n";
       fprintf oc "	.uleb128	0\n"
 
 
-    let print_abbrv oc =
-      let abbrvs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) !abbrvs in
-      Defs.abbrv_section_start oc;
+    let print_abbrv occ =
+      let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) !abbrevs in
+      ()
+      (*Defs.abbrv_section_start oc;
       List.iter (fun (s,id) ->
         Defs.abbrv_prologue oc id;
         output_string oc s;
         Defs.abbrv_epilogue oc) abbrvs;
-      Defs.abbrv_section_end oc
+      Defs.abbrv_section_end oc*)
 
 
     let rec print_entry oc entry has_sibling =
@@ -329,28 +302,23 @@ module DwarfPrinter(Defs:DWARF_DEFS) :
       print_abbrv oc
 
     let print_debug_info oc entry =
-      print_debug_abbrv oc entry;
-      let abbrv_start =  DwarfDiab.AbbrvPrinter.get_abbrv_start_addr () in
-      let debug_start = new_label () in
-      let print_info () =
-        fprintf oc"	.section	.debug_info,,n\n" in
-      print_info ();
-      fprintf oc "%a\n" label debug_start;
-      let debug_length_start = new_label () in (* Address used for length calculation *)
-      let debug_end = new_label () in
-      fprintf oc "	.4byte	%a-%a\n" label debug_end label debug_length_start;
-      fprintf oc "%a\n" label debug_length_start;
-      fprintf oc "	.2byte	0x2\n"; (* Dwarf version *)
-      fprintf oc "	.4byte	%a\n" label abbrv_start; (* Offset into the abbreviation *)
-      fprintf oc "	.byte	%X\n" !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *)
-      print_entry oc entry false;
-      fprintf oc "%a\n" label debug_end; (* End of the debug section *)
-      fprintf oc "	.sleb128	0\n"
-    
-      
-    let abbrv_start_addr = ref (-1)
-        
-    let get_abbrv_start_addr () = !abbrv_start_addr
-      
-
-  end)
+      print_debug_abbrv oc entry
+      (* (\* let abbrv_start =  DwarfDiab.AbbrvPrinter.get_abbrv_start_addr () in *\) *)
+      (* (\* let debug_start = new_label () in *\) *)
+      (* let print_info () = *)
+      (*   fprintf oc"	.section	.debug_info,,n\n" in *)
+      (* print_info (); *)
+      (* fprintf oc "%a\n" label debug_start; *)
+      (* let debug_length_start = new_label () in (\* Address used for length calculation *\) *)
+      (* let debug_end = new_label () in *)
+      (* fprintf oc "	.4byte	%a-%a\n" label debug_end label debug_length_start; *)
+      (* fprintf oc "%a\n" label debug_length_start; *)
+      (* fprintf oc "	.2byte	0x2\n"; (\* Dwarf version *\) *)
+      (* fprintf oc "	.4byte	%a\n" label abbrv_start; (\* Offset into the abbreviation *\) *)
+      (* fprintf oc "	.byte	%X\n" !Machine.config.Machine.sizeof_ptr; (\* Sizeof pointer type *\) *)
+      (* print_entry oc entry false; *)
+      (* fprintf oc "%a\n" label debug_end; (\* End of the debug section *\) *)
+      (* fprintf oc "	.sleb128	0\n" *)
+
+      let print_debug _ _ = failwith "TODO implement"
+  end
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index 79516e65..cc1f267d 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -16,7 +16,7 @@ open DwarfTypes
 
 let id = ref 0
 
-let next_id () = 
+let next_id () =
   let nid = !id in
   incr id; nid
 
@@ -27,7 +27,7 @@ let reset_id () =
 let type_table: (string, int) Hashtbl.t = Hashtbl.create 7
 
 (* Clear the type map *)
-let reset_type_table () = 
+let reset_type_table () =
   Hashtbl.clear type_table
 
 (* Generate a new entry from a given tag *)
@@ -86,3 +86,34 @@ let dw_form_ref4     = 0x13
 let dw_form_ref8     = 0x14
 let dw_ref_udata     = 0x15
 let dw_ref_indirect  = 0x16
+
+module DefaultAbbrevs =
+  struct
+    let sibling_type_abbr = dw_form_ref4
+    let decl_file_type_abbr = dw_form_data4
+    let decl_line_type_abbr = dw_form_udata
+    let type_abbr = dw_form_ref_addr
+    let name_type_abbr = dw_form_string
+    let encoding_type_abbr = dw_form_data1
+    let byte_size_type_abbr = dw_form_data1
+    let high_pc_type_abbr = dw_form_addr
+    let low_pc_type_abbr = dw_form_addr
+    let stmt_list_type_abbr = dw_form_data4
+    let declaration_type_abbr = dw_form_flag
+    let external_type_abbr = dw_form_flag
+    let prototyped_type_abbr = dw_form_flag
+    let bit_offset_type_abbr = dw_form_data1
+    let comp_dir_type_abbr = dw_form_string
+    let language_type_abbr = dw_form_udata
+    let producer_type_abbr = dw_form_string
+    let value_type_abbr = dw_form_sdata
+    let artificial_type_abbr = dw_form_flag
+    let variable_parameter_type_abbr = dw_form_flag
+    let bit_size_type_abbr = dw_form_data1
+    let location_const_type_abbr = dw_form_data4
+    let location_block_type_abbr = dw_form_block
+    let data_location_block_type_abbr = dw_form_block
+    let data_location_ref_type_abbr = dw_form_ref4
+    let bound_const_type_abbr = dw_form_udata
+    let bound_ref_type_abbr=dw_form_ref4
+  end
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 39f8be23..cc16890c 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -970,6 +970,13 @@ module Target(System: SYSTEM):TARGET =
     let comment = comment
 
     let default_falignment = 16
+
+    let get_start_addr () = -1 (* Dummy constant *)
+        
+    let get_end_addr () = -1 (* Dummy constant *)
+
+    let get_stmt_list_addr () = -1 (* Dummy constant *)
+
 end
 
 let sel_target () =
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 70aec6c0..90e9b880 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -38,6 +38,7 @@ module type SYSTEM =
       val cfi_adjust: out_channel -> int32 -> unit
       val cfi_rel_offset: out_channel -> string -> int32 -> unit
       val print_prologue: out_channel -> unit
+      val print_epilogue: out_channel -> unit
     end
 
 let symbol = elf_symbol
@@ -68,6 +69,14 @@ let float_reg_name = function
   | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27"
   | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31"
 
+let start_addr = ref (-1)
+
+let end_addr = ref (-1)
+
+let stmt_list_addr = ref (-1)
+
+let label = elf_label
+
 module Linux_System : SYSTEM =
   struct
 
@@ -117,6 +126,9 @@ module Linux_System : SYSTEM =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\",\"a%s%s\",@progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
+      | Section_debug_info -> ".debug_info,\"\",@progbits"
+      | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits"
+
 
     let print_file_line oc file line =
       PrintAnnot.print_file_line oc comment file line
@@ -131,6 +143,8 @@ module Linux_System : SYSTEM =
     let cfi_rel_offset = cfi_rel_offset
 
     let print_prologue oc = ()
+
+    let print_epilogue oc = ()
   
   end
     
@@ -182,9 +196,11 @@ module Diab_System : SYSTEM =
             | true, false -> 'd'                (* data *)
             | false, true -> 'c'                (* text *)
             | false, false -> 'r')              (* const *)
+      | Section_debug_info -> ".debug_info,,n"
+      | Section_debug_abbrev -> ".debug_abbrev,,n"
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line_d1 oc comment file line
+      PrintAnnot.print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
     let cfi_startproc oc = ()
@@ -198,8 +214,35 @@ module Diab_System : SYSTEM =
     let print_prologue oc =
       fprintf oc "	.xopt	align-fill-text=0x60000000\n";
       if !Clflags.option_g then
-        fprintf oc "	.xopt	asm-debug-on\n"
-  
+        begin
+          fprintf oc "	.text\n";
+          fprintf oc "	.section	.debug_line,,n\n";
+          let label_line_start = new_label () in
+          stmt_list_addr := label_line_start;
+          fprintf oc "%a:\n" label label_line_start;
+          fprintf oc "	.text\n";
+          let label_start = new_label () in
+          start_addr := label_start;
+          fprintf oc "%a:\n" label label_start;
+          fprintf oc "	.d2_line_start	.debug_line\n";
+        end
+
+    let filenum : (string,int) Hashtbl.t = Hashtbl.create 7
+
+    let print_epilogue oc =
+      if !Clflags.option_g then
+        begin
+          fprintf oc "\n";
+          let label_end = new_label () in
+          end_addr := label_end;
+          fprintf oc "%a:\n" label label_end;
+          fprintf oc "	.text\n";
+          Hashtbl.iter (fun file _ ->
+            let label = new_label () in
+            Hashtbl.add filenum file label;
+            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) PrintAnnot.filename_info;
+          fprintf oc "	.d2_line_end\n"
+        end
   end
 
 module Target (System : SYSTEM):TARGET =
@@ -212,7 +255,7 @@ module Target (System : SYSTEM):TARGET =
     let raw_symbol oc s =
       fprintf oc "%s" s
 
-    let label = elf_label
+    let label = label
 
     let label_low oc lbl =
       fprintf oc ".L%d@l" lbl
@@ -726,8 +769,6 @@ module Target (System : SYSTEM):TARGET =
     let print_align oc align  =
       fprintf oc "	.balign	%d\n" align
 
-    let print_epilogue _ = ()
-
     let print_jumptable oc jmptbl = 
       let print_jumptable oc (lbl, tbl) =
         fprintf oc "%a:" label lbl;
@@ -742,6 +783,13 @@ module Target (System : SYSTEM):TARGET =
       end
 
     let default_falignment = 4
+        
+    let get_start_addr () = !start_addr
+
+    let get_end_addr () = !end_addr
+
+    let get_stmt_list_addr () = !stmt_list_addr
+
   end
 
 let sel_target () =