Starting to remove the seperate printers for each backend.

9 files changed, 432 insertions, 276 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 7f511912..582b70e7 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -177,6 +177,8 @@ let name_of_section = function
   | 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 -> sprintf ".section	.debug_info,\"\",@progbits"
+  | Section_debug_abbrev -> sprintf ".section	.debug_abbrev,\"\",@progbits"
 
 let section oc sec =
   fprintf oc "	%s\n" (name_of_section sec)
diff --git a/common/Sections.ml b/common/Sections.ml
index c6d4c4c2..086c860e 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -27,6 +27,8 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
+  | Section_debug
+  | Section_debug_abbrev
 
 type access_mode =
   | Access_default
diff --git a/common/Sections.mli b/common/Sections.mli
index 38b99db0..be716e48 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -26,6 +26,8 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
+  | Section_debug
+  | Section_debug_abbrev
 
 type access_mode =
   | Access_default
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)
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index b0ef0180..c77347da 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -98,6 +98,8 @@ module Cygwin_System =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\", \"%s\"\n"
             s (if ex then "xr" else if wr then "d" else "dr")
+      | Section_debug -> ".section	.debug_info,\"\""
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\""
 
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
 
@@ -147,7 +149,10 @@ module ELF_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 -> sprintf ".section	.debug_info,\"\",@progbits"
+      | Section_debug_abbrev -> sprintf ".section	.debug_abbrev,\"\",@progbits"
             
+
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
                     
     let print_align oc n =
@@ -201,6 +206,8 @@ module MacOS_System =
           sprintf ".section	\"%s\", %s, %s"
             (if wr then "__DATA" else "__TEXT") s
             (if ex then "regular, pure_instructions" else "regular")
+      | Section_debug -> ".section	__DWARF,__debug_info,regular,debug"
+      | Section_debug_abbrev -> ".section	__DWARF,__debug_abbrev,regular,debug"
     
     let stack_alignment =  16 (* mandatory *)
          
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 8a064d52..77eb2378 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -20,16 +20,263 @@ open Sections
 open AST
 open Memdata
 open Asm
-open PrintUtil
-open PrintLinux
-open PrintDiab
+
+(* Recognition of target ABI and asm syntax *)
+
+module type SYSTEM =
+    sig
+      val comment: string
+      val constant: out_channel -> constant -> unit
+      val ireg: out_channel -> ireg -> unit
+      val freg: out_channel -> freg -> unit
+      val creg: out_channel -> int -> unit
+      val name_of_section: section_name -> string
+      val print_file_line: out_channel -> string -> int -> unit
+      val cfi_startproc: out_channel -> unit
+      val cfi_endproc: out_channel -> unit
+      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 *)
+      (* val print_addr_label: out_channel -> int -> unit *)
+      (* val set_compilation_unit_addrs: int -> int -> unit *)
+    end
+
+let symbol oc symb =
+  fprintf oc "%s" (extern_atom symb)
+
+let symbol_offset oc (symb, ofs) =
+  symbol oc symb;
+  if ofs <> 0l then fprintf oc " + %ld" ofs
+
+let symbol_fragment oc s n op =
+      fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op
+
+
+let int_reg_name = function
+  | GPR0 -> "0"  | GPR1 -> "1"  | GPR2 -> "2"  | GPR3 -> "3"
+  | GPR4 -> "4"  | GPR5 -> "5"  | GPR6 -> "6"  | GPR7 -> "7"
+  | GPR8 -> "8"  | GPR9 -> "9"  | GPR10 -> "10" | GPR11 -> "11"
+  | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15"
+  | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19"
+  | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23"
+  | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27"
+  | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31"
+
+let float_reg_name = function
+  | FPR0 -> "0"  | FPR1 -> "1"  | FPR2 -> "2"  | FPR3 -> "3"
+  | FPR4 -> "4"  | FPR5 -> "5"  | FPR6 -> "6"  | FPR7 -> "7"
+  | FPR8 -> "8"  | FPR9 -> "9"  | FPR10 -> "10" | FPR11 -> "11"
+  | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15"
+  | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19"
+  | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23"
+  | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27"
+  | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31"
+
+module Linux_System : SYSTEM =
+  struct
+    let comment =  "#"
+
+    let constant oc cst =
+      match cst with
+      | Cint n ->
+          fprintf oc "%ld" (camlint_of_coqint n)
+      | Csymbol_low(s, n) ->
+          symbol_fragment oc s n "@l"
+      | Csymbol_high(s, n) ->
+          symbol_fragment oc s n "@ha"
+      | Csymbol_sda(s, n) ->
+          symbol_fragment oc s n "@sda21"
+            (* 32-bit relative addressing is supported by the Diab tools but not by
+               GNU binutils.  In the latter case, for testing purposes, we treat
+               them as absolute addressings.  The default base register being GPR0,
+               this produces correct code, albeit with absolute addresses. *)
+      | Csymbol_rel_low(s, n) ->
+          symbol_fragment oc s n "@l"
+      | Csymbol_rel_high(s, n) ->
+          symbol_fragment oc s n "@ha"
+
+    let ireg oc r =
+      output_string oc (int_reg_name r)
+
+    let freg oc r =
+      output_string oc (float_reg_name r)
+        
+    let creg oc r = 
+      fprintf oc "%d" r
+ 
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data i ->
+          if i then ".data" else "COMM"
+      | Section_small_data i -> 
+          if i then ".section	.sdata,\"aw\",@progbits" else "COMM"
+      | Section_const i ->
+          if i then ".rodata" else "COMM"
+      | Section_small_const i ->
+          if i then ".section	.sdata2,\"a\",@progbits" else "COMM"
+      | Section_string -> ".rodata"
+      | Section_literal -> ".section	.rodata.cst8,\"aM\",@progbits,8"
+      | Section_jumptable -> ".text"
+      | 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 -> sprintf ".section	.debug_info,\"\",@progbits"
+      | Section_debug_abbrev -> sprintf ".section	.debug_abbrev,\"\",@progbits"
+
+    let print_file_line oc file line =
+      PrintAnnot.print_file_line oc comment file line
+    
+    (* Emit .cfi directives *)      
+    let cfi_startproc =
+      if Configuration.asm_supports_cfi then
+        (fun oc -> fprintf oc "	.cfi_startproc\n")
+      else
+        (fun _ -> ())
+
+    let cfi_endproc =
+      if Configuration.asm_supports_cfi then
+        (fun oc -> fprintf oc "	.cfi_endproc\n")
+      else
+        (fun _ -> ())
+
+              
+    let cfi_adjust =
+      if Configuration.asm_supports_cfi then
+       (fun oc delta -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta)
+      else
+        (fun _ _ -> ())
+              
+    let cfi_rel_offset =
+      if Configuration.asm_supports_cfi then
+        (fun oc reg ofs -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs)
+      else
+        (fun _ _ _ -> ())
+
+
+    let print_prologue oc = ()
+  
+  end
+    
+module Diab_System : SYSTEM =
+  struct
+    let comment =  ";"
+        
+    let constant oc cst =
+      match cst with
+      | Cint n ->
+          fprintf oc "%ld" (camlint_of_coqint n)
+      | Csymbol_low(s, n) ->
+          symbol_fragment oc s n "@l"
+      | Csymbol_high(s, n) ->
+          symbol_fragment oc s n "@ha"
+      | Csymbol_sda(s, n) ->
+          symbol_fragment oc s n "@sdarx"
+      | Csymbol_rel_low(s, n) ->
+          symbol_fragment oc s n "@sdax@l"
+      | Csymbol_rel_high(s, n) ->
+          symbol_fragment oc s n "@sdarx@ha"
+ 
+    let ireg oc r =
+      output_char oc 'r';
+      output_string oc (int_reg_name r)
+
+    let freg oc r =
+      output_char oc 'f';
+      output_string oc (float_reg_name r)
+        
+    let creg oc r =
+      fprintf oc "cr%d" r
+        
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data i -> if i then ".data" else "COMM"
+      | Section_small_data i -> if i then ".sdata" else ".sbss"
+      | Section_const _ -> ".text"
+      | Section_small_const _ -> ".sdata2"
+      | Section_string -> ".text"
+      | Section_literal -> ".text"
+      | Section_jumptable -> ".text"
+      | Section_user(s, wr, ex) ->
+          sprintf ".section	\"%s\",,%c"
+               s
+            (match wr, ex with
+            | true, true -> 'm'                 (* text+data *)
+            | true, false -> 'd'                (* data *)
+            | false, true -> 'c'                (* text *)
+            | false, false -> 'r')              (* const *)
+      | Section_debug -> ".section	.debug_info,,n"
+      | Section_debug_abbrev -> ".section	.debug_abbrev,,n"
+
+    let print_file_line oc file line =
+      PrintAnnot.print_file_line_d2 oc comment file line
+
+    (* Emit .cfi directives *)
+    let cfi_startproc oc = ()
+
+    let cfi_endproc oc = ()
+
+    let cfi_adjust oc delta = ()
+
+    let cfi_rel_offset oc reg ofs = ()
+        
+    let print_prologue oc =
+      fprintf oc "	.xopt	align-fill-text=0x60000000\n";
+      if !Clflags.option_g then
+        fprintf oc "	.xopt	asm-debug-on\n"
+  
+  end
 
 module AsmPrinter (Target : SYSTEM) =
   struct
     include Target
 
+(* On-the-fly label renaming *)
+
+let next_label = ref 100
+
+let new_label() =
+  let lbl = !next_label in incr next_label; lbl
+
+let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
+
+let transl_label lbl =
+  try
+    Hashtbl.find current_function_labels lbl
+  with Not_found ->
+    let lbl' = new_label() in
+    Hashtbl.add current_function_labels lbl lbl';
+    lbl'
+
 (* Basic printing functions *)
 
+let coqint oc n =
+  fprintf oc "%ld" (camlint_of_coqint n)
+
+let raw_symbol oc s =
+  fprintf oc "%s" s
+
+
+let label oc lbl =
+  fprintf oc ".L%d" lbl
+
+let label_low oc lbl =
+  fprintf oc ".L%d@l" lbl
+
+let label_high oc lbl =
+  fprintf oc ".L%d@ha" lbl
+
+
+let num_crbit = function
+  | CRbit_0 -> 0
+  | CRbit_1 -> 1
+  | CRbit_2 -> 2
+  | CRbit_3 -> 3
+  | CRbit_6 -> 6
+
+let crbit oc bit =
+  fprintf oc "%d" (num_crbit bit)
+
 let ireg_or_zero oc r =
   if r = GPR0 then output_string oc "0" else ireg oc r
 
@@ -46,8 +293,29 @@ let section oc sec =
 let print_location oc loc =
   if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
 
+(* Encoding masks for rlwinm instructions *)
+
+let rolm_mask n =
+  let mb = ref 0       (* location of last 0->1 transition *)
+  and me = ref 32      (* location of last 1->0 transition *)
+  and last = ref ((Int32.logand n 1l) <> 0l)  (* last bit seen *)
+  and count = ref 0    (* number of transitions *)
+  and mask = ref 0x8000_0000l in
+  for mx = 0 to 31 do
+    if Int32.logand n !mask <> 0l then
+      if !last then () else (incr count; mb := mx; last := true)
+    else
+      if !last then (incr count; me := mx; last := false) else ();
+    mask := Int32.shift_right_logical !mask 1
+  done;
+  if !me = 0 then me := 32;
+  assert (!count = 2 || (!count = 0 && !last));
+  (!mb, !me-1)
+
 (* Handling of annotations *)
 
+let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
+
 let print_annot_stmt oc txt targs args =
   if Str.string_match re_file_line txt 0 then begin
     print_file_line oc (Str.matched_group 1 txt)
@@ -57,6 +325,14 @@ let print_annot_stmt oc txt targs args =
     PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
   end
 
+(* Determine if the displacement of a conditional branch fits the short form *)
+
+let short_cond_branch tbl pc lbl_dest =
+  match PTree.get lbl_dest tbl with
+  | None -> assert false
+  | Some pc_dest -> 
+      let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000
+
 (* Printing of instructions *)
 
 let float_literals : (int * int64) list ref = ref []
@@ -388,6 +664,37 @@ let print_instruction oc tbl pc fallthrough = function
   | Pcfi_rel_offset n ->
       cfi_rel_offset oc "lr" (camlint_of_coqint n)
 
+(* Determine if an instruction falls through *)
+
+let instr_fall_through = function
+  | Pb _ -> false
+  | Pbctr _ -> false
+  | Pbs _ -> false
+  | Pblr -> false
+  | _ -> true
+
+(* Estimate the size of an Asm instruction encoding, in number of actual
+   PowerPC instructions.  We can over-approximate. *)
+
+let instr_size = function
+  | Pbf(bit, lbl) -> 2
+  | Pbt(bit, lbl) -> 2
+  | Pbtbl(r, tbl) -> 5
+  | Plfi(r1, c) -> 2
+  | Plfis(r1, c) -> 2
+  | Plabel lbl -> 0
+  | Pbuiltin(ef, args, res) -> 0
+  | Pannot(ef, args) -> 0
+  | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
+  | _ -> 1
+
+(* Build a table label -> estimated position in generated code.
+   Used to predict if relative conditional branches can use the short form. *)
+
+let rec label_positions tbl pc = function
+  | [] -> tbl
+  | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c
+  | i :: c -> label_positions tbl (pc + instr_size i) c
 
 (* Emit a sequence of instructions *)
 
@@ -540,9 +847,9 @@ let print_program oc p =
   | Linux -> (module Linux_System:SYSTEM)
   | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in
   let module Printer = AsmPrinter(Target) in
-  Printer.set_compilation_unit_addrs 1 2; (* TODO This is dummy code *)
+  (* Printer.set_compilation_unit_addrs 1 2; (\* TODO This is dummy code *\) *)
   PrintAnnot.reset_filenames();
   PrintAnnot.print_version_and_options oc Printer.comment;
   Printer.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
-  Printer.print_epilogue oc
+  (* Printer.print_epilogue oc *)
diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml
index e431a8c7..61a4eff9 100644
--- a/powerpc/PrintDiab.ml
+++ b/powerpc/PrintDiab.ml
@@ -16,7 +16,7 @@ open Printf
 open Datatypes
 open DwarfTypes
 open DwarfUtil
-open DwarfAbbrvPrinter
+open DwarfPrinter
 open Camlcoq
 open Sections
 open Asm
@@ -145,87 +145,6 @@ module Diab_System =
           fprintf oc "	.d2_line_end\n";
         end
 
-    module AbbrvPrinter = DwarfAbbrvPrinter(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 abbrv_start_addr = ref (-1)
-
-        let get_abbrv_start_addr () = !abbrv_start_addr
-
-        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
-
-
-        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"
-
-      end)
-
-    let rec print_entry oc entry has_sibling =
-      ()
-
-    let print_debug_info oc entry =
-      AbbrvPrinter.print_debug_abbrv oc entry;
-      let abbrv_start = 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"
-    
+
 
   end:SYSTEM)
diff --git a/powerpc/PrintUtil.ml b/powerpc/PrintUtil.ml
deleted file mode 100644
index e007b273..00000000
--- a/powerpc/PrintUtil.ml
+++ /dev/null
@@ -1,180 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Common functions for the AsmPrinter *)
-
-open Printf
-open Maps
-open Camlcoq
-open Sections
-open Asm
-
-(* Recognition of target ABI and asm syntax *)
-
-module type SYSTEM =
-    sig
-      val comment: string
-      val constant: out_channel -> constant -> unit
-      val ireg: out_channel -> ireg -> unit
-      val freg: out_channel -> freg -> unit
-      val creg: out_channel -> int -> unit
-      val name_of_section: section_name -> string
-      val print_file_line: out_channel -> string -> int -> unit
-      val cfi_startproc: out_channel -> unit
-      val cfi_endproc: out_channel -> unit
-      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
-      val print_addr_label: out_channel -> int -> unit
-      val set_compilation_unit_addrs: int -> int -> unit
-    end
-
-let symbol oc symb =
-  fprintf oc "%s" (extern_atom symb)
-
-let symbol_offset oc (symb, ofs) =
-  symbol oc symb;
-  if ofs <> 0l then fprintf oc " + %ld" ofs
-
-let symbol_fragment oc s n op =
-      fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op
-
-
-let int_reg_name = function
-  | GPR0 -> "0"  | GPR1 -> "1"  | GPR2 -> "2"  | GPR3 -> "3"
-  | GPR4 -> "4"  | GPR5 -> "5"  | GPR6 -> "6"  | GPR7 -> "7"
-  | GPR8 -> "8"  | GPR9 -> "9"  | GPR10 -> "10" | GPR11 -> "11"
-  | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15"
-  | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19"
-  | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23"
-  | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27"
-  | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31"
-
-let float_reg_name = function
-  | FPR0 -> "0"  | FPR1 -> "1"  | FPR2 -> "2"  | FPR3 -> "3"
-  | FPR4 -> "4"  | FPR5 -> "5"  | FPR6 -> "6"  | FPR7 -> "7"
-  | FPR8 -> "8"  | FPR9 -> "9"  | FPR10 -> "10" | FPR11 -> "11"
-  | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15"
-  | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19"
-  | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23"
-  | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27"
-  | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31"
-
-(* On-the-fly label renaming *)
-
-let next_label = ref 100
-
-let new_label() =
-  let lbl = !next_label in incr next_label; lbl
-
-let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
-
-let transl_label lbl =
-  try
-    Hashtbl.find current_function_labels lbl
-  with Not_found ->
-    let lbl' = new_label() in
-    Hashtbl.add current_function_labels lbl lbl';
-    lbl'
-
-(* Basic printing functions *)
-
-let coqint oc n =
-  fprintf oc "%ld" (camlint_of_coqint n)
-
-let raw_symbol oc s =
-  fprintf oc "%s" s
-
-
-let label oc lbl =
-  fprintf oc ".L%d" lbl
-
-let label_low oc lbl =
-  fprintf oc ".L%d@l" lbl
-
-let label_high oc lbl =
-  fprintf oc ".L%d@ha" lbl
-
-let num_crbit = function
-  | CRbit_0 -> 0
-  | CRbit_1 -> 1
-  | CRbit_2 -> 2
-  | CRbit_3 -> 3
-  | CRbit_6 -> 6
-
-let crbit oc bit =
-  fprintf oc "%d" (num_crbit bit)
-
-
-(* Encoding masks for rlwinm instructions *)
-
-let rolm_mask n =
-  let mb = ref 0       (* location of last 0->1 transition *)
-  and me = ref 32      (* location of last 1->0 transition *)
-  and last = ref ((Int32.logand n 1l) <> 0l)  (* last bit seen *)
-  and count = ref 0    (* number of transitions *)
-  and mask = ref 0x8000_0000l in
-  for mx = 0 to 31 do
-    if Int32.logand n !mask <> 0l then
-      if !last then () else (incr count; mb := mx; last := true)
-    else
-      if !last then (incr count; me := mx; last := false) else ();
-    mask := Int32.shift_right_logical !mask 1
-  done;
-  if !me = 0 then me := 32;
-  assert (!count = 2 || (!count = 0 && !last));
-  (!mb, !me-1)
-
-(* Handling of annotations *)
-
-let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
-
-(* Determine if the displacement of a conditional branch fits the short form *)
-
-let short_cond_branch tbl pc lbl_dest =
-  match PTree.get lbl_dest tbl with
-  | None -> assert false
-  | Some pc_dest -> 
-      let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000
-
-(* Determine if an instruction falls through *)
-
-let instr_fall_through = function
-  | Pb _ -> false
-  | Pbctr _ -> false
-  | Pbs _ -> false
-  | Pblr -> false
-  | _ -> true
-
-(* Estimate the size of an Asm instruction encoding, in number of actual
-   PowerPC instructions.  We can over-approximate. *)
-
-let instr_size = function
-  | Pbf(bit, lbl) -> 2
-  | Pbt(bit, lbl) -> 2
-  | Pbtbl(r, tbl) -> 5
-  | Plfi(r1, c) -> 2
-  | Plfis(r1, c) -> 2
-  | Plabel lbl -> 0
-  | Pbuiltin(ef, args, res) -> 0
-  | Pannot(ef, args) -> 0
-  | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
-  | _ -> 1
-
-(* Build a table label -> estimated position in generated code.
-   Used to predict if relative conditional branches can use the short form. *)
-
-let rec label_positions tbl pc = function
-  | [] -> tbl
-  | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c
-  | i :: c -> label_positions tbl (pc + instr_size i) c