Started moving common backend functions into one file.

3 files changed, 114 insertions, 84 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 7f511912..41a815d6 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -19,6 +19,7 @@ open Sections
 open AST
 open Memdata
 open Asm
+open PrintAsmaux
 
 (* Type for the ABI versions *)
 type float_abi_type =
@@ -45,38 +46,18 @@ module AsmPrinter (Opt: PRINTER_OPTIONS) =
 
 let literals_in_code = ref true     (* to be turned into a proper option *)
 
-(* 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 label_for_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 print_symb oc symb =
-  fprintf oc "%s" (extern_atom symb)
-
 let print_label oc lbl =
-  fprintf oc ".L%d" (label_for_label lbl)
+  fprintf oc ".L%d" (transl_label lbl)
 
 let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
 
 let comment = "@"
 
-let print_symb_ofs oc (symb, ofs) =
-  print_symb oc symb;
+let symbol_offset oc (symb, ofs) =
+  symbol oc symb;
   let ofs = camlint_of_coqint ofs in
   if ofs <> 0l then fprintf oc " + %ld" ofs
 
@@ -254,7 +235,7 @@ let emit_constants oc =
   Hashtbl.iter
     (fun (id, ofs) lbl ->
       fprintf oc ".L%d:	.word	%a\n"
-          lbl print_symb_ofs (id, ofs))
+          lbl symbol_offset (id, ofs))
     symbol_labels;
   reset_constants ()
 
@@ -263,13 +244,13 @@ let emit_constants oc =
 let loadsymbol oc r id ofs =
   if !Clflags.option_mthumb then begin
     fprintf oc "	movw	%a, #:lower16:%a\n"
-            ireg r print_symb_ofs (id, ofs);
+            ireg r symbol_offset (id, ofs);
     fprintf oc "	movt	%a, #:upper16:%a\n"
-            ireg r print_symb_ofs (id, ofs); 2
+            ireg r symbol_offset (id, ofs); 2
   end else begin
     let lbl = label_symbol id ofs in
     fprintf oc "	ldr	%a, .L%d @ %a\n" 
-            ireg r lbl print_symb_ofs (id, ofs); 1
+            ireg r lbl symbol_offset (id, ofs); 1
   end
 
 (* Emit instruction sequences that set or offset a register by a constant. *)
@@ -483,10 +464,6 @@ let print_builtin_vstore_global oc chunk id ofs args =
 
 (* Handling of varargs *)
 
-let current_function_stacksize = ref 0l
-let current_function_sig =
-  ref { sig_args = []; sig_res = None; sig_cc = cc_default }
-
 let align n a = (n + a - 1) land (-a)
 
 let rec next_arg_location ir ofs = function
@@ -761,7 +738,7 @@ let print_instruction oc = function
       fprintf oc "	b%s	%a\n" (condition_name bit) print_label lbl; 1
   | Pbsymb(id, sg) ->
       let n = fixup_arguments oc Outgoing sg in
-      fprintf oc "	b	%a\n" print_symb id;
+      fprintf oc "	b	%a\n" symbol id;
       n + 1
   | Pbreg(r, sg) ->
       let n = 
@@ -772,7 +749,7 @@ let print_instruction oc = function
       n + 1
   | Pblsymb(id, sg) ->
       let n1 = fixup_arguments oc Outgoing sg in
-      fprintf oc "	bl	%a\n" print_symb id;
+      fprintf oc "	bl	%a\n" symbol id;
       let n2 = fixup_result oc Incoming sg in
       n1 + 1 + n2
   | Pblreg(r, sg) ->
@@ -1084,18 +1061,18 @@ let print_function oc name fn =
     match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
   fprintf oc "	.balign %d\n" alignment;
   if not (C2C.atom_is_static name) then
-    fprintf oc "	.global	%a\n" print_symb name;
+    fprintf oc "	.global	%a\n" symbol name;
   if !Clflags.option_mthumb then
     fprintf oc "	.thumb_func\n";
-  fprintf oc "%a:\n" print_symb name;
+  fprintf oc "%a:\n" symbol name;
   print_location oc (C2C.atom_location name);
   Opt.cfi_startproc oc;
   ignore (fixup_arguments oc Incoming fn.fn_sig);
   print_instructions oc fn.fn_code;
   if !literals_in_code then emit_constants oc;
   Opt.cfi_endproc oc;
-  fprintf oc "	.type	%a, %%function\n" print_symb name;
-  fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name;
+  fprintf oc "	.type	%a, %%function\n" symbol name;
+  fprintf oc "	.size	%a, . - %a\n" symbol name symbol name;
   if not !literals_in_code && !size_constants > 0 then begin
     section oc lit;
     emit_constants oc
@@ -1122,7 +1099,7 @@ let print_init oc = function
       if Z.gt n Z.zero then
         fprintf oc "	.space	%s\n" (Z.to_string n)
   | Init_addrof(symb, ofs) ->
-      fprintf oc "	.word	%a\n" print_symb_ofs (symb, ofs)
+      fprintf oc "	.word	%a\n" symbol_offset (symb, ofs)
 
 let print_init_data oc name id =
   if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
@@ -1151,18 +1128,18 @@ let print_var oc name v =
         fprintf oc "	%s\n" name_sec;
         fprintf oc "	.balign	%d\n" align;
         if not (C2C.atom_is_static name) then
-          fprintf oc "	.global	%a\n" print_symb name;
-        fprintf oc "%a:\n" print_symb name;
+          fprintf oc "	.global	%a\n" symbol name;
+        fprintf oc "%a:\n" symbol name;
         print_init_data oc name v.gvar_init;
-        fprintf oc "	.type	%a, %%object\n" print_symb name;
-        fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name
+        fprintf oc "	.type	%a, %%object\n" symbol name;
+        fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
       end else begin
         let sz =
           match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
         if C2C.atom_is_static name then
-          fprintf oc "	.local	%a\n" print_symb name;
+          fprintf oc "	.local	%a\n" symbol name;
         fprintf oc "	.comm	%a, %s, %d\n"
-          print_symb name
+          symbol name
           (Z.to_string sz)
           align
       end
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
new file mode 100644
index 00000000..3493e912
--- /dev/null
+++ b/backend/PrintAsmaux.ml
@@ -0,0 +1,84 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open Asm
+open Camlcoq
+open Datatypes
+open Printf
+open Sections
+
+(** Auxiliary functions for printing of asm *)
+
+module type TARGET =
+    sig
+      val print_prologue: out_channel -> unit
+      val print_epilogue: out_channel -> unit
+      val print_align: out_channel -> int -> unit
+      val print_comm_symb:  out_channel -> P.t -> int -> unit
+      val print_var_info: out_channel -> P.t -> unit
+      val print_fun_info: out_channel -> P.t -> unit
+      val print_init: out_channel -> init_data -> unit
+      val reset_constants: unit -> unit
+      val get_section_names: unit -> section_name * section_name * section_name
+      val print_file_line: out_channel -> string -> int -> unit
+      val print_optional_fun_info: out_channel -> unit
+      val cfi_startproc: out_channel -> unit
+      val print_instructions: out_channel -> code -> unit
+      val cfi_endproc: out_channel -> unit
+      val emit_constants: out_channel -> section_name -> unit
+      val print_jumptable: out_channel -> section_name -> unit
+      val section: out_channel -> section_name -> unit
+    end
+
+(* 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'
+
+
+(* List of literals and jumptables used in the code *)
+
+let float64_literals : (int * int64) list ref = ref []
+let float32_literals : (int * int32) list ref = ref []
+let jumptables : (int * label list) list ref = ref []
+
+(* Variables used for the handling of varargs *)
+
+let current_function_stacksize = ref 0l
+let current_function_sig =
+  ref { sig_args = []; sig_res = None; sig_cc = cc_default }
+
+(* Functions for printing of symbol names *)
+let symbol oc symb =
+  fprintf oc "%s" (extern_atom symb)
+
+let symbol_offset oc (symb, ofs) =
+  symbol oc symb;
+  let ofs = camlint_of_coqint ofs in
+  if ofs <> 0l then fprintf oc " + %ld" ofs
+
+(* The comment deliminiter *)
+let comment = "#"
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 0c4356ec..6e9e1a4f 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -20,12 +20,12 @@ open Sections
 open AST
 open Memdata
 open Asm
+open PrintAsmaux
 
 (* 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
@@ -39,15 +39,8 @@ module type SYSTEM =
       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
+      fprintf oc "(%a)%s" symbol_offset (s, n) op
 
 
 let int_reg_name = function
@@ -72,7 +65,6 @@ let float_reg_name = function
 
 module Linux_System : SYSTEM =
   struct
-    let comment =  "#"
 
     let constant oc cst =
       match cst with
@@ -155,7 +147,6 @@ module Linux_System : SYSTEM =
     
 module Diab_System : SYSTEM =
   struct
-    let comment =  ";"
         
     let constant oc cst =
       match cst with
@@ -224,23 +215,6 @@ 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 coqint oc n =
@@ -249,7 +223,6 @@ let coqint oc n =
 let raw_symbol oc s =
   fprintf oc "%s" s
 
-
 let label oc lbl =
   fprintf oc ".L%d" lbl
 
@@ -328,10 +301,6 @@ let short_cond_branch tbl pc lbl_dest =
 
 (* Printing of instructions *)
 
-let float_literals : (int * int64) list ref = ref []
-let float32_literals : (int * int32) list ref = ref []
-let jumptables : (int * label list) list ref = ref []
-
 let print_instruction oc tbl pc fallthrough = function
   | Padd(r1, r2, r3) ->
       fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
@@ -516,7 +485,7 @@ let print_instruction oc tbl pc fallthrough = function
       let lbl = new_label() in
       fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
       fprintf oc "	lfd	%a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c);
-      float_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float_literals;
+      float64_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float64_literals;
   | Plfis(r1, c) ->
       let lbl = new_label() in
       fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
@@ -715,7 +684,7 @@ let print_jumptable oc (lbl, tbl) =
 
 let print_function oc name fn =
   Hashtbl.clear current_function_labels;
-  float_literals := [];
+  float64_literals := [];
   float32_literals := [];
   jumptables := [];
   let (text, lit, jmptbl) =
@@ -736,12 +705,12 @@ let print_function oc name fn =
   cfi_endproc oc;
   fprintf oc "	.type	%a, @function\n" symbol name;
   fprintf oc "	.size	%a, . - %a\n" symbol name symbol name;
-  if !float_literals <> [] || !float32_literals <> [] then begin
+  if !float64_literals <> [] || !float32_literals <> [] then begin
     section oc lit;
     fprintf oc "	.balign 8\n";
-    List.iter (print_literal64 oc) !float_literals;
+    List.iter (print_literal64 oc) !float64_literals;
     List.iter (print_literal32 oc) !float32_literals;
-    float_literals := []; float32_literals := []
+    float64_literals := []; float32_literals := []
   end;
   if !jumptables <> [] then begin
     section oc jmptbl;
@@ -777,7 +746,7 @@ let print_init oc = function
         fprintf oc "	.space	%s\n" (Z.to_string n)
   | Init_addrof(symb, ofs) ->
       fprintf oc "	.long	%a\n" 
-                 symbol_offset (symb, camlint_of_coqint ofs)
+                 symbol_offset (symb, ofs)
 
 let print_init_data oc name id =
   if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
@@ -840,7 +809,7 @@ let print_program oc p =
   | Linux -> (module Linux_System:SYSTEM)
   | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in
   PrintAnnot.reset_filenames();
-  PrintAnnot.print_version_and_options oc Target.comment;
+  PrintAnnot.print_version_and_options oc comment;
   let module Printer = AsmPrinter(Target) in
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;