Changed the ASM printer of the powerpc to the generalized backend.

3 files changed, 119 insertions, 2 deletions

diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
new file mode 100644
index 00000000..aa317a09
--- /dev/null
+++ b/backend/PrintAsm.ml
@@ -0,0 +1,99 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 PrintAsmaux
+open Printf
+open Sections
+open TargetPrinter
+
+module Target = (val (sel_target ()):TARGET) 
+
+let print_location oc loc =
+  if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
+      
+let print_function oc name fn =
+  Hashtbl.clear current_function_labels;
+  Target.reset_constants ();
+  let (text, lit, jmptbl) = Target.get_section_names name in
+  Target.section oc text;
+  let alignment =
+    match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
+  Target.print_align oc alignment;
+  if not (C2C.atom_is_static name) then
+    fprintf oc "	.globl %a\n" symbol name;
+  Target.print_optional_fun_info oc;
+  fprintf oc "%a:\n" symbol name;
+  print_location oc (C2C.atom_location name);
+  Target.cfi_startproc oc;
+  Target.print_instructions oc fn.fn_code;
+  Target.cfi_endproc oc;
+  if Target.print_fun_info then
+    print_fun_info oc name;
+  Target.emit_constants oc lit;
+  Target.print_jumptable oc jmptbl
+    
+
+let print_init_data oc name id =
+  if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
+      && List.for_all (function Init_int8 _ -> true | _ -> false) id
+  then
+    fprintf oc "	.ascii	\"%s\"\n" (PrintCsyntax.string_of_init id)
+  else
+    List.iter (Target.print_init oc) id
+      
+let print_var oc name v =
+  match v.gvar_init with
+  | [] -> ()
+  | _  ->
+      let sec =
+        match C2C.atom_sections name with
+        | [s] -> s
+        |  _  -> Section_data true
+      and align =
+        match C2C.atom_alignof name with
+        | Some a -> a
+        | None -> 8 in (* 8-alignment is a safe default *)
+      let name_sec = Target.name_of_section sec in
+      if name_sec <> "COMM" then begin
+        fprintf oc "	%s\n" name_sec;
+        Target.print_align oc align;
+        if not (C2C.atom_is_static name) then
+          fprintf oc "	.global	%a\n" symbol name;
+        fprintf oc "%a:\n" symbol name;
+        print_init_data oc name v.gvar_init;
+        if Target.print_var_info then
+          print_var_info oc name;
+      end else
+        let sz =
+          match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
+        Target.print_comm_symb oc sz name align
+          
+
+let print_globdef oc (name,gdef) =
+  match gdef with
+  | Gfun (Internal code) -> print_function oc name code
+  | Gfun (External ef) ->   ()
+  | Gvar v -> print_var oc name v
+        
+
+let print_program oc p =
+  PrintAnnot.reset_filenames ();
+  PrintAnnot.print_version_and_options oc Target.comment;
+  Target.print_prologue oc;
+  List.iter (print_globdef oc) p.prog_defs;
+  Target.print_epilogue oc;
+  PrintAnnot.close_filenames ()
diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli
new file mode 100644
index 00000000..eb63f1be
--- /dev/null
+++ b/backend/PrintAsm.mli
@@ -0,0 +1,16 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 PrintAsmaux
+
+val print_program: out_channel -> Asm.program -> unit
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 75ecfa40..381ef5df 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -25,12 +25,12 @@ module type TARGET =
       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_comm_symb:  out_channel -> Z.t -> P.t -> int -> unit
       val print_var_info: bool
       val print_fun_info: bool
       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 get_section_names: P.t -> 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
@@ -39,6 +39,8 @@ module type TARGET =
       val emit_constants: out_channel -> section_name -> unit
       val print_jumptable: out_channel -> section_name -> unit
       val section: out_channel -> section_name -> unit
+      val name_of_section: section_name -> string
+      val comment: string
     end
 
 (* On-the-fly label renaming *)