Starting to remove the seperate printers for each backend.

2 files changed, 105 insertions, 8 deletions

diff --git a/debug/DwarfDiab.ml b/debug/DwarfDiab.ml
new file mode 100644
index 00000000..a852053f
--- /dev/null
+++ b/debug/DwarfDiab.ml
@@ -0,0 +1,55 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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/DwarfAbbrvPrinter.ml b/debug/DwarfPrinter.ml
index 214484b6..81f36a24 100644
--- a/debug/DwarfAbbrvPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -14,15 +14,11 @@
 open DwarfTypes
 open DwarfUtil
 
-module type DWARF_ABBRV_DEFS =
+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 abbrv_section_start: out_channel -> unit
-      val abbrv_section_end: out_channel -> unit
-      val abbrv_prologue: out_channel -> int -> unit
-      val abbrv_epilogue: out_channel -> unit
       val get_abbrv_start_addr: unit -> int
       (* The form constants of the types *)
       val sibling_type_abbr: int
@@ -54,9 +50,9 @@ module type DWARF_ABBRV_DEFS =
       val bound_ref_type_abbr: int
     end
 
-module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) :
+module DwarfPrinter(Defs:DWARF_DEFS) :
     sig
-      val print_debug_abbrv: out_channel -> dw_entry -> unit
+      val print_debug: out_channel -> dw_entry -> unit
       val get_abbrv: dw_entry -> bool -> int
       val get_abbrv_start_addr: unit -> int
     end =
@@ -295,6 +291,25 @@ module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) :
         | None -> false
         | Some _ -> true in
         ignore (get_abbrv entry has_sib)) entry
+      
+    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 = 
+      fprintf oc "	.section	.debug_abbrev,,n\n";
+      fprintf oc "	.sleb128	0\n"
+        
+    let abbrv_prologue oc id = 
+      fprintf oc "	.section	.debug_abbrev,,n\n";
+      fprintf oc "	.uleb128	%d\n" id
+        
+    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
@@ -305,10 +320,37 @@ module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) :
         Defs.abbrv_epilogue oc) abbrvs;
       Defs.abbrv_section_end oc
 
+
+    let rec print_entry oc entry has_sibling =
+      ()
+
     let print_debug_abbrv oc entry =
       compute_abbrv entry;
       print_abbrv oc
 
-    let get_abbrv_start_addr = Defs.get_abbrv_start_addr
+    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)