2 files changed, 456 insertions, 338 deletions

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 8828faa3..5c84af6b 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -22,58 +22,7 @@ open Asm
 
 module StringSet = Set.Make(String)
 
-(* Recognition of target ABI and asm syntax *)
-
-type target = ELF | MacOS | Cygwin
-
-let target = 
-  match Configuration.system with
-  | "macosx" -> MacOS
-  | "linux"  -> ELF
-  | "bsd"    -> ELF
-  | "cygwin" -> Cygwin
-  | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported")
-
-(* 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 =
-  match target with
-  | ELF -> fprintf oc "%s" s
-  | MacOS | Cygwin -> fprintf oc "_%s" s
-
-let symbol oc symb =
-  raw_symbol oc (extern_atom symb)
-
-let symbol_offset oc (symb, ofs) =
-  symbol oc symb;
-  if ofs <> 0l then fprintf oc " + %ld" ofs
-
-let label oc lbl =
-  match target with
-  | ELF -> fprintf oc ".L%d" lbl
-  | MacOS | Cygwin -> fprintf oc "L%d" lbl
-
-let comment = "#"
+(* Basic printing functions used in definition of the systems *)
 
 let int_reg_name = function
   | EAX -> "%eax"  | EBX -> "%ebx"  | ECX -> "%ecx"  | EDX -> "%edx"
@@ -106,6 +55,194 @@ let preg oc = function
   | FR r -> freg oc r
   | _    -> assert false
 
+
+(* System dependend printer functions *)
+module type SYSTEM=
+    sig
+      val raw_symbol: out_channel -> string -> unit
+      val symbol: out_channel -> P.t -> unit
+      val label: out_channel -> int -> unit
+      val name_of_section: section_name -> string
+      val stack_alignment: int
+      val print_align: out_channel -> int -> unit
+      val print_mov_ra: out_channel -> ireg -> ident -> unit
+      val print_fun_info: out_channel -> P.t -> unit
+      val print_var_info: out_channel -> P.t -> unit
+      val print_epilogue: out_channel -> unit
+    end
+
+(* Printer functions for cygwin *)
+module Cygwin_System =
+  (struct
+
+    let raw_symbol oc s =
+       fprintf oc "_%s" s
+
+    let symbol oc symb =
+      fprintf oc "%s" (extern_atom symb)
+
+    let label oc lbl =
+       fprintf oc "L%d" lbl
+        
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data _ | Section_small_data _ -> ".data"
+      | Section_const  | Section_small_const -> ".section	.rdata,\"dr\""
+      | Section_string -> ".section	.rdata,\"dr\""
+      | Section_literal -> ".section	.rdata,\"dr\""
+      | Section_jumptable -> ".text"
+      | Section_user(s, wr, ex) ->
+          sprintf ".section	\"%s\", \"%s\"\n"
+            s (if ex then "xr" else if wr then "d" else "dr")
+
+    let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
+
+    let print_align oc n =
+      fprintf oc "	.align	%d\n" n
+    
+    let print_mov_ra oc rd id =   
+      fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
+
+    let print_fun_info _ _ = ()
+        
+    let print_var_info _ _ = ()
+
+    let print_epilogue _ = ()
+  end:SYSTEM)
+
+(* Printer functions for ELF *)
+module ELF_System =
+  (struct
+    
+    let raw_symbol oc s =
+      fprintf oc "%s" s
+  
+    let symbol oc symb =
+      fprintf oc "%s" (extern_atom symb)
+
+    let label oc lbl =
+      fprintf oc ".L%d" lbl
+
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data i | Section_small_data i -> if i then ".data" else "COMM"
+      | Section_const | Section_small_const -> ".section	.rodata"
+      | Section_string -> ".section	.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 "")
+            
+    let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
+                    
+    let print_align oc n =
+      fprintf oc "	.align	%d\n" n
+        
+    let print_mov_ra  oc rd id = 
+         fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
+
+    let print_fun_info oc name =
+      fprintf oc "	.type	%a, @function\n" symbol name;
+      fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+
+    let print_var_info oc name =
+      fprintf oc "	.type	%a, @object\n" symbol name;
+      fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+
+    let print_epilogue _ = ()
+  end:SYSTEM)
+
+(* Printer functions for MacOS *)
+module MacOS_System =
+  (struct
+    
+    let raw_symbol oc s =
+     fprintf oc "_%s" s
+
+    let symbol oc symb =
+      fprintf oc "%s" (extern_atom symb)
+
+    let label oc lbl =
+      fprintf oc "L%d" lbl
+
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data _ | Section_small_data _ -> ".data"
+      | Section_const  | Section_small_const -> ".const"
+      | Section_string -> ".const"
+      | Section_literal -> ".literal8"
+      | Section_jumptable -> ".const"
+      | Section_user(s, wr, ex) ->
+          sprintf ".section	\"%s\", %s, %s"
+            (if wr then "__DATA" else "__TEXT") s
+            (if ex then "regular, pure_instructions" else "regular")
+    
+    let stack_alignment =  16 (* mandatory *)
+         
+    (* Base-2 log of a Caml integer *)           
+    let rec log2 n =
+      assert (n > 0);
+      if n = 1 then 0 else 1 + log2 (n lsr 1)
+
+    let print_align oc n =
+      fprintf oc "	.align	%d\n" (log2 n)
+        
+    let indirect_symbols : StringSet.t ref = ref StringSet.empty
+
+    let print_mov_ra oc rd id = 
+      let id = extern_atom id in
+      indirect_symbols := StringSet.add id !indirect_symbols;
+      fprintf oc "	movl	L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd
+
+    let print_fun_info _ _ = ()
+ 
+    let print_var_info _ _ = ()
+    
+    let print_epilogue oc = 
+      fprintf oc "	.section __IMPORT,__pointers,non_lazy_symbol_pointers\n";
+      StringSet.iter
+        (fun s ->
+          fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s;
+          fprintf oc "	.indirect_symbol %a\n" raw_symbol s;
+          fprintf oc "	.long	0\n")
+        !indirect_symbols
+
+  end:SYSTEM)
+
+
+module AsmPrinter(Target: SYSTEM) =
+  (struct
+    open 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 comment = "#"
+
+let symbol_offset oc (symb, ofs) =
+  symbol oc symb;
+  if ofs <> 0l then fprintf oc " + %ld" ofs
+
+let coqint oc n =
+  fprintf oc "%ld" (camlint_of_coqint n)
+
 let addressing oc (Addrmode(base, shift, cst)) =
   begin match cst with
   | Coq_inl n ->
@@ -136,58 +273,13 @@ let name_of_neg_condition = function
   | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le"
   | Cond_p -> "np" | Cond_np -> "p" 
 
-(* Names of sections *)
-
-let name_of_section_ELF = function
-  | Section_text -> ".text"
-  | Section_data i | Section_small_data i -> if i then ".data" else "COMM"
-  | Section_const | Section_small_const -> ".section	.rodata"
-  | Section_string -> ".section	.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 "")
-
-let name_of_section_MacOS = function
-  | Section_text -> ".text"
-  | Section_data _ | Section_small_data _ -> ".data"
-  | Section_const  | Section_small_const -> ".const"
-  | Section_string -> ".const"
-  | Section_literal -> ".literal8"
-  | Section_jumptable -> ".const"
-  | Section_user(s, wr, ex) ->
-       sprintf ".section	\"%s\", %s, %s"
-               (if wr then "__DATA" else "__TEXT") s
-               (if ex then "regular, pure_instructions" else "regular")
-
-let name_of_section_Cygwin = function
-  | Section_text -> ".text"
-  | Section_data _ | Section_small_data _ -> ".data"
-  | Section_const  | Section_small_const -> ".section	.rdata,\"dr\""
-  | Section_string -> ".section	.rdata,\"dr\""
-  | Section_literal -> ".section	.rdata,\"dr\""
-  | Section_jumptable -> ".text"
-  | Section_user(s, wr, ex) ->
-       sprintf ".section	\"%s\", \"%s\"\n"
-             s (if ex then "xr" else if wr then "d" else "dr")
-
-let name_of_section =
-  match target with
-  | ELF    -> name_of_section_ELF
-  | MacOS  -> name_of_section_MacOS
-  | Cygwin -> name_of_section_Cygwin
 
+(* Names of sections *)
 let section oc sec =
   fprintf oc "	%s\n" (name_of_section sec)
 
 (* SP adjustment to allocate or free a stack frame *)
 
-let stack_alignment =
-  match target with
-  | ELF | Cygwin -> 8               (* minimum is 4, 8 is better for perfs *)
-  | MacOS -> 16                     (* mandatory *)
-
 let int32_align n a =
   if n >= 0l
   then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
@@ -209,11 +301,6 @@ let rec log2 n =
 
 (* Emit a align directive *)
 
-let print_align oc n =
-  match target with
-  | ELF | Cygwin -> fprintf oc "	.align	%d\n" n
-  | MacOS        -> fprintf oc "	.align	%d\n" (log2 n)
-
 let need_masks = ref false
 
 (* Emit .file / .loc debugging directives *)
@@ -562,12 +649,7 @@ let print_instruction oc = function
   | Pmov_ri(rd, n) ->
       fprintf oc "	movl	$%ld, %a\n" (camlint_of_coqint n) ireg rd
   | Pmov_ra(rd, id) ->
-      if target = MacOS then begin
-        let id = extern_atom id in
-        indirect_symbols := StringSet.add id !indirect_symbols;
-        fprintf oc "	movl	L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd
-      end else
-        fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
+      print_mov_ra oc rd id
   | Pmov_rm(rd, a) | Pmov_rm_a(rd, a) ->
       fprintf oc "	movl	%a, %a\n" addressing a ireg rd
   | Pmov_mr(a, r1) | Pmov_mr_a(a, r1) ->
@@ -841,10 +923,7 @@ let print_function oc name fn =
   cfi_startproc oc;
   List.iter (print_instruction oc) fn.fn_code;
   cfi_endproc oc;
-  if target = ELF then begin
-    fprintf oc "	.type	%a, @function\n" symbol name;
-    fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
-  end;
+  print_fun_info oc name;
   if !float64_literals <> [] || !float32_literals <> [] then begin
     section oc lit;
     print_align oc 8;
@@ -913,10 +992,7 @@ let print_var oc name v =
           fprintf oc "	.globl	%a\n" symbol name;
         fprintf oc "%a:\n" symbol name;
         print_init_data oc name v.gvar_init;
-        if target = ELF then begin
-          fprintf oc "	.type	%a, @object\n" symbol name;
-          fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
-        end
+        print_var_info oc name
       end else begin
         let sz =
           match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
@@ -933,31 +1009,37 @@ let print_globdef oc (name, gdef) =
   | Gfun(Internal code) -> print_function oc name code
   | Gfun(External ef) -> ()
   | Gvar v -> print_var oc name v
+end)
+
+type target = ELF | MacOS | Cygwin
+
 
 let print_program oc p =
-  PrintAnnot.print_version_and_options oc comment;
-  need_masks := false;
-  indirect_symbols := StringSet.empty;
-  Hashtbl.clear filename_num;
-  List.iter (print_globdef oc) p.prog_defs;
-  if !need_masks then begin
-    section oc Section_const;  (* not Section_literal because not 8-bytes *)
-    print_align oc 16;
+  let target =   
+    match Configuration.system with
+    | "macosx" -> MacOS
+    | "linux"  -> ELF
+    | "bsd"    -> ELF
+    | "cygwin" -> Cygwin
+    | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported") in
+  let module Target = (val (match target with
+  | MacOS -> (module MacOS_System:SYSTEM)
+  | ELF -> (module ELF_System:SYSTEM)
+  | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in
+  let module Printer = AsmPrinter(Target) in
+  PrintAnnot.print_version_and_options oc Printer.comment;
+  Printer.need_masks := false;
+  Hashtbl.clear Printer.filename_num;
+  List.iter (Printer.print_globdef oc) p.prog_defs;
+  if !Printer.need_masks then begin
+    Printer.section oc Section_const;  (* not Section_literal because not 8-bytes *)
+    Target.print_align oc 16;
     fprintf oc "%a:	.quad   0x8000000000000000, 0\n"
-               raw_symbol "__negd_mask";
+               Target.raw_symbol "__negd_mask";
     fprintf oc "%a:	.quad   0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n"
-               raw_symbol "__absd_mask";
+               Target.raw_symbol "__absd_mask";
     fprintf oc "%a:	.long   0x80000000, 0, 0, 0\n"
-               raw_symbol "__negs_mask";
+               Target.raw_symbol "__negs_mask";
     fprintf oc "%a:	.long   0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
-               raw_symbol "__abss_mask"
-  end;
-  if target = MacOS then begin
-    fprintf oc "	.section __IMPORT,__pointers,non_lazy_symbol_pointers\n";
-    StringSet.iter
-      (fun s ->
-        fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s;
-        fprintf oc "	.indirect_symbol %a\n" raw_symbol s;
-        fprintf oc "	.long	0\n")
-      !indirect_symbols
+               Target.raw_symbol "__abss_mask"
   end
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index d2ec5613..587dfccf 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -23,13 +23,227 @@ open Asm
 
 (* Recognition of target ABI and asm syntax *)
 
-type target = Linux | Diab
+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 -> string -> unit
+      val reset_file_line: unit -> 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
+    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 target = 
-  match Configuration.system with
-  | "linux"  -> Linux
-  | "diab"   -> Diab
-  | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported")
+
+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 =
+  (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 ".section	.sbss,\"aw\",@progbits"
+      | Section_const -> ".rodata"
+      | Section_small_const -> ".section	.sdata2,\"a\",@progbits"
+      | 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 "")
+
+    let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
+    let reset_file_line () = Hashtbl.clear filename_num
+    let print_file_line oc file line =
+      if !Clflags.option_g && file <> "" then begin
+        let filenum = 
+          try
+            Hashtbl.find filename_num file
+          with Not_found ->
+            let n = Hashtbl.length filename_num + 1 in
+            Hashtbl.add filename_num file n;
+            fprintf oc "	.file	%d %S\n" n file;
+            n
+        in fprintf oc "	.loc	%d %s\n" filenum line
+      end
+    
+    (* 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:SYSTEM)
+    
+module Diab_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 ".bss"
+      | 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 *)
+
+    let last_file = ref ""
+    let reset_file_line () = last_file := ""
+    let print_file_line oc file line =
+      if !Clflags.option_g && file <> "" then begin
+        if file <> !last_file then begin
+          fprintf oc "	.d1file	%S\n" file;
+          last_file := file
+        end;
+        fprintf oc "	.d1line	%s\n" line
+      end
+
+    (* 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:SYSTEM)
+
+module AsmPrinter (Target : SYSTEM) =
+  (struct
+    open Target
 
 (* On-the-fly label renaming *)
 
@@ -56,12 +270,6 @@ let coqint oc n =
 let raw_symbol oc s =
   fprintf oc "%s" s
 
-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 label oc lbl =
   fprintf oc ".L%d" lbl
@@ -72,35 +280,6 @@ let label_low oc lbl =
 let label_high oc lbl =
   fprintf oc ".L%d@ha" lbl
 
-let comment =
-  match target with
-  | Linux -> "#"
-  | Diab -> ";"
-
-let symbol_fragment oc s n op =
-      fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op
-
-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
-        (match target with Linux -> "@sda21" | Diab  -> "@sdarx")
-  (* 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
-        (match target with Linux -> "@l" | Diab  -> "@sdax@l")
-  | Csymbol_rel_high(s, n) ->
-      symbol_fragment oc s n
-        (match target with Linux -> "@ha" | Diab -> "@sdarx@ha")
 
 let num_crbit = function
   | CRbit_0 -> 0
@@ -112,170 +291,23 @@ let num_crbit = function
 let crbit oc bit =
   fprintf oc "%d" (num_crbit bit)
 
-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"
-
-let ireg oc r =
-  begin match target with
-  | Diab  -> output_char oc 'r'
-  | Linux -> ()
-  end;
-  output_string oc (int_reg_name r)
-
 let ireg_or_zero oc r =
   if r = GPR0 then output_string oc "0" else ireg oc r
 
-let freg oc r =
-  begin match target with
-  | Diab  -> output_char oc 'f'
-  | Linux -> ()
-  end;
-  output_string oc (float_reg_name r)
-
-let creg oc r =
-  match target with
-  | Diab  -> fprintf oc "cr%d" r
-  | Linux -> fprintf oc "%d" r
-
 let preg oc = function
   | IR r -> ireg oc r
   | FR r -> freg oc r
   | _    -> assert false
 
-(* Names of sections *)
-
-let name_of_section_Linux = 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 ".section	.sbss,\"aw\",@progbits"
-  | Section_const -> ".rodata"
-  | Section_small_const -> ".section	.sdata2,\"a\",@progbits"
-  | 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 "")
-
-let name_of_section_Diab = function
-  | Section_text -> ".text"
-  | Section_data i -> if i then ".data" else ".bss"
-  | 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 *)
-
-let name_of_section =
-  match target with
-  | Linux -> name_of_section_Linux
-  | Diab  -> name_of_section_Diab
-
 let section oc sec =
   let name = name_of_section sec in
   assert (name <> "COMM");
   fprintf oc "	%s\n" name
 
-(* Emit .file / .loc debugging directives *)
-
-module DebugLinux = struct
-  let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
-  let reset () = Hashtbl.clear filename_num
-  let print_file_line oc file line =
-    if !Clflags.option_g && file <> "" then begin
-      let filenum = 
-        try
-          Hashtbl.find filename_num file
-        with Not_found ->
-          let n = Hashtbl.length filename_num + 1 in
-          Hashtbl.add filename_num file n;
-          fprintf oc "	.file	%d %S\n" n file;
-          n
-      in fprintf oc "	.loc	%d %s\n" filenum line
-    end
-end
-
-module DebugDiab = struct
-  let last_file = ref ""
-  let reset () = last_file := ""
-  let print_file_line oc file line =
-    if !Clflags.option_g && file <> "" then begin
-      if file <> !last_file then begin
-        fprintf oc "	.d1file	%S\n" file;
-        last_file := file
-      end;
-      fprintf oc "	.d1line	%s\n" line
-    end
-end
-
-let print_file_line =
-  match target with
-  | Linux -> DebugLinux.print_file_line
-  | Diab  -> DebugDiab.print_file_line
-
 let print_location oc loc =
   if loc <> Cutil.no_loc then
     print_file_line oc (fst loc) (string_of_int (snd loc))
 
-let reset_file_line =
-  match target with
-  | Linux -> DebugLinux.reset
-  | Diab  -> DebugDiab.reset
-
-(* Emit .cfi directives *)
-
-let cfi_startproc oc =
-  if Configuration.asm_supports_cfi then
-    match target with
-    | Linux -> fprintf oc "	.cfi_startproc\n"
-    | Diab  -> ()
-
-let cfi_endproc oc =
-  if Configuration.asm_supports_cfi then
-    match target with
-    | Linux -> fprintf oc "	.cfi_endproc\n"
-    | Diab  -> ()
-
-let cfi_adjust oc delta =
-  if Configuration.asm_supports_cfi then
-    match target with
-    | Linux -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
-    | Diab  -> ()
-
-let cfi_rel_offset oc reg ofs =
-  if Configuration.asm_supports_cfi then
-    match target with
-    | Linux -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs
-    | Diab  -> ()
 
 (* Encoding masks for rlwinm instructions *)
 
@@ -824,18 +856,22 @@ let print_globdef oc (name, gdef) =
   | Gfun f -> print_fundef oc name f
   | Gvar v -> print_var oc name v
 
-let print_prologue oc =
-  match target with
-  | Linux ->
-      ()
-  | Diab ->
-      fprintf oc "	.xopt	align-fill-text=0x60000000\n";
-      if !Clflags.option_g then
-        fprintf oc "	.xopt	asm-debug-on\n"
+  end)
+
+type target = Linux | Diab
 
 let print_program oc p =
-  reset_file_line();
-  PrintAnnot.print_version_and_options oc comment;
-  print_prologue oc;
-  List.iter (print_globdef oc) p.prog_defs
+  let target = 
+    (match Configuration.system with
+    | "linux"  -> Linux
+    | "diab"   -> Diab
+    | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) in
+  let module Target = (val (match target with
+  | Linux -> (module Linux_System:SYSTEM)
+  | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in
+  Target.reset_file_line();
+  PrintAnnot.print_version_and_options oc Target.comment;
+  let module Printer = AsmPrinter(Target) in
+  Target.print_prologue oc;
+  List.iter (Printer.print_globdef oc) p.prog_defs