Use PowerPC 64 bits instructions (when available) for int<->FP conversions.

Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence.

Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".

14 files changed, 170 insertions, 14 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 058b057f..cf1a0fe3 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -43,3 +43,7 @@ Global Opaque big_endian
               default_pl_64 choose_binop_pl_64
               default_pl_32 choose_binop_pl_32
               float_of_single_preserves_sNaN.
+
+(** Can we use the 64-bit extensions to the PowerPC architecture? *)
+Parameter ppc64: bool.
+
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 3c7bdd15..c1cc1052 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -178,13 +178,19 @@ Inductive instruction : Type :=
   | 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 *)
+  | Pextsw: ireg -> ireg -> instruction                       (**r 64-bit sign extension (PPC64) *)
   | 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 *)
+  | Pfcfi: freg -> ireg -> instruction                        (**r signed-int-to-float conversion (pseudo, PPC64) *)
+  | Pfcfiu: freg -> ireg -> instruction                       (**r unsigned-int-to-float conversion (pseudo, PPC64) *)
+  | Pfcfid: freg -> freg -> instruction                       (**r signed-long-to-float conversion (PPC64) *)
   | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion, round towards 0 (pseudo) *)
+  | Pfctiu: ireg -> freg -> instruction                       (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *)
+  | Pfctidz: freg -> freg -> instruction                      (**r float-to-signed-long conversion, round towards 0 (PPC64) *) 
   | 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 *)
@@ -252,6 +258,7 @@ Inductive instruction : Type :=
   | Porc: ireg -> ireg -> ireg -> instruction                 (**r bitwise or-complement *)
   | Pori: ireg -> ireg -> constant -> instruction             (**r or with immediate *)
   | Poris: ireg -> ireg -> constant -> instruction            (**r or with immediate high *)
+  | Prldicl: ireg -> ireg -> int -> int -> instruction        (**r rotate and mask left (PPC64) *)
   | Prlwinm: ireg -> ireg -> int -> int -> instruction        (**r rotate and mask *)
   | Prlwimi: ireg -> ireg -> int -> int -> instruction        (**r rotate and insert *)
   | Pslw: ireg -> ireg -> ireg -> instruction                 (**r shift left *)
@@ -260,6 +267,7 @@ Inductive instruction : Type :=
   | Psrw: ireg -> ireg -> ireg -> instruction                 (**r shift right unsigned *)
   | Pstb: ireg -> constant -> ireg -> instruction             (**r store 8-bit int *)
   | Pstbx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
+  | Pstdu: ireg -> constant -> ireg -> instruction           (**r store 64-bit integer with update (PPC64) *)
   | 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 *)
@@ -716,8 +724,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
   | Pfcmpu r1 r2 =>
       Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
+  | Pfcfi rd r1 =>
+      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m
+  | Pfcfiu rd r1 =>
+      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m
   | Pfcti rd r1 =>
       Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
+  | Pfctiu rd r1 =>
+      Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m
   | Pfdiv rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
   | Pfdivs rd r1 r2 =>
@@ -883,7 +897,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pdcbtst _ _ _
   | Pdcbtls _ _ _
   | Pdcbz _ _
+  | Pextsw _ _
   | Peieio
+  | Pfcfid _ _
+  | Pfctidz _ _
   | Pfctiw _ _
   | Pfctiwz _ _
   | Pfmadd _ _ _ _
@@ -907,6 +924,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmfcr _
   | Pmfspr _ _
   | Pmtspr _ _
+  | Prldicl _ _ _ _
+  | Pstdu _ _ _
   | Pstwbrx _ _ _
   | Pstwcx_ _ _ _
   | Pstfdu _ _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index a7e66701..d82b9730 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -188,13 +188,19 @@ let p_instruction oc ic =
   | Peqv (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Peqv\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pextsb (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsb\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
+  | Pextsw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pfreeframe (c,i) -> assert false (* Should not occur *)
   | Pfabs (fr1,fr2) 
   | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3
   | Pfadds (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadds\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3
   | Pfcmpu (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcmpu\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
+  | Pfcfi (ir,fr) -> assert false (* Should not occur *)
+  | Pfcfid (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcfid\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
+  | Pfcfiu (ir,fr) -> assert false (* Should not occur *)
   | Pfcti (ir,fr) -> assert false (* Should not occur *)
+  | Pfctiu (ir,fr) -> assert false (* Should not occur *)
+  | Pfctidz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctidz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfctiw (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiw\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfctiwz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiwz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfdiv (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdiv\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3
@@ -263,6 +269,7 @@ let p_instruction oc ic =
   | Porc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Porc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Poris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Poris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
+  | Prldicl (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prldicl\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2
   | Prlwinm (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwinm\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2
   | Prlwimi  (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwimi\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2
   | Pslw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pslw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
@@ -271,6 +278,7 @@ let p_instruction oc ic =
   | Psrw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pstb (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2
   | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
+  | Pstdu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2
   | Pstfd (fr,c,ir)
   | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
   | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 3fffc037..49f796ca 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -23,6 +23,13 @@ open Asmexpandaux
 
 exception Error of string
 
+(* FreeScale's EREF extensions *)
+
+let eref =
+  match Configuration.model with
+  | "e5500" -> true
+  | _ -> false
+
 (* Useful constants and helper functions *)
 
 let _0 = Integers.Int.zero
@@ -485,8 +492,24 @@ let expand_builtin_inline name args res =
       emit (Plwz (res, Cint! retaddr_offset,GPR1))
   (* isel *)
   | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) ->
-      emit (Pcmpwi (a1,Cint (Int.zero)));
-      emit (Pisel (res,a3,a2,CRbit_2))
+      if eref then begin
+        emit (Pcmpwi (a1,Cint (Int.zero)));
+        emit (Pisel (res,a3,a2,CRbit_2))
+      end else if a2 = a3 then
+        emit (Pmr (res, a2))
+      else begin
+        (* a1 has type _Bool, hence it is 0 or 1 *)
+        emit (Psubfic (GPR0, a1, Cint _0));
+        (* r0 = 0xFFFF_FFFF if a1 is true, r0 = 0 if a1 is false *)
+        if res <> a3 then begin
+          emit (Pand_ (res, a2, GPR0));
+          emit (Pandc (GPR0, a3, GPR0))
+        end else begin
+          emit (Pandc (res, a3, GPR0));
+          emit (Pand_ (GPR0, a2, GPR0))
+        end;
+        emit (Por (res, res, GPR0))
+      end
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -547,6 +570,24 @@ let expand_instruction instr =
         emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz)))
       else
         emit (Plwz(GPR1, Cint ofs, GPR1))
+  | Pfcfi(r1, r2) ->
+      assert (Archi.ppc64);
+      emit (Pextsw(GPR0, r2));
+      emit (Pstdu(GPR0, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Plfd(r1, Cint _0, GPR1));
+      emit (Pfcfid(r1, r1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
+  | Pfcfiu(r1, r2) ->
+      assert (Archi.ppc64);
+      emit (Prldicl(GPR0, r2, _0, coqint_of_camlint 32l));
+      emit (Pstdu(GPR0, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Plfd(r1, Cint _0, GPR1));
+      emit (Pfcfid(r1, r1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
   | Pfcti(r1, r2) ->
       emit (Pfctiwz(FPR13, r2));
       emit (Pstfdu(FPR13, Cint _m8, GPR1));
@@ -554,6 +595,14 @@ let expand_instruction instr =
       emit (Plwz(r1, Cint _4, GPR1));
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
+  | Pfctiu(r1, r2) ->
+      assert (Archi.ppc64);
+      emit (Pfctidz(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);
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index db3b7028..fe3a6441 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -496,6 +496,15 @@ Definition transl_op
   | Ointoffloat, a1 :: nil =>
       do r1 <- freg_of a1; do r <- ireg_of res;
       OK (Pfcti r r1 :: k)
+  | Ointuoffloat, a1 :: nil =>
+      do r1 <- freg_of a1; do r <- ireg_of res;
+      OK (Pfctiu r r1 :: k)
+  | Ofloatofint, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- freg_of res;
+      OK (Pfcfi r r1 :: k)
+  | Ofloatofintu, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- freg_of res;
+      OK (Pfcfiu r r1 :: k)
   | Ofloatofwords, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res;
       OK (Pfmake r r1 r2 :: k)
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index cb94c555..25e8bf07 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -941,6 +941,18 @@ Opaque Val.add.
   replace v with (Val.maketotal (Val.intoffloat (rs x))).
   TranslOpSimpl.
   rewrite H1; auto.
+  (* Ointuoffloat *)
+  replace v with (Val.maketotal (Val.intuoffloat (rs x))).
+  TranslOpSimpl.
+  rewrite H1; auto.
+  (* Ofloatofint *)
+  replace v with (Val.maketotal (Val.floatofint (rs x))).
+  TranslOpSimpl.
+  rewrite H1; auto.
+  (* Ofloatofintu *)
+  replace v with (Val.maketotal (Val.floatofintu (rs x))).
+  TranslOpSimpl.
+  rewrite H1; auto.
   (* Ocmp *)
   destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto.
   exists rs'; auto with asmgen.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index a2017dca..e4006523 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -134,7 +134,7 @@ Definition destroyed_by_op (op: operation): list mreg :=
   match op with
   | Ofloatconst _ => R12 :: nil
   | Osingleconst _ => R12 :: nil
-  | Ointoffloat => F13 :: nil
+  | Ointoffloat | Ointuoffloat => F13 :: nil
   | _ => nil
   end.
 
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index e1307492..71c16ab9 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -56,7 +56,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Onegfs | Oabsfs => op1 (default nv)
   | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
   | Osingleoffloat | Ofloatofsingle => op1 (default nv)
-  | Ointoffloat => op1 (default nv)
+  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
   | Ofloatofwords | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocmp c => needs_of_condition c
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 3ff08791..6866b086 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -107,6 +107,9 @@ Inductive operation : Type :=
   | Ofloatofsingle: operation           (**r [rd] is [r1] extended to double-precision float *)
 (*c Conversions between int and float: *)
   | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
+  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *)
+  | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] (PPC64 only) *)
+  | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *)
   | Ofloatofwords: operation            (**r [rd = float_of_words(r1,r2)] *)
 (*c Manipulating 64-bit integers: *)
   | Omakelong: operation                (**r [rd = r1 << 32 | r2] *)
@@ -231,6 +234,9 @@ Definition eval_operation
   | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
   | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1)
   | Ointoffloat, v1::nil => Val.intoffloat v1
+  | Ointuoffloat, v1::nil => Val.intuoffloat v1
+  | Ofloatofint, v1::nil => Val.floatofint v1
+  | Ofloatofintu, v1::nil => Val.floatofintu v1
   | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2)
   | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
   | Olowlong, v1::nil => Some(Val.loword v1)
@@ -332,6 +338,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoffloat => (Tfloat :: nil, Tsingle)
   | Ofloatofsingle => (Tsingle :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
+  | Ointuoffloat => (Tfloat :: nil, Tint)
+  | Ofloatofint => (Tint :: nil, Tfloat)
+  | Ofloatofintu => (Tint :: nil, Tfloat)
   | Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
   | Omakelong => (Tint :: Tint :: nil, Tlong)
   | Olowlong => (Tlong :: nil, Tint)
@@ -420,6 +429,9 @@ Proof with (try exact I).
   destruct v0...
   destruct v0...
   destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2...
+  destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2...
+  destruct v0; simpl in H0; inv H0...
+  destruct v0; simpl in H0; inv H0...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0...
@@ -783,6 +795,10 @@ Proof.
   inv H4; simpl; auto.
   inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2.
   exists (Vint i); auto.
+  inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2.
+  exists (Vint i); auto.
+  inv H4; simpl in H1; inv H1; simpl. TrivialExists.
+  inv H4; simpl in H1; inv H1; simpl. TrivialExists.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 6d39569e..a1fcecc7 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -466,19 +466,23 @@ Nondetfunction cast16signed (e: expr) :=
 Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 
 Definition intuoffloat (e: expr) :=
-  Elet e
-  (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
-    (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
-      (intoffloat (Eletvar 1))
-      (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
+  if Archi.ppc64 then
+    Eop Ointuoffloat (e ::: Enil)
+  else
+    Elet e
+    (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
+      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+        (intoffloat (Eletvar 1))
+        (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
 Nondetfunction floatofintu (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil =>
       Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
-      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
-           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
+      if Archi.ppc64 then Eop Ofloatofintu (e ::: Enil) else
+        subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
+             (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
   end.
 
 Nondetfunction floatofint (e: expr) :=
@@ -486,9 +490,10 @@ Nondetfunction floatofint (e: expr) :=
   | Eop (Ointconst n) Enil =>
       Eop (Ofloatconst (Float.of_int n)) Enil
   | _ =>
-      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
-                               ::: addimm Float.ox8000_0000 e ::: Enil))
-           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
+      if Archi.ppc64 then Eop Ofloatofint (e ::: Enil) else
+        subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
+                                 ::: addimm Float.ox8000_0000 e ::: Enil))
+             (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
   end.
 
 Definition intofsingle (e: expr) :=
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 147132dd..ad1adc47 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -838,6 +838,8 @@ Proof.
   intros. destruct x; simpl in H0; try discriminate.
   destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
   exists (Vint n); split; auto. unfold intuoffloat.
+  destruct Archi.ppc64.
+  econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto.
   set (im := Int.repr Int.half_modulus).
   set (fm := Float.of_intu im).
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
@@ -875,6 +877,8 @@ Theorem eval_floatofint:
 Proof.
   intros until y. unfold floatofint. destruct (floatofint_match a); intros.
   InvEval. TrivialExists. 
+  destruct Archi.ppc64.
+  TrivialExists. 
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_int i)); split; auto.
   set (t1 := addimm Float.ox8000_0000 a).
@@ -897,6 +901,8 @@ Theorem eval_floatofintu:
 Proof.
   intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
   InvEval. TrivialExists.
+  destruct Archi.ppc64.
+  TrivialExists. 
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_intu i)); split; auto.
   unfold floatofintu.
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index eca7a1b8..bc990de5 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -484,6 +484,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	extsb	%a, %a\n" ireg r1 ireg r2
       | Pextsh(r1, r2) ->
           fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
+      | Pextsw(r1, r2) ->
+          fprintf oc "	extsw	%a, %a\n" ireg r1 ireg r2
       | Pfreeframe(sz, ofs) ->
           assert false
       | Pfabs(r1, r2) | Pfabss(r1, r2) ->
@@ -494,8 +496,18 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fadds	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfcmpu(r1, r2) ->
           fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
+      | Pfcfi(r1, r2) ->
+          assert false
+      | Pfcfid(r1, r2) ->
+          fprintf oc "	fcfid	%a, %a\n" freg r1 freg r2
+      | Pfcfiu(r1, r2) ->
+          assert false
       | Pfcti(r1, r2) ->
           assert false
+      | Pfctidz(r1, r2) ->
+          fprintf oc "	fctidz	%a, %a\n" freg r1 freg r2
+      | Pfctiu(r1, r2) ->
+          assert false
       | Pfctiw(r1, r2) ->
           fprintf oc "	fctiw	%a, %a\n" freg r1 freg r2
       | Pfctiwz(r1, r2) ->
@@ -628,6 +640,9 @@ module Target (System : SYSTEM):TARGET =
           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 constant c
+      | Prldicl(r1, r2, c1, c2) ->
+          fprintf oc "	rldicl	%a, %a, %ld, %ld\n"
+            ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
       | Prlwinm(r1, r2, c1, c2) ->
           let (mb, me) = rolm_mask (camlint_of_coqint c2) in
           fprintf oc "	rlwinm	%a, %a, %ld, %d, %d %s 0x%lx\n"
@@ -650,6 +665,8 @@ module Target (System : SYSTEM):TARGET =
           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
+      | Pstdu(r1, c, r2) ->
+          fprintf oc "	stdu	%a, %a(%a)\n" ireg r1 constant c ireg r2
       | 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) ->
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 8cb29145..bcd1e80e 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -102,6 +102,9 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoffloat, v1::nil => singleoffloat v1
   | Ofloatofsingle, v1::nil => floatofsingle v1
   | Ointoffloat, v1::nil => intoffloat v1
+  | Ointuoffloat, v1::nil => intuoffloat v1
+  | Ofloatofint, v1::nil => floatofint v1
+  | Ofloatofintu, v1::nil => floatofintu v1
   | Ofloatofwords, v1::v2::nil => floatofwords v1 v2
   | Omakelong, v1::v2::nil => longofwords v1 v2
   | Olowlong, v1::nil => loword v1
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index b448e3d2..b0f05536 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -23,3 +23,11 @@ Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data".
 Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
 Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
 Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
+
+(* Choice of PPC variant *)
+Extract Constant Archi.ppc64 =>
+  "begin match Configuration.model with
+   | ""ppc64"" -> true
+   | ""e5500"" -> true
+   | _ -> false
+   end".