Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


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

16 files changed, 550 insertions, 311 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 0b871d9..070f7cc 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -25,10 +25,18 @@ Definition big_endian := true.
 Notation align_int64 := 8%Z (only parsing).
 Notation align_float64 := 8%Z (only parsing).
 
-Program Definition default_pl : bool * nan_pl 53 := 
+Program Definition default_pl_64 : bool * nan_pl 53 := 
   (false, nat_iter 51 xO xH).
 
-Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
+Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
   false.                        (**r always choose first NaN *)
 
-Global Opaque big_endian default_pl choose_binop_pl.
+Program Definition default_pl_32 : bool * nan_pl 24 := 
+  (false, nat_iter 22 xO xH).
+
+Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
+  false.                        (**r always choose first NaN *)
+
+Global Opaque big_endian
+              default_pl_64 choose_binop_pl_64
+              default_pl_32 choose_binop_pl_32.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index aba78d4..a7e5eaf 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -165,20 +165,29 @@ Inductive instruction : Type :=
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
   | Pfreeframe: Z -> int -> instruction                       (**r deallocate stack frame and restore previous frame *)
   | 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 *)
   | 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 *)
   | Pfmr: freg -> freg -> instruction                         (**r float move *)
   | Pfmul: freg -> freg -> freg -> instruction                (**r float multiply *)
+  | Pfmuls: freg -> freg -> freg -> instruction               (**r float multiply *)
   | Pfneg: freg -> freg -> instruction                        (**r float negation *)
+  | Pfnegs: freg -> freg -> instruction                       (**r float negation *)
   | Pfrsp: freg -> freg -> instruction                        (**r float round to single precision *)
+  | 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 *)
   | 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 *)
   | Plfdx: freg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
+  | Plfd_a: freg -> constant -> ireg -> instruction           (**r load 64-bit quantity to float reg *)
+  | Plfdx_a: freg -> ireg -> ireg -> instruction              (**r same, with 2 index regs *)
   | Plfs: freg -> constant -> ireg -> instruction             (**r load 32-bit float *)
   | Plfsx: freg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plha: ireg -> constant -> ireg -> instruction             (**r load 16-bit signed int *)
@@ -186,8 +195,11 @@ Inductive instruction : Type :=
   | 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 *)
   | 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 *)
   | Pmflr: ireg -> instruction                                (**r move LR to reg *)
   | Pmr: ireg -> ireg -> instruction                          (**r integer move *)
@@ -196,7 +208,7 @@ Inductive instruction : Type :=
   | Pmulli: ireg -> ireg -> constant -> instruction           (**r integer multiply immediate *)
   | Pmullw: ireg -> ireg -> ireg -> instruction               (**r integer multiply *)
   | Pmulhw: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
-  | Pmulhwu: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
+  | Pmulhwu: ireg -> ireg -> ireg -> instruction              (**r multiply high signed *)
   | Pnand: ireg -> ireg -> ireg -> instruction                (**r bitwise not-and *)
   | Pnor: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-or *)
   | Por: ireg -> ireg -> ireg -> instruction                  (**r bitwise or *)
@@ -213,12 +225,16 @@ Inductive instruction : Type :=
   | Pstbx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Pstfd: freg -> constant -> ireg -> instruction            (**r store 64-bit float *)
   | 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 *)
   | Pstfs: freg -> constant -> ireg -> instruction            (**r store 32-bit float *)
   | 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 *)
   | Pstw: ireg -> constant -> ireg -> instruction             (**r store 32-bit int *)
   | Pstwx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
+  | 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 *)
   | Psubfc: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction *)
   | Psubfe: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction with carry *)
   | Psubfic: ireg -> ireg -> constant -> instruction          (**r integer subtraction from immediate *)
@@ -645,26 +661,40 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | Pfabs rd r1 =>
       Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m
+  | Pfabss rd r1 =>
+      Next (nextinstr (rs#rd <- (Val.absfs rs#r1))) m
   | Pfadd rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m
+  | Pfadds rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
   | Pfcmpu r1 r2 =>
       Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
   | Pfcti rd r1 =>
       Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
   | Pfdiv rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
+  | Pfdivs rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.divfs rs#r1 rs#r2))) m
   | Pfmake rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m
   | Pfmr rd r1 =>
       Next (nextinstr (rs#rd <- (rs#r1))) m
   | Pfmul rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m
+  | Pfmuls rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.mulfs rs#r1 rs#r2))) m
   | Pfneg rd r1 =>
       Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m
+  | Pfnegs rd r1 =>
+      Next (nextinstr (rs#rd <- (Val.negfs rs#r1))) m
   | Pfrsp rd r1 =>
       Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m
+  | Pfxdp rd r1 =>
+      Next (nextinstr (rs#rd <- (Val.floatofsingle rs#r1))) m
   | Pfsub rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
+  | Pfsubs rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.subfs rs#r1 rs#r2))) m
   | Plbz rd cst r1 =>
       load1 Mint8unsigned rd cst r1 rs m
   | Plbzx rd r1 r2 =>
@@ -673,6 +703,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       load1 Mfloat64 rd cst r1 rs m
   | Plfdx rd r1 r2 =>
       load2 Mfloat64 rd r1 r2 rs m
+  | Plfd_a rd cst r1 =>
+      load1 Many64 rd cst r1 rs m
+  | Plfdx_a rd r1 r2 =>
+      load2 Many64 rd r1 r2 rs m
   | Plfs rd cst r1 =>
       load1 Mfloat32 rd cst r1 rs m
   | Plfsx rd r1 r2 =>
@@ -687,10 +721,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       load2 Mint16unsigned rd r1 r2 rs m
   | Plfi rd f =>
       Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m
+  | Plfis rd f =>
+      Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vsingle f))) m
   | Plwz rd cst r1 =>
       load1 Mint32 rd cst r1 rs m
   | Plwzx rd r1 r2 =>
       load2 Mint32 rd r1 r2 rs m
+  | Plwz_a rd cst r1 =>
+      load1 Many32 rd cst r1 rs m
+  | Plwzx_a rd r1 r2 =>
+      load2 Many32 rd r1 r2 rs m
   | Pmfcrbit rd bit =>
       Next (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m
   | Pmflr rd =>
@@ -742,16 +782,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       store1 Mfloat64 rd cst r1 rs m
   | Pstfdx rd r1 r2 =>
       store2 Mfloat64 rd r1 r2 rs m
+  | Pstfd_a rd cst r1 =>
+      store1 Many64 rd cst r1 rs m
+  | Pstfdx_a rd r1 r2 =>
+      store2 Many64 rd r1 r2 rs m
   | Pstfs rd cst r1 =>
-      match store1 Mfloat32 rd cst r1 rs m with
-      | Next rs' m' => Next (rs'#FPR13 <- Vundef) m'
-      | Stuck => Stuck
-      end
+      store1 Mfloat32 rd cst r1 rs m
   | Pstfsx rd r1 r2 =>
-      match store2 Mfloat32 rd r1 r2 rs m with
-      | Next rs' m' => Next (rs'#FPR13 <- Vundef) m'
-      | Stuck => Stuck
-      end
+      store2 Mfloat32 rd r1 r2 rs m
   | Psth rd cst r1 =>
       store1 Mint16unsigned rd cst r1 rs m
   | Psthx rd r1 r2 =>
@@ -760,6 +798,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       store1 Mint32 rd cst r1 rs m
   | Pstwx rd r1 r2 =>
       store2 Mint32 rd r1 r2 rs m
+  | Pstw_a rd cst r1 =>
+      store1 Many32 rd cst r1 rs m
+  | Pstwx_a rd r1 r2 =>
+      store2 Many32 rd r1 r2 rs m
   | Psubfc rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1)
                        #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 6b66686..5ca770d 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -122,40 +122,32 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) :=
 
 (** Accessing slots in the stack frame.  *)
 
+Definition accessind {A: Type}
+       (instr1: A -> constant -> ireg -> instruction)
+       (instr2: A -> ireg -> ireg -> instruction)
+       (base: ireg) (ofs: int) (r: A) (k: code) :=
+  if Int.eq (high_s ofs) Int.zero 
+  then instr1 r (Cint ofs) base :: k
+  else loadimm GPR0 ofs (instr2 r base GPR0 :: k).
+
 Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
-  match ty with
-  | Tint =>
-      do r <- ireg_of dst;
-      OK (if Int.eq (high_s ofs) Int.zero then
-            Plwz r (Cint ofs) base :: k
-          else
-            loadimm GPR0 ofs (Plwzx r base GPR0 :: k))
-  | Tfloat =>
-      do r <- freg_of dst;
-      OK (if Int.eq (high_s ofs) Int.zero then
-            Plfd r (Cint ofs) base :: k
-          else
-            loadimm GPR0 ofs (Plfdx r base GPR0 :: k))
-  | Tlong | Tsingle =>
-      Error (msg "Asmgen.loadind")
+  match ty, preg_of dst with
+  | Tint, IR r => OK(accessind Plwz Plwzx base ofs r k)
+  | Tany32, IR r => OK(accessind Plwz_a Plwzx_a base ofs r k)
+  | Tsingle, FR r => OK(accessind Plfs Plfsx base ofs r k)
+  | Tfloat, FR r => OK(accessind Plfd Plfdx base ofs r k)
+  | Tany64, FR r => OK(accessind Plfd_a Plfdx_a base ofs r k)
+  | _, _ => Error (msg "Asmgen.loadind")
   end.
 
 Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
-  match ty with
-  | Tint =>
-      do r <- ireg_of src;
-      OK (if Int.eq (high_s ofs) Int.zero then
-            Pstw r (Cint ofs) base :: k
-          else
-            loadimm GPR0 ofs (Pstwx r base GPR0 :: k))
-  | Tfloat =>
-      do r <- freg_of src;
-      OK (if Int.eq (high_s ofs) Int.zero then
-            Pstfd r (Cint ofs) base :: k
-          else
-            loadimm GPR0 ofs (Pstfdx r base GPR0 :: k))
-  | Tlong | Tsingle =>
-      Error (msg "Asmgen.storeind")
+  match ty, preg_of src with
+  | Tint, IR r => OK(accessind Pstw Pstwx base ofs r k)
+  | Tany32, IR r => OK(accessind Pstw_a Pstwx_a base ofs r k)
+  | Tsingle, FR r => OK(accessind Pstfs Pstfsx base ofs r k)
+  | Tfloat, FR r => OK(accessind Pstfd Pstfdx base ofs r k)
+  | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a base ofs r k)
+  | _, _ => Error (msg "Asmgen.storeind")
   end.
 
 (** Constructor for a floating-point comparison.  The PowerPC has
@@ -340,6 +332,8 @@ Definition transl_op
       do r <- ireg_of res; OK (loadimm r n k)
   | Ofloatconst f, nil =>
       do r <- freg_of res; OK (Plfi r f :: k)
+  | Osingleconst f, nil =>
+      do r <- freg_of res; OK (Plfis r f :: k)
   | Oaddrsymbol s ofs, nil =>
       do r <- ireg_of res;
       OK (if symbol_is_small_data s ofs then
@@ -477,9 +471,30 @@ Definition transl_op
   | Odivf, a1 :: a2 :: nil =>
       do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
       OK (Pfdiv r r1 r2 :: k)
+  | Onegfs, a1 :: nil =>
+      do r1 <- freg_of a1; do r <- freg_of res;
+      OK (Pfnegs r r1 :: k)
+  | Oabsfs, a1 :: nil =>
+      do r1 <- freg_of a1; do r <- freg_of res;
+      OK (Pfabss r r1 :: k)
+  | Oaddfs, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfadds r r1 r2 :: k)
+  | Osubfs, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfsubs r r1 r2 :: k)
+  | Omulfs, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfmuls r r1 r2 :: k)
+  | Odivfs, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfdivs r r1 r2 :: k)
   | Osingleoffloat, a1 :: nil =>
       do r1 <- freg_of a1; do r <- freg_of res;
       OK (Pfrsp r r1 :: k)
+  | Ofloatofsingle, a1 :: nil =>
+      do r1 <- freg_of a1; do r <- freg_of res;
+      OK (Pfxdp r r1 :: k)
   | Ointoffloat, a1 :: nil =>
       do r1 <- freg_of a1; do r <- ireg_of res;
       OK (Pfcti r r1 :: k)
@@ -566,7 +581,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
   | Mfloat64 =>
       do r <- freg_of dst;
       transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k
-  | Mint64 =>
+  | _ =>
       Error (msg "Asmgen.transl_load")
   end.
 
@@ -589,7 +604,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
   | Mfloat64 =>
       do r <- freg_of src;
       transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k
-  | Mint64 =>
+  | _ =>
       Error (msg "Asmgen.transl_store")
   end.
 
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 879d752..913fb50 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -196,17 +196,21 @@ Remark loadind_label:
   forall base ofs ty dst k c,
   loadind base ofs ty dst k = OK c -> tail_nolabel k c.
 Proof.
-  unfold loadind; intros.
-  destruct ty; destruct (Int.eq (high_s ofs) Int.zero);
+  unfold loadind, accessind; intros.
+  destruct ty; try discriminate;
+  destruct (preg_of dst); try discriminate;
+  destruct (Int.eq (high_s ofs) Int.zero);
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
 Remark storeind_label:
   forall base ofs ty src k c,
-  storeind base src ofs ty k = OK c -> tail_nolabel k c.
+  storeind src base ofs ty k = OK c -> tail_nolabel k c.
 Proof.
-  unfold storeind; intros.
-  destruct ty; destruct (Int.eq (high_s ofs) Int.zero);
+  unfold storeind, accessind; intros.
+  destruct ty; try discriminate;
+  destruct (preg_of src); try discriminate;
+  destruct (Int.eq (high_s ofs) Int.zero);
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index cfeb823..e1ab9a1 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -435,6 +435,36 @@ Qed.
 
 (** Indexed memory loads. *)
 
+Lemma accessind_load_correct:
+  forall (A: Type) (inj: A -> preg)
+       (instr1: A -> constant -> ireg -> instruction)
+       (instr2: A -> ireg -> ireg -> instruction)
+       (base: ireg) ofs rx chunk v (rs: regset) m k,
+  (forall rs m r1 cst r2,
+   exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) ->
+  (forall rs m r1 r2 r3,
+   exec_instr ge fn (instr2 r1 r2 r3) rs m = load2 chunk (inj r1) r2 r3 rs m) ->
+  Mem.loadv chunk m (Val.add rs#base (Vint ofs)) = Some v ->
+  base <> GPR0 -> inj rx <> PC ->
+  exists rs',
+     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m
+  /\ rs'#(inj rx) = v
+  /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r.
+Proof.
+  intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero).
+- econstructor; split. apply exec_straight_one. 
+  rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl.
+  rewrite H1. eauto. unfold nextinstr. repeat Simplif.
+  split. unfold nextinstr. repeat Simplif. 
+  intros. repeat Simplif. 
+- exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]].
+  econstructor; split. eapply exec_straight_trans. eexact P.
+  apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. 
+  rewrite H1. reflexivity. unfold nextinstr. repeat Simplif.
+  split. repeat Simplif.
+  intros. repeat Simplif.
+Qed.
+
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k (rs: regset) m v c,
   loadind base ofs ty dst k = OK c ->
@@ -445,38 +475,44 @@ Lemma loadind_correct:
   /\ rs'#(preg_of dst) = v
   /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
-Opaque Int.eq.
-  unfold loadind; intros. destruct ty; monadInv H; simpl in H0.
-(* integer *)
-  rewrite (ireg_of_eq _ _ EQ).
-  destruct (Int.eq (high_s ofs) Int.zero).
-  (* one load *)
-  econstructor; split. apply exec_straight_one. simpl.
-  unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
-  intuition Simpl.
-  (* loadimm + load *)
-  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  exists (nextinstr (rs'#x <- v)); split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
-  simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. 
-  intuition Simpl. 
-(* float *)
-  rewrite (freg_of_eq _ _ EQ).
-  destruct (Int.eq (high_s ofs) Int.zero).
-  (* one load *)
-  econstructor; split. apply exec_straight_one. simpl.
-  unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
-  intuition Simpl.
-  (* loadimm + load *)
-  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  exists (nextinstr (rs'#x <- v)); split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
-  simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. 
-  intuition Simpl. 
+  unfold loadind; intros. destruct ty; try discriminate; destruct (preg_of dst); inv H; simpl in H0.
+  apply accessind_load_correct with (inj := IR) (chunk := Mint32); auto with asmgen.
+  apply accessind_load_correct with (inj := FR) (chunk := Mfloat64); auto with asmgen.
+  apply accessind_load_correct with (inj := FR) (chunk := Mfloat32); auto with asmgen.
+  apply accessind_load_correct with (inj := IR) (chunk := Many32); auto with asmgen.
+  apply accessind_load_correct with (inj := FR) (chunk := Many64); auto with asmgen.
 Qed.
 
 (** Indexed memory stores. *)
 
+Lemma accessind_store_correct:
+  forall (A: Type) (inj: A -> preg)
+       (instr1: A -> constant -> ireg -> instruction)
+       (instr2: A -> ireg -> ireg -> instruction)
+       (base: ireg) ofs rx chunk (rs: regset) m m' k,
+  (forall rs m r1 cst r2,
+   exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) ->
+  (forall rs m r1 r2 r3,
+   exec_instr ge fn (instr2 r1 r2 r3) rs m = store2 chunk (inj r1) r2 r3 rs m) ->
+  Mem.storev chunk m (Val.add rs#base (Vint ofs)) (rs (inj rx)) = Some m' ->
+  base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 ->
+  exists rs',
+     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
+Proof.
+  intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero).
+- econstructor; split. apply exec_straight_one. 
+  rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl.
+  rewrite H1. eauto. unfold nextinstr. repeat Simplif.
+  intros. repeat Simplif. 
+- exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]].
+  econstructor; split. eapply exec_straight_trans. eexact P.
+  apply exec_straight_one. rewrite H0. unfold store2.
+  rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. 
+  rewrite H1. reflexivity. unfold nextinstr. repeat Simplif.
+  intros. repeat Simplif.
+Qed.
+
 Lemma storeind_correct:
   forall (base: ireg) ofs ty src k (rs: regset) m m' c,
   storeind src base ofs ty k = OK c ->
@@ -488,33 +524,12 @@ Lemma storeind_correct:
 Proof.
   unfold storeind; intros.
   assert (preg_of src <> GPR0) by auto with asmgen.
-  destruct ty; monadInv H; simpl in H0.
-(* integer *)
-  rewrite (ireg_of_eq _ _ EQ) in *.
-  destruct (Int.eq (high_s ofs) Int.zero).
-  (* one store *)
-  econstructor; split. apply exec_straight_one. simpl.
-  unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
-  intros; Simpl.
-  (* loadimm + store *)
-  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  exists (nextinstr rs'); split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
-  simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. 
-  intuition Simpl. 
-(* float *)
-  rewrite (freg_of_eq _ _ EQ) in *.
-  destruct (Int.eq (high_s ofs) Int.zero).
-  (* one store *)
-  econstructor; split. apply exec_straight_one. simpl.
-  unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
-  intuition Simpl.
-  (* loadimm + store *)
-  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  exists (nextinstr rs'); split. 
-  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
-  simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. 
-  intuition Simpl. 
+  destruct ty; try discriminate; destruct (preg_of src) ; inv H; simpl in H0.
+  apply accessind_store_correct with (inj := IR) (chunk := Mint32); auto with asmgen.
+  apply accessind_store_correct with (inj := FR) (chunk := Mfloat64); auto with asmgen.
+  apply accessind_store_correct with (inj := FR) (chunk := Mfloat32); auto with asmgen.
+  apply accessind_store_correct with (inj := IR) (chunk := Many32); auto with asmgen.
+  apply accessind_store_correct with (inj := FR) (chunk := Many64); auto with asmgen.
 Qed.
 
 (** Float comparisons. *)
@@ -1210,15 +1225,7 @@ Local Transparent destroyed_by_store.
 - (* Mint32 *)
   eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
 - (* Mfloat32 *)
-  rewrite (freg_of_eq _ _ EQ) in H1.
-  eapply transl_memory_access_correct. eauto. eauto. eauto. 
-  intros. econstructor; split. apply exec_straight_one. 
-  simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. 
-Local Transparent destroyed_by_store.
-  simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
-  intros. econstructor; split. apply exec_straight_one. 
-  simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. 
-  simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
+  eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
 - (* Mfloat64 *)
   eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
 Qed.
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index e1e1960..bba0fad 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -136,18 +136,19 @@ Definition make_xorimm (n: int) (r: reg) :=
   else (Oxorimm n, r :: nil).
 
 Definition make_mulfimm (n: float) (r r1 r2: reg) :=
-  if Float.eq_dec n (Float.floatofint (Int.repr 2))
+  if Float.eq_dec n (Float.of_int (Int.repr 2))
   then (Oaddf, r :: r :: nil)
   else (Omulf, r1 :: r2 :: nil).
 
+Definition make_mulfsimm (n: float32) (r r1 r2: reg) :=
+  if Float32.eq_dec n (Float32.of_int (Int.repr 2))
+  then (Oaddfs, r :: r :: nil)
+  else (Omulfs, r1 :: r2 :: nil).
+
 Definition make_cast8signed (r: reg) (a: aval) :=
   if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil).
 Definition make_cast16signed (r: reg) (a: aval) :=
   if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil).
-Definition make_singleoffloat (r: reg) (a: aval) :=
-  if vincl a Fsingle && generate_float_constants tt
-  then (Omove, r :: nil)
-  else (Osingleoffloat, r :: nil).
 
 Nondetfunction op_strength_reduction 
               (op: operation) (args: list reg) (vl: list aval) :=
@@ -174,10 +175,11 @@ Nondetfunction op_strength_reduction
   | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
-  | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
   | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
+  | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2
+  | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2
   | _, _, _ => (op, args)
   end.
 
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 584865a..8498868 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -80,6 +80,10 @@ Ltac SimplVM :=
       let E := fresh in
       assert (E: v = Vfloat n) by (inversion H; auto);
       rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (FS ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vsingle n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
       assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
@@ -315,7 +319,7 @@ Lemma make_mulfimm_correct:
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
   simpl. econstructor; split. eauto. rewrite H; subst n.
   destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. 
   simpl. econstructor; split; eauto. 
@@ -328,13 +332,40 @@ Lemma make_mulfimm_correct_2:
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
   simpl. econstructor; split. eauto. rewrite H; subst n.
   destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. 
   rewrite Float.mul_commut; auto. 
   simpl. econstructor; split; eauto. 
 Qed.
 
+Lemma make_mulfsimm_correct:
+  forall n r1 r2,
+  rs#r2 = Vsingle n ->
+  let (op, args) := make_mulfsimm n r1 r1 r2 in
+  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
+Proof.
+  intros; unfold make_mulfsimm. 
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  simpl. econstructor; split. eauto. rewrite H; subst n.
+  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto. 
+  simpl. econstructor; split; eauto. 
+Qed.
+
+Lemma make_mulfsimm_correct_2:
+  forall n r1 r2,
+  rs#r1 = Vsingle n ->
+  let (op, args) := make_mulfsimm n r2 r1 r2 in
+  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
+Proof.
+  intros; unfold make_mulfsimm. 
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  simpl. econstructor; split. eauto. rewrite H; subst n.
+  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto. 
+  rewrite Float32.mul_commut; auto. 
+  simpl. econstructor; split; eauto. 
+Qed.
+
 Lemma make_cast8signed_correct:
   forall r x,
   vmatch bc rs#r x ->
@@ -363,21 +394,6 @@ Proof.
   econstructor; split; simpl; eauto.
 Qed.
 
-Lemma make_singleoffloat_correct:
-  forall r x,
-  vmatch bc rs#r x ->
-  let (op, args) := make_singleoffloat r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.singleoffloat rs#r) v.
-Proof.
-  intros; unfold make_singleoffloat. 
-  destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. 
-  InvBooleans. exists rs#r; split; auto. 
-  assert (V: vmatch bc rs#r Fsingle).
-  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
-  inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto.
-  econstructor; split; simpl; eauto.
-Qed.
-
 Lemma op_strength_reduction_correct:
   forall op args vl v,
   vl = map (fun r => AE.get r ae) args ->
@@ -424,14 +440,16 @@ Proof.
   InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto.
 (* shru *)
   InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
-(* singleoffloat *)
-  InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cmp *)
   inv H0. apply make_cmp_correct; auto.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2).
   rewrite <- H2. apply make_mulfimm_correct_2; auto.
+(* mulfs *)
+  InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfsimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. fold (Val.mulfs (Vsingle n1) rs#r2).
+  rewrite <- H2. apply make_mulfsimm_correct_2; auto.
 (* default *)
   exists v; auto.
 Qed.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index baad496..f7ed779 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -54,23 +54,13 @@ Global Opaque mreg_eq.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
-  | R3 => Tint  | R4 => Tint  | R5 => Tint  | R6 => Tint
-  | R7 => Tint  | R8 => Tint  | R9 => Tint  | R10 => Tint
-  | R11 => Tint | R12 => Tint
-  | R14 => Tint | R15 => Tint | R16 => Tint
-  | R17 => Tint | R18 => Tint | R19 => Tint | R20 => Tint
-  | R21 => Tint | R22 => Tint | R23 => Tint | R24 => Tint
-  | R25 => Tint | R26 => Tint | R27 => Tint | R28 => Tint
-  | R29 => Tint | R30 => Tint | R31 => Tint
-  | F0 => Tfloat
-  | F1 => Tfloat  | F2 => Tfloat  | F3 => Tfloat  | F4 => Tfloat
-  | F5 => Tfloat  | F6 => Tfloat  | F7 => Tfloat  | F8 => Tfloat
-  | F9 => Tfloat  | F10 => Tfloat | F11 => Tfloat | F12 => Tfloat
-  | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat
-  | F16 => Tfloat | F17 => Tfloat | F18 => Tfloat | F19 => Tfloat
-  | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat
-  | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat
-  | F28 => Tfloat | F29 => Tfloat | F30 => Tfloat | F31 => Tfloat
+  | R3  | R4  | R5  | R6  | R7  | R8  | R9  | R10  | R11 | R12
+  | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24
+  | R25 | R26 | R27 | R28 | R29 | R30 | R31 => Tany32
+  | F0  | F1  | F2  | F3  | F4  | F5  | F6  | F7
+  | F8  | F9  | F10 | F11 | F12 | F13 | F14 | F15
+  | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23
+  | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => Tany64
   end.
 
 Open Scope positive_scope.
@@ -112,6 +102,7 @@ Definition is_stack_reg (r: mreg) : bool := false.
 Definition destroyed_by_op (op: operation): list mreg :=
   match op with
   | Ofloatconst _ => R12 :: nil
+  | Osingleconst _ => R12 :: nil
   | Ointoffloat => F13 :: nil
   | _ => nil
   end.
@@ -120,10 +111,7 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg
   R12 :: nil.
 
 Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
-  match chunk with
-  | Mfloat32 => R11 :: R12 :: F13 :: nil
-  | _ => R11 :: R12 :: nil
-  end.
+  R11 :: R12 :: nil.
 
 Definition destroyed_by_cond (cond: condition): list mreg :=
   nil.
@@ -135,21 +123,16 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_builtin _ _ => F13 :: nil
   | EF_vload _ => nil
-  | EF_vstore Mfloat32 => F13 :: nil
   | EF_vstore _ => nil
   | EF_vload_global _ _ _ => R11 :: nil
   | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil
-  | EF_vstore_global Mfloat32 _ _ => R11 :: R12 :: F13 :: nil
   | EF_vstore_global _ _ _ => R11 :: R12 :: nil
   | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil
   | _ => nil
   end.
 
 Definition destroyed_by_setstack (ty: typ): list mreg :=
-  match ty with
-  | Tsingle => F13 :: nil
-  | _ => nil
-  end.
+  nil.
 
 Definition destroyed_at_function_entry: list mreg :=
   nil.
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index d43af3c..e130749 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -25,6 +25,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Omove => op1 nv
   | Ointconst n => nil
   | Ofloatconst n => nil
+  | Osingleconst n => nil
   | Oaddrsymbol id ofs => nil
   | Oaddrstack ofs => nil
   | Ocast8signed => op1 (sign_ext 8 nv)
@@ -52,7 +53,9 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oroli amount mask => op1 (default nv)
   | Onegf | Oabsf => op1 (default nv)
   | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
-  | Osingleoffloat => op1 (singleoffloat nv)
+  | Onegfs | Oabsfs => op1 (default nv)
+  | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
+  | Osingleoffloat | Ofloatofsingle => op1 (default nv)
   | Ointoffloat => op1 (default nv)
   | Ofloatofwords | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
@@ -66,7 +69,6 @@ Definition operation_is_redundant (op: operation) (nv: nval): bool :=
   | Oandimm n => andimm_redundant nv n
   | Oorimm n => orimm_redundant nv n
   | Orolm amount mask => rolm_redundant nv amount mask
-  | Osingleoffloat => singleoffloat_redundant nv
   | _ => false
   end.
 
@@ -136,7 +138,6 @@ Proof.
 - apply or_sound; auto. apply notint_sound; rewrite bitwise_idem; auto.
 - apply shrimm_sound; auto.
 - apply rolm_sound; auto. 
-- apply singleoffloat_sound; auto. 
 - destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. 
   erewrite needs_of_condition_sound by eauto.
   subst v; simpl. auto with na.
@@ -156,7 +157,6 @@ Proof.
 - apply andimm_redundant_sound; auto. 
 - apply orimm_redundant_sound; auto.
 - apply rolm_redundant_sound; auto.
-- apply singleoffloat_redundant_sound; auto.
 Qed.
 
 End SOUNDNESS.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 17cf072..dbec275 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -54,6 +54,7 @@ Inductive operation : Type :=
   | Omove: operation                    (**r [rd = r1] *)
   | Ointconst: int -> operation         (**r [rd] is set to the given integer constant *)
   | Ofloatconst: float -> operation     (**r [rd] is set to the given float constant *)
+  | Osingleconst: float32 -> operation  (**r [rd] is set to the given float constant *)
   | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
   | Oaddrstack: int -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
 (*c Integer arithmetic: *)
@@ -96,7 +97,14 @@ Inductive operation : Type :=
   | Osubf: operation                    (**r [rd = r1 - r2] *)
   | Omulf: operation                    (**r [rd = r1 * r2] *)
   | Odivf: operation                    (**r [rd = r1 / r2] *)
+  | Onegfs: operation                   (**r [rd = - r1] *)
+  | Oabsfs: operation                   (**r [rd = abs(r1)] *)
+  | Oaddfs: operation                   (**r [rd = r1 + r2] *)
+  | Osubfs: operation                   (**r [rd = r1 - r2] *)
+  | Omulfs: operation                   (**r [rd = r1 * r2] *)
+  | Odivfs: operation                   (**r [rd = r1 / r2] *)
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
+  | 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)] *)
   | Ofloatofwords: operation            (**r [rd = float_of_words(r1,r2)] *)
@@ -130,7 +138,7 @@ Defined.
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
   generalize Int.eq_dec; intro.
-  generalize Float.eq_dec; intro.
+  generalize Float.eq_dec Float32.eq_dec; intros.
   assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
   generalize eq_condition; intro.
   decide equality.
@@ -172,6 +180,7 @@ Definition eval_operation
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
+  | Osingleconst n, nil => Some (Vsingle n)
   | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) 
   | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
   | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
@@ -213,7 +222,14 @@ Definition eval_operation
   | Osubf, v1::v2::nil => Some(Val.subf v1 v2)
   | Omulf, v1::v2::nil => Some(Val.mulf v1 v2)
   | Odivf, v1::v2::nil => Some(Val.divf v1 v2)
+  | Onegfs, v1::nil => Some(Val.negfs v1)
+  | Oabsfs, v1::nil => Some(Val.absfs v1)
+  | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2)
+  | Osubfs, v1::v2::nil => Some(Val.subfs v1 v2)
+  | Omulfs, v1::v2::nil => Some(Val.mulfs v1 v2)
+  | Odivfs, v1::v2::nil => Some(Val.divfs v1 v2)
   | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
+  | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1)
   | Ointoffloat, v1::nil => Val.intoffloat v1
   | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2)
   | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
@@ -265,7 +281,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   match op with
   | Omove => (nil, Tint)   (* treated specially *)
   | Ointconst _ => (nil, Tint)
-  | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat)
+  | Ofloatconst f => (nil, Tfloat)
+  | Osingleconst f => (nil, Tsingle)
   | Oaddrsymbol _ _ => (nil, Tint)
   | Oaddrstack _ => (nil, Tint)
   | Ocast8signed => (Tint :: nil, Tint)
@@ -306,7 +323,14 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
+  | Onegfs => (Tsingle :: nil, Tsingle)
+  | Oabsfs => (Tsingle :: nil, Tsingle)
+  | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle)
+  | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle)
+  | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle)
+  | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle)
   | Osingleoffloat => (Tfloat :: nil, Tsingle)
+  | Ofloatofsingle => (Tsingle :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
   | Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
   | Omakelong => (Tint :: Tint :: nil, Tlong)
@@ -343,7 +367,8 @@ Proof with (try exact I).
   destruct op; simpl in H0; FuncInv; subst; simpl.
   congruence.
   exact I.
-  destruct (Float.is_single_dec f); auto. 
+  auto.
+  auto.
   unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)...
   destruct sp...
   destruct v0...
@@ -386,8 +411,15 @@ Proof with (try exact I).
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
-  destruct v0... simpl. apply Float.singleoffloat_is_single.
-  destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2...
+  destruct v0...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0...
+  destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0...
@@ -521,35 +553,6 @@ Proof.
   rewrite Val.add_assoc. auto. 
 Qed.
 
-(** Transformation of addressing modes with two operands or more
-  into an equivalent arithmetic operation.  This is used in the [Reload]
-  pass when a store instruction cannot be reloaded directly because
-  it runs out of temporary registers. *)
-
-(** For the PowerPC, there is only one binary addressing mode: [Aindexed2].
-  The corresponding operation is [Oadd]. *)
-
-Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
-
-Lemma eval_op_for_binary_addressing:
-  forall (F V: Type) (ge: Genv.t F V) sp addr args v m,
-  (length args >= 2)%nat ->
-  eval_addressing ge sp addr args = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
-Proof.
-  intros.
-  destruct addr; simpl in H0; FuncInv; simpl in H; try omegaContradiction.
-  simpl; congruence.
-Qed.
-
-Lemma type_op_for_binary_addressing:
-  forall addr,
-  (length (type_of_addressing addr) >= 2)%nat ->
-  type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint).
-Proof.
-  intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
-Qed.
-
 (** Operations that are so cheap to recompute that CSE should not factor them out. *)
 
 Definition is_trivial_op (op: operation) : bool :=
@@ -578,61 +581,6 @@ Proof.
   destruct c; simpl; auto; discriminate. 
 Qed.
 
-(** Checking whether two addressings, applied to the same arguments, produce
-  separated memory addresses.  Used in [CSE]. *)
-
-Definition addressing_separated (chunk1: memory_chunk) (addr1: addressing)
-                               (chunk2: memory_chunk) (addr2: addressing) : bool :=
-  match addr1, addr2 with
-  | Aindexed ofs1, Aindexed ofs2 => 
-      Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
-  | Aglobal s1 ofs1, Aglobal s2 ofs2 => 
-      if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true
-  | Abased s1 ofs1, Abased s2 ofs2 => 
-      if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true
-  | Ainstack ofs1, Ainstack ofs2 =>
-      Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
-  | _, _ => false
-  end.
-
-Lemma addressing_separated_sound:
-  forall (F V: Type) (ge: Genv.t F V) sp chunk1 addr1 chunk2 addr2 vl b1 n1 b2 n2,
-  addressing_separated chunk1 addr1 chunk2 addr2 = true ->
-  eval_addressing ge sp addr1 vl = Some(Vptr b1 n1) ->
-  eval_addressing ge sp addr2 vl = Some(Vptr b2 n2) ->
-  b1 <> b2 \/ Int.unsigned n1 + size_chunk chunk1 <= Int.unsigned n2 \/ Int.unsigned n2 + size_chunk chunk2 <= Int.unsigned n1.
-Proof.
-  unfold addressing_separated; intros.
-  generalize (size_chunk_pos chunk1) (size_chunk_pos chunk2); intros SZ1 SZ2.
-  destruct addr1; destruct addr2; try discriminate; simpl in *; FuncInv.
-(* Aindexed *)
-  destruct v; simpl in *; inv H1; inv H2.
-  right. apply Int.no_overlap_sound; auto. 
-(* Aglobal *)
-  unfold Genv.symbol_address in *. 
-  destruct (Genv.find_symbol ge i1) eqn:?; inv H2.
-  destruct (Genv.find_symbol ge i) eqn:?; inv H1.
-  destruct (ident_eq i i1). subst.
-  replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)).
-  replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)).
-  right. apply Int.no_overlap_sound; auto. 
-  rewrite Int.add_commut; rewrite Int.add_zero; auto.
-  rewrite Int.add_commut; rewrite Int.add_zero; auto.
-  left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
-(* Abased *)
-  unfold Genv.symbol_address in *. 
-  destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate.
-  destruct v; inv H2.
-  destruct (Genv.find_symbol ge i) eqn:?; inv H1.
-  destruct (ident_eq i i1). subst.
-  rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3).
-  right. apply Int.no_overlap_sound; auto. 
-  left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
-(* Ainstack *)
-  destruct sp; simpl in *; inv H1; inv H2.
-  right. apply Int.no_overlap_sound; auto. 
-Qed.
-
 (** * Invariance and compatibility properties. *)
 
 (** [eval_operation] and [eval_addressing] depend on a global environment
@@ -719,6 +667,8 @@ Ltac InvInject :=
       inv H; InvInject
   | [ H: val_inject _ (Vfloat _) _ |- _ ] =>
       inv H; InvInject
+  | [ H: val_inject _ (Vsingle _) _ |- _ ] =>
+      inv H; InvInject
   | [ H: val_inject _ (Vptr _ _) _ |- _ ] =>
       inv H; InvInject
   | [ H: val_list_inject _ nil _ |- _ ] =>
@@ -806,7 +756,14 @@ Proof.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
-  inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  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; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index b90b9f2..e3f0724 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -395,11 +395,11 @@ let print_builtin_vload_common oc chunk base offset 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, IR res ->
+  | (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, FR res ->
+  | (Mfloat64 | Many64), FR res ->
       fprintf oc "	lfd	%a, %a(%a)\n" freg res constant offset ireg base
   (* Mint64 is special-cased below *)
   | _ ->
@@ -451,12 +451,11 @@ let print_builtin_vstore_common oc chunk base offset 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, IR src ->
+  | (Mint32 | Many32), IR src ->
       fprintf oc "	stw	%a, %a(%a)\n" ireg src constant offset ireg base
   | Mfloat32, FR src ->
-      fprintf oc "	frsp	%a, %a\n" freg FPR13 freg src;
-      fprintf oc "	stfs	%a, %a(%a)\n" freg FPR13 constant offset ireg base
-  | Mfloat64, 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 *)
   | _ ->
@@ -512,11 +511,11 @@ let align n a = (n + a - 1) land (-a)
 let rec next_arg_locations ir fr ofs = function
   | [] ->
       (ir, fr, ofs)
-  | Tint :: l ->
+  | (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) :: 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
@@ -676,6 +675,7 @@ let short_cond_branch tbl pc lbl_dest =
 (* Printing of instructions *)
 
 let float_literals : (int * int64) list ref = ref []
+let float32_literals : (int * int32) list ref = ref []
 let jumptables : (int * label list) list ref = ref []
 
 let print_instruction oc tbl pc fallthrough = function
@@ -804,10 +804,12 @@ let print_instruction oc tbl pc fallthrough = function
         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
-  | Pfabs(r1, r2) ->
+  | Pfabs(r1, r2) | Pfabss(r1, r2) ->
       fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
   | Pfadd(r1, r2, r3) ->
       fprintf oc "	fadd	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pfadds(r1, r2, r3) ->
+      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
   | Pfcti(r1, r2) ->
@@ -821,6 +823,8 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "%s end pseudoinstr fcti\n" comment
   | 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;
@@ -835,25 +839,37 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
   | Pfmul(r1, r2, r3) ->
       fprintf oc "	fmul	%a, %a, %a\n" freg r1 freg r2 freg r3
-  | Pfneg(r1, r2) ->
+  | Pfmuls(r1, r2, r3) ->
+      fprintf oc "	fmuls	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pfneg(r1, r2) | Pfnegs(r1, r2) ->
       fprintf oc "	fneg	%a, %a\n" freg r1 freg r2
   | 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
   | 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
   | Plbz(r1, c, r2) ->
       fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plbzx(r1, r2, r3) ->
       fprintf oc "	lbzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
-  | Plfd(r1, c, r2) ->
+  | Plfd(r1, c, r2)  | Plfd_a(r1, c, r2) ->
       fprintf oc "	lfd	%a, %a(%a)\n" freg r1 constant c ireg r2
-  | Plfdx(r1, r2, r3) ->
+  | 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.bits_of_double c)) :: !float_literals;
+      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) ->
@@ -866,9 +882,9 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	lhz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plhzx(r1, r2, r3) ->
       fprintf oc "	lhzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
-  | Plwz(r1, c, r2) ->
+  | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) ->
       fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 constant c ireg r2
-  | Plwzx(r1, r2, r3) ->
+  | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) ->
       fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pmfcrbit(r1, bit) ->
       fprintf oc "	mfcr	%a\n" ireg r1;
@@ -924,23 +940,21 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	stb	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Pstbx(r1, r2, r3) ->
       fprintf oc "	stbx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
-  | Pstfd(r1, c, r2) ->
+  | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) ->
       fprintf oc "	stfd	%a, %a(%a)\n" freg r1 constant c ireg r2
-  | Pstfdx(r1, r2, r3) ->
+  | 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) ->
-      fprintf oc "	frsp	%a, %a\n" freg FPR13 freg r1;
-      fprintf oc "	stfs	%a, %a(%a)\n" freg FPR13 constant c ireg r2
+      fprintf oc "	stfs	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Pstfsx(r1, r2, r3) ->
-      fprintf oc "	frsp	%a, %a\n" freg FPR13 freg r1;
-      fprintf oc "	stfsx	%a, %a, %a\n" freg FPR13 ireg r2 ireg r3
+      fprintf oc "	stfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Psth(r1, c, r2) ->
       fprintf oc "	sth	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Psthx(r1, r2, r3) ->
       fprintf oc "	sthx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
-  | Pstw(r1, c, r2) ->
+  | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) ->
       fprintf oc "	stw	%a, %a(%a)\n" ireg r1 constant c ireg r2
-  | Pstwx(r1, r2, r3) ->
+  | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) ->
       fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfc(r1, r2, r3) ->
       fprintf oc "	subfc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
@@ -1061,11 +1075,14 @@ let rec print_instructions oc tbl pc fallthrough = function
 
 (* Print the code for a function *)
 
-let print_literal oc (lbl, n) =
+let print_literal64 oc (lbl, n) =
   let nlo = Int64.to_int32 n
   and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
   fprintf oc "%a:	.long	0x%lx, 0x%lx\n" label lbl nhi nlo
 
+let print_literal32 oc (lbl, n) =
+  fprintf oc "%a:	.long	0x%lx\n" label lbl n
+
 let print_jumptable oc (lbl, tbl) =
   fprintf oc "%a:" label lbl;
   List.iter
@@ -1075,6 +1092,7 @@ let print_jumptable oc (lbl, tbl) =
 let print_function oc name fn =
   Hashtbl.clear current_function_labels;
   float_literals := [];
+  float32_literals := [];
   jumptables := [];
   current_function_sig := fn.fn_sig;
   let (text, lit, jmptbl) =
@@ -1095,11 +1113,12 @@ let print_function oc name fn =
   cfi_endproc oc;
   fprintf oc "	.type	%a, @function\n" symbol name;
   fprintf oc "	.size	%a, . - %a\n" symbol name symbol name;
-  if !float_literals <> [] then begin
+  if !float_literals <> [] || !float32_literals <> [] then begin
     section oc lit;
     fprintf oc "	.balign 8\n";
-    List.iter (print_literal oc) !float_literals;
-    float_literals := []
+    List.iter (print_literal64 oc) !float_literals;
+    List.iter (print_literal32 oc) !float32_literals;
+    float_literals := []; float32_literals := []
   end;
   if !jumptables <> [] then begin
     section oc jmptbl;
@@ -1131,10 +1150,10 @@ let print_init oc = function
                  (Int64.logand b 0xFFFFFFFFL)
   | Init_float32 n ->
       fprintf oc "	.long	0x%lx %s %.18g\n"
-                 (camlint_of_coqint (Floats.Float.bits_of_single n))
+                 (camlint_of_coqint (Floats.Float32.to_bits n))
                  comment (camlfloat_of_coqfloat n)
   | Init_float64 n ->
-      let b = camlint64_of_coqint (Floats.Float.bits_of_double n) in
+      let b = camlint64_of_coqint (Floats.Float.to_bits n) in
       fprintf oc "	.long	0x%Lx, 0x%Lx %s %.18g\n"
                  (Int64.shift_right_logical b 32)
                  (Int64.logand b 0xFFFFFFFFL)
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 371a08a..70b1feb 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -374,6 +374,12 @@ Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
 Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
 
+Definition negfs (e: expr) :=  Eop Onegfs (e ::: Enil).
+Definition absfs (e: expr) :=  Eop Oabsfs (e ::: Enil).
+Definition addfs (e1 e2: expr) :=  Eop Oaddfs (e1 ::: e2 ::: Enil).
+Definition subfs (e1 e2: expr) :=  Eop Osubfs (e1 ::: e2 ::: Enil).
+Definition mulfs (e1 e2: expr) :=  Eop Omulfs (e1 ::: e2 ::: Enil).
+
 (** ** Comparisons *)
 
 Nondetfunction compimm (default: comparison -> int -> condition)
@@ -433,6 +439,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
 Definition compf (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
 
+Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
+  Eop (Ocmp (Ccompf c)) (Eop Ofloatofsingle (e1 ::: Enil) :::
+                         Eop Ofloatofsingle (e2 ::: Enil) ::: Enil).
+
 (** ** Integer conversions *)
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
@@ -457,7 +467,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 
 Definition intuoffloat (e: expr) :=
   Elet e
-  (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)
+  (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.
@@ -465,7 +475,7 @@ Definition intuoffloat (e: expr) :=
 Nondetfunction floatofintu (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil =>
-      Eop (Ofloatconst (Float.floatofintu 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)
@@ -474,14 +484,27 @@ Nondetfunction floatofintu (e: expr) :=
 Nondetfunction floatofint (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil =>
-      Eop (Ofloatconst (Float.floatofint 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)
   end.
 
+Definition intofsingle (e: expr) :=
+  intoffloat (Eop Ofloatofsingle (e ::: Enil)).
+
+Definition singleofint (e: expr) :=
+  Eop Osingleoffloat (floatofint e ::: Enil).
+
+Definition intuofsingle (e: expr) :=
+  intuoffloat (Eop Ofloatofsingle (e ::: Enil)).
+
+Definition singleofintu (e: expr) :=
+  Eop Osingleoffloat (floatofintu e ::: Enil).
+
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
+Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 (** ** Recognition of addressing modes for load and store operations *)
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index cb48d51..8311b82 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -639,6 +639,31 @@ Proof.
   red; intros; TrivialExists.
 Qed.
 
+Theorem eval_negfs: unary_constructor_sound negfs Val.negfs.
+Proof.
+  red; intros. TrivialExists. 
+Qed.
+
+Theorem eval_absfs: unary_constructor_sound absfs Val.absfs.
+Proof.
+  red; intros. TrivialExists. 
+Qed.
+
+Theorem eval_addfs: binary_constructor_sound addfs Val.addfs.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+ 
+Theorem eval_subfs: binary_constructor_sound subfs Val.subfs.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
 Section COMP_IMM.
 
 Variable default: comparison -> int -> condition.
@@ -746,6 +771,18 @@ Proof.
   intros; red; intros. unfold compf. TrivialExists.
 Qed.
 
+Theorem eval_compfs:
+  forall c, binary_constructor_sound (compfs c) (Val.cmpfs c).
+Proof.
+  intros; red; intros. unfold compfs.
+  replace (Val.cmpfs c x y) with
+          (Val.cmpf c (Val.floatofsingle x) (Val.floatofsingle y)).
+  TrivialExists. constructor. EvalOp. simpl; reflexivity. 
+  constructor. EvalOp. simpl; reflexivity. constructor.
+  auto. 
+  destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl. 
+  rewrite Float32.cmp_double. auto. 
+Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
@@ -778,6 +815,11 @@ Proof.
   red; intros. unfold singleoffloat. TrivialExists.
 Qed.
 
+Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle.
+Proof.
+  red; intros. unfold floatofsingle. TrivialExists.
+Qed.
+
 Theorem eval_intoffloat:
   forall le a x y,
   eval_expr ge sp e m le a x ->
@@ -794,10 +836,10 @@ Theorem eval_intuoffloat:
   exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros. destruct x; simpl in H0; try discriminate.
-  destruct (Float.intuoffloat f) as [n|] eqn:?; simpl in H0; inv H0.
+  destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
   exists (Vint n); split; auto. unfold intuoffloat.
   set (im := Int.repr Int.half_modulus).
-  set (fm := Float.floatofintu im).
+  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.
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)).
@@ -807,9 +849,9 @@ Proof.
   eapply eval_Econdition with (va := Float.cmp Clt f fm).
   eauto with evalexpr.
   destruct (Float.cmp Clt f fm) eqn:?.
-  exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
+  exploit Float.to_intu_to_int_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
-  exploit Float.intuoffloat_intoffloat_2; eauto. 
+  exploit Float.to_intu_to_int_2; eauto. 
   change Float.ox8000_0000 with im. fold fm. intro EQ.
   set (t2 := subf (Eletvar (S O)) (Eletvar O)).
   set (t3 := intoffloat t2).
@@ -834,7 +876,7 @@ Proof.
   intros until y. unfold floatofint. destruct (floatofint_match a); intros.
   InvEval. TrivialExists. 
   rename e0 into a. destruct x; simpl in H0; inv H0.
-  exists (Vfloat (Float.floatofint i)); split; auto.
+  exists (Vfloat (Float.of_int i)); split; 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).
@@ -844,7 +886,7 @@ Proof.
   unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. 
   unfold eval_operation. eauto. 
   instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.  
-  intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.floatofint_from_words. auto.
+  intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_int_from_words. auto.
 Qed.
 
 Theorem eval_floatofintu:
@@ -856,7 +898,7 @@ Proof.
   intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
   InvEval. TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
-  exists (Vfloat (Float.floatofintu i)); split; auto.
+  exists (Vfloat (Float.of_intu i)); split; auto.
   unfold floatofintu.
   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).
@@ -864,7 +906,73 @@ Proof.
   unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. 
   unfold eval_operation. eauto. 
   instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.
-  intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.floatofintu_from_words. auto.
+  intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_intu_from_words. auto.
+Qed.
+
+Theorem eval_intofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.intofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold intofsingle. 
+  assert (Val.intoffloat (Val.floatofsingle x) = Some y).
+  { destruct x; simpl in H0; try discriminate.
+    destruct (Float32.to_int f) eqn:F; inv H0. 
+    apply Float32.to_int_double in F. 
+    simpl. unfold Float32.to_double in F; rewrite F; auto.  
+  }
+  apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp. 
+Qed.
+
+Theorem eval_singleofint:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.singleofint x = Some y ->
+  exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
+Proof.
+  intros. unfold singleofint.
+  assert (exists z, Val.floatofint x = Some z /\ y = Val.singleoffloat z).
+  {
+    destruct x; inv H0. simpl. exists (Vfloat (Float.of_int i)); simpl; split; auto.
+    f_equal. apply Float32.of_int_double. 
+  }
+  destruct H1 as (z & A & B). subst y. 
+  exploit eval_floatofint; eauto. intros (v & C & D). 
+  exists (Val.singleoffloat v); split. EvalOp. inv D; auto. 
+Qed.
+
+Theorem eval_intuofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.intuofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold intuofsingle. 
+  assert (Val.intuoffloat (Val.floatofsingle x) = Some y).
+  { destruct x; simpl in H0; try discriminate.
+    destruct (Float32.to_intu f) eqn:F; inv H0. 
+    apply Float32.to_intu_double in F. 
+    simpl. unfold Float32.to_double in F; rewrite F; auto.  
+  }
+  apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp. 
+Qed.
+
+Theorem eval_singleofintu:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.singleofintu x = Some y ->
+  exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
+Proof.
+  intros. unfold singleofintu.
+  assert (exists z, Val.floatofintu x = Some z /\ y = Val.singleoffloat z).
+  {
+    destruct x; inv H0. simpl. exists (Vfloat (Float.of_intu i)); simpl; split; auto.
+    f_equal. apply Float32.of_intu_double. 
+  }
+  destruct H1 as (z & A & B). subst y. 
+  exploit eval_floatofintu; eauto. intros (v & C & D). 
+  exists (Val.singleoffloat v); split. EvalOp. inv D; auto. 
 Qed.
 
 Theorem eval_addressing:
diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
index 49c0774..2d3efe3 100644
--- a/powerpc/Unusedglob1.ml
+++ b/powerpc/Unusedglob1.ml
@@ -42,18 +42,22 @@ let referenced_instr = function
   | Pcmpwi(_, c)
   | Plbz(_, c, _)
   | Plfd(_, c, _)
+  | Plfd_a(_, c, _)
   | Plfs(_, c, _)
   | Plha(_, c, _)
   | Plhz(_, c, _)
   | Plwz(_, c, _)
+  | Plwz_a(_, c, _)
   | Pmulli(_, _, c)
   | Pori(_, _, c)
   | Poris(_, _, c)
   | Pstb(_, c, _)
   | Pstfd(_, c, _)
+  | Pstfd_a(_, c, _)
   | Pstfs(_, c, _)
   | Psth(_, c, _) 
   | Pstw(_, c, _) 
+  | Pstw_a(_, c, _) 
   | Psubfic(_, _, c)
   | Pxori(_, _, c)
   | Pxoris(_, _, c) -> referenced_constant c
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 77463f4..a5a1db8 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -52,6 +52,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Omove, v1::nil => v1
   | Ointconst n, nil => I n
   | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop
+  | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop
   | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs)
   | Oaddrstack ofs, nil => Ptr (Stk ofs)
   | Ocast8signed, v1 :: nil => sign_ext 8 v1
@@ -92,7 +93,14 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osubf, v1::v2::nil => subf v1 v2
   | Omulf, v1::v2::nil => mulf v1 v2
   | Odivf, v1::v2::nil => divf v1 v2
+  | Onegfs, v1::nil => negfs v1
+  | Oabsfs, v1::nil => absfs v1
+  | Oaddfs, v1::v2::nil => addfs v1 v2
+  | Osubfs, v1::v2::nil => subfs v1 v2
+  | Omulfs, v1::v2::nil => mulfs v1 v2
+  | Odivfs, v1::v2::nil => divfs v1 v2
   | Osingleoffloat, v1::nil => singleoffloat v1
+  | Ofloatofsingle, v1::nil => floatofsingle v1
   | Ointoffloat, v1::nil => intoffloat v1
   | Ofloatofwords, v1::v2::nil => floatofwords v1 v2
   | Omakelong, v1::v2::nil => longofwords v1 v2
@@ -163,6 +171,7 @@ Proof.
   unfold eval_operation, eval_static_operation; intros;
   destruct op; InvHyps; eauto with va.
   destruct (propagate_float_constants tt); constructor.
+  destruct (propagate_float_constants tt); constructor.
   rewrite Int.add_zero_l; eauto with va.
   fold (Val.sub (Vint i) a1). auto with va.
   apply floatofwords_sound; auto. 
diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v
index 2db1f73..866e73d 100644
--- a/powerpc/eabi/Conventions1.v
+++ b/powerpc/eabi/Conventions1.v
@@ -15,6 +15,7 @@
 
 Require Import Coqlib.
 Require Import AST.
+Require Import Events.
 Require Import Locations.
 
 (** * Classification of machine registers *)
@@ -180,13 +181,13 @@ Proof.
 Qed.
 
 Lemma int_callee_save_type:
-  forall r, In r int_callee_save_regs -> mreg_type r = Tint.
+  forall r, In r int_callee_save_regs -> mreg_type r = Tany32.
 Proof.
   intro. simpl; ElimOrEq; reflexivity.
 Qed.
 
 Lemma float_callee_save_type:
-  forall r, In r float_callee_save_regs -> mreg_type r = Tfloat.
+  forall r, In r float_callee_save_regs -> mreg_type r = Tany64.
 Proof.
   intro. simpl; ElimOrEq; reflexivity.
 Qed.
@@ -239,12 +240,21 @@ Qed.
 Definition loc_result (s: signature) : list mreg :=
   match s.(sig_res) with
   | None => R3 :: nil
-  | Some Tint => R3 :: nil
-  | Some (Tfloat | Tsingle) => F1 :: nil
+  | Some (Tint | Tany32) => R3 :: nil
+  | Some (Tfloat | Tsingle | Tany64) => F1 :: nil
   | Some Tlong => R3 :: R4 :: nil
   end.
 
-(** The result location is a caller-save register *)
+(** The result registers have types compatible with that given in the signature. *)
+
+Lemma loc_result_type:
+  forall sig,
+  subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true.
+Proof.
+  intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto.
+Qed.
+
+(** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
   forall (s: signature) (r: mreg), 
@@ -278,18 +288,18 @@ Fixpoint loc_arguments_rec
     (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc :=
   match tyl with
   | nil => nil
-  | Tint :: tys =>
+  | (Tint | Tany32) as ty :: tys =>
       match list_nth_z int_param_regs ir with
       | None =>
-          S Outgoing ofs Tint :: loc_arguments_rec tys ir fr (ofs + 1)
+          S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 1)
       | Some ireg =>
           R ireg :: loc_arguments_rec tys (ir + 1) fr ofs
       end
-  | (Tfloat | Tsingle) :: tys =>
+  | (Tfloat | Tsingle | Tany64) as ty :: tys =>
       match list_nth_z float_param_regs fr with
       | None =>
           let ofs := align ofs 2 in
-          S Outgoing ofs Tfloat :: loc_arguments_rec tys ir fr (ofs + 2)
+          S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 2)
       | Some freg =>
           R freg :: loc_arguments_rec tys ir (fr + 1) ofs
       end
@@ -316,12 +326,12 @@ Definition loc_arguments (s: signature) : list loc :=
 Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
   match tyl with
   | nil => ofs
-  | Tint :: tys =>
+  | (Tint | Tany32) :: tys =>
       match list_nth_z int_param_regs ir with
       | None => size_arguments_rec tys ir fr (ofs + 1)
       | Some ireg => size_arguments_rec tys (ir + 1) fr ofs
       end
-  | (Tfloat | Tsingle) :: tys =>
+  | (Tfloat | Tsingle | Tany64) :: tys =>
       match list_nth_z float_param_regs fr with
       | None => size_arguments_rec tys ir fr (align ofs 2 + 2)
       | Some freg => size_arguments_rec tys ir (fr + 1) ofs
@@ -393,7 +403,7 @@ Opaque list_nth_z.
   destruct H. subst. split. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
   assert (ofs <= align ofs 2) by (apply align_le; omega). 
-  destruct H. subst. split. omega. congruence. 
+  destruct H. subst. split. omega. congruence.
   destruct H. subst. split. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. 
 - (* single *)
@@ -404,6 +414,20 @@ Opaque list_nth_z.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
   assert (ofs <= align ofs 2) by (apply align_le; omega). 
   intuition omega.
+- (* any32 *)
+  destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
+  subst. left. eapply list_nth_z_in; eauto.
+  eapply IHtyl; eauto.
+  subst. split. omega. congruence.
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* any64 *)
+  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. 
+  subst. right. eapply list_nth_z_in; eauto.
+  eapply IHtyl; eauto.
+  subst. split. apply Zle_ge. apply align_le. omega. congruence.
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
+  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  intuition omega.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -441,6 +465,10 @@ Proof.
   destruct (list_nth_z float_param_regs fr); eauto.
   apply Zle_trans with (align ofs0 2). apply align_le; omega.
   apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+  destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega.
+  destruct (list_nth_z float_param_regs fr); eauto.
+  apply Zle_trans with (align ofs0 2). apply align_le; omega.
+  apply Zle_trans with (align ofs0 2 + 2); auto; omega.
 Qed.
 
 Lemma size_arguments_above:
@@ -493,6 +521,18 @@ Proof.
   destruct (list_nth_z float_param_regs fr); destruct H0. 
   congruence.
   eauto.
+  inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
+  eauto.
+- (* any32 *)
+  destruct (list_nth_z int_param_regs ir); destruct H0. 
+  congruence.
+  eauto.
+  inv H0. apply size_arguments_rec_above.
+  eauto.
+- (* any64 *)
+  destruct (list_nth_z float_param_regs fr); destruct H0. 
+  congruence.
+  eauto.
   inv H0. apply size_arguments_rec_above. eauto. 
   }
   eauto.