PowerPC port: refactored the expansion of built-in functions and

pseudo-instructions so that it does not need to be re-done in
cchecklink.
cchecklink: updated accordingly.
testsuite: compile with -sdump and run cchecklink if supported.


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

5 files changed, 711 insertions, 507 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index a7e5eaf..ab52ca5 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -69,7 +69,8 @@ Inductive preg: Type :=
   | CR0_0: preg                         (**r bit 0 of the condition register  *)
   | CR0_1: preg                         (**r bit 1 of the condition register  *)
   | CR0_2: preg                         (**r bit 2 of the condition register  *)
-  | CR0_3: preg.                        (**r bit 3 of the condition register  *)
+  | CR0_3: preg                         (**r bit 3 of the condition register  *)
+  | CR1_2: preg.                        (**r bit 6 of the condition register  *)
 
 Coercion IR: ireg >-> preg.
 Coercion FR: freg >-> preg.
@@ -114,14 +115,15 @@ Inductive constant: Type :=
   range.  Of course, our PPC generator (file [Asmgen]) is
   careful to respect this range. *)
 
-(** Bits in the condition register.  We are only interested in the
-  first 4 bits. *)
+(** Bits in the condition register.  We are only interested in bits
+  0, 1, 2, 3 and 6. *)
 
 Inductive crbit: Type :=
   | CRbit_0: crbit
   | CRbit_1: crbit
   | CRbit_2: crbit
-  | CRbit_3: crbit.
+  | CRbit_3: crbit
+  | CRbit_6: crbit.
 
 (** The instruction set.  Most instructions correspond exactly to
   actual instructions of the PowerPC processor. See the PowerPC
@@ -134,12 +136,13 @@ Definition label := positive.
 
 Inductive instruction : Type :=
   | Padd: ireg -> ireg -> ireg -> instruction                 (**r integer addition *)
-  | Padde: ireg -> ireg -> ireg -> instruction                 (**r integer addition with carry *)
+  | Paddc: ireg -> ireg -> ireg -> instruction                (**r integer addition and set carry *)
+  | Padde: ireg -> ireg -> ireg -> instruction                (**r integer addition with carry *)
   | Paddi: ireg -> ireg -> constant -> instruction            (**r add immediate *)
-  | Paddic: ireg -> ireg -> constant -> instruction            (**r add immediate and set carry *)
+  | Paddic: ireg -> ireg -> constant -> instruction           (**r add immediate and set carry *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add carry *)
-  | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame *)
+  | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame (pseudo) *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -147,32 +150,39 @@ Inductive instruction : Type :=
   | Pb: label -> instruction                                  (**r unconditional branch *)
   | Pbctr: signature -> instruction                           (**r branch to contents of register CTR *)
   | Pbctrl: signature -> instruction                          (**r branch to contents of CTR and link *)
+  | Pbdnz: label -> instruction                               (**r decrement CTR and branch if not zero *)
   | Pbf: crbit -> label -> instruction                        (**r branch if false *)
   | Pbl: ident -> signature -> instruction                    (**r branch and link *)
   | Pbs: ident -> signature -> instruction                    (**r branch to symbol *)
   | Pblr: instruction                                         (**r branch to contents of register LR *)
   | Pbt: crbit -> label -> instruction                        (**r branch if true *)
-  | Pbtbl: ireg -> list label -> instruction                  (**r N-way branch through a jump table *)
+  | Pbtbl: ireg -> list label -> instruction                  (**r N-way branch through a jump table (pseudo) *)
   | Pcmplw: ireg -> ireg -> instruction                       (**r unsigned integer comparison *)
   | Pcmplwi: ireg -> constant -> instruction                  (**r same, with immediate argument *)
   | Pcmpw: ireg -> ireg -> instruction                        (**r signed integer comparison *)
   | Pcmpwi: ireg -> constant -> instruction                   (**r same, with immediate argument *)
+  | Pcntlz: ireg -> ireg -> instruction                       (**r count leading zeros *)
+  | Pcreqv: crbit -> crbit -> crbit -> instruction            (**r not-xor between condition bits *)
   | Pcror: crbit -> crbit -> crbit -> instruction             (**r or between condition bits *)
+  | Pcrxor: crbit -> crbit -> crbit -> instruction            (**r xor between condition bits *)
   | Pdivw: ireg -> ireg -> ireg -> instruction                (**r signed division *)
   | Pdivwu: ireg -> ireg -> ireg -> instruction               (**r unsigned division *)
+  | Peieio: instruction                                       (**r EIEIO barrier *)
   | Peqv: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-xor *)
   | Pextsb: ireg -> ireg -> instruction                       (**r 8-bit sign extension *)
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
-  | Pfreeframe: Z -> int -> instruction                       (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: Z -> int -> instruction                       (**r deallocate stack frame and restore previous frame (pseudo) *)
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfabss: freg -> freg -> instruction                       (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfadds: freg -> freg -> freg -> instruction               (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
-  | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion *)
+  | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion, round towards 0 (pseudo) *)
+  | Pfctiw: freg -> freg -> instruction                       (**r float-to-signed-int conversion, round by default *) 
+  | Pfctiwz: freg -> freg -> instruction                      (**r float-to-signed-int conversion, round towards 0 *) 
   | Pfdiv: freg -> freg -> freg -> instruction                (**r float division *)
   | Pfdivs: freg -> freg -> freg -> instruction               (**r float division *)
-  | Pfmake: freg -> ireg -> ireg -> instruction               (**r build a float from 2 ints *)
+  | Pfmake: freg -> ireg -> ireg -> instruction               (**r build a float from 2 ints (pseudo) *)
   | Pfmr: freg -> freg -> instruction                         (**r float move *)
   | Pfmul: freg -> freg -> freg -> instruction                (**r float multiply *)
   | Pfmuls: freg -> freg -> freg -> instruction               (**r float multiply *)
@@ -182,6 +192,15 @@ Inductive instruction : Type :=
   | Pfxdp: freg -> freg -> instruction                        (**r float extend to double precision (pseudo) *)
   | Pfsub: freg -> freg -> freg -> instruction                (**r float subtraction *)
   | Pfsubs: freg -> freg -> freg -> instruction               (**r float subtraction *)
+  | Pfmadd: freg -> freg -> freg -> freg -> instruction       (**r fused multiply-add *)
+  | Pfmsub: freg -> freg -> freg -> freg -> instruction       (**r fused multiply-sub *)
+  | Pfnmadd: freg -> freg -> freg -> freg -> instruction      (**r fused neg-multiply-add *)
+  | Pfnmsub: freg -> freg -> freg -> freg -> instruction      (**r fused neg-multiply-sub *)
+  | Pfsqrt: freg -> freg -> instruction                       (**r square root *)
+  | Pfrsqrte: freg -> freg -> instruction                     (**r approximate reciprocal of square root *)
+  | Pfres: freg -> freg -> instruction                        (**r approximate inverse *)
+  | Pfsel: freg -> freg -> freg -> freg -> instruction        (**r FP conditional move *)
+  | Pisync: instruction                                       (**r ISYNC barrier *)
   | Plbz: ireg -> constant -> ireg -> instruction             (**r load 8-bit unsigned int *)
   | Plbzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plfd: freg -> constant -> ireg -> instruction             (**r load 64-bit float *)
@@ -192,15 +211,19 @@ Inductive instruction : Type :=
   | Plfsx: freg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plha: ireg -> constant -> ireg -> instruction             (**r load 16-bit signed int *)
   | Plhax: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
+  | Plhbrx: ireg -> ireg -> ireg -> instruction               (**r load 16-bit int and reverse endianness *)
   | Plhz: ireg -> constant -> ireg -> instruction             (**r load 16-bit unsigned int *)
   | Plhzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plfi: freg -> float -> instruction                        (**r load float constant *)
   | Plfis: freg -> float32 -> instruction                     (**r load float constant *)
   | Plwz: ireg -> constant -> ireg -> instruction             (**r load 32-bit int *)
+  | Plwzu: ireg -> constant -> ireg -> instruction            (**r load 32-bit int with update *)
   | Plwzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plwz_a: ireg -> constant -> ireg -> instruction           (**r load 32-bit quantity to int reg *)
   | Plwzx_a: ireg -> ireg -> ireg -> instruction              (**r same, with 2 index regs *)
-  | Pmfcrbit: ireg -> crbit -> instruction                    (**r move condition bit to reg *)
+  | Plwbrx: ireg -> ireg -> ireg -> instruction               (**r load 32-bit int and reverse endianness *)
+  | Pmfcr: ireg -> instruction                                (**r move condition register to reg *)
+  | Pmfcrbit: ireg -> crbit -> instruction                    (**r move condition bit to reg (pseudo) *)
   | Pmflr: ireg -> instruction                                (**r move LR to reg *)
   | Pmr: ireg -> ireg -> instruction                          (**r integer move *)
   | Pmtctr: ireg -> instruction                               (**r move ireg to CTR *)
@@ -224,6 +247,7 @@ Inductive instruction : Type :=
   | Pstb: ireg -> constant -> ireg -> instruction             (**r store 8-bit int *)
   | Pstbx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Pstfd: freg -> constant -> ireg -> instruction            (**r store 64-bit float *)
+  | Pstfdu: freg -> constant -> ireg -> instruction           (**r store 64-bit float with update *)
   | Pstfdx: freg -> ireg -> ireg -> instruction               (**r same, with 2 index regs *)
   | Pstfd_a: freg -> constant -> ireg -> instruction          (**r store 64-bit quantity from float reg *)
   | Pstfdx_a: freg -> ireg -> ireg -> instruction             (**r same, with 2 index regs *)
@@ -231,19 +255,28 @@ Inductive instruction : Type :=
   | Pstfsx: freg -> ireg -> ireg -> instruction               (**r same, with 2 index regs *)
   | Psth: ireg -> constant -> ireg -> instruction             (**r store 16-bit int *)
   | Psthx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
+  | Psthbrx: ireg -> ireg -> ireg -> instruction              (**r store 16-bit int with reverse endianness *)
   | Pstw: ireg -> constant -> ireg -> instruction             (**r store 32-bit int *)
+  | Pstwu: ireg -> constant -> ireg -> instruction            (**r store 32-bit int with update *)
   | Pstwx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
+  | Pstwxu: ireg -> ireg -> ireg -> instruction               (**r same, with 2 index regs and update *)
   | Pstw_a: ireg -> constant -> ireg -> instruction           (**r store 32-bit quantity from int reg *)
   | Pstwx_a: ireg -> ireg -> ireg -> instruction              (**r same, with 2 index regs *)
+  | Pstwbrx: ireg -> ireg -> ireg -> instruction              (**r store 32-bit int with reverse endianness *)
   | Psubfc: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction *)
   | Psubfe: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction with carry *)
+  | Psubfze: ireg -> ireg -> instruction                      (**r integer opposite with carry *)
   | Psubfic: ireg -> ireg -> constant -> instruction          (**r integer subtraction from immediate *)
+  | Psync: instruction                                        (**r SYNC barrier *)
+  | Ptrap: instruction                                        (**r unconditional trap *)
   | Pxor: ireg -> ireg -> ireg -> instruction                 (**r bitwise xor *)
   | Pxori: ireg -> ireg -> constant -> instruction            (**r bitwise xor with immediate *)
   | Pxoris: ireg -> ireg -> constant -> instruction           (**r bitwise xor with immediate high *)
   | Plabel: label -> instruction                              (**r define a code label *)
-  | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *)
-  | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *)
+  | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *)
+  | Pannot: external_function -> list annot_param -> instruction (**r annotation statement (pseudo) *)
+  | Pcfi_adjust: int -> instruction                           (**r .cfi_adjust debug directive *)
+  | Pcfi_rel_offset: int -> instruction                       (**r .cfi_rel_offset lr debug directive *)
 
 with annot_param : Type :=
   | APreg: preg -> annot_param
@@ -528,6 +561,7 @@ Definition reg_of_crbit (bit: crbit) :=
   | CRbit_1 => CR0_1
   | CRbit_2 => CR0_2
   | CRbit_3 => CR0_3
+  | CRbit_6 => CR1_2
   end.
 
 Definition compare_sint (rs: regset) (v1 v2: val) :=
@@ -564,6 +598,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   match i with
   | Padd rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m
+  | Paddc rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2)
+                        #CARRY <- (Val.add_carry rs#r1 rs#r2 Vzero))) m
   | Padde rd r1 r2 =>
       Next (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY)
                         #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m
@@ -819,10 +856,44 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m
   | Plabel lbl =>
       Next (nextinstr rs) m
+  | Pcfi_rel_offset ofs =>
+      Next (nextinstr rs) m
   | Pbuiltin ef args res =>
       Stuck    (**r treated specially below *)
   | Pannot ef args =>
       Stuck    (**r treated specially below *)
+  (** The following instructions and directives are not generated directly by Asmgen,
+      so we do not model them. *)
+  | Pbdnz _
+  | Pcntlz _ _
+  | Pcreqv _ _ _
+  | Pcrxor _ _ _
+  | Peieio
+  | Pfctiw _ _
+  | Pfctiwz _ _
+  | Pfmadd _ _ _ _
+  | Pfmsub _ _ _ _
+  | Pfnmadd _ _ _ _
+  | Pfnmsub _ _ _ _
+  | Pfsqrt _ _
+  | Pfrsqrte _ _
+  | Pfres _ _
+  | Pfsel _ _ _ _
+  | Plwbrx _ _ _
+  | Pisync
+  | Plhbrx _ _ _
+  | Plwzu _ _ _
+  | Pmfcr _
+  | Pstwbrx _ _ _
+  | Pstfdu _ _ _
+  | Psthbrx _ _ _
+  | Pstwu _ _ _
+  | Pstwxu _ _ _
+  | Psubfze _ _
+  | Psync
+  | Ptrap
+  | Pcfi_adjust _ =>
+      Stuck
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
new file mode 100644
index 0000000..243a4d9
--- /dev/null
+++ b/powerpc/Asmexpand.ml
@@ -0,0 +1,525 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Expanding built-ins and some pseudo-instructions by rewriting
+   of the PPC assembly code. *)
+
+open Datatypes
+open Camlcoq
+open Integers
+open AST
+open Memdata
+open Asm
+
+(* Buffering the expanded code *)
+
+let current_code = ref ([]: instruction list)
+
+let emit i = current_code := i :: !current_code
+
+let emit_loadimm r n =
+  List.iter emit (Asmgen.loadimm r n [])
+
+let emit_addimm rd rs n =
+  List.iter emit (Asmgen.addimm rd rs n [])
+
+let get_code () =
+  let c = List.rev !current_code in current_code := []; c
+
+(* Generation of fresh labels *)
+
+let dummy_function = { fn_code = []; fn_sig = signature_main }
+let current_function = ref dummy_function
+let next_label = ref (None : label option)
+
+let new_label () =
+  let lbl =
+    match !next_label with
+    | Some l -> l
+    | None ->
+        (* on-demand computation of the next available label *)
+        List.fold_left
+          (fun next instr ->
+            match instr with
+            | Plabel l -> if P.lt l next then next else P.succ l
+            | _ -> next)
+          P.one (!current_function).fn_code
+  in
+    next_label := Some (P.succ lbl);
+    lbl
+
+let set_current_function f =
+  current_function := f; next_label := None
+
+(* Useful constants *)
+
+let _0 = Integers.Int.zero
+let _1 = Integers.Int.one
+let _2 = coqint_of_camlint 2l
+let _4 = coqint_of_camlint 4l
+let _6 = coqint_of_camlint 6l
+let _8 = coqint_of_camlint 8l
+let _m4 = coqint_of_camlint (-4l)
+let _m8 = coqint_of_camlint (-8l)
+
+(* Handling of annotations *)
+
+let expand_annot_val txt targ args res =
+  emit (Pannot(EF_annot(txt, [AA_arg targ]), List.map (fun r -> APreg r) args));
+  begin match args, res with
+  | [IR src], [IR dst] ->
+      if dst <> src then emit (Pmr(dst, src))
+  | [FR src], [FR dst] ->
+      if dst <> src then emit (Pfmr(dst, src))
+  | _, _ ->
+      assert false
+  end
+
+(* Handling of memcpy *)
+
+(* On the PowerPC, unaligned accesses to 16- and 32-bit integers are
+   fast, but unaligned accesses to 64-bit floats can be slow
+   (not so much on G5, but clearly so on Power7).
+   So, use 64-bit accesses only if alignment >= 4.
+   Note that lfd and stfd cannot trap on ill-formed floats. *)
+
+let expand_builtin_memcpy_small sz al src dst =
+  let rec copy ofs sz =
+    if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
+      emit (Plfd(FPR13, Cint ofs, src));
+      emit (Pstfd(FPR13, Cint ofs, dst));
+      copy (Int.add ofs _8) (sz - 8)
+    end else if sz >= 4 then begin
+      emit (Plwz(GPR0, Cint ofs, src));
+      emit (Pstw(GPR0, Cint ofs, dst));
+      copy (Int.add ofs _4) (sz - 4)
+    end else if sz >= 2 then begin
+      emit (Plhz(GPR0, Cint ofs, src));
+      emit (Psth(GPR0, Cint ofs, dst));
+      copy (Int.add ofs _2) (sz - 2)
+    end else if sz >= 1 then begin
+      emit (Plbz(GPR0, Cint ofs, src));
+      emit (Pstb(GPR0, Cint ofs, dst));
+      copy (Int.add ofs _1) (sz - 1)
+    end in
+  copy _0 sz
+
+let expand_builtin_memcpy_big sz al src dst =
+  assert (sz >= 4);
+  emit_loadimm GPR0 (Z.of_uint (sz / 4));
+  emit (Pmtctr GPR0);
+  let (s,d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in
+  emit (Paddi(s, src, Cint _m4));
+  emit (Paddi(d, dst, Cint _m4));
+  let lbl = new_label() in
+  emit (Plabel lbl);
+  emit (Plwzu(GPR0, Cint _4, s));
+  emit (Pstwu(GPR0, Cint _4, d));
+  emit (Pbdnz lbl);
+  (* s and d lag behind by 4 bytes *)
+  match sz land 3 with
+  | 1 -> emit (Plbz(GPR0, Cint _4, s));
+         emit (Pstb(GPR0, Cint _4, d))
+  | 2 -> emit (Plhz(GPR0, Cint _4, s));
+         emit (Psth(GPR0, Cint _4, d))
+  | 3 -> emit (Plhz(GPR0, Cint _4, s));
+         emit (Psth(GPR0, Cint _4, d));
+         emit (Plbz(GPR0, Cint _6, s));
+         emit (Pstb(GPR0, Cint _6, d))
+  | _ -> ()
+
+let expand_builtin_memcpy sz al args =
+  let (dst, src) =
+    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+  if sz <= (if !Clflags.option_ffpu && al >= 4
+            then if !Clflags.option_Osize then 35 else 51
+	    else if !Clflags.option_Osize then 19 else 27)
+  then expand_builtin_memcpy_small sz al src dst
+  else expand_builtin_memcpy_big sz al src dst
+
+(* Handling of volatile reads and writes *)
+
+let expand_builtin_vload_common chunk base offset res =
+  match chunk, res with
+  | Mint8unsigned, IR res ->
+      emit (Plbz(res, offset, base))
+  | Mint8signed, IR res ->
+      emit (Plbz(res, offset, base));
+      emit (Pextsb(res, res))
+  | Mint16unsigned, IR res ->
+      emit (Plhz(res, offset, base))
+  | Mint16signed, IR res ->
+      emit (Plha(res, offset, base))
+  | (Mint32 | Many32), IR res ->
+      emit (Plwz(res, offset, base))
+  | Mfloat32, FR res ->
+      emit (Plfs(res, offset, base))
+  | (Mfloat64 | Many64), FR res ->
+      emit (Plfd(res, offset, base))
+  (* Mint64 is special-cased below *)
+  | _ ->
+      assert false
+
+let expand_builtin_vload chunk args res =
+  begin match args, res with
+  | [IR addr], [res] when chunk <> Mint64 ->
+      expand_builtin_vload_common chunk addr (Cint _0) res
+  | [IR addr], [IR res1; IR res2] when chunk = Mint64 ->
+      if addr <> res1 then begin
+        emit (Plwz(res1, Cint _0, addr));
+        emit (Plwz(res2, Cint _4, addr))
+      end else begin
+        emit (Plwz(res2, Cint _4, addr));
+        emit (Plwz(res1, Cint _0, addr))
+      end
+  | _ ->
+      assert false
+  end
+
+let expand_builtin_vload_global chunk id ofs args res =
+  begin match res with
+  | [res] when chunk <> Mint64 ->
+      emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs)));
+      expand_builtin_vload_common chunk GPR11 (Csymbol_low(id, ofs)) res
+  | [IR res1; IR res2] when chunk = Mint64 ->
+      emit (Paddis(res1, GPR0, Csymbol_high(id, ofs)));
+      emit (Plwz(res1, Csymbol_low(id, ofs), res1));
+      let ofs = Int.add ofs _4 in
+      emit (Paddis(res2, GPR0, Csymbol_high(id, ofs)));
+      emit (Plwz(res2, Csymbol_low(id, ofs), res2))
+  | _ ->
+      assert false
+  end
+
+let expand_builtin_vload_sda chunk id ofs args res =
+  begin match res with
+  | [res] when chunk <> Mint64 ->
+      expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res
+  | [IR res1; IR res2] when chunk = Mint64 ->
+      emit (Plwz(res1, Csymbol_sda(id, ofs), GPR0));
+      let ofs = Int.add ofs _4 in
+      emit (Plwz(res2, Csymbol_sda(id, ofs), GPR0))
+  | _ ->
+      assert false
+  end
+
+let expand_builtin_vstore_common chunk base offset src =
+  match chunk, src with
+  | (Mint8signed | Mint8unsigned), IR src ->
+      emit (Pstb(src, offset, base))
+  | (Mint16signed | Mint16unsigned), IR src ->
+      emit (Psth(src, offset, base))
+  | (Mint32 | Many32), IR src ->
+      emit (Pstw(src, offset, base))
+  | Mfloat32, FR src ->
+      emit (Pstfs(src, offset, base))
+  | (Mfloat64 | Many64), FR src ->
+      emit (Pstfd(src, offset, base))
+  (* Mint64 is special-cased below *)
+  | _ ->
+      assert false
+
+let expand_builtin_vstore chunk args =
+  begin match args with
+  | [IR addr; src] when chunk <> Mint64 ->
+      expand_builtin_vstore_common chunk addr (Cint _0) src
+  | [IR addr; IR src1; IR src2] when chunk = Mint64 ->
+      emit (Pstw(src1, Cint _0, addr));
+      emit (Pstw(src2, Cint _4, addr))
+  | _ ->
+      assert false
+  end
+
+let expand_builtin_vstore_global chunk id ofs args =
+  begin match args with
+  | [src] when chunk <> Mint64 ->
+      let tmp = if src = IR GPR11 then GPR12 else GPR11 in
+      emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
+      expand_builtin_vstore_common chunk tmp (Csymbol_low(id, ofs)) src
+  | [IR src1; IR src2] when chunk = Mint64 ->
+      let tmp =
+        if not (List.mem GPR12 [src1; src2]) then GPR12 else
+        if not (List.mem GPR11 [src1; src2]) then GPR11 else GPR10 in
+      emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
+      emit (Pstw(src1, Csymbol_low(id, ofs), tmp));
+      let ofs = Int.add ofs _4 in
+      emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
+      emit (Pstw(src2, Csymbol_low(id, ofs), tmp))
+  | _ ->
+      assert false
+  end
+
+let expand_builtin_vstore_sda chunk id ofs args =
+  begin match args with
+  | [src] when chunk <> Mint64 ->
+      expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src
+  | [IR src1; IR src2] when chunk = Mint64 ->
+      emit (Pstw(src1, Csymbol_sda(id, ofs), GPR0));
+      emit (Pstw(src2, Csymbol_sda(id, ofs), GPR0))
+  | _ ->
+      assert false
+  end
+
+(* Handling of varargs *)
+
+let current_function_stacksize = ref 0l
+
+let align n a = (n + a - 1) land (-a)
+
+let rec next_arg_locations ir fr ofs = function
+  | [] ->
+      (ir, fr, ofs)
+  | (Tint | Tany32) :: l ->
+      if ir < 8
+      then next_arg_locations (ir + 1) fr ofs l
+      else next_arg_locations ir fr (ofs + 4) l
+  | (Tfloat | Tsingle | Tany64) :: l ->
+      if fr < 8
+      then next_arg_locations ir (fr + 1) ofs l
+      else next_arg_locations ir fr (align ofs 8 + 8) l
+  | Tlong :: l ->
+      if ir < 7
+      then next_arg_locations (align ir 2 + 2) fr ofs l
+      else next_arg_locations ir fr (align ofs 8 + 8) l
+
+let expand_builtin_va_start r =
+  if not (!current_function).fn_sig.sig_cc.cc_vararg then
+    invalid_arg "Fatal error: va_start used in non-vararg function";
+  let (ir, fr, ofs) =
+    next_arg_locations 0 0 0 (!current_function).fn_sig.sig_args in
+  emit_loadimm GPR0 (Z.of_uint ir);
+  emit (Pstb(GPR0, Cint _0, r));
+  emit_loadimm GPR0 (Z.of_uint fr);
+  emit (Pstb(GPR0, Cint _1, r));
+  emit_addimm GPR0 GPR1 (coqint_of_camlint
+                           Int32.(add (add !current_function_stacksize 8l)
+                                      (of_int ofs)));
+  emit (Pstw(GPR0, Cint _4, r));
+  emit_addimm GPR0 GPR1 (coqint_of_camlint
+                           Int32.(sub !current_function_stacksize 96l));
+  emit (Pstw(GPR0, Cint _8, r))
+
+(* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
+   two instructions, one computing the low 32 bits of the result,
+   followed by another computing the high 32 bits.  In cases where
+   the first instruction would overwrite arguments to the second
+   instruction, we must go through GPR0 to hold the low 32 bits of the result.
+*)
+
+let expand_int64_arith conflict rl fn =
+  if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl
+
+(* Handling of compiler-inlined builtins *)
+
+let expand_builtin_inline name args res =
+  (* Can use as temporaries: GPR0, FPR13 *)
+  match name, args, res with
+  (* Integer arithmetic *)
+  | "__builtin_mulhw", [IR a1; IR a2], [IR res] ->
+      emit (Pmulhw(res, a1, a2))
+  | "__builtin_mulhwu", [IR a1; IR a2], [IR res] ->
+      emit (Pmulhwu(res, a1, a2))
+  | "__builtin_cntlz", [IR a1], [IR res] ->
+      emit (Pcntlz(res, a1))
+  | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
+      emit (Pstwu(a1, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Plwbrx(res, GPR0, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
+  | "__builtin_bswap16", [IR a1], [IR res] ->
+      emit (Prlwinm(GPR0, a1, _8, coqint_of_camlint 0x0000FF00l));
+      emit (Prlwinm(res, a1, coqint_of_camlint 24l,
+                                  coqint_of_camlint 0x000000FFl));
+      emit (Por(res, GPR0, res))
+  (* Float arithmetic *)
+  | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] ->
+      emit (Pfmadd(res, a1, a2, a3))
+  | "__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] ->
+      emit (Pfmsub(res, a1, a2, a3))
+  | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] ->
+      emit (Pfnmadd(res, a1, a2, a3))
+  | "__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] ->
+      emit (Pfnmsub(res, a1, a2, a3))
+  | "__builtin_fabs", [FR a1], [FR res] ->
+      emit (Pfabs(res, a1))
+  | "__builtin_fsqrt", [FR a1], [FR res] ->
+      emit (Pfsqrt(res, a1))
+  | "__builtin_frsqrte", [FR a1], [FR res] ->
+      emit (Pfrsqrte(res, a1))
+  | "__builtin_fres", [FR a1], [FR res] ->
+      emit (Pfres(res, a1))
+  | "__builtin_fsel", [FR a1; FR a2; FR a3], [FR res] ->
+      emit (Pfsel(res, a1, a2, a3))
+  | "__builtin_fcti", [FR a1], [IR res] ->
+      emit (Pfctiw(FPR13, a1));
+      emit (Pstfdu(FPR13, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Plwz(res, Cint _4, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
+  (* 64-bit integer arithmetic *)
+  | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
+      expand_int64_arith (rl = ah) rl (fun rl' ->
+        emit (Psubfic(rl', al, Cint _0));
+        emit (Psubfze(rh, ah)))
+  | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+      expand_int64_arith (rl = ah || rl = bh) rl (fun rl' ->
+        emit (Paddc(rl', al, bl));
+        emit (Padde(rh, ah, bh)))
+  | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+      expand_int64_arith (rl = ah || rl = bh) rl (fun rl' ->
+        emit (Psubfc(rl', bl, al));
+        emit (Psubfe(rh, bh, ah)))
+  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+      expand_int64_arith (rl = a || rl = b) rl (fun rl' ->
+        emit (Pmullw(rl, a, b));
+        emit (Pmulhwu(rh, a, b)))
+  (* Memory accesses *)
+  | "__builtin_read16_reversed", [IR a1], [IR res] ->
+      emit (Plhbrx(res, GPR0, a1))
+  | "__builtin_read32_reversed", [IR a1], [IR res] ->
+      emit (Plwbrx(res, GPR0, a1))
+  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
+      emit (Psthbrx(a2, GPR0, a1))
+  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
+      emit (Pstwbrx(a2, GPR0, a1))
+  (* Synchronization *)
+  | "__builtin_eieio", [], _ ->
+      emit (Peieio)
+  | "__builtin_sync", [], _ ->
+      emit (Psync)
+  | "__builtin_isync", [], _ ->
+      emit (Pisync)
+  | "__builtin_trap", [], _ ->
+      emit (Ptrap)
+  (* Vararg stuff *)
+  | "__builtin_va_start", [IR a], _ ->
+      expand_builtin_va_start a
+  (* Catch-all *)
+  | _ ->
+      invalid_arg ("unrecognized builtin " ^ name)
+
+(* Calls to variadic functions: condition bit 6 must be set
+   if at least one argument is a float; clear otherwise.
+   Note that variadic functions cannot have arguments of type Tsingle. *)
+
+let set_cr6 sg =
+  if sg.sig_cc.cc_vararg then begin
+    if List.mem Tfloat sg.sig_args
+    then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6))
+    else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
+  end
+
+(* Expand instructions *)
+
+let num_crbit = function
+  | CRbit_0 -> 0
+  | CRbit_1 -> 1
+  | CRbit_2 -> 2
+  | CRbit_3 -> 3
+  | CRbit_6 -> 6
+
+let expand_instruction instr =
+  match instr with
+  | Pallocframe(sz, ofs) ->
+      let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
+      let sz = camlint_of_coqint sz in
+      assert (ofs = Int.zero);
+      let sz = if variadic then Int32.add sz 96l else sz in
+      let adj = Int32.neg sz in
+      if adj >= -0x8000l then
+        emit (Pstwu(GPR1, Cint(coqint_of_camlint adj), GPR1))
+      else begin
+        emit_loadimm GPR0 (coqint_of_camlint adj);
+        emit (Pstwxu(GPR1, GPR1, GPR0))
+      end;
+      emit (Pcfi_adjust (coqint_of_camlint sz));
+      if variadic then begin
+        emit (Pmflr GPR0);
+        emit (Pbl(intern_string "__compcert_va_saveregs",
+                  {sig_args = []; sig_res = None; sig_cc = cc_default}));
+        emit (Pmtlr GPR0)
+      end;
+      current_function_stacksize := sz
+  | Pbctr sg | Pbctrl sg | Pbl(_, sg) | Pbs(_, sg) ->
+      set_cr6 sg;
+      emit instr
+  | Pfreeframe(sz, ofs) ->
+      let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
+      let sz = camlint_of_coqint sz in
+      let sz = if variadic then Int32.add sz 96l else sz in
+      if sz < 0x8000l then
+        emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz)))
+      else
+        emit (Plwz(GPR1, Cint ofs, GPR1))
+  | Pfcti(r1, r2) ->
+      emit (Pfctiwz(FPR13, r2));
+      emit (Pstfdu(FPR13, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Plwz(r1, Cint _4, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
+  | Pfmake(rd, r1, r2) ->
+      emit (Pstwu(r1, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Pstw(r2, Cint _4, GPR1));
+      emit (Plfd(rd, Cint _0, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8);
+  | Pfxdp(r1, r2) ->
+      if r1 <> r2 then emit(Pfmr(r1, r2))
+  | Pmfcrbit(r1, bit) ->
+      emit (Pmfcr r1);
+      emit (Prlwinm(r1, r1, Z.of_uint (1 + num_crbit bit), _1))
+  | Pbuiltin(ef, args, res) ->
+      begin match ef with
+      | EF_builtin(name, sg) ->
+          expand_builtin_inline (extern_atom name) args res
+      | EF_vload chunk ->
+          expand_builtin_vload chunk args res
+      | EF_vstore chunk ->
+          expand_builtin_vstore chunk args
+      | EF_vload_global(chunk, id, ofs) ->
+          if symbol_is_small_data id ofs
+          then expand_builtin_vload_sda chunk id ofs args res
+          else expand_builtin_vload_global chunk id ofs args res
+      | EF_vstore_global(chunk, id, ofs) ->
+          if symbol_is_small_data id ofs
+          then expand_builtin_vstore_sda chunk id ofs args
+          else expand_builtin_vstore_global chunk id ofs args
+      | EF_memcpy(sz, al) ->
+          expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
+      | EF_annot_val(txt, targ) ->
+          expand_annot_val txt targ args res
+      | EF_inline_asm txt ->
+          emit instr
+      | _ ->
+          assert false
+      end
+  | _ ->
+      emit instr
+
+let expand_function fn =
+  set_current_function fn;
+  current_code := [];
+  List.iter expand_instruction fn.fn_code;
+  let c = get_code() in
+  set_current_function dummy_function;
+  { fn with fn_code = c }
+
+let expand_fundef = function
+  | Internal f -> Internal (expand_function f)
+  | External ef -> External ef
+
+let expand_program (p: Asm.program) : Asm.program =
+  AST.transform_program expand_fundef p
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 5ca770d..5c4ffde 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -721,7 +721,8 @@ Definition transl_function (f: Mach.function) :=
   OK (mkfunction f.(Mach.fn_sig)
        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
         Pmflr GPR0 ::
-        Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c)).
+        Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+        Pcfi_rel_offset f.(fn_retaddr_ofs) :: c)).
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
   do tf <- transl_function f;
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 913fb50..2b52fe0 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -918,30 +918,36 @@ Local Transparent destroyed_by_jumptable.
   set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)).
   set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))).
   set (rs4 := nextinstr rs3).
+  set (rs5 := nextinstr rs4).
   assert (EXEC_PROLOGUE:
             exec_straight tge x
               x.(fn_code) rs0 m'
-              x1 rs4 m3').
+              x1 rs5 m3').
   rewrite <- H5 at 2. simpl. 
-  apply exec_straight_three with rs2 m2' rs3 m2'.
+  apply exec_straight_step with rs2 m2'.
   unfold exec_instr. rewrite C. fold sp.
-  rewrite <- (sp_val _ _ _ AG). rewrite F. auto. 
-  simpl. auto.
+  rewrite <- (sp_val _ _ _ AG). rewrite F. auto. auto.
+  apply exec_straight_step with rs3 m2'.
+  simpl. auto. auto.
+  apply exec_straight_two with rs4 m3'.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
   change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. 
   rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence.
   auto. auto. auto.
-  left; exists (State rs4 m3'); split.
+  left; exists (State rs5 m3'); split.
   eapply exec_straight_steps_1; eauto. omega. constructor. 
   econstructor; eauto. 
-  change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). 
+  change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone).
   rewrite ATPC. simpl. constructor; eauto.
-  subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. 
+  subst x; simpl in g. unfold fn_code.
   eapply code_tail_next_int. omega. 
   eapply code_tail_next_int. omega. 
+  eapply code_tail_next_int. omega.
+  eapply code_tail_next_int. omega.
   constructor.
-  unfold rs4, rs3, rs2.
-  apply agree_nextinstr. apply agree_set_other; auto. apply agree_set_other; auto. 
+  unfold rs5, rs4, rs3, rs2.
+  apply agree_nextinstr. apply agree_nextinstr. 
+  apply agree_set_other; auto. apply agree_set_other; auto. 
   apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. unfold sp; congruence.
   congruence.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index e3f0724..691ecfb 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -102,6 +102,7 @@ let num_crbit = function
   | CRbit_1 -> 1
   | CRbit_2 -> 2
   | CRbit_3 -> 3
+  | CRbit_6 -> 6
 
 let crbit oc bit =
   fprintf oc "%d" (num_crbit bit)
@@ -287,16 +288,6 @@ let rolm_mask n =
   assert (!count = 2 || (!count = 0 && !last));
   (!mb, !me-1)
 
-(* Built-ins.  They come in three flavors: 
-   - annotation statements: take their arguments in registers or stack
-     locations; generate no code;
-   - inlined by the compiler: take their arguments in arbitrary
-     registers; preserve all registers except the reserved temporaries
-     (GPR0, GPR11, GPR12, FPR13);
-   - inlined while printing asm code; take their arguments in
-     locations dictated by the calling conventions; preserve
-     callee-save regs only. *)
-
 (* Handling of annotations *)
 
 let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
@@ -309,361 +300,6 @@ let print_annot_stmt oc txt targs args =
     PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
   end
 
-let print_annot_val oc txt args res =
-  fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_val preg oc txt args;
-  match args, res with
-  | [IR src], [IR dst] ->
-      if dst <> src then fprintf oc "	mr	%a, %a\n" ireg dst ireg src 
-  | [FR src], [FR dst] ->
-      if dst <> src then fprintf oc "	fmr	%a, %a\n" freg dst freg src 
-  | _, _ ->
-      assert false
-
-(* Handling of memcpy *)
-
-(* On the PowerPC, unaligned accesses to 16- and 32-bit integers are
-   fast, but unaligned accesses to 64-bit floats can be slow
-   (not so much on G5, but clearly so on Power7).
-   So, use 64-bit accesses only if alignment >= 4.
-   Note that lfd and stfd cannot trap on ill-formed floats. *)
-
-let print_builtin_memcpy_small oc sz al src dst =
-  let rec copy ofs sz =
-    if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
-      fprintf oc "	lfd	%a, %d(%a)\n" freg FPR13 ofs ireg src;
-      fprintf oc "	stfd	%a, %d(%a)\n" freg FPR13 ofs ireg dst;
-      copy (ofs + 8) (sz - 8)
-    end else if sz >= 4 then begin
-      fprintf oc "	lwz	%a, %d(%a)\n" ireg GPR0 ofs ireg src;
-      fprintf oc "	stw	%a, %d(%a)\n" ireg GPR0 ofs ireg dst;
-      copy (ofs + 4) (sz - 4)
-    end else if sz >= 2 then begin
-      fprintf oc "	lhz	%a, %d(%a)\n" ireg GPR0 ofs ireg src;
-      fprintf oc "	sth	%a, %d(%a)\n" ireg GPR0 ofs ireg dst;
-      copy (ofs + 2) (sz - 2)
-    end else if sz >= 1 then begin
-      fprintf oc "	lbz	%a, %d(%a)\n" ireg GPR0 ofs ireg src;
-      fprintf oc "	stb	%a, %d(%a)\n" ireg GPR0 ofs ireg dst;
-      copy (ofs + 1) (sz - 1)
-    end in
-  copy 0 sz
-
-let print_builtin_memcpy_big oc sz al src dst =
-  assert (sz >= 4);
-  fprintf oc "	li	%a, %d\n" ireg GPR0 (sz / 4);
-  fprintf oc "	mtctr	%a\n" ireg GPR0;
-  let (s,d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in
-  fprintf oc "	addi	%a, %a, -4\n" ireg s ireg src;
-  fprintf oc "	addi	%a, %a, -4\n" ireg d ireg dst;
-  let lbl = new_label() in
-  fprintf oc "%a:	lwzu	%a, 4(%a)\n" label lbl ireg GPR0 ireg s;
-  fprintf oc "	stwu	%a, 4(%a)\n" ireg GPR0 ireg d;
-  fprintf oc "	bdnz	%a\n" label lbl;
-  (* s and d lag behind by 4 bytes *)
-  match sz land 3 with
-  | 1 -> fprintf oc "	lbz	%a, 4(%a)\n" ireg GPR0 ireg s;
-         fprintf oc "	stb	%a, 4(%a)\n" ireg GPR0 ireg d
-  | 2 -> fprintf oc "	lhz	%a, 4(%a)\n" ireg GPR0 ireg s;
-         fprintf oc "	sth	%a, 4(%a)\n" ireg GPR0 ireg d
-  | 3 -> fprintf oc "	lhz	%a, 4(%a)\n" ireg GPR0 ireg s;
-         fprintf oc "	sth	%a, 4(%a)\n" ireg GPR0 ireg d;
-         fprintf oc "	lbz	%a, 6(%a)\n" ireg GPR0 ireg s;
-         fprintf oc "	stb	%a, 6(%a)\n" ireg GPR0 ireg d
-  | _ -> ()
-
-let print_builtin_memcpy oc sz al args =
-  let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
-  fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
-          comment sz al;
-  if sz <= (if !Clflags.option_ffpu then 48 else 24)
-  then print_builtin_memcpy_small oc sz al src dst
-  else print_builtin_memcpy_big oc sz al src dst;
-  fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment
-
-(* Handling of volatile reads and writes *)
-
-let print_builtin_vload_common oc chunk base offset res =
-  match chunk, res with
-  | Mint8unsigned, IR res ->
-      fprintf oc "	lbz	%a, %a(%a)\n" ireg res constant offset ireg base
-  | Mint8signed, IR res ->
-      fprintf oc "	lbz	%a, %a(%a)\n" ireg res constant offset ireg base;
-      fprintf oc "	extsb	%a, %a\n" ireg res ireg res
-  | Mint16unsigned, IR res ->
-      fprintf oc "	lhz	%a, %a(%a)\n" ireg res constant offset ireg base
-  | Mint16signed, IR res ->
-      fprintf oc "	lha	%a, %a(%a)\n" ireg res constant offset ireg base
-  | (Mint32 | Many32), IR res ->
-      fprintf oc "	lwz	%a, %a(%a)\n" ireg res constant offset ireg base
-  | Mfloat32, FR res ->
-      fprintf oc "	lfs	%a, %a(%a)\n" freg res constant offset ireg base
-  | (Mfloat64 | Many64), FR res ->
-      fprintf oc "	lfd	%a, %a(%a)\n" freg res constant offset ireg base
-  (* Mint64 is special-cased below *)
-  | _ ->
-      assert false
-
-let print_builtin_vload oc chunk args res =
-  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
-  begin match args, res with
-  | [IR addr], [res] when chunk <> Mint64 ->
-      print_builtin_vload_common oc chunk addr (Cint Integers.Int.zero) res
-  | [IR addr], [IR res1; IR res2] when chunk = Mint64 ->
-      if addr <> res1 then begin
-        fprintf oc "	lwz	%a, 0(%a)\n" ireg res1 ireg addr;
-        fprintf oc "	lwz	%a, 4(%a)\n" ireg res2 ireg addr
-      end else begin
-        fprintf oc "	lwz	%a, 4(%a)\n" ireg res2 ireg addr;
-        fprintf oc "	lwz	%a, 0(%a)\n" ireg res1 ireg addr
-      end
-  | _ ->
-      assert false
-  end;
-  fprintf oc "%s end builtin __builtin_volatile_read\n" comment
-
-let print_builtin_vload_global oc chunk id ofs args res =
-  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
-  begin match res with
-  | [res] when chunk <> Mint64 ->
-      fprintf oc "	addis	%a, %a, %a\n"
-                 ireg GPR11 ireg_or_zero GPR0 constant (Csymbol_high(id, ofs));
-      print_builtin_vload_common oc chunk GPR11 (Csymbol_low(id, ofs)) res
-  | [IR res1; IR res2] when chunk = Mint64 ->
-      fprintf oc "	addis	%a, %a, %a\n"
-                 ireg res1 ireg_or_zero GPR0 constant (Csymbol_high(id, ofs));
-      fprintf oc "	lwz	%a, %a(%a)\n"
-                 ireg res1 constant (Csymbol_low(id, ofs)) ireg res1;
-      let ofs = Integers.Int.add ofs (coqint_of_camlint 4l) in
-      fprintf oc "	addis	%a, %a, %a\n"
-                 ireg res2 ireg_or_zero GPR0 constant (Csymbol_high(id, ofs));
-      fprintf oc "	lwz	%a, %a(%a)\n"
-                 ireg res2 constant (Csymbol_low(id, ofs)) ireg res2
-  | _ ->
-      assert false
-  end;
-  fprintf oc "%s end builtin __builtin_volatile_read\n" comment
-
-let print_builtin_vstore_common oc chunk base offset src =
-  match chunk, src with
-  | (Mint8signed | Mint8unsigned), IR src ->
-      fprintf oc "	stb	%a, %a(%a)\n" ireg src constant offset ireg base
-  | (Mint16signed | Mint16unsigned), IR src ->
-      fprintf oc "	sth	%a, %a(%a)\n" ireg src constant offset ireg base
-  | (Mint32 | Many32), IR src ->
-      fprintf oc "	stw	%a, %a(%a)\n" ireg src constant offset ireg base
-  | Mfloat32, FR src ->
-      fprintf oc "	stfs	%a, %a(%a)\n" freg src constant offset ireg base
-  | (Mfloat64 | Many64), FR src ->
-      fprintf oc "	stfd	%a, %a(%a)\n" freg src constant offset ireg base
-  (* Mint64 is special-cased below *)
-  | _ ->
-      assert false
-
-let print_builtin_vstore oc chunk args =
-  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
-  begin match args with
-  | [IR addr; src] when chunk <> Mint64 ->
-      print_builtin_vstore_common oc chunk addr (Cint Integers.Int.zero) src
-  | [IR addr; IR src1; IR src2] when chunk = Mint64 ->
-      fprintf oc "	stw	%a, 0(%a)\n" ireg src1 ireg addr;
-      fprintf oc "	stw	%a, 4(%a)\n" ireg src2 ireg addr
-  | _ ->
-      assert false
-  end;
-  fprintf oc "%s end builtin __builtin_volatile_write\n" comment
-
-let print_builtin_vstore_global oc chunk id ofs args =
-  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
-  begin match args with
-  | [src] when chunk <> Mint64 ->
-      let tmp = if src = IR GPR11 then GPR12 else GPR11 in
-      fprintf oc "	addis	%a, %a, %a\n"
-                 ireg tmp ireg_or_zero GPR0 constant (Csymbol_high(id, ofs));
-      print_builtin_vstore_common oc chunk tmp (Csymbol_low(id, ofs)) src
-  | [IR src1; IR src2] when chunk = Mint64 ->
-      let tmp =
-        if not (List.mem GPR12 [src1; src2]) then GPR12 else
-        if not (List.mem GPR11 [src1; src2]) then GPR11 else GPR10 in
-      fprintf oc "	addis	%a, %a, %a\n"
-                 ireg tmp ireg_or_zero GPR0 constant (Csymbol_high(id, ofs));
-      fprintf oc "	stw	%a, %a(%a)\n"
-                 ireg src1 constant (Csymbol_low(id, ofs)) ireg tmp;
-      let ofs = Integers.Int.add ofs (coqint_of_camlint 4l) in
-      fprintf oc "	addis	%a, %a, %a\n"
-                 ireg tmp ireg_or_zero GPR0 constant (Csymbol_high(id, ofs));
-      fprintf oc "	stw	%a, %a(%a)\n"
-                 ireg src2 constant (Csymbol_low(id, ofs)) ireg tmp
-  | _ ->
-      assert false
-  end;
-  fprintf oc "%s end builtin __builtin_volatile_write\n" comment
-
-(* 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_locations ir fr ofs = function
-  | [] ->
-      (ir, fr, ofs)
-  | (Tint | Tany32) :: l ->
-      if ir < 8
-      then next_arg_locations (ir + 1) fr ofs l
-      else next_arg_locations ir fr (ofs + 4) l
-  | (Tfloat | Tsingle | Tany64) :: l ->
-      if fr < 8
-      then next_arg_locations ir (fr + 1) ofs l
-      else next_arg_locations ir fr (align ofs 8 + 8) l
-  | Tlong :: l ->
-      if ir < 7
-      then next_arg_locations (align ir 2 + 2) fr ofs l
-      else next_arg_locations ir fr (align ofs 8 + 8) l
-
-let print_builtin_va_start oc r =
-  if not (!current_function_sig).sig_cc.cc_vararg then
-    invalid_arg "Fatal error: va_start used in non-vararg function";
-  let (ir, fr, ofs) =
-    next_arg_locations 0 0 0 (!current_function_sig).sig_args in
-  fprintf oc "	li	%a, %d\n" ireg GPR0 ir;
-  fprintf oc "	stb     %a, 0(%a)\n" ireg GPR0 ireg r;
-  fprintf oc "	li	%a, %d\n" ireg GPR0 fr;
-  fprintf oc "	stb     %a, 1(%a)\n" ireg GPR0 ireg r;
-  fprintf oc "	addi	%a, %a, %ld\n" ireg GPR0 ireg GPR1
-                             Int32.(add (add !current_function_stacksize 8l)
-                                        (of_int ofs));
-  fprintf oc "	stw	%a, 4(%a)\n" ireg GPR0 ireg r;
-  fprintf oc "	addi	%a, %a, %ld\n" ireg GPR0 ireg GPR1
-                             Int32.(sub !current_function_stacksize 96l);
-  fprintf oc "	stw	%a, 8(%a)\n" ireg GPR0 ireg r
-
-(* Handling of compiler-inlined builtins *)
-
-let print_builtin_inline oc name args res =
-  fprintf oc "%s begin builtin %s\n" comment name;
-  (* Can use as temporaries: GPR0, FPR13 *)
-  begin match name, args, res with
-  (* Integer arithmetic *)
-  | "__builtin_mulhw", [IR a1; IR a2], [IR res] ->
-      fprintf oc "	mulhw	%a, %a, %a\n" ireg res ireg a1 ireg a2
-  | "__builtin_mulhwu", [IR a1; IR a2], [IR res] ->
-      fprintf oc "	mulhwu	%a, %a, %a\n" ireg res ireg a1 ireg a2
-  | "__builtin_cntlz", [IR a1], [IR res] ->
-      fprintf oc "	cntlzw	%a, %a\n" ireg res ireg a1
-  | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
-      fprintf oc "	stwu	%a, -8(%a)\n" ireg a1 ireg GPR1;
-      cfi_adjust oc 8l;
-      fprintf oc "	lwbrx	%a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
-      cfi_adjust oc (-8l)
-  | "__builtin_bswap16", [IR a1], [IR res] ->
-      fprintf oc "	rlwinm	%a, %a, 8, 16, 23\n" ireg GPR0 ireg a1;
-      fprintf oc "	rlwinm	%a, %a, 24, 24, 31\n" ireg res ireg a1;
-      fprintf oc "	or	%a, %a, %a\n" ireg res ireg GPR0 ireg res
-  (* Float arithmetic *)
-  | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] ->
-      fprintf oc "	fmadd	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
-  | "__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] ->
-      fprintf oc "	fmsub	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
-  | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] ->
-      fprintf oc "	fnmadd	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
-  | "__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] ->
-      fprintf oc "	fnmsub	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
-  | "__builtin_fabs", [FR a1], [FR res] ->
-      fprintf oc "	fabs	%a, %a\n" freg res freg a1
-  | "__builtin_fsqrt", [FR a1], [FR res] ->
-      fprintf oc "	fsqrt	%a, %a\n" freg res freg a1
-  | "__builtin_frsqrte", [FR a1], [FR res] ->
-      fprintf oc "	frsqrte	%a, %a\n" freg res freg a1
-  | "__builtin_fres", [FR a1], [FR res] ->
-      fprintf oc "	fres	%a, %a\n" freg res freg a1
-  | "__builtin_fsel", [FR a1; FR a2; FR a3], [FR res] ->
-      fprintf oc "	fsel	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
-  | "__builtin_fcti", [FR a1], [IR res] ->
-      fprintf oc "	fctiw	%a, %a\n" freg FPR13 freg a1;
-      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13 ireg GPR1;
-      cfi_adjust oc 8l;
-      fprintf oc "	lwz	%a, 4(%a)\n" ireg res ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
-      cfi_adjust oc (-8l)
-  (* 64-bit integer arithmetic *)
-  | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
-      if rl = ah then begin
-        fprintf oc "	subfic	%a, %a, 0\n" ireg GPR0 ireg al;
-        fprintf oc "	subfze	%a, %a\n" ireg rh ireg ah;
-        fprintf oc "	mr	%a, %a\n" ireg rl ireg GPR0
-      end else begin
-        fprintf oc "	subfic	%a, %a, 0\n" ireg rl ireg al;
-        fprintf oc "	subfze	%a, %a\n" ireg rh ireg ah
-      end
-  | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      if rl = ah || rl = bh then begin
-        fprintf oc "	addc	%a, %a, %a\n" ireg GPR0 ireg al ireg bl;
-        fprintf oc "	adde	%a, %a, %a\n" ireg rh ireg ah ireg bh;
-        fprintf oc "	mr	%a, %a\n" ireg rl ireg GPR0
-      end else begin
-        fprintf oc "	addc	%a, %a, %a\n" ireg rl ireg al ireg bl;
-        fprintf oc "	adde	%a, %a, %a\n" ireg rh ireg ah ireg bh
-      end
-  | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      if rl = ah || rl = bh then begin
-        fprintf oc "	subfc	%a, %a, %a\n" ireg GPR0 ireg bl ireg al;
-        fprintf oc "	subfe	%a, %a, %a\n" ireg rh ireg bh ireg ah;
-        fprintf oc "	mr	%a, %a\n" ireg rl ireg GPR0
-      end else begin
-        fprintf oc "	subfc	%a, %a, %a\n" ireg rl ireg bl ireg al;
-        fprintf oc "	subfe	%a, %a, %a\n" ireg rh ireg bh ireg ah
-      end
-  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
-      if rl = a || rl = b then begin
-        fprintf oc "	mullw	%a, %a, %a\n" ireg GPR0 ireg a ireg b;
-        fprintf oc "	mulhwu	%a, %a, %a\n" ireg rh ireg a ireg b;
-        fprintf oc "	mr	%a, %a\n" ireg rl ireg GPR0
-      end else begin
-        fprintf oc "	mullw	%a, %a, %a\n" ireg rl ireg a ireg b;
-        fprintf oc "	mulhwu	%a, %a, %a\n" ireg rh ireg a ireg b
-      end
-  (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
-      fprintf oc "	lhbrx	%a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg a1
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
-      fprintf oc "	lwbrx	%a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg a1
-  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
-      fprintf oc "	sthbrx	%a, %a, %a\n" ireg a2 ireg_or_zero GPR0 ireg a1
-  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
-      fprintf oc "	stwbrx	%a, %a, %a\n" ireg a2 ireg_or_zero GPR0 ireg a1
-  (* Synchronization *)
-  | "__builtin_eieio", [], _ ->
-      fprintf oc "	eieio\n"
-  | "__builtin_sync", [], _ ->
-      fprintf oc "	sync\n"
-  | "__builtin_isync", [], _ ->
-      fprintf oc "	isync\n"
-  | "__builtin_trap", [], _ ->
-      fprintf oc "	trap\n"
-  (* Vararg stuff *)
-  | "__builtin_va_start", [IR a], _ ->
-      print_builtin_va_start oc a
-  (* Catch-all *)
-  | _ ->
-      invalid_arg ("unrecognized builtin " ^ name)
-  end;
-  fprintf oc "%s end builtin %s\n" comment name
-
-(* Calls to variadic functions: condition bit 6 must be set
-   if at least one argument is a float; clear otherwise *)
-
-let set_cr6 oc sg =
-  if sg.sig_cc.cc_vararg then begin
-    if List.mem Tfloat sg.sig_args
-    then fprintf oc "	creqv	6, 6, 6\n"
-    else fprintf oc "	crxor	6, 6, 6\n"
-  end
-
 (* Determine if the displacement of a conditional branch fits the short form *)
 
 let short_cond_branch tbl pc lbl_dest =
@@ -681,6 +317,8 @@ 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
+  | Paddc(r1, r2, r3) ->
+      fprintf oc "	addc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Padde(r1, r2, r3) ->
       fprintf oc "	adde	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Paddi(r1, r2, c) ->
@@ -692,28 +330,7 @@ let print_instruction oc tbl pc fallthrough = function
   | Paddze(r1, r2) ->
       fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
   | Pallocframe(sz, ofs) ->
-      let sz = camlint_of_coqint sz
-      and ofs = camlint_of_coqint ofs in
-      assert (ofs = 0l);
-      let sz = 
-        if (!current_function_sig).sig_cc.cc_vararg
-        then Int32.add sz 96l
-        else sz in
-      let adj = Int32.neg sz in
-      if adj >= -0x8000l then
-        fprintf oc "	stwu	%a, %ld(%a)\n" ireg GPR1 adj ireg GPR1
-      else begin
-        fprintf oc "	addis	%a, 0, %ld\n" ireg GPR0 (Int32.shift_right_logical adj 16);
-        fprintf oc "	ori	%a, %a, %ld\n" ireg GPR0 ireg GPR0 (Int32.logand adj 0xFFFFl);
-        fprintf oc "	stwux	%a, %a, %a\n" ireg GPR1 ireg GPR1 ireg GPR0
-      end;
-      cfi_adjust oc sz;
-      if (!current_function_sig).sig_cc.cc_vararg then begin
-        fprintf oc "	mflr	%a\n" ireg GPR0;
-        fprintf oc "	bl	__compcert_va_saveregs\n";
-        fprintf oc "	mtlr	%a\n" ireg GPR0
-      end;
-      current_function_stacksize := sz
+      assert false
   | Pand_(r1, r2, r3) ->
       fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pandc(r1, r2, r3) ->
@@ -725,11 +342,11 @@ let print_instruction oc tbl pc fallthrough = function
   | Pb lbl ->
       fprintf oc "	b	%a\n" label (transl_label lbl)
   | Pbctr sg ->
-      set_cr6 oc sg;
       fprintf oc "	bctr\n"
   | Pbctrl sg ->
-      set_cr6 oc sg;
       fprintf oc "	bctrl\n"
+  | Pbdnz lbl ->
+      fprintf oc "	bdnz	%a\n" label (transl_label lbl)
   | Pbf(bit, lbl) ->
       if !Clflags.option_faligncondbranchs > 0 then
         fprintf oc "	.balign	%d\n" !Clflags.option_faligncondbranchs;
@@ -742,10 +359,8 @@ let print_instruction oc tbl pc fallthrough = function
         fprintf oc "%a:\n" label next
       end
   | Pbl(s, sg) ->
-      set_cr6 oc sg;
       fprintf oc "	bl	%a\n" symbol s
   | Pbs(s, sg) ->
-      set_cr6 oc sg;
       fprintf oc "	b	%a\n" symbol s
   | Pblr ->
       fprintf oc "	blr\n"
@@ -781,12 +396,20 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	cmpw	%a, %a, %a\n" creg 0 ireg r1 ireg r2
   | Pcmpwi(r1, c) ->
       fprintf oc "	cmpwi	%a, %a, %a\n" creg 0 ireg r1 constant c
+  | Pcntlz(r1, r2) ->
+      fprintf oc "	cntlz	%a, %a\n" ireg r1 ireg r2
+  | Pcreqv(c1, c2, c3) ->
+      fprintf oc "	creqv	%a, %a, %a\n" crbit c1 crbit c2 crbit c3
   | Pcror(c1, c2, c3) ->
       fprintf oc "	cror	%a, %a, %a\n" crbit c1 crbit c2 crbit c3
+  | Pcrxor(c1, c2, c3) ->
+      fprintf oc "	crxor	%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) ->
       fprintf oc "	divwu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Peieio ->
+      fprintf oc "	eieio\n"
   | Peqv(r1, r2, r3) ->
       fprintf oc "	eqv	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pextsb(r1, r2) ->
@@ -794,16 +417,7 @@ let print_instruction oc tbl pc fallthrough = function
   | Pextsh(r1, r2) ->
       fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
   | Pfreeframe(sz, ofs) ->
-      let sz = camlint_of_coqint sz
-      and ofs = camlint_of_coqint ofs in
-      let sz = 
-        if (!current_function_sig).sig_cc.cc_vararg
-        then Int32.add sz 96l
-        else sz in
-      if sz < 0x8000l then
-        fprintf oc "	addi	%a, %a, %ld\n" ireg GPR1 ireg GPR1 sz
-      else
-        fprintf oc "	lwz	%a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1
+      assert false
   | Pfabs(r1, r2) | Pfabss(r1, r2) ->
       fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
   | Pfadd(r1, r2, r3) ->
@@ -813,28 +427,17 @@ let print_instruction oc tbl pc fallthrough = function
   | Pfcmpu(r1, r2) ->
       fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
   | Pfcti(r1, r2) ->
-      fprintf oc "%s begin pseudoinstr %a = fcti(%a)\n" comment ireg r1 freg r2;
-      fprintf oc "	fctiwz	%a, %a\n" freg FPR13 freg r2;
-      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13 ireg GPR1;
-      cfi_adjust oc 8l;
-      fprintf oc "	lwz	%a, 4(%a)\n" ireg r1 ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
-      cfi_adjust oc (-8l);
-      fprintf oc "%s end pseudoinstr fcti\n" comment
+      assert false
+  | Pfctiw(r1, r2) ->
+      fprintf oc "	fctiw	%a, %a\n" freg r1 freg r2
+  | Pfctiwz(r1, r2) ->
+      fprintf oc "	fctiwz	%a, %a\n" freg r1 freg r2
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfdivs(r1, r2, r3) ->
       fprintf oc "	fdivs	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfmake(rd, r1, r2) ->
-      fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n"
-              comment freg rd ireg r1 ireg r2;
-      fprintf oc "	stwu	%a, -8(%a)\n" ireg r1 ireg GPR1;
-      cfi_adjust oc 8l;
-      fprintf oc "	stw	%a, 4(%a)\n" ireg r2 ireg GPR1;
-      fprintf oc "	lfd	%a, 0(%a)\n" freg rd ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
-      cfi_adjust oc (-8l);
-      fprintf oc "%s end pseudoinstr fmake\n" comment
+      assert false
   | Pfmr(r1, r2) ->
       fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
   | Pfmul(r1, r2, r3) ->
@@ -846,12 +449,29 @@ let print_instruction oc tbl pc fallthrough = function
   | Pfrsp(r1, r2) ->
       fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
   | Pfxdp(r1, r2) ->
-      if r1 <> r2 then
-        fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
+      assert false
   | Pfsub(r1, r2, r3) ->
       fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfsubs(r1, r2, r3) ->
       fprintf oc "	fsubs	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pfmadd(r1, r2, r3, r4) ->
+      fprintf oc "	fmadd	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfmsub(r1, r2, r3, r4) ->
+      fprintf oc "	fmsub	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfnmadd(r1, r2, r3, r4) ->
+      fprintf oc "	fnmadd	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfnmsub(r1, r2, r3, r4) ->
+      fprintf oc "	fnmsub	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfsqrt(r1, r2) ->
+      fprintf oc "	fsqrt	%a, %a\n" freg r1 freg r2    
+  | Pfrsqrte(r1, r2) ->
+      fprintf oc "	frsqrte	%a, %a\n" freg r1 freg r2    
+  | Pfres(r1, r2) ->
+      fprintf oc "	fres	%a, %a\n" freg r1 freg r2    
+  | Pfsel(r1, r2, r3, r4) ->
+      fprintf oc "	fsel	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pisync ->
+      fprintf oc "	isync\n"
   | Plbz(r1, c, r2) ->
       fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plbzx(r1, r2, r3) ->
@@ -860,16 +480,6 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	lfd	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Plfdx(r1, r2, r3) | Plfdx_a(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	%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;
-  | Plfis(r1, c) ->
-      let lbl = new_label() in
-      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
-      fprintf oc "	lfs	%a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c);
-      float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals;
   | Plfs(r1, c, r2) ->
       fprintf oc "	lfs	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Plfsx(r1, r2, r3) ->
@@ -878,20 +488,36 @@ let print_instruction oc tbl pc fallthrough = function
       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
+  | Plhbrx(r1, r2, r3) ->
+      fprintf oc "	lhbrx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plhz(r1, c, 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
+  | Plfi(r1, c) ->
+      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;
+  | Plfis(r1, c) ->
+      let lbl = new_label() in
+      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
+      fprintf oc "	lfs	%a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c);
+      float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals;
+  | Plwbrx(r1, r2, r3) ->
+      fprintf oc "	lwbrx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) ->
       fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 constant c ireg r2
+  | Plwzu(r1, c, r2) ->
+      fprintf oc "	lwzu	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) ->
       fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pmfcr(r1) ->
+      fprintf oc "	mfcr	%a\n" ireg r1
   | Pmfcrbit(r1, bit) ->
-      fprintf oc "	mfcr	%a\n" ireg r1;
-      fprintf oc "	rlwinm	%a, %a, %d, 31, 31\n" ireg r1  ireg r1 (1 + num_crbit bit)
+      assert false
   | Pmflr(r1) ->
-      fprintf oc "	mflr	%a\n" ireg r1;
-      cfi_rel_offset oc "lr" 8l
+      fprintf oc "	mflr	%a\n" ireg r1
   | Pmr(r1, r2) ->
       fprintf oc "	mr	%a, %a\n" ireg r1 ireg r2
   | Pmtctr(r1) ->
@@ -942,6 +568,8 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	stbx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) ->
       fprintf oc "	stfd	%a, %a(%a)\n" freg r1 constant c ireg r2
+  | Pstfdu(r1, c, r2) ->
+      fprintf oc "	stfdu	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Pstfdx(r1, r2, r3) | Pstfdx_a(r1, r2, r3) ->
       fprintf oc "	stfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Pstfs(r1, c, r2) ->
@@ -952,16 +580,30 @@ let print_instruction oc tbl pc fallthrough = function
       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
+  | Psthbrx(r1, r2, r3) ->
+      fprintf oc "	sthbrx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) ->
       fprintf oc "	stw	%a, %a(%a)\n" ireg r1 constant c ireg r2
+  | Pstwu(r1, c, r2) ->
+      fprintf oc "	stwu	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) ->
       fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pstwxu(r1, r2, r3) ->
+      fprintf oc "	stwxu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pstwbrx(r1, r2, r3) ->
+      fprintf oc "	stwbrx	%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
   | Psubfe(r1, r2, r3) ->
       fprintf oc "	subfe	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Psubfze(r1, r2) ->
+      fprintf oc "	subfze	%a, %a\n" ireg r1 ireg r2
   | Psubfic(r1, r2, c) ->
       fprintf oc "	subfic	%a, %a, %a\n" ireg r1 ireg r2 constant c
+  | Psync ->
+      fprintf oc "	sync\n"
+  | Ptrap ->
+      fprintf oc "	trap\n"
   | Pxor(r1, r2, r3) ->
       fprintf oc "	xor	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pxori(r1, r2, c) ->
@@ -974,21 +616,6 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "%a:\n" label (transl_label lbl)
   | Pbuiltin(ef, args, res) ->
       begin match ef with
-      | EF_builtin(name, sg) ->
-          print_builtin_inline oc (extern_atom name) args res
-      | EF_vload chunk ->
-          print_builtin_vload oc chunk args res
-      | EF_vstore chunk ->
-          print_builtin_vstore oc chunk args
-      | EF_vload_global(chunk, id, ofs) ->
-          print_builtin_vload_global oc chunk id ofs args res
-      | EF_vstore_global(chunk, id, ofs) ->
-          print_builtin_vstore_global oc chunk id ofs args
-      | EF_memcpy(sz, al) ->
-          print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
-                                  (Int32.to_int (camlint_of_coqint al)) args
-      | EF_annot_val(txt, targ) ->
-          print_annot_val oc (extern_atom txt) args res
       | EF_inline_asm txt ->
           fprintf oc "%s begin inline assembly\n" comment;
           fprintf oc "	%s\n" (extern_atom txt);
@@ -1003,6 +630,10 @@ let print_instruction oc tbl pc fallthrough = function
       | _ ->
           assert false
       end
+  | Pcfi_adjust n ->
+      cfi_adjust oc (camlint_of_coqint n)
+  | Pcfi_rel_offset n ->
+      cfi_rel_offset oc "lr" (camlint_of_coqint n)
 
 (* Determine if an instruction falls through *)
 
@@ -1017,44 +648,15 @@ let instr_fall_through = function
    PowerPC instructions.  We can over-approximate. *)
 
 let instr_size = function
-  | Pallocframe(sz, ofs) -> 3
   | Pbf(bit, lbl) -> 2
   | Pbt(bit, lbl) -> 2
-  | Pbtbl(r, tbl) -> 4
-  | Pfcti(r1, r2) -> 4
-  | Pfmake(rd, r1, r2) -> 4
+  | Pbtbl(r, tbl) -> 5
   | Plfi(r1, c) -> 2
-  | Pmfcrbit(r1, bit) -> 2
-  | Pstfs(r1, c, r2) -> 2
-  | Pstfsx(r1, r2, r3) -> 2
+  | Plfis(r1, c) -> 2
   | Plabel lbl -> 0
-  | Pbuiltin(ef, args, res) ->
-      begin match ef with
-      | EF_builtin(name, sg) ->
-          begin match extern_atom name with
-          | "__builtin_bswap" | "__builtin_bswap32" | "__builtin_bswap16" -> 3
-          | "__builtin_fcti" -> 4
-          | _ -> 1
-          end
-      | EF_vload chunk ->
-          if chunk = Mint8signed then 2 else 1
-      | EF_vstore chunk ->
-          if chunk = Mfloat32 then 2 else 1
-      | EF_vload_global(chunk, id, ofs) ->
-          if chunk = Mint8signed then 3 else 2
-      | EF_vstore_global(chunk, id, ofs) ->
-          if chunk = Mfloat32 then 3 else 2
-      | EF_memcpy(sz, al) ->
-          let sz = Int32.to_int (camlint_of_coqint sz) in
-          if sz <= 64 then (sz / 4) * 2 + 6 else 11
-      | EF_annot_val(txt, targ) ->
-          0
-      | EF_inline_asm txt ->
-          8 (* reasonable? default *)
-      | _ ->
-          assert false
-      end
+  | Pbuiltin(ef, args, res) -> 0
   | Pannot(ef, args) -> 0
+  | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
   | _ -> 1
 
 (* Build a table label -> estimated position in generated code.
@@ -1094,7 +696,6 @@ let print_function oc name fn =
   float_literals := [];
   float32_literals := [];
   jumptables := [];
-  current_function_sig := fn.fn_sig;
   let (text, lit, jmptbl) =
     match C2C.atom_sections name with
     | [t;l;j] -> (t, l, j)