Continuation of PowerPC/EABI port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 375 insertions, 149 deletions

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 0e45c84..40d7ac5 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -19,6 +19,16 @@ open Camlcoq
 open AST
 open Asm
 
+(* Recognition of target ABI and asm syntax *)
+
+type target = MacOS | EABI
+
+let target = 
+  match Configuration.variant with
+  | "macosx" -> MacOS
+  | "eabi"   -> EABI
+  |  _       -> assert false
+
 (* On-the-fly label renaming *)
 
 let next_label = ref 100
@@ -28,7 +38,7 @@ let new_label() =
 
 let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
 
-let label_for_label lbl =
+let transl_label lbl =
   try
     Hashtbl.find current_function_labels lbl
   with Not_found ->
@@ -36,38 +46,66 @@ let label_for_label lbl =
     Hashtbl.add current_function_labels lbl lbl';
     lbl'
 
-(* Record identifiers of external functions *)
+(* Record identifiers of functions that need a special stub *)
 
 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
+let stubbed_functions = ref IdentSet.empty
 
 (* Basic printing functions *)
 
-let print_symb oc 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)
+let coqint oc n =
+  fprintf oc "%ld" (camlint_of_coqint n)
 
-let print_symb_ofs oc (symb, ofs) =
-  print_symb oc symb;
+let raw_symbol oc s =
+  match target with
+  | MacOS -> fprintf oc "_%s" s
+  | EABI  -> fprintf oc "%s" s
+
+let symbol oc symb =
+  match target with
+  | MacOS ->
+      if IdentSet.mem symb !stubbed_functions
+      then fprintf oc "L%s$stub" (extern_atom symb)
+      else fprintf oc "_%s" (extern_atom symb)
+  | EABI ->
+      if IdentSet.mem symb !stubbed_functions
+      then fprintf oc ".L%s$stub" (extern_atom symb)
+      else fprintf oc "%s" (extern_atom symb)
+
+let symbol_offset oc (symb, ofs) =
+  symbol oc symb;
   if ofs <> 0l then fprintf oc " + %ld" ofs
 
-let print_constant oc = function
+let label oc lbl =
+  match target with
+  | MacOS -> fprintf oc "L%d" lbl
+  | EABI  -> fprintf oc ".L%d" lbl
+
+let label_low oc lbl =
+  match target with
+  | MacOS -> fprintf oc "lo16(L%d)" lbl
+  | EABI  -> fprintf oc ".L%d@l" lbl
+
+let label_high oc lbl =
+  match target with
+  | MacOS -> fprintf oc "ha16(L%d)" lbl
+  | EABI  -> fprintf oc ".L%d@ha" lbl
+
+let constant oc cst =
+  match cst with
   | Cint n ->
       fprintf oc "%ld" (camlint_of_coqint n)
   | Csymbol_low(s, n) ->
-      fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
+      begin match target with
+      | MacOS -> fprintf oc "lo16(%a)" symbol_offset (s, camlint_of_coqint n)
+      | EABI  -> fprintf oc "%a@l" symbol_offset (s, camlint_of_coqint n)
+      end
   | Csymbol_high(s, n) ->
-      fprintf oc "ha16(%a)" print_symb_ofs (s, camlint_of_coqint n)
+      begin match target with
+      | MacOS -> fprintf oc "ha16(%a)" symbol_offset (s, camlint_of_coqint n)
+      | EABI  -> fprintf oc "%a@ha" symbol_offset (s, camlint_of_coqint n)
+      end
 
 let num_crbit = function
   | CRbit_0 -> 0
@@ -75,51 +113,180 @@ let num_crbit = function
   | CRbit_2 -> 2
   | CRbit_3 -> 3
 
-let print_crbit oc bit =
+let crbit oc bit =
   fprintf oc "%d" (num_crbit bit)
 
-let print_coqint oc n =
-  fprintf oc "%ld" (camlint_of_coqint n)
-
 let int_reg_name = function
-  | GPR0 -> "r0"  | GPR1 -> "r1"  | GPR2 -> "r2"  | GPR3 -> "r3"
-  | GPR4 -> "r4"  | GPR5 -> "r5"  | GPR6 -> "r6"  | GPR7 -> "r7"
-  | GPR8 -> "r8"  | GPR9 -> "r9"  | GPR10 -> "r10" | GPR11 -> "r11"
-  | GPR12 -> "r12" | GPR13 -> "r13" | GPR14 -> "r14" | GPR15 -> "r15"
-  | GPR16 -> "r16" | GPR17 -> "r17" | GPR18 -> "r18" | GPR19 -> "r19"
-  | GPR20 -> "r20" | GPR21 -> "r21" | GPR22 -> "r22" | GPR23 -> "r23"
-  | GPR24 -> "r24" | GPR25 -> "r25" | GPR26 -> "r26" | GPR27 -> "r27"
-  | GPR28 -> "r28" | GPR29 -> "r29" | GPR30 -> "r30" | GPR31 -> "r31"
+  | 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 -> "f0"  | FPR1 -> "f1"  | FPR2 -> "f2"  | FPR3 -> "f3"
-  | FPR4 -> "f4"  | FPR5 -> "f5"  | FPR6 -> "f6"  | FPR7 -> "f7"
-  | FPR8 -> "f8"  | FPR9 -> "f9"  | FPR10 -> "f10" | FPR11 -> "f11"
-  | FPR12 -> "f12" | FPR13 -> "f13" | FPR14 -> "f14" | FPR15 -> "f15"
-  | FPR16 -> "f16" | FPR17 -> "f17" | FPR18 -> "f18" | FPR19 -> "f19"
-  | FPR20 -> "f20" | FPR21 -> "f21" | FPR22 -> "f22" | FPR23 -> "f23"
-  | FPR24 -> "f24" | FPR25 -> "f25" | FPR26 -> "f26" | FPR27 -> "f27"
-  | FPR28 -> "f28" | FPR29 -> "f29" | FPR30 -> "f30" | FPR31 -> "f31"
-
-let ireg oc r = 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 = output_string oc (float_reg_name r)
+  | 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
+  | MacOS -> output_char oc 'r'
+  | EABI  -> ()
+  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
+  | MacOS -> output_char oc 'f'
+  | EABI  -> ()
+  end;
+  output_string oc (float_reg_name r)
+
+let creg oc r =
+  match target with
+  | MacOS -> fprintf oc "cr%d" r
+  | EABI  -> fprintf oc "%d" r
+
+let text oc =
+  fprintf oc "	.text\n"
+let data oc =
+  fprintf oc "	.data\n"
+let const oc =
+  match target with
+  | MacOS -> fprintf oc "	.const_data\n"
+  | EABI  -> fprintf oc "	.section	.rodata.cst8,\"aM\",@progbits,8\n"
 
 (* Printing of instructions *)
 
 module Labelset = Set.Make(struct type t = label let compare = compare end)
 
+(*
+let _add oc r1 r2 r3 =         fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+let _addi oc r1 r2 c =         fprintf oc "	addi	%a, %a, %s\n" ireg r1 ireg r2 c
+let _addis oc r1 r2 c =        fprintf oc "	addis	%a, %a, %s\n" ireg r1 ireg r2 c
+let _addze oc r1 r2 =          fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
+let _and_ oc r1 r2 r3 =        fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+let _andc oc r1 r2 r3 =        fprintf oc "	andc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+let _andi_ oc r1 r2 c =        fprintf oc "	andi.	%a, %a, %s\n" ireg r1 ireg r2 c
+let _andis_ oc r1 r2 c =       fprintf oc "	andis.	%a, %a, %s\n" ireg r1 ireg r2 c
+let _b oc l =                  fprintf oc "	b	%s\n" l
+let _bctr oc =                 fprintf oc "	bctr\n"
+let _bctrl oc =                fprintf oc "	bctrl\n"
+let _beq oc l =                fprintf oc "	beq	%s\n" l
+let _bf oc b l =               fprintf oc "	bf	%d, %s\n" b l
+let _bl oc l =                 fprintf oc "	bl	%s\n" l
+let _blr oc l =                fprintf oc "	blr	%s\n" l
+let _bt oc b l =               fprintf oc "	bt	%d, %s\n" b l
+let _cmplw oc cr r1 r2 =       fprintf oc "	cmplw	%a, %a, %a\n" creg cr ireg r1 ireg r2
+let _cmplwi oc cr r1 c =       fprintf oc "	cmplwi	%a, %a, %s\n" creg cr ireg r1 c
+let _cmpw oc cr r1 r2 =        fprintf oc "	cmpw	%a, %a, %a\n" creg cr ireg r1 ireg r2
+let _cmpwi oc cr r1 c =        fprintf oc "	cmpwi	%a, %a, %s\n" creg cr ireg r1 c
+let _cror oc r1 r2 r3 =        fprintf oc "	cror	%d, %d, %d\n" r1 r2 r3
+
+
+let _divw
+let _divwu
+let _eqv
+let _extsb
+let _extsh
+let _fabs
+let _fadd
+let _fcmp
+let _fcmpu
+let _fctiwz
+let _fdiv
+let _fmadd
+let _fmr
+let _fmsub
+let _fmul
+let _fneg
+let _fsrp
+let _fsub
+let _lbz
+let _lbzx
+let _lfd
+let _lfd
+let _lfdx
+let _lfs
+let _lfsx
+let _lha
+let _lhax
+let _lhz
+let _long
+let _lwz
+let _lwzx
+let _mfcr
+let _mflr
+let _mr
+let _mtctr
+let _mtlr
+let _mulli
+let _mullw
+let _nand
+let _nor
+let _or
+let _orc
+let _ori
+let _oris
+let _rlwinm
+let _slw
+let _sraw
+let _srawi
+let _srw
+let _stb
+let _stbx
+let _stfd
+let _stfdu
+let _stfdx
+let _stfs
+let _stfsx
+let _sth
+let _sthx
+let _stw
+let _stwu
+let _stwx
+let _subfc
+let _subfic
+let _xor
+let _xori
+let _xoris
+
+let _byte
+let _quad
+let _short
+let _space
+
+let _text
+let _const
+let _data
+let _deflabel
+let _startfun
+let _endfun
+let _globvar
+*)
+
 let print_instruction oc labels = function
   | Padd(r1, r2, r3) ->
       fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Paddi(r1, r2, c) ->
-      fprintf oc "	addi	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
+      fprintf oc "	addi	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
   | Paddis(r1, r2, c) ->
-      fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
+      fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
   | Paddze(r1, r2) ->
       fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
   | Pallocblock ->
-      fprintf oc "	bl	_compcert_alloc\n"
+      fprintf oc "	bl	%a\n" raw_symbol "compcert_alloc"
   | Pallocframe(lo, hi, ofs) ->
       let lo = camlint_of_coqint lo
       and hi = camlint_of_coqint hi
@@ -128,41 +295,41 @@ let print_instruction oc labels = function
       (* Keep stack 16-aligned *)
       let sz16 = Int32.logand (Int32.add sz 15l) 0xFFFF_FFF0l in
       assert (ofs = 0l);
-      fprintf oc "	stwu	r1, %ld(r1)\n" (Int32.neg sz16)
+      fprintf oc "	stwu	%a, %ld(%a)\n" ireg GPR1 (Int32.neg sz16) ireg GPR1
   | Pand_(r1, r2, r3) ->
       fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pandc(r1, r2, r3) ->
       fprintf oc "	andc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pandi_(r1, r2, c) ->
-      fprintf oc "	andi.	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	andi.	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pandis_(r1, r2, c) ->
-      fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pb lbl ->
-      fprintf oc "	b	%a\n" print_label lbl
+      fprintf oc "	b	%a\n" label (transl_label lbl)
   | Pbctr ->
       fprintf oc "	bctr\n"
   | Pbctrl ->
       fprintf oc "	bctrl\n"
   | Pbf(bit, lbl) ->
-      fprintf oc "	bf	%a, %a\n" print_crbit bit print_label lbl
+      fprintf oc "	bf	%a, %a\n" crbit bit label (transl_label lbl)
   | Pbl s ->
-      fprintf oc "	bl	%a\n" print_symb s
+      fprintf oc "	bl	%a\n" symbol s
   | Pbs s ->
-      fprintf oc "	b	%a\n" print_symb s
+      fprintf oc "	b	%a\n" symbol s
   | Pblr ->
       fprintf oc "	blr\n"
   | Pbt(bit, lbl) ->
-      fprintf oc "	bt	%a, %a\n" print_crbit bit print_label lbl
+      fprintf oc "	bt	%a, %a\n" crbit bit label (transl_label lbl)
   | Pcmplw(r1, r2) ->
-      fprintf oc "	cmplw	cr0, %a, %a\n" ireg r1 ireg r2
+      fprintf oc "	cmplw	%a, %a, %a\n" creg 0 ireg r1 ireg r2
   | Pcmplwi(r1, c) ->
-      fprintf oc "	cmplwi	cr0, %a, %a\n" ireg r1 print_constant c
+      fprintf oc "	cmplwi	%a, %a, %a\n" creg 0 ireg r1 constant c
   | Pcmpw(r1, r2) ->
-      fprintf oc "	cmpw	cr0, %a, %a\n" ireg r1 ireg r2
+      fprintf oc "	cmpw	%a, %a, %a\n" creg 0 ireg r1 ireg r2
   | Pcmpwi(r1, c) ->
-      fprintf oc "	cmpwi	cr0, %a, %a\n" ireg r1 print_constant c
+      fprintf oc "	cmpwi	%a, %a, %a\n" creg 0 ireg r1 constant c
   | Pcror(c1, c2, c3) ->
-      fprintf oc "	cror	%a, %a, %a\n" print_crbit c1 print_crbit c2 print_crbit c3
+      fprintf oc "	cror	%a, %a, %a\n" crbit c1 crbit c2 crbit c3
   | Pdivw(r1, r2, r3) ->
       fprintf oc "	divw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pdivwu(r1, r2, r3) ->
@@ -174,39 +341,40 @@ let print_instruction oc labels = function
   | Pextsh(r1, r2) ->
       fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
   | Pfreeframe ofs ->
-      fprintf oc "	lwz	r1, %ld(r1)\n" (camlint_of_coqint ofs)
+      fprintf oc "	lwz	%a, %ld(%a)\n" ireg GPR1  (camlint_of_coqint ofs)  ireg GPR1
   | Pfabs(r1, r2) ->
       fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
   | Pfadd(r1, r2, r3) ->
       fprintf oc "	fadd	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfcmpu(r1, r2) ->
-      fprintf oc "	fcmpu	cr0, %a, %a\n" freg r1 freg r2
+      fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
   | Pfcti(r1, r2) ->
-      fprintf oc "	fctiwz	f13, %a\n" freg r2;
-      fprintf oc "	stfd	f13, -8(r1)\n";
-      fprintf oc "	lwz	%a, -4(r1)\n" ireg r1
+      fprintf oc "	fctiwz	%a, %a\n" freg FPR13 freg r2;
+      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13 ireg GPR1;
+      fprintf oc "	lwz	%a, 4(%a)\n" ireg r1 ireg GPR1;
+      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1
   | Pfctiu(r1, r2) ->
       let lbl1 = new_label() in
       let lbl2 = new_label() in
       let lbl3 = new_label() in
-      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl1;
-      fprintf oc "	lfd	f13, lo16(L%d)(r12)\n" lbl1;
-      fprintf oc "	fcmpu	cr7, %a, f13\n" freg r2;
+      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12  label_high lbl1;
+      fprintf oc "	lfd	%a, %a(%a)\n" freg FPR13  label_low lbl1  ireg GPR12;
+      fprintf oc "	fcmpu	%a, %a, %a\n" creg 7  freg r2  freg FPR13;
       fprintf oc "	cror	30, 29, 30\n";
-      fprintf oc "	beq	cr7, L%d\n" lbl2;
-      fprintf oc "	fctiwz	f13, %a\n" freg r2;
-      fprintf oc "	stfdu	f13, -8(r1)\n";
-      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
-      fprintf oc "	b	L%d\n" lbl3;
-      fprintf oc "L%d:	fsub	f13, %a, f13\n" lbl2 freg r2;
-      fprintf oc "	fctiwz	f13, f13\n";
-      fprintf oc "	stfdu	f13, -8(r1)\n";
-      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
+      fprintf oc "	beq	%a, %a\n" creg 7  label lbl2;
+      fprintf oc "	fctiwz	%a, %a\n" freg FPR13  freg r2;
+      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13  ireg GPR1;
+      fprintf oc "	lwz	%a, 4(%a)\n" ireg r1  ireg GPR1;
+      fprintf oc "	b	%a\n" label lbl3;
+      fprintf oc "%a:	fsub	%a, %a, %a\n" label lbl2  freg FPR13  freg r2  freg FPR13;
+      fprintf oc "	fctiwz	%a, %a\n" freg FPR13  freg FPR13;
+      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13  ireg GPR1;
+      fprintf oc "	lwz	%a, 4(%a)\n" ireg r1  ireg GPR1;
       fprintf oc "	addis	%a, %a, 0x8000\n" ireg r1 ireg r1;
-      fprintf oc "L%d:	addi	r1, r1, 8\n" lbl3;
-      fprintf oc "	.const_data\n";
-      fprintf oc "L%d:	.long	0x41e00000, 0x00000000\n" lbl1;
-      fprintf oc "	.text\n"
+      fprintf oc "%a:	addi	%a, %a, 8\n" label lbl3  ireg GPR1  ireg GPR1;
+      const oc;
+      fprintf oc "%a:	.long	0x41e00000, 0x00000000\n" label lbl1;
+      text oc
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfmadd(r1, r2, r3, r4) ->
@@ -225,66 +393,68 @@ let print_instruction oc labels = function
       fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pictf(r1, r2) ->
       let lbl = new_label() in
-      fprintf oc "	addis	r12, 0, 0x4330\n";
-      fprintf oc "	stw	r12, -8(r1)\n";
-      fprintf oc "	addis	r12, %a, 0x8000\n" ireg r2;
-      fprintf oc "	stw	r12, -4(r1)\n";
-      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl;
-      fprintf oc "	lfd	f13, lo16(L%d)(r12)\n" lbl;
-      fprintf oc "	lfd	%a, -8(r1)\n" freg r1;
-      fprintf oc "	fsub	%a, %a, f13\n" freg r1 freg r1;
-      fprintf oc "	.const_data\n";
-      fprintf oc "L%d:	.long	0x43300000, 0x80000000\n" lbl;
-      fprintf oc "	.text\n"
+      fprintf oc "	addis	%a, 0, 0x4330\n" ireg GPR12;
+      fprintf oc "	stwu	%a, -8(%a)\n" ireg GPR12  ireg GPR1;
+      fprintf oc "	addis	%a, %a, 0x8000\n" ireg GPR12  ireg r2;
+      fprintf oc "	stw	%a, 4(%a)\n" ireg GPR12  ireg GPR1;
+      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12  label_high lbl;
+      fprintf oc "	lfd	%a, %a(%a)\n" freg FPR13  label_low lbl  ireg GPR12;
+      fprintf oc "	lfd	%a, 0(%a)\n" freg r1  ireg GPR1;
+      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1  ireg GPR1;
+      fprintf oc "	fsub	%a, %a, %a\n" freg r1  freg r1  freg FPR13;
+      const oc;
+      fprintf oc "%a:	.long	0x43300000, 0x80000000\n" label lbl;
+      text oc
   | Piuctf(r1, r2) ->
       let lbl = new_label() in
-      fprintf oc "	addis	r12, 0, 0x4330\n";
-      fprintf oc "	stw	r12, -8(r1)\n";
-      fprintf oc "	stw	%a, -4(r1)\n" ireg r2;
-      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl;
-      fprintf oc "	lfd	f13, lo16(L%d)(r12)\n" lbl;
-      fprintf oc "	lfd	%a, -8(r1)\n" freg r1;
-      fprintf oc "	fsub	%a, %a, f13\n" freg r1 freg r1;
-      fprintf oc "	.const_data\n";
-      fprintf oc "L%d:	.long	0x43300000, 0x00000000\n" lbl;
-      fprintf oc "	.text\n"
+      fprintf oc "	addis	%a, 0, 0x4330\n" ireg GPR12;
+      fprintf oc "	stwu	%a, -8(%a)\n" ireg GPR12  ireg GPR1;
+      fprintf oc "	stw	%a, 4(%a)\n" ireg r2  ireg GPR1;
+      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12  label_high lbl;
+      fprintf oc "	lfd	%a, %a(%a)\n" freg FPR13  label_low lbl  ireg GPR12;
+      fprintf oc "	lfd	%a, 0(%a)\n" freg r1  ireg GPR1;
+      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1  ireg GPR1;
+      fprintf oc "	fsub	%a, %a, %a\n" freg r1  freg r1  freg FPR13;
+      const oc;
+      fprintf oc "%a:	.long	0x43300000, 0x00000000\n" label lbl;
+      text oc
   | Plbz(r1, c, r2) ->
-      fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plbzx(r1, r2, r3) ->
       fprintf oc "	lbzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plfd(r1, c, r2) ->
-      fprintf oc "	lfd	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+      fprintf oc "	lfd	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Plfdx(r1, r2, r3) ->
       fprintf oc "	lfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Plfi(r1, c) ->
       let lbl = new_label() in
-      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl;
-      fprintf oc "	lfd	%a, lo16(L%d)(r12)\n" freg r1 lbl;
-      fprintf oc "	.const_data\n";
+      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
+      fprintf oc "	lfd	%a, %a(%a)\n" freg r1 label_low lbl ireg GPR12;
+      const oc;
       let n = Int64.bits_of_float c in
       let nlo = Int64.to_int32 n
       and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
-      fprintf oc "L%d:	.long	0x%lx, 0x%lx   ; %f\n" lbl nhi nlo c;
-      fprintf oc "	.text\n"
+      fprintf oc "%a:	.long	0x%lx, 0x%lx\n" label lbl nhi nlo;
+      text oc
   | Plfs(r1, c, r2) ->
-      fprintf oc "	lfs	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+      fprintf oc "	lfs	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Plfsx(r1, r2, r3) ->
       fprintf oc "	lfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Plha(r1, c, r2) ->
-      fprintf oc "	lha	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	lha	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plhax(r1, r2, r3) ->
       fprintf oc "	lhax	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plhz(r1, c, r2) ->
-      fprintf oc "	lhz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	lhz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plhzx(r1, r2, r3) ->
       fprintf oc "	lhzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plwz(r1, c, r2) ->
-      fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plwzx(r1, r2, r3) ->
       fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pmfcrbit(r1, bit) ->
-      fprintf oc "	mfcr	r2\n";
-      fprintf oc "	rlwinm	%a, r2, %d, 1\n" ireg r1 (1 + num_crbit bit)
+      fprintf oc "	mfcr	%a\n" ireg GPR12;
+      fprintf oc "	rlwinm	%a, %a, %d, 1\n" ireg r1  ireg GPR12  (1 + num_crbit bit)
   | Pmflr(r1) ->
       fprintf oc "	mflr	%a\n" ireg r1
   | Pmr(r1, r2) ->
@@ -294,7 +464,7 @@ let print_instruction oc labels = function
   | Pmtlr(r1) ->
       fprintf oc "	mtlr	%a\n" ireg r1
   | Pmulli(r1, r2, c) ->
-      fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pmullw(r1, r2, r3) ->
       fprintf oc "	mullw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pnand(r1, r2, r3) ->
@@ -306,9 +476,9 @@ let print_instruction oc labels = function
   | Porc(r1, r2, r3) ->
       fprintf oc "	orc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pori(r1, r2, c) ->
-      fprintf oc "	ori	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	ori	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Poris(r1, r2, c) ->
-      fprintf oc "	oris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	oris	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Prlwinm(r1, r2, c1, c2) ->
       fprintf oc "	rlwinm	%a, %a, %ld, 0x%lx\n"
                 ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
@@ -321,37 +491,38 @@ let print_instruction oc labels = function
   | Psrw(r1, r2, r3) ->
       fprintf oc "	srw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstb(r1, c, r2) ->
-      fprintf oc "	stb	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	stb	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Pstbx(r1, r2, r3) ->
       fprintf oc "	stbx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstfd(r1, c, r2) ->
-      fprintf oc "	stfd	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+      fprintf oc "	stfd	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Pstfdx(r1, r2, r3) ->
       fprintf oc "	stfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Pstfs(r1, c, r2) ->
-      fprintf oc "	stfs	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+      fprintf oc "	stfs	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Pstfsx(r1, r2, r3) ->
       fprintf oc "	stfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Psth(r1, c, r2) ->
-      fprintf oc "	sth	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	sth	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Psthx(r1, r2, r3) ->
       fprintf oc "	sthx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstw(r1, c, r2) ->
-      fprintf oc "	stw	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+      fprintf oc "	stw	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Pstwx(r1, r2, r3) ->
       fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfc(r1, r2, r3) ->
       fprintf oc "	subfc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfic(r1, r2, c) ->
-      fprintf oc "	subfic	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	subfic	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pxor(r1, r2, r3) ->
       fprintf oc "	xor	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pxori(r1, r2, c) ->
-      fprintf oc "	xori	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	xori	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pxoris(r1, r2, c) ->
-      fprintf oc "	xoris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+      fprintf oc "	xoris	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Plabel lbl ->
-      if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl
+      if Labelset.mem lbl labels then
+        fprintf oc "%a:\n" label (transl_label lbl)
 
 let rec labels_of_code = function
   | [] -> Labelset.empty
@@ -363,10 +534,18 @@ let print_function oc name code =
   Hashtbl.clear current_function_labels;
   fprintf oc "	.text\n";
   fprintf oc "	.align 2\n";
-  fprintf oc "	.globl %a\n" print_symb name;
-  fprintf oc "%a:\n" print_symb name;
+  fprintf oc "	.globl %a\n" symbol name;
+  fprintf oc "%a:\n" symbol name;
   List.iter (print_instruction oc (labels_of_code code)) code
 
+(* Generation of stub functions *)
+
+let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$"
+
+(* Stubs for MacOS X *)
+
+module Stubs_MacOS = struct
+
 (* Generation of stub code for variadic functions, e.g. printf.
    Calling conventions for variadic functions are:
      - always reserve 8 stack words (offsets 24 to 52) so that the
@@ -459,9 +638,7 @@ let non_variadic_stub oc name =
   fprintf oc "	.indirect_symbol _%s\n" name;
   fprintf oc "	.long	0\n"
 
-let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$"
-
-let print_external_function oc name ef =
+let stub_function oc name ef =
   let name = extern_atom name in
   fprintf oc "	.text\n";
   fprintf oc "	.align 2\n";
@@ -470,10 +647,56 @@ let print_external_function oc name ef =
   then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args
   else non_variadic_stub oc name
 
+let function_needs_stub name = true
+
+end
+
+(* Stubs for EABI *)
+
+module Stubs_EABI = struct
+
+let variadic_stub oc stub_name fun_name args =
+  fprintf oc "	.text\n";
+  fprintf oc "	.align 2\n";
+  fprintf oc ".L%s$stub:\n" stub_name;
+  (* bit 6 must be set if at least one argument is a float; clear otherwise *)
+  if List.mem Tfloat args
+  then fprintf oc "	creqv	6, 6, 6\n"
+  else fprintf oc "	crxor	6, 6, 6\n";
+  fprintf oc "	b	%s\n" fun_name
+
+let stub_function oc name ef =
+  let name = extern_atom name in
+  (* Only variadic functions need a stub *)
+  if Str.string_match re_variadic_stub name 0
+  then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args
+
+let function_needs_stub name =
+  Str.string_match re_variadic_stub (extern_atom name) 0
+
+end
+
+let function_needs_stub =
+  match target with
+  | MacOS -> Stubs_MacOS.function_needs_stub
+  | EABI  -> Stubs_EABI.function_needs_stub
+
+let stub_function =
+  match target with
+  | MacOS -> Stubs_MacOS.stub_function
+  | EABI  -> Stubs_EABI.stub_function
+
 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 ef
+  | External ef -> stub_function oc name ef
+
+let record_extfun (Coq_pair(name, defn)) =
+  match defn with
+  | Internal _ -> ()
+  | External _ -> 
+      if function_needs_stub name then
+        stubbed_functions := IdentSet.add name !stubbed_functions
 
 let init_data_queue = ref []
 
@@ -485,20 +708,19 @@ let print_init oc = function
   | 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
+      fprintf oc "	.long	%ld\n" (Int32.bits_of_float n)
   | Init_float64 n ->
       (* .quad not working on all versions of the MacOSX assembler *)
       let b = Int64.bits_of_float n in
-      fprintf oc "	.long	%Ld, %Ld ; %g \n"
+      fprintf oc "	.long	%Ld, %Ld\n"
                  (Int64.shift_right_logical b 32)
                  (Int64.logand b 0xFFFFFFFFL)
-                 n
   | Init_space n ->
       let n = camlint_of_z n in
       if n > 0l then fprintf oc "	.space	%ld\n" n
   | Init_pointer id ->
       let lbl = new_label() in
-      fprintf oc "	.long	L%d\n" lbl;
+      fprintf oc "	.long	%a\n" label lbl;
       init_data_queue := (lbl, id) :: !init_data_queue
 
 let print_init_data oc id =
@@ -509,7 +731,7 @@ let print_init_data oc id =
     | [] -> ()
     | (lbl, id) :: rem ->
         init_data_queue := rem;
-        fprintf oc "L%d:\n" lbl;
+        fprintf oc "%a:\n" label lbl;
         List.iter (print_init oc) id;
         print_remainder()
   in print_remainder()
@@ -520,12 +742,12 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   | _  ->
       fprintf oc "	.data\n";
       fprintf oc "	.align	3\n";
-      fprintf oc "	.globl	%a\n" print_symb name;
-      fprintf oc "%a:\n" print_symb name;
+      fprintf oc "	.globl	%a\n" symbol name;
+      fprintf oc "%a:\n" symbol name;
       print_init_data oc init_data
 
 let print_program oc p =
-  extfuns := IdentSet.empty;
+  stubbed_functions := IdentSet.empty;
   List.iter record_extfun p.prog_funct;
   List.iter (print_var oc) p.prog_vars;
   List.iter (print_fundef oc) p.prog_funct
diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v
index f641847..48e26a7 100644
--- a/powerpc/eabi/Stacklayout.v
+++ b/powerpc/eabi/Stacklayout.v
@@ -19,10 +19,13 @@ Require Import Bounds.
   the general shape of activation records is as follows,
   from bottom (lowest offsets) to top:
 - 8 reserved bytes.  The first 4 bytes hold the back pointer to the
-  activation record of the caller.  The next 4 bytes hold the
-  return address.
+  activation record of the caller.  The next 4 bytes are reserved
+  for called functions to store their return addresses.
+  Since we would rather store our return address in our own
+  frame, we will not use these 4 bytes, and just reserve them.
 - Space for outgoing arguments to function calls.
 - Local stack slots of integer type.
+- Saved return address into caller.
 - Saved values of integer callee-save registers used by the function.
 - One word of padding, if necessary to align the following data
   on a 8-byte boundary.
@@ -59,20 +62,21 @@ Record frame_env : Set := mk_frame_env {
 
 Definition make_env (b: bounds) :=
   let oil := 8 + 4 * b.(bound_outgoing) in    (* integer locals *)
-  let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *)
+  let ora := oil + 4 * b.(bound_int_local) in (* saved return address *)
+  let oics := ora + 4 in            (* integer callee-saves *)
   let oendi := oics + 4 * b.(bound_int_callee_save) in
   let ofl := align oendi 8 in       (* float locals *)
   let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
   let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *)
-  mk_frame_env sz 0 4
+  mk_frame_env sz 0 ora
                   oil oics b.(bound_int_callee_save)
                   ofl ofcs b.(bound_float_callee_save).
 
 
 Remark align_float_part:
   forall b,
-  8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <=
-  align (8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8.
+  8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b <=
+  align (8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b) 8.
 Proof.
   intros. apply align_le. omega.
 Qed.
diff --git a/test/c/aes.c b/test/c/aes.c
index 7734ccb..c430cc3 100644
--- a/test/c/aes.c
+++ b/test/c/aes.c
@@ -36,7 +36,7 @@ typedef unsigned char	u8;
 typedef unsigned short	u16;	
 typedef unsigned int	u32;
 
-#if defined(__ppc__)
+#if defined(__ppc__) || defined(__PPC__)
 #define ARCH_BIG_ENDIAN
 #elif defined(__i386__) || defined(__x86_64__)
 #undef ARCH_BIG_ENDIAN
diff --git a/test/c/sha1.c b/test/c/sha1.c
index ca187bf..49c5a13 100644
--- a/test/c/sha1.c
+++ b/test/c/sha1.c
@@ -5,7 +5,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-#if defined(__ppc__)
+#if defined(__ppc__) || defined(__PPC__)
 #define ARCH_BIG_ENDIAN
 #elif defined(__i386__) || defined(__x86_64__)
 #undef ARCH_BIG_ENDIAN