summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--powerpc/PrintAsm.ml504
-rw-r--r--powerpc/eabi/Stacklayout.v16
-rw-r--r--test/c/aes.c2
-rw-r--r--test/c/sha1.c2
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