Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3

19 files changed, 90 insertions, 148 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 8f96dafc..5b9d67cc 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for PowerPC *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := false.
 
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 4fb38ff8..d9901960 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -200,12 +200,9 @@ Inductive instruction : Type :=
   | 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) *)
   | Pfcfl: freg -> ireg -> instruction                        (**r signed-long-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) *)
   | Pfctid: ireg -> freg -> instruction                       (**r float-to-signed-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 *)
@@ -825,16 +822,10 @@ 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
   | Pfcfl rd r1 =>
       Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong 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
   | Pfctid rd r1 =>
       Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m
   | Pfdiv rd r1 r2 =>
@@ -1204,7 +1195,7 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
               (set_res res vres
-                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
+                (undef_regs (IR GPR0 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 38f4bc75..1f32dd62 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -198,12 +198,9 @@ let pp_instructions pp ic =
   | Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3]
   | Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3]
   | Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2]
-  | Pfcfi (ir,fr)
   | Pfcfl (ir,fr) -> assert false (* Should not occur *)
   | Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2]
-  | Pfcfiu _ (* Should not occur *)
   | Pfcti _ (* Should not occur *)
-  | Pfctiu _ (* Should not occur *)
   | Pfctid _ -> assert false (* Should not occur *)
   | Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2]
   | Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2]
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index ce88778c..cb6a659f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -594,9 +594,7 @@ let expand_builtin_inline name args res =
       emit (Pfnmadd(res, a1, a2, a3))
   | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfnmsub(res, a1, a2, a3))
-  | "__builtin_fabs", [BA(FR a1)], BR(FR res) ->
-      emit (Pfabs(res, a1))
-  | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) ->
+  | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) ->
       emit (Pfsqrt(res, a1))
   | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) ->
       emit (Pfrsqrte(res, a1))
@@ -767,6 +765,8 @@ let expand_builtin_inline name args res =
       emit (Pori (GPR0, GPR0, Cint _0))
   (* atomic operations *)
   | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
+      (* Register constraints imposed by Machregs.v *)
+      assert(a1 = GPR3 && a2 = GPR4 && a3 = GPR5);
       emit (Plwz (GPR10,Cint _0,a2));
       emit (Psync);
       let lbl = new_label() in
@@ -786,6 +786,8 @@ let expand_builtin_inline name args res =
       emit (Pisync);
       emit (Pstw (GPR0,Cint _0, a2))
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
+      (* Register constraints imposed by Machregs.v *)
+      assert (a1 = GPR4 && a2 = GPR5 && res = GPR3);
       let lbl = new_label() in
       emit (Psync);
       emit (Plabel lbl);
@@ -795,6 +797,8 @@ let expand_builtin_inline name args res =
       emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
+      (* Register constraints imposed by Machregs.v *)
+      assert (dst = GPR4 && exp = GPR5 && des = GPR6 && res = GPR3);
       let lbls = new_label ()
       and lblneq = new_label ()
       and lblsucc = new_label () in
@@ -871,15 +875,6 @@ 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)
   | Pfcfl(r1, r2) ->
       assert (Archi.ppc64);
       emit (Pstdu(r2, Cint _m8, GPR1));
@@ -888,15 +883,6 @@ let expand_instruction instr =
       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, _32));
-      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));
@@ -904,14 +890,6 @@ 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)
   | Pfctid(r1, r2) ->
       assert (Archi.ppc64);
       emit (Pfctidz(FPR13, r2));
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 29e2c028..d0c44f08 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -611,15 +611,6 @@ 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/Asmgenproof.v b/powerpc/Asmgenproof.v
index 21d5ce48..93589a31 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -789,16 +789,18 @@ Opaque loadind.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
   unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2.
+  rewrite set_res_other. simpl. rewrite undef_regs_other_2.
+  rewrite Pregmap.gso by auto with asmgen.
   rewrite <- H1. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   rewrite preg_notin_charact. intros. auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
+  eapply agree_undef_regs; eauto.
+  intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen.
   congruence.
   intros. Simpl. rewrite set_res_other by auto.
-  rewrite undef_regs_other_2; auto with asmgen.
+  simpl. rewrite undef_regs_other_2; auto with asmgen.
 
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 1b797999..850e95c7 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1500,18 +1500,6 @@ 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/Builtins1.v b/powerpc/Builtins1.v
index 53c83d7e..9d7aadd9 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.v
@@ -19,15 +19,55 @@ Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+  | BI_isel
+  | BI_uisel
+  | BI_isel64
+  | BI_uisel64
+  | BI_bsel
+  | BI_mulhw
+  | BI_mulhwu
+  | BI_mulhd
+  | BI_mulhdu.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+     ("__builtin_isel", BI_isel)
+  :: ("__builtin_uisel", BI_uisel)
+  :: ("__builtin_isel64", BI_isel64)
+  :: ("__builtin_uisel64", BI_uisel64)
+  :: ("__builtin_bsel", BI_bsel)
+  :: ("__builtin_mulhw", BI_mulhw)
+  :: ("__builtin_mulhwu", BI_mulhwu)
+  :: ("__builtin_mulhd", BI_mulhd)
+  :: ("__builtin_mulhdu", BI_mulhdu)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_isel | BI_uisel | BI_bsel =>
+     mksignature (Tint :: Tint :: Tint :: nil) Tint cc_default
+  | BI_isel64 | BI_uisel64 =>
+     mksignature (Tint :: Tlong :: Tlong :: nil) Tlong cc_default
+  | BI_mulhw | BI_mulhwu =>
+     mksignature (Tint :: Tint :: nil) Tint cc_default
+  | BI_mulhd | BI_mulhdu =>
+     mksignature (Tlong :: Tlong :: nil) Tlong cc_default
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_isel | BI_uisel | BI_bsel =>
+    mkbuiltin_n3t Tint Tint Tint Tint (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1)
+  | BI_isel64 | BI_uisel64 =>
+    mkbuiltin_n3t Tint Tlong Tlong Tlong (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1)
+  | BI_mulhw =>
+    mkbuiltin_n2t Tint Tint Tint Int.mulhs
+  | BI_mulhwu =>
+    mkbuiltin_n2t Tint Tint Tint Int.mulhu
+  | BI_mulhd =>
+    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
+  | BI_mulhdu =>
+    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
+  end.
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index e29a41f1..e0826877 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -28,18 +28,6 @@ let builtins = {
       (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false);
     "__builtin_mulhwu",
       (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
-    "__builtin_clz",
-      (TInt(IInt, []), [TInt(IUInt, [])], false);
-    "__builtin_clzl",
-      (TInt(IInt, []), [TInt(IULong, [])], false);
-    "__builtin_clzll",
-      (TInt(IInt, []), [TInt(IULongLong, [])], false);
-    "__builtin_ctz",
-      (TInt(IInt, []), [TInt(IUInt, [])], false);
-    "__builtin_ctzl",
-      (TInt(IInt, []), [TInt(IULong, [])], false);
-    "__builtin_ctzll",
-      (TInt(IInt, []), [TInt(IULongLong, [])], false);
     "__builtin_cmpb",
       (TInt (IUInt, []),  [TInt(IUInt, []);TInt(IUInt, [])], false);
     (* Integer arithmetic in 32/64-bit hybrid mode *)
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index e7c8758b..9967bbae 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg :=
   | Ofloatconst _ => R12 :: nil
   | Osingleconst _ => R12 :: nil
   | Olongconst _ => R12 :: nil
-  | Ointoffloat | Ointuoffloat => F13 :: nil
+  | Ointoffloat => F13 :: nil
   | Olongoffloat => F13 :: nil
   | Oaddlimm _ => R12 :: nil
   | Oandlimm _ => R12 :: nil
@@ -232,7 +232,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list
     | EF_builtin id sg =>
       if string_dec id "__builtin_atomic_exchange" then ((Some R3)::(Some R4)::(Some R5)::nil,nil)
       else if string_dec id "__builtin_sync_fetch_and_add" then ((Some R4)::(Some R5)::nil,(Some R3)::nil)
-      else if string_dec id "___builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
+      else if string_dec id "__builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
       else (nil, nil)
     | _ => (nil, nil)
   end.
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 0b0d4548..d17382ad 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -12,27 +12,7 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register s = s = "R0" || s = "r0"
-
-let name_of_register r =
-  try Some (Hashtbl.find register_names r) with Not_found -> None
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
-
-let can_reserve_register r =
-  List.mem r Conventions1.int_callee_save_regs
-  || List.mem r Conventions1.float_callee_save_regs
                                               
 let class_of_type = function
   | AST.Tint | AST.Tlong -> 0
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index d7117c21..01b0f9fd 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -12,9 +12,6 @@
 
 (** Auxiliary functions on machine registers *)
 
-val name_of_register: Machregs.mreg -> string option
-val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
-val can_reserve_register: Machregs.mreg -> bool
 
 val class_of_type: AST.typ -> int
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index 5ea09bd8..74ee6b85 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -61,7 +61,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 | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
+  | Ointoffloat => 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 457b868a..7ddbcc34 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -105,7 +105,7 @@ Inductive operation : Type :=
   | Osubl: operation                    (**r [rd = r1 - r2] *)
   | Onegl: operation                    (**r [rd = - r1] *)
   | Omull: operation                    (**r [rd = r1 * r2] *)
-  | Omullhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omullhs: operation                  (**r [rd = high part of r1 * r2, signed] *)
   | Omullhu: operation                  (**r [rd = high part of r1 * r2, unsigned] *)
   | Odivl: operation                    (**r [rd = r1 / r2] (signed) *)
   | Odivlu: operation                   (**r [rd = r1 / r2] (unsigned) *)
@@ -141,9 +141,6 @@ 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] *)
@@ -299,9 +296,6 @@ 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)
@@ -449,9 +443,6 @@ 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)
@@ -570,9 +561,6 @@ Proof with (try exact I; try reflexivity).
   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...
@@ -1053,10 +1041,6 @@ 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/PrintOp.ml b/powerpc/PrintOp.ml
index 8d7f17ab..77791827 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -42,6 +42,14 @@ let print_condition reg pp = function
       fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n)
   | (Cmasknotzero n, [r1]) ->
       fprintf pp "%a & 0x%lx != 0" reg r1 (camlint_of_coqint n)
+  | (Ccompl c, [r1;r2]) ->
+      fprintf pp "%a %sls %a" reg r1 (comparison_name c) reg r2
+  | (Ccomplu c, [r1;r2]) ->
+      fprintf pp "%a %slu %a" reg r1 (comparison_name c) reg r2
+  | (Ccomplimm(c, n), [r1]) ->
+      fprintf pp "%a %sls %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n)
+  | (Ccompluimm(c, n), [r1]) ->
+      fprintf pp "%a %slu %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n)
   | _ ->
       fprintf pp "<bad condition>"
 
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 52f4f855..fe8b5453 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -468,7 +468,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 
 Definition intuoffloat (e: expr) :=
   if Archi.ppc64 then
-    Eop Ointuoffloat (e ::: Enil)
+    Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil)
   else
     Elet e
     (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
@@ -482,7 +482,8 @@ Nondetfunction floatofintu (e: expr) :=
       Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
       if Archi.ppc64 then
-        Eop Ofloatofintu (e ::: Enil)  else
+        Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: 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.
@@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) :=
       Eop (Ofloatconst (Float.of_int n)) Enil
   | _ =>
       if Archi.ppc64 then
-        Eop Ofloatofint (e ::: Enil) else
+        Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: 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)
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 8135bad6..ed81c83f 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -855,8 +855,13 @@ Proof.
   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).
+- apply Float.to_intu_to_long in Heqo.
+  econstructor. constructor. econstructor. econstructor; eauto. constructor.
+  simpl; rewrite Heqo; simpl; eauto. constructor.
+  simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto.
+  assert (Int.modulus < Int64.max_unsigned) by (compute; auto).
+  generalize (Int.unsigned_range n). omega.  
+- 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)).
     constructor. auto.
@@ -893,11 +898,12 @@ 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).
+  destruct Archi.ppc64.
+- rewrite Float.of_int_of_long.
+  EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
+- set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
   exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1.
@@ -917,12 +923,12 @@ 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.
-  set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
+  destruct Archi.ppc64.
+- rewrite Float.of_intu_of_long.
+  EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
+- set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
   exploit (eval_subf le t2).
   unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3ea03786..554bfe09 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -557,22 +557,16 @@ 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
       | Pfcfl(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
       | Pfctid(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) ->
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index a270d857..c81f1a6c 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -133,9 +133,6 @@ 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