From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Sep 2006 15:08:29 +0000
Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S
 dans les semantiques - Ajout constructions switch et allocation dynamique -
 Initialisation des variables globales - Portage Coq 8.1 beta Debut
 d'integration du front-end C: - Traduction Clight -> Csharpminor dans
 cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/PrintPPC.ml | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 62 insertions(+), 5 deletions(-)

(limited to 'caml/PrintPPC.ml')

diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index 830de0d5..eaa383b4 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -26,10 +26,23 @@ let label_for_label lbl =
     Hashtbl.add current_function_labels lbl lbl';
     lbl'
 
+(* Record identifiers of external functions *)
+
+module IdentSet = Set.Make(struct type t = ident let compare = compare end)
+
+let extfuns = ref IdentSet.empty
+
+let record_extfun (Coq_pair(name, defn)) =
+  match defn with
+  | Internal _ -> ()
+  | External _ -> extfuns := IdentSet.add name !extfuns
+
 (* Basic printing functions *)
 
 let print_symb oc symb =
-  fprintf oc "_%s" (extern_atom symb)
+  if IdentSet.mem symb !extfuns
+  then fprintf oc "L%s$stub" (extern_atom symb)
+  else fprintf oc "_%s" (extern_atom symb)
 
 let print_label oc lbl =
   fprintf oc "L%d" (label_for_label lbl)
@@ -99,6 +112,8 @@ let print_instruction oc labels = function
       fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
   | Paddze(r1, r2) ->
       fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
+  | Pallocblock ->
+      fprintf oc "	bl	_compcert_alloc\n"
   | Pallocframe(lo, hi) ->
       let lo = camlint_of_coqint lo
       and hi = camlint_of_coqint hi in
@@ -317,7 +332,7 @@ let rec labels_of_code = function
       Labelset.add lbl (labels_of_code c)
   | Coq_cons(_, c) -> labels_of_code c
 
-let print_function oc (Coq_pair(name, code)) =
+let print_function oc name code =
   Hashtbl.clear current_function_labels;
   fprintf oc "	.text\n";
   fprintf oc "	.align 2\n";
@@ -325,10 +340,52 @@ let print_function oc (Coq_pair(name, code)) =
   fprintf oc "%a:\n" print_symb name;
   coqlist_iter (print_instruction oc (labels_of_code code)) code
 
-let print_var oc (Coq_pair(name, size)) =
-  fprintf oc "	.comm	%a, %ld\n" print_symb name (camlint_of_z size)
+let print_external_function oc name =
+  let name = extern_atom name in
+  fprintf oc "	.text\n";
+  fprintf oc "	.align 2\n";
+  fprintf oc "L%s$stub:\n" name;
+  fprintf oc "	addis	r11, 0, ha16(L%s$ptr)\n" name;
+  fprintf oc "	lwz	r11, lo16(L%s$ptr)(r11)\n" name;
+  fprintf oc "	mtctr	r11\n";
+  fprintf oc "	bctr\n";
+  fprintf oc "	.non_lazy_symbol_pointer\n";
+  fprintf oc "L%s$ptr:\n" name;
+  fprintf oc "	.indirect_symbol _%s\n" name;
+  fprintf oc "	.long	0\n"
+
+let print_fundef oc (Coq_pair(name, defn)) =
+  match defn with
+  | Internal code -> print_function oc name code
+  | External ef -> print_external_function oc name
+
+let print_init_data oc = function
+  | Init_int8 n ->
+      fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
+  | Init_int16 n ->
+      fprintf oc "	.short	%ld\n" (camlint_of_coqint n)
+  | Init_int32 n ->
+      fprintf oc "	.long	%ld\n" (camlint_of_coqint n)
+  | Init_float32 n ->
+      fprintf oc "	.long	%ld # %g \n" (Int32.bits_of_float n) n
+  | Init_float64 n ->
+      fprintf oc "	.quad	%Ld # %g \n" (Int64.bits_of_float n) n
+  | Init_space n ->
+      let n = camlint_of_z n in
+      if n > 0l then fprintf oc "	.space	%ld\n" n
+
+let print_var oc (Coq_pair(name, init_data)) =
+  match init_data with
+  | Coq_nil -> ()
+  | _  ->
+      fprintf oc "	.data\n";
+      fprintf oc "	.globl	%a\n" print_symb name;
+      fprintf oc "%a:" print_symb name;
+      coqlist_iter (print_init_data oc) init_data
 
 let print_program oc p =
+  extfuns := IdentSet.empty;
+  coqlist_iter record_extfun p.prog_funct;
   coqlist_iter (print_var oc) p.prog_vars;
-  coqlist_iter (print_function oc) p.prog_funct
+  coqlist_iter (print_fundef oc) p.prog_funct
 
-- 
cgit