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

27 files changed, 1011 insertions, 1134 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index f4fcd6e..919843b 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -609,6 +609,20 @@ Definition subst_loc (l1 l2: loc) (e: eqs) : option eqs :=
      (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e))
      (Some e).
 
+(** [loc_type_compat env l e] checks that for all equations [r = l] in [e],
+  the type [env r] of [r] is compatible with the type of [l]. *)
+
+Definition sel_type (k: equation_kind) (ty: typ) : typ :=
+  match k with
+  | Full => ty
+  | Low | High => Tint
+  end.
+
+Definition loc_type_compat (env: regenv) (l: loc) (e: eqs) : bool :=
+  EqSet2.for_all_between
+    (fun q => subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l))
+    (select_loc_l l) (select_loc_h l) (eqs2 e).
+
 (** [add_equations [r1...rN] [m1...mN] e] adds to [e] the [N] equations
     [ri = R mi [Full]].  Return [None] if the two lists have different lengths.
 *)
@@ -759,18 +773,25 @@ Definition destroyed_by_move (src dst: loc) :=
   | _, _ => destroyed_by_op Omove
   end.
 
+Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool :=
+  match dst with
+  | R r => true
+  | S sl ofs ty => loc_type_compat env dst e
+  end.
+
 (** Simulate the effect of a sequence of moves [mv] on a set of
   equations [e].  The set [e] is the equations that must hold
   after the sequence of moves.  Return the set of equations that
   must hold before the sequence of moves.  Return [None] if the
   set of equations [e] cannot hold after the sequence of moves. *)
 
-Fixpoint track_moves (mv: moves) (e: eqs) : option eqs :=
+Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs :=
   match mv with
   | nil => Some e
   | (src, dst) :: mv =>
-      do e1 <- track_moves mv e;
+      do e1 <- track_moves env mv e;
       assertion (can_undef_except dst (destroyed_by_move src dst)) e1;
+      assertion (well_typed_move env dst e1);
       subst_loc dst src e1
   end.
 
@@ -803,89 +824,90 @@ Definition kind_second_word := if Archi.big_endian then Low else High.
   equations that must hold "before" these instructions, or [None] if
   impossible. *)
 
-Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option eqs :=
+Definition transfer_aux (f: RTL.function) (env: regenv)
+                        (shape: block_shape) (e: eqs) : option eqs :=
   match shape with
   | BSnop mv s =>
-      track_moves mv e
+      track_moves env mv e
   | BSmove src dst mv s =>
-      track_moves mv (subst_reg dst src e)
+      track_moves env mv (subst_reg dst src e)
   | BSmakelong src1 src2 dst mv s =>
       let e1 := subst_reg_kind dst High src1 Full e in
       let e2 := subst_reg_kind dst Low src2 Full e1 in
       assertion (reg_unconstrained dst e2);
-      track_moves mv e2
+      track_moves env mv e2
   | BSlowlong src dst mv s =>
       let e1 := subst_reg_kind dst Full src Low e in
       assertion (reg_unconstrained dst e1);
-      track_moves mv e1
+      track_moves env mv e1
   | BShighlong src dst mv s =>
       let e1 := subst_reg_kind dst Full src High e in
       assertion (reg_unconstrained dst e1);
-      track_moves mv e1
+      track_moves env mv e1
   | BSop op args res mv1 args' res' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args res args' res' (destroyed_by_op op) e1;
-      track_moves mv1 e2
+      track_moves env mv1 e2
   | BSopdead op args res mv s =>
       assertion (reg_unconstrained res e);
-      track_moves mv e
+      track_moves env mv e
   | BSload chunk addr args dst mv1 args' dst' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1;
-      track_moves mv1 e2
+      track_moves env mv1 e2
   | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s =>
-      do e1 <- track_moves mv3 e;
+      do e1 <- track_moves env mv3 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in
       assertion (loc_unconstrained (R dst2') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr') e2);
       do e3 <- add_equations args args2' e2;
-      do e4 <- track_moves mv2 e3;
+      do e4 <- track_moves env mv2 e3;
       let e5 := remove_equation (Eq kind_first_word dst (R dst1')) e4 in
       assertion (loc_unconstrained (R dst1') e5);
       assertion (can_undef (destroyed_by_load Mint32 addr) e5);
       assertion (reg_unconstrained dst e5);
       do e6 <- add_equations args args1' e5;
-      track_moves mv1 e6
+      track_moves env mv1 e6
   | BSload2_1 addr args dst mv1 args' dst' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr) e2);
       do e3 <- add_equations args args' e2;
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr') e2);
       do e3 <- add_equations args args' e2;
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BSloaddead chunk addr args dst mv s =>
       assertion (reg_unconstrained dst e);
-      track_moves mv e
+      track_moves env mv e
   | BSstore chunk addr args src mv args' src' s =>
       assertion (can_undef (destroyed_by_store chunk addr) e);
       do e1 <- add_equations (src :: args) (src' :: args') e;
-      track_moves mv e1
+      track_moves env mv e1
   | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s =>
       assertion (can_undef (destroyed_by_store Mint32 addr') e);
       do e1 <- add_equations args args2' 
                   (add_equation (Eq kind_second_word src (R src2')) e);
-      do e2 <- track_moves mv2 e1;
+      do e2 <- track_moves env mv2 e1;
       assertion (can_undef (destroyed_by_store Mint32 addr) e2);
       do e3 <- add_equations args args1' 
                   (add_equation (Eq kind_first_word src (R src1')) e2);
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BScall sg ros args res mv1 ros' mv2 s =>
       let args' := loc_arguments sg in
       let res' := map R (loc_result sg) in
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       do e2 <- remove_equations_res res (sig_res sg) res' e1;
       assertion (forallb (fun l => reg_loc_unconstrained res l e2) res');
       assertion (no_caller_saves e2);
       do e3 <- add_equation_ros ros ros' e2;
       do e4 <- add_equations_args args (sig_args sg) args' e3;
-      track_moves mv1 e4
+      track_moves env mv1 e4
   | BStailcall sg ros args mv1 ros' =>
       let args' := loc_arguments sg in
       assertion (tailcall_is_possible sg);
@@ -893,9 +915,9 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option
       assertion (ros_compatible_tailcall ros');
       do e1 <- add_equation_ros ros ros' empty_eqs;
       do e2 <- add_equations_args args (sig_args sg) args' e1;
-      track_moves mv1 e2
+      track_moves env mv1 e2
   | BSbuiltin ef args res mv1 args' res' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       let args' := map R args' in
       let res' := map R res' in
       do e2 <- remove_equations_res res (sig_res (ef_sig ef)) res' e1;
@@ -903,23 +925,23 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option
       assertion (forallb (fun l => loc_unconstrained l e2) res');
       assertion (can_undef (destroyed_by_builtin ef) e2);
       do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2;
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BSannot txt typ args res mv1 args' s =>
       do e1 <- add_equations_args args (annot_args_typ typ) args' e;
-      track_moves mv1 e1
+      track_moves env mv1 e1
   | BScond cond args mv args' s1 s2 =>
       assertion (can_undef (destroyed_by_cond cond) e);
       do e1 <- add_equations args args' e;
-      track_moves mv e1
+      track_moves env mv e1
   | BSjumptable arg mv arg' tbl =>
       assertion (can_undef destroyed_by_jumptable e);
-      track_moves mv (add_equation (Eq Full arg (R arg')) e)
+      track_moves env mv (add_equation (Eq Full arg (R arg')) e)
   | BSreturn None mv =>
-      track_moves mv empty_eqs
+      track_moves env mv empty_eqs
   | BSreturn (Some arg) mv =>
       let arg' := map R (loc_result (RTL.fn_sig f)) in
       do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
-      track_moves mv e1
+      track_moves env mv e1
   end.
 
 (** The main transfer function for the dataflow analysis.  Like [transfer_aux],
@@ -927,7 +949,7 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option
   equations that must hold "after".  It also handles error propagation
   and reporting. *)
 
-Definition transfer (f: RTL.function) (shapes: PTree.t block_shape)
+Definition transfer (f: RTL.function) (env: regenv) (shapes: PTree.t block_shape)
                     (pc: node) (after: res eqs) : res eqs :=
   match after with
   | Error _ => after
@@ -935,7 +957,7 @@ Definition transfer (f: RTL.function) (shapes: PTree.t block_shape)
       match shapes!pc with
       | None => Error(MSG "At PC " :: POS pc :: MSG ": unmatched block" :: nil)
       | Some shape =>
-          match transfer_aux f shape e with
+          match transfer_aux f env shape e with
           | None => Error(MSG "At PC " :: POS pc :: MSG ": invalid register allocation" :: nil)
           | Some e' => OK e'
           end
@@ -1083,8 +1105,8 @@ Definition successors_block_shape (bsh: block_shape) : list node :=
   | BSreturn optarg mv => nil
   end.
 
-Definition analyze (f: RTL.function) (bsh: PTree.t block_shape) :=
-  DS.fixpoint_allnodes bsh successors_block_shape (transfer f bsh).
+Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) :=
+  DS.fixpoint_allnodes bsh successors_block_shape (transfer f env bsh).
 
 (** * Validating and translating functions and programs *)
 
@@ -1118,9 +1140,9 @@ Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e
   and stack size. *)
 
 Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function)
-                                 (e1: eqs) : option unit :=
+                                 (env: regenv) (e1: eqs) : option unit :=
   do mv <- pair_entrypoints rtl ltl;
-  do e2 <- track_moves mv e1;
+  do e2 <- track_moves env mv e1;
   assertion (compat_entry (RTL.fn_params rtl)
                           (sig_args (RTL.fn_sig rtl))
                           (loc_parameters (RTL.fn_sig rtl)) e2);
@@ -1133,10 +1155,10 @@ Local Close Scope option_monad_scope.
 Local Open Scope error_monad_scope.
 
 Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function)
-                             (bsh: PTree.t block_shape)
+                             (env: regenv) (bsh: PTree.t block_shape)
                              (a: PMap.t LEq.t): res unit :=
-  do e1 <- transfer rtl bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl);
-  match check_entrypoints_aux rtl ltl e1 with
+  do e1 <- transfer rtl env bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl);
+  match check_entrypoints_aux rtl ltl env e1 with
   | None => Error (msg "invalid register allocation at entry point")
   | Some _ => OK tt
   end.
@@ -1145,11 +1167,11 @@ Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function)
   a source RTL function and an LTL function generated by the external
   register allocator. *)
 
-Definition check_function (rtl: RTL.function) (ltl: LTL.function) : res unit :=
+Definition check_function (rtl: RTL.function) (ltl: LTL.function) (env: regenv): res unit :=
   let bsh := pair_codes rtl ltl in
-  match analyze rtl bsh with
+  match analyze rtl env bsh with
   | None => Error (msg "allocation analysis diverges")
-  | Some a => check_entrypoints rtl ltl bsh a
+  | Some a => check_entrypoints rtl ltl env bsh a
   end.
 
 (** [regalloc] is the external register allocator.  It is written in OCaml
@@ -1165,7 +1187,7 @@ Definition transf_function (f: RTL.function) : res LTL.function :=
   | OK env =>
       match regalloc f with
       | Error m => Error m
-      | OK tf => do x <- check_function f tf; OK tf
+      | OK tf => do x <- check_function f tf env; OK tf
       end
   end.
 
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 9303878..588a674 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -451,7 +451,7 @@ Lemma add_equations_args_lessdef:
   forall rs ls rl tyl ll e e',
   add_equations_args rl tyl ll e = Some e' ->
   satisf rs ls e' ->
-  Val.has_type_list (rs##rl) (normalize_list tyl) ->
+  Val.has_type_list (rs##rl) tyl ->
   Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)).
 Proof.
   intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros.
@@ -969,7 +969,6 @@ Proof.
   split. apply eqs_same; auto. auto. 
 Qed.
 
-(*
 Lemma loc_type_compat_charact:
   forall env l e q,
   loc_type_compat env l e = true ->
@@ -1009,8 +1008,7 @@ Proof.
   destruct (rs#r); exact I.
   eelim Loc.diff_not_eq. eexact A. auto.
 Qed.
-*)
-(*
+
 Remark val_lessdef_normalize:
   forall v v' ty,
   Val.has_type v ty -> Val.lessdef v v' ->
@@ -1018,19 +1016,23 @@ Remark val_lessdef_normalize:
 Proof.
   intros. inv H0. rewrite Val.load_result_same; auto. auto. 
 Qed.
-*)
 
 Lemma subst_loc_satisf:
   forall env src dst rs ls e e',
   subst_loc dst src e = Some e' ->
-  (*well_typed_move env dst e = true ->*)
+  well_typed_move env dst e = true ->
   wt_regset env rs ->
   satisf rs ls e' ->
   satisf rs (Locmap.set dst (ls src) ls) e.
 Proof.
   intros; red; intros.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
-  subst dst. rewrite Locmap.gss. apply (H1 _ B).
+  subst dst. rewrite Locmap.gss.
+  destruct q as [k r l]; simpl in *.
+  exploit well_typed_move_charact; eauto.
+  destruct l as [mr | sl ofs ty]; intros.
+  apply (H2 _ B). 
+  apply val_lessdef_normalize; auto. apply (H2 _ B). 
   rewrite Locmap.gso; auto.
 Qed.
 
@@ -1077,18 +1079,22 @@ Proof.
 Qed.
 
 Lemma subst_loc_undef_satisf:
-  forall src dst rs ls ml e e',
+  forall env src dst rs ls ml e e',
   subst_loc dst src e = Some e' ->
-  (*well_typed_move env dst e = true ->*)
+  well_typed_move env dst e = true ->
   can_undef_except dst ml e = true ->
-  (*wt_regset env rs ->*)
+  wt_regset env rs ->
   satisf rs ls e' ->
   satisf rs (Locmap.set dst (ls src) (undef_regs ml ls)) e.
 Proof.
   intros; red; intros.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
   subst dst. rewrite Locmap.gss.
-  destruct q as [k r l]; simpl in *. apply (H1 _ B). 
+  destruct q as [k r l]; simpl in *.
+  exploit well_typed_move_charact; eauto.
+  destruct l as [mr | sl ofs ty]; intros.
+  apply (H3 _ B). 
+  apply val_lessdef_normalize; auto. apply (H3 _ B). 
   rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. 
   eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto.
 Qed.
@@ -1327,30 +1333,45 @@ Proof.
   auto. congruence.
 Qed.
 
+Lemma loadv_int64_split:
+  forall m a v,
+  Mem.loadv Mint64 m a = Some v ->
+  exists v1 v2,
+     Mem.loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
+  /\ Mem.loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
+  /\ Val.lessdef (Val.hiword v) v1
+  /\ Val.lessdef (Val.loword v) v2.
+Proof.
+  intros. exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & A & B & C).
+  exists v1, v2. split; auto. split; auto. 
+  inv C; auto. destruct v1, v2; simpl; auto. 
+  rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. 
+Qed.
+
 (** * Properties of the dataflow analysis *)
 
 Lemma analyze_successors:
-  forall f bsh an pc bs s e,
-  analyze f bsh = Some an ->
+  forall f env bsh an pc bs s e,
+  analyze f env bsh = Some an ->
   bsh!pc = Some bs ->
   In s (successors_block_shape bs) ->
   an!!pc = OK e ->
-  exists e', transfer f bsh s an!!s = OK e' /\ EqSet.Subset e' e.
+  exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e.
 Proof.
   unfold analyze; intros. exploit DS.fixpoint_allnodes_solution; eauto.
-  rewrite H2. unfold DS.L.ge. destruct (transfer f bsh s an#s); intros.
+  rewrite H2. unfold DS.L.ge. destruct (transfer f env bsh s an#s); intros.
   exists e0; auto. 
   contradiction.
 Qed.
 
 Lemma satisf_successors:
-  forall f bsh an pc bs s e rs ls,
-  analyze f bsh = Some an ->
+  forall f env bsh an pc bs s e rs ls,
+  analyze f env bsh = Some an ->
   bsh!pc = Some bs ->
   In s (successors_block_shape bs) ->
   an!!pc = OK e ->
   satisf rs ls e ->
-  exists e', transfer f bsh s an!!s = OK e' /\ satisf rs ls e'.
+  exists e', transfer f env bsh s an!!s = OK e' /\ satisf rs ls e'.
 Proof.
   intros. exploit analyze_successors; eauto. intros [e' [A B]]. 
   exists e'; split; auto. eapply satisf_incr; eauto.
@@ -1360,12 +1381,13 @@ Qed.
 
 Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop :=
   | transf_function_spec_intro:  
-      forall an mv k e1 e2,
-      analyze f (pair_codes f tf) = Some an ->
+      forall env an mv k e1 e2,
+      wt_function f env ->
+      analyze f env (pair_codes f tf) = Some an ->
       (LTL.fn_code tf)!(LTL.fn_entrypoint tf) = Some(expand_moves mv (Lbranch (RTL.fn_entrypoint f) :: k)) ->
       wf_moves mv ->
-      transfer f (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
-      track_moves mv e1 = Some e2 ->
+      transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
+      track_moves env mv e1 = Some e2 ->
       compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true ->
       can_undef destroyed_at_function_entry e2 = true ->
       RTL.fn_stacksize f = LTL.fn_stacksize tf ->
@@ -1380,33 +1402,36 @@ Proof.
   unfold transf_function; intros.
   destruct (type_function f) as [env|] eqn:TY; try discriminate.
   destruct (regalloc f); try discriminate.
-  destruct (check_function f f0) as [] eqn:?; inv H.
+  destruct (check_function f f0 env) as [] eqn:?; inv H.
   unfold check_function in Heqr. 
-  destruct (analyze f (pair_codes f tf)) as [an|] eqn:?; try discriminate.
+  destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate.
   monadInv Heqr. 
-  destruct (check_entrypoints_aux f tf x) as [y|] eqn:?; try discriminate.
+  destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate.
   unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv.
   exploit extract_moves_sound; eauto. intros [A B]. subst b.
   exploit check_succ_sound; eauto. intros [k EQ1]. subst b0.
-  econstructor; eauto. congruence. 
+  econstructor; eauto. eapply type_function_correct; eauto. congruence. 
 Qed.
 
 Lemma invert_code:
-  forall f tf pc i opte e,
+  forall f env tf pc i opte e,
+  wt_function f env ->
   (RTL.fn_code f)!pc = Some i ->
-  transfer f (pair_codes f tf) pc opte = OK e ->
+  transfer f env (pair_codes f tf) pc opte = OK e ->
   exists eafter, exists bsh, exists bb,
   opte = OK eafter /\ 
   (pair_codes f tf)!pc = Some bsh /\
   (LTL.fn_code tf)!pc = Some bb /\
   expand_block_shape bsh i bb /\
-  transfer_aux f bsh eafter = Some e.
+  transfer_aux f env bsh eafter = Some e /\
+  wt_instr f env i.
 Proof.
-  intros. destruct opte as [eafter|]; simpl in H0; try discriminate. exists eafter.
+  intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter.
   destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. 
   exploit matching_instr_block; eauto. intros [bb [A B]].
-  destruct (transfer_aux f bsh eafter) as [e1|] eqn:?; inv H0. 
-  exists bb. tauto. 
+  destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. 
+  exists bb. exploit wt_instr_at; eauto.
+  tauto. 
 Qed.
 
 (** * Semantic preservation *)
@@ -1480,10 +1505,11 @@ Proof.
 Qed.
 
 Lemma exec_moves:
-  forall mv rs s f sp bb m e e' ls,
-  track_moves mv e = Some e' ->
+  forall mv env rs s f sp bb m e e' ls,
+  track_moves env mv e = Some e' ->
   wf_moves mv ->
   satisf rs ls e' ->
+  wt_regset env rs ->
   exists ls',
     star step tge (Block s f sp (expand_moves mv bb) ls m)
                E0 (Block s f sp bb ls' m)
@@ -1495,7 +1521,7 @@ Opaque destroyed_by_op.
 - unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto.
   (* step *)
 - destruct a as [src dst]. unfold expand_moves. simpl. 
-  destruct (track_moves mv e) as [e1|] eqn:?; MonadInv.
+  destruct (track_moves env mv e) as [e1|] eqn:?; MonadInv.
   assert (wf_moves mv). red; intros. apply H0; auto with coqlib. 
   destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst].
   (* reg-reg *)
@@ -1521,13 +1547,17 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
       sg.(sig_res) = Some Tint ->
       match_stackframes nil nil sg
   | match_stackframes_cons:
-      forall res f sp pc rs s tf bb ls ts sg an e
+      forall res f sp pc rs s tf bb ls ts sg an e env
         (STACKS: match_stackframes s ts (fn_sig tf))
         (FUN: transf_function f = OK tf)
-        (ANL: analyze f (pair_codes f tf) = Some an)
-        (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e)
+        (ANL: analyze f env (pair_codes f tf) = Some an)
+        (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e)
+        (WTF: wt_function f env)
+        (WTRS: wt_regset env rs)
+        (WTRES: env res = proj_sig_res sg)
         (STEPS: forall v ls1 m,
            Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) ->
+           Val.has_type v (env res) ->
            agree_callee_save ls ls1 ->
            exists ls2,
            star LTL.step tge (Block ts tf sp bb ls1 m)
@@ -1540,13 +1570,15 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
 
 Inductive match_states: RTL.state -> LTL.state -> Prop :=
   | match_states_intro:
-      forall s f sp pc rs m ts tf ls m' an e
+      forall s f sp pc rs m ts tf ls m' an e env
         (STACKS: match_stackframes s ts (fn_sig tf))
         (FUN: transf_function f = OK tf)
-        (ANL: analyze f (pair_codes f tf) = Some an)
-        (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e)
+        (ANL: analyze f env (pair_codes f tf) = Some an)
+        (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e)
         (SAT: satisf rs ls e)
-        (MEM: Mem.extends m m'),
+        (MEM: Mem.extends m m')
+        (WTF: wt_function f env)
+        (WTRS: wt_regset env rs),
       match_states (RTL.State s f sp pc rs m)
                    (LTL.State ts tf sp pc ls m')
   | match_states_call:
@@ -1555,7 +1587,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
         (FUN: transf_fundef f = OK tf)
         (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf)))))
         (AG: agree_callee_save (parent_locset ts) ls)
-        (MEM: Mem.extends m m'),
+        (MEM: Mem.extends m m')
+        (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
       match_states (RTL.Callstate s f args m)
                    (LTL.Callstate ts tf ls m')
   | match_states_return:
@@ -1563,7 +1596,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
         (STACKS: match_stackframes s ts sg)
         (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg))))
         (AG: agree_callee_save (parent_locset ts) ls)
-        (MEM: Mem.extends m m'),
+        (MEM: Mem.extends m m')
+        (WTRES: Val.has_type res (proj_sig_res sg)),
       match_states (RTL.Returnstate s res m)
                    (LTL.Returnstate ts ls m').
 
@@ -1576,13 +1610,14 @@ Proof.
   intros. inv H. 
   constructor. congruence.
   econstructor; eauto.
+  unfold proj_sig_res in *. rewrite H0; auto. 
   intros. unfold loc_result in H; rewrite H0 in H; eauto. 
 Qed.
 
 Ltac UseShape :=
   match goal with
-  | [ CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ = OK _ |- _ ] =>
-      destruct (invert_code _ _ _ _ _ _ CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR); 
+  | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] =>
+      destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); 
       inv EBS; unfold transfer_aux in TR; MonadInv
   end.
 
@@ -1626,7 +1661,8 @@ Proof.
   econstructor; eauto. 
 
 (* op move *)
-- simpl in H0. inv H0.  
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0.  
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1637,7 +1673,8 @@ Proof.
   econstructor; eauto.
 
 (* op makelong *)
-- simpl in H0. inv H0. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1649,7 +1686,8 @@ Proof.
   econstructor; eauto.
 
 (* op lowlong *)
-- simpl in H0. inv H0. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1661,7 +1699,8 @@ Proof.
   econstructor; eauto.
 
 (* op highlong *)
-- simpl in H0. inv H0. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1673,7 +1712,8 @@ Proof.
   econstructor; eauto.
 
 (* op regular *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_operation_lessdef; eauto. intros [v' [F G]]. 
   exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]].
@@ -1697,9 +1737,11 @@ Proof.
   eapply reg_unconstrained_satisf; eauto. 
   intros [enext [U V]]. 
   econstructor; eauto.
+  eapply wt_exec_Iop; eauto. 
 
 (* load regular *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
   exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. 
@@ -1715,7 +1757,8 @@ Proof.
   econstructor; eauto.
 
 (* load pair *)
-- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
@@ -1729,15 +1772,12 @@ Proof.
     eapply reg_unconstrained_satisf. eauto. 
     eapply add_equations_satisf; eauto. assumption.
     rewrite Regmap.gss. apply Val.lessdef_trans with v1'; auto. 
-    subst v. unfold v1', kind_first_word.
-    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
   }
   exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. 
   assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')).
   { replace (rs##args) with ((rs#dst<-v)##args). 
     eapply add_equations_lessdef; eauto. 
     apply list_map_exten; intros. rewrite Regmap.gso; auto.
-    exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
     eapply addressing_not_long; eauto. 
   }
   exploit eval_addressing_lessdef. eexact LD3.
@@ -1747,9 +1787,7 @@ Proof.
   assert (SAT4: satisf (rs#dst <- v) ls4 e0).
   { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. 
     eapply add_equations_satisf; eauto. assumption.
-    apply Val.lessdef_trans with v2'; auto. 
-    rewrite Regmap.gss. subst v. unfold v2', kind_second_word.
-    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
+    rewrite Regmap.gss. apply Val.lessdef_trans with v2'; auto.
   }
   exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]].
   econstructor; split.
@@ -1769,7 +1807,8 @@ Proof.
   econstructor; eauto.
 
 (* load first word of a pair *)
-- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
@@ -1781,8 +1820,6 @@ Proof.
   assert (SAT2: satisf (rs#dst <- v) ls2 e0).
   { eapply parallel_assignment_satisf; eauto.
     apply Val.lessdef_trans with v1'; auto. 
-    subst v. unfold v1', kind_first_word.
-    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
     eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   }
   exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. 
@@ -1799,7 +1836,8 @@ Proof.
   econstructor; eauto.
 
 (* load second word of a pair *)
-- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
@@ -1812,8 +1850,6 @@ Proof.
   assert (SAT2: satisf (rs#dst <- v) ls2 e0).
   { eapply parallel_assignment_satisf; eauto.
     apply Val.lessdef_trans with v2'; auto. 
-    subst v. unfold v2', kind_second_word.
-    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
     eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   }
   exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. 
@@ -1839,6 +1875,7 @@ Proof.
   eapply reg_unconstrained_satisf; eauto. 
   intros [enext [U V]]. 
   econstructor; eauto.
+  eapply wt_exec_Iload; eauto.
 
 (* store *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
@@ -1918,19 +1955,21 @@ Proof.
   exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]].
   econstructor; eauto.
   econstructor; eauto.
+  inv WTI. congruence.
   intros. exploit (exec_moves mv2). eauto. eauto. 
   eapply function_return_satisf with (v := v) (ls_before := ls1) (ls_after := ls0); eauto.
   eapply add_equation_ros_satisf; eauto. 
   eapply add_equations_args_satisf; eauto. 
   congruence.
+  apply wt_regset_assign; auto. 
   intros [ls2 [A2 B2]].
   exists ls2; split. 
   eapply star_right. eexact A2. constructor. traceEq.
   apply satisf_incr with eafter; auto. 
   rewrite SIG. eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
   inv WTI. rewrite <- H7. apply wt_regset_list; auto. 
-  simpl. red; auto.
+  simpl. red; auto. 
+  inv WTI. rewrite SIG. rewrite <- H7. apply wt_regset_list; auto. 
 
 (* tailcall *)
 - set (sg := RTL.funsig fd) in *.
@@ -1951,15 +1990,15 @@ Proof.
   eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq.
   destruct (transf_function_inv _ _ FUN); auto.
   rewrite SIG. rewrite return_regs_arg_values; auto. eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
   inv WTI. rewrite <- H6. apply wt_regset_list; auto. 
   apply return_regs_agree_callee_save.
+  rewrite SIG. inv WTI. rewrite <- H6. apply wt_regset_list; auto. 
 
 (* builtin *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- assert (WTRS': wt_regset env (rs#res <- v)) by (eapply wt_exec_Ibuiltin; eauto).
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit external_call_mem_extends; eauto.
   eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
   inv WTI. rewrite <- H4. apply wt_regset_list; auto. 
   intros [v' [m'' [F [G [J K]]]]].
   assert (E: map ls1 (map R args') = reglist ls1 args').
@@ -1990,7 +2029,6 @@ Proof.
 (* annot *)
 - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. 
   exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
   inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. 
   intros [v' [m'' [F [G [J K]]]]].
   assert (v = Vundef). red in H0; inv H0. auto.
@@ -2009,6 +2047,7 @@ Proof.
   econstructor; eauto.
   change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). 
   simpl. subst v. assumption.
+  apply wt_regset_assign; auto. subst v. constructor. 
 
 (* cond *)
 - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
@@ -2040,43 +2079,44 @@ Proof.
 
 (* return *)
 - destruct (transf_function_inv _ _ FUN). 
-  exploit Mem.free_parallel_extends; eauto. rewrite H9. intros [m'' [P Q]].
-  destruct or as [r|]; MonadInv.
-  (* with an argument *)
-+ exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+  exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]].
+  inv WTI; MonadInv.
++ (* without an argument *)
+  exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto. rewrite <- H10.
-  replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f))))
-     with (map ls1 (map R (loc_result (RTL.fn_sig f)))).
-  eapply add_equations_res_lessdef; eauto.
-  rewrite !list_map_compose. apply list_map_exten; intros.
-  unfold return_regs. apply pred_dec_true. eapply loc_result_caller_save; eauto.
+  simpl. econstructor; eauto.
+  unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto.
   apply return_regs_agree_callee_save.
-
-  (* without an argument *)
-+ assert (SG: f.(RTL.fn_sig).(sig_res) = None).
-  { exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
-    inv WTI; auto. }
+  constructor.
++ (* with an argument *)
   exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto.
-  unfold encode_long, loc_result. rewrite <- H10. rewrite SG. simpl; auto.
+  simpl. econstructor; eauto. rewrite <- H11.
+  replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f))))
+     with (map ls1 (map R (loc_result (RTL.fn_sig f)))).
+  eapply add_equations_res_lessdef; eauto.
+  rewrite !list_map_compose. apply list_map_exten; intros.
+  unfold return_regs. apply pred_dec_true. eapply loc_result_caller_save; eauto.
   apply return_regs_agree_callee_save.
+  unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS. 
 
 (* internal function *)
 - monadInv FUN. simpl in *.
   destruct (transf_function_inv _ _ EQ). 
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H7; apply Zle_refl. 
+  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. 
   intros [m'' [U V]].
+  assert (WTRS: wt_regset env (init_regs args (fn_params f))).
+  { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. }
   exploit (exec_moves mv). eauto. eauto.
     eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. 
-    rewrite call_regs_param_values. rewrite H8. eexact ARGS.
+    rewrite call_regs_param_values. rewrite H9. eexact ARGS.
+    exact WTRS.
   intros [ls1 [A B]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -2108,13 +2148,15 @@ Proof.
   exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'. 
   destruct l; simpl; auto. red; intros; subst r0; elim H0.
   eapply loc_result_caller_save; eauto.
- 
+  simpl. eapply external_call_well_typed; eauto. 
+
 (* return *)
 - inv STACKS.
-  exploit STEPS; eauto. intros [ls2 [A B]].
+  exploit STEPS; eauto. rewrite WTRES0; auto. intros [ls2 [A B]].
   econstructor; split.
   eapply plus_left. constructor. eexact A. traceEq.
   econstructor; eauto.
+  apply wt_regset_assign; auto. rewrite WTRES0; auto.
 Qed.
 
 Lemma initial_states_simulation:
@@ -2135,6 +2177,7 @@ Proof.
   rewrite SIG; rewrite H3; simpl; auto.
   red; auto.
   apply Mem.extends_refl.
+  rewrite SIG, H3. constructor.
 Qed.
 
 Lemma final_states_simulation:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 5e46d76..02c3f21 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -34,12 +34,16 @@ let tint = Base Tint
 let tfloat = Base Tfloat
 let tlong = Base Tlong
 let tsingle = Base Tsingle
+let tany32 = Base Tany32
+let tany64 = Base Tany64
 
 let ty_of_typ = function
   | Tint -> tint
   | Tfloat -> tfloat
   | Tlong -> tlong
-  | Tsingle -> tfloat (* should be tsingle when supported *)
+  | Tsingle -> tsingle
+  | Tany32 -> tany32
+  | Tany64 -> tany64
 
 let ty_of_sig_args tyl = List.map ty_of_typ tyl
 
@@ -88,6 +92,7 @@ let name_of_comparison = function
 let type_constant = function
   | Ointconst _ -> tint
   | Ofloatconst _ -> tfloat
+  | Osingleconst _ -> tsingle
   | Olongconst _ -> tlong
   | Oaddrsymbol _ -> tint
   | Oaddrstack _ -> tint
@@ -101,11 +106,18 @@ let type_unary_operation = function
   | Onotint -> tint, tint
   | Onegf -> tfloat, tfloat
   | Oabsf -> tfloat, tfloat
-  | Osingleoffloat -> tfloat, tfloat
+  | Onegfs -> tsingle, tsingle
+  | Oabsfs -> tsingle, tsingle
+  | Osingleoffloat -> tfloat, tsingle
+  | Ofloatofsingle -> tsingle, tfloat
   | Ointoffloat -> tfloat, tint
   | Ointuoffloat -> tfloat, tint
   | Ofloatofint -> tint, tfloat
   | Ofloatofintu -> tint, tfloat
+  | Ointofsingle -> tsingle, tint
+  | Ointuofsingle -> tsingle, tint
+  | Osingleofint -> tint, tsingle
+  | Osingleofintu -> tint, tsingle
   | Onegl -> tlong, tlong
   | Onotl -> tlong, tlong
   | Ointoflong -> tlong, tint
@@ -115,6 +127,8 @@ let type_unary_operation = function
   | Olonguoffloat -> tfloat, tlong
   | Ofloatoflong -> tlong, tfloat
   | Ofloatoflongu -> tlong, tfloat
+  | Olongofsingle -> tsingle, tlong
+  | Olonguofsingle -> tsingle, tlong
   | Osingleoflong -> tlong, tfloat
   | Osingleoflongu -> tlong, tfloat
 
@@ -136,6 +150,10 @@ let type_binary_operation = function
   | Osubf -> tfloat, tfloat, tfloat
   | Omulf -> tfloat, tfloat, tfloat
   | Odivf -> tfloat, tfloat, tfloat
+  | Oaddfs -> tsingle, tsingle, tsingle
+  | Osubfs -> tsingle, tsingle, tsingle
+  | Omulfs -> tsingle, tsingle, tsingle
+  | Odivfs -> tsingle, tsingle, tsingle
   | Oaddl -> tlong, tlong, tlong
   | Osubl -> tlong, tlong, tlong
   | Omull -> tlong, tlong, tlong
@@ -152,6 +170,7 @@ let type_binary_operation = function
   | Ocmp _ -> tint, tint, tint
   | Ocmpu _ -> tint, tint, tint
   | Ocmpf _ -> tfloat, tfloat, tint
+  | Ocmpfs _ -> tsingle, tsingle, tint
   | Ocmpl _ -> tlong, tlong, tint
   | Ocmplu _ -> tlong, tlong, tint
 
@@ -166,8 +185,10 @@ let type_chunk = function
   | Mint16unsigned -> tint
   | Mint32 -> tint
   | Mint64 -> tlong
-  | Mfloat32 -> tfloat
+  | Mfloat32 -> tsingle
   | Mfloat64 -> tfloat
+  | Many32 -> tany32
+  | Many64 -> tany64
 
 let name_of_chunk = PrintAST.name_of_chunk
 
diff --git a/backend/CSE.v b/backend/CSE.v
index 373acce..fa22987 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -293,7 +293,6 @@ Definition store_normalized_range (chunk: memory_chunk) : aval :=
   | Mint8unsigned => Uns 8
   | Mint16signed => Sgn 16
   | Mint16unsigned => Uns 16
-  | Mfloat32 => Fsingle
   | _ => Vtop
   end.
 
@@ -380,7 +379,7 @@ Variable n: numbering.
 Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) :=
   match niter with
   | O => None
-  | S niter' =>
+  | Datatypes.S niter' =>
       match f (fun v => find_valnum_num v n.(num_eqs)) op args with
       | None => None
       | Some(op', args') =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 317fb82..af138f8 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -497,7 +497,6 @@ Proof.
 - inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto.
 - inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto.
 - inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto.
-- inv H. rewrite Float.singleoffloat_of_single by auto. auto.
 Qed.
 
 Lemma add_store_result_hold:
diff --git a/backend/Cminor.v b/backend/Cminor.v
index aaf7510..bf20de2 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -35,7 +35,8 @@ Require Import Switch.
 
 Inductive constant : Type :=
   | Ointconst: int -> constant     (**r integer constant *)
-  | Ofloatconst: float -> constant (**r floating-point constant *)
+  | Ofloatconst: float -> constant (**r double-precision floating-point constant *)
+  | Osingleconst: float32 -> constant (**r single-precision floating-point constant *)
   | Olongconst: int64 -> constant  (**r long integer constant *)
   | Oaddrsymbol: ident -> int -> constant (**r address of the symbol plus the offset *)
   | Oaddrstack: int -> constant.   (**r stack pointer plus the given offset *)
@@ -47,22 +48,31 @@ Inductive unary_operation : Type :=
   | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
   | Onegint: unary_operation               (**r integer opposite *)
   | Onotint: unary_operation               (**r bitwise complement  *)
-  | Onegf: unary_operation                 (**r float opposite *)
-  | Oabsf: unary_operation                 (**r float absolute value *)
+  | Onegf: unary_operation                 (**r float64 opposite *)
+  | Oabsf: unary_operation                 (**r float64 absolute value *)
+  | Onegfs: unary_operation                (**r float32 opposite *)
+  | Oabsfs: unary_operation                (**r float32 absolute value *)
   | Osingleoffloat: unary_operation        (**r float truncation to float32 *)
-  | Ointoffloat: unary_operation           (**r signed integer to float *)
-  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
-  | Ofloatofint: unary_operation           (**r float to signed integer *)
-  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
+  | Ofloatofsingle: unary_operation        (**r float extension to float64 *)
+  | Ointoffloat: unary_operation           (**r signed integer to float64 *)
+  | Ointuoffloat: unary_operation          (**r unsigned integer to float64 *)
+  | Ofloatofint: unary_operation           (**r float64 to signed integer *)
+  | Ofloatofintu: unary_operation          (**r float64 to unsigned integer *)
+  | Ointofsingle: unary_operation          (**r signed integer to float32 *)
+  | Ointuofsingle: unary_operation         (**r unsigned integer to float32 *)
+  | Osingleofint: unary_operation          (**r float32 to signed integer *)
+  | Osingleofintu: unary_operation        (**r float32 to unsigned integer *)
   | Onegl: unary_operation                 (**r long integer opposite *)
   | Onotl: unary_operation                 (**r long bitwise complement *)
   | Ointoflong: unary_operation            (**r long to int *)
   | Olongofint: unary_operation            (**r signed int to long *)
   | Olongofintu: unary_operation           (**r unsigned int to long *)
-  | Olongoffloat: unary_operation          (**r float to signed long *)
-  | Olonguoffloat: unary_operation         (**r float to unsigned long *)
-  | Ofloatoflong: unary_operation          (**r signed long to float *)
-  | Ofloatoflongu: unary_operation         (**r unsigned long to float *)
+  | Olongoffloat: unary_operation          (**r float64 to signed long *)
+  | Olonguoffloat: unary_operation         (**r float64 to unsigned long *)
+  | Ofloatoflong: unary_operation          (**r signed long to float64 *)
+  | Ofloatoflongu: unary_operation         (**r unsigned long to float64 *)
+  | Olongofsingle: unary_operation         (**r float32 to signed long *)
+  | Olonguofsingle: unary_operation        (**r float32 to unsigned long *)
   | Osingleoflong: unary_operation         (**r signed long to float32 *)
   | Osingleoflongu: unary_operation.       (**r unsigned long to float32 *)
 
@@ -80,10 +90,14 @@ Inductive binary_operation : Type :=
   | Oshl: binary_operation                 (**r integer left shift *)
   | Oshr: binary_operation                 (**r integer right signed shift *)
   | Oshru: binary_operation                (**r integer right unsigned shift *)
-  | Oaddf: binary_operation                (**r float addition *)
-  | Osubf: binary_operation                (**r float subtraction *)
-  | Omulf: binary_operation                (**r float multiplication *)
-  | Odivf: binary_operation                (**r float division *)
+  | Oaddf: binary_operation                (**r float64 addition *)
+  | Osubf: binary_operation                (**r float64 subtraction *)
+  | Omulf: binary_operation                (**r float64 multiplication *)
+  | Odivf: binary_operation                (**r float64 division *)
+  | Oaddfs: binary_operation               (**r float32 addition *)
+  | Osubfs: binary_operation               (**r float32 subtraction *)
+  | Omulfs: binary_operation               (**r float32 multiplication *)
+  | Odivfs: binary_operation               (**r float32 division *)
   | Oaddl: binary_operation                (**r long addition *)
   | Osubl: binary_operation                (**r long subtraction *)
   | Omull: binary_operation                (**r long multiplication *)
@@ -99,7 +113,8 @@ Inductive binary_operation : Type :=
   | Oshrlu: binary_operation               (**r long right unsigned shift *)
   | Ocmp: comparison -> binary_operation   (**r integer signed comparison *)
   | Ocmpu: comparison -> binary_operation  (**r integer unsigned comparison *)
-  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
+  | Ocmpf: comparison -> binary_operation  (**r float64 comparison *)
+  | Ocmpfs: comparison -> binary_operation (**r float32 comparison *)
   | Ocmpl: comparison -> binary_operation  (**r long signed comparison *)
   | Ocmplu: comparison -> binary_operation. (**r long unsigned comparison *)
 
@@ -240,6 +255,7 @@ Definition eval_constant (sp: val) (cst: constant) : option val :=
   match cst with
   | Ointconst n => Some (Vint n)
   | Ofloatconst n => Some (Vfloat n)
+  | Osingleconst n => Some (Vsingle n)
   | Olongconst n => Some (Vlong n)
   | Oaddrsymbol s ofs =>
       Some(match Genv.find_symbol ge s with
@@ -258,11 +274,18 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Onotint => Some (Val.notint arg)
   | Onegf => Some (Val.negf arg)
   | Oabsf => Some (Val.absf arg)
+  | Onegfs => Some (Val.negfs arg)
+  | Oabsfs => Some (Val.absfs arg)
   | Osingleoffloat => Some (Val.singleoffloat arg)
+  | Ofloatofsingle => Some (Val.floatofsingle arg)
   | Ointoffloat => Val.intoffloat arg
   | Ointuoffloat => Val.intuoffloat arg
   | Ofloatofint => Val.floatofint arg
   | Ofloatofintu => Val.floatofintu arg
+  | Ointofsingle => Val.intofsingle arg
+  | Ointuofsingle => Val.intuofsingle arg
+  | Osingleofint => Val.singleofint arg
+  | Osingleofintu => Val.singleofintu arg
   | Onegl => Some (Val.negl arg)
   | Onotl => Some (Val.notl arg)
   | Ointoflong => Some (Val.loword arg)
@@ -272,6 +295,8 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Olonguoffloat => Val.longuoffloat arg
   | Ofloatoflong => Val.floatoflong arg
   | Ofloatoflongu => Val.floatoflongu arg
+  | Olongofsingle => Val.longofsingle arg
+  | Olonguofsingle => Val.longuofsingle arg
   | Osingleoflong => Val.singleoflong arg
   | Osingleoflongu => Val.singleoflongu arg
   end.
@@ -296,6 +321,10 @@ Definition eval_binop
   | Osubf => Some (Val.subf arg1 arg2)
   | Omulf => Some (Val.mulf arg1 arg2)
   | Odivf => Some (Val.divf arg1 arg2)
+  | Oaddfs => Some (Val.addfs arg1 arg2)
+  | Osubfs => Some (Val.subfs arg1 arg2)
+  | Omulfs => Some (Val.mulfs arg1 arg2)
+  | Odivfs => Some (Val.divfs arg1 arg2)
   | Oaddl => Some (Val.addl arg1 arg2)
   | Osubl => Some (Val.subl arg1 arg2)
   | Omull => Some (Val.mull arg1 arg2)
@@ -312,6 +341,7 @@ Definition eval_binop
   | Ocmp c => Some (Val.cmp c arg1 arg2)
   | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2)
   | Ocmpf c => Some (Val.cmpf c arg1 arg2)
+  | Ocmpfs c => Some (Val.cmpfs c arg1 arg2)
   | Ocmpl c => Val.cmpl c arg1 arg2
   | Ocmplu c => Val.cmplu c arg1 arg2
   end.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index d2c4d44..bdfc4b1 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -75,6 +75,7 @@ Definition const_for_result (a: aval) : option operation :=
   match a with
   | I n => Some(Ointconst n)
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
+  | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
   | Ptr(Gl symb ofs) => Some(Oaddrsymbol symb ofs)
   | Ptr(Stk ofs) => Some(Oaddrstack ofs)
   | _ => None
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index ecae5dc..b79c721 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -159,6 +159,8 @@ Proof.
   inv H. inv H0. exists (Vint n); auto.
 - (* float *)
   destruct (Compopts.generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto.
+- (* single *)
+  destruct (Compopts.generate_float_constants tt); inv H. inv H0. exists (Vsingle f); auto.
 - (* pointer *)
   destruct p; try discriminate.
   + (* global *)
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 6cb17e3..dcd8624 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -35,7 +35,7 @@ type node =
   { ident: int;                         (*r unique identifier *)
     typ: typ;                           (*r its type *)
     var: var;                           (*r the XTL variable it comes from *)
-    regclass: int;                      (*r identifier of register class *)
+    mutable regclass: int;              (*r identifier of register class *)
     mutable accesses: int;              (*r number of defs and uses *)
     mutable spillcost: float;           (*r estimated cost of spilling *)
     mutable adjlist: node list;         (*r all nodes it interferes with *)
@@ -239,15 +239,20 @@ type graph = {
 
 (* Register classes and reserved registers *)
 
-let num_register_classes = 2
+(* We have two main register classes:
+     0 for integer registers
+     1 for floating-point registers
+   plus a third pseudo-class 2 that has no registers and forces
+   stack allocation.  XTL variables are mapped to classes 0 and 1
+   according to their types.  A variable can be forced into class 2
+   by giving it a negative spill cost. *)
 
 let class_of_type = function
-  | Tint -> 0
-  | Tfloat | Tsingle -> 1
+  | Tint | Tany32 -> 0
+  | Tfloat | Tsingle | Tany64 -> 1
   | Tlong -> assert false
 
-let type_of_class c =
-  if c = 0 then Tint else Tfloat
+let no_spill_class = 2
 
 let reserved_registers = ref ([]: mreg list)
 
@@ -267,14 +272,19 @@ let init costs =
   and float_callee_save = remove_reserved float_callee_save_regs in
   {
     caller_save_registers =
-      [| Array.of_list int_caller_save; Array.of_list float_caller_save |];
+      [| Array.of_list int_caller_save;
+         Array.of_list float_caller_save;
+         [||] |];
     callee_save_registers =
-      [| Array.of_list int_callee_save; Array.of_list float_callee_save |];
+      [| Array.of_list int_callee_save;
+         Array.of_list float_callee_save;
+         [||] |];
     num_available_registers =
       [| List.length int_caller_save + List.length int_callee_save;
-         List.length float_caller_save + List.length float_callee_save |];
+         List.length float_caller_save + List.length float_callee_save;
+         0 |];
     start_points =
-      [| 0; 0 |];
+      [| 0; 0; 0 |];
     allocatable_registers =
       int_caller_save @ int_callee_save @ float_caller_save @ float_callee_save;
     stats_of_reg = costs;
@@ -303,10 +313,13 @@ let newNodeOfReg g r ty =
   let st = g.stats_of_reg r in
   g.nextIdent <- g.nextIdent + 1;
   { ident = g.nextIdent; typ = ty; 
-    var = V(r, ty); regclass = class_of_type ty;
+    var = V(r, ty);
+    regclass = if st.cost >= 0 then class_of_type ty else no_spill_class;
     accesses = st.usedefs;
     spillcost = weightedSpillCost st;
-    adjlist = []; degree = 0; movelist = []; extra_adj = []; extra_pref = [];
+    adjlist = [];
+    degree = if st.cost >= 0 then 0 else 1;
+    movelist = []; extra_adj = []; extra_pref = [];
     alias = None;
     color = None;
     nstate = Initial;
@@ -382,11 +395,19 @@ let recordExtraPref n1 n2 =
       mnext = DLinkMove.dummy; mprev = DLinkMove.dummy } in
   n1.extra_pref <- m :: n1.extra_pref
 
+let recordExtraPref2 n1 n2 =
+  let m =
+    { src = n1; dst = n2; mstate = FrozenMoves;
+      mnext = DLinkMove.dummy; mprev = DLinkMove.dummy } in
+  n1.extra_pref <- m :: n1.extra_pref;
+  n2.extra_pref <- m :: n2.extra_pref
+
 let addMovePref g n1 n2 =
-  assert (n1.regclass = n2.regclass);
   match n1.color, n2.color with
   | None, None ->
-      recordMove g n1 n2
+      if n1.regclass = n2.regclass
+      then recordMove g n1 n2
+      else recordExtraPref2 n1 n2
   | Some (R mr1), None ->
       if List.mem mr1 g.allocatable_registers then recordMove g n1 n2
   | None, Some (R mr2) ->
@@ -866,7 +887,7 @@ let assign_color g n =
           n.color <- Some loc
       | None ->
           (* Last, pick a Local stack slot *)
-          n.color <- Some (find_slot slot_conflicts (type_of_class n.regclass))
+          n.color <- Some (find_slot slot_conflicts n.typ)
 
 (* Extract the location of a variable *)
 
@@ -884,7 +905,7 @@ let location_of_var g v =
         match ty with
         | Tint -> R dummy_int_reg
         | Tfloat | Tsingle -> R dummy_float_reg
-        | Tlong -> assert false
+        | Tlong | Tany32 | Tany64 -> assert false
 
 (* The exported interface *)
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 8e20442..2564a73 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -691,6 +691,7 @@ Proof.
   apply Zone_divide.
   apply Zone_divide.
   apply H2; omega.
+  apply H2; omega.
 Qed.
 
 (** Preservation by external calls *)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index b08fe87..ccf17e1 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -12,15 +12,12 @@
 
 (** Type-checking Linear code. *)
 
-Require Import FSets.
-Require FSetAVL.
 Require Import Coqlib.
-Require Import Ordered.
-Require Import Maps.
-Require Import Iteration.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
+Require Import Globalenvs.
+Require Import Memory.
 Require Import Events.
 Require Import Op.
 Require Import Machregs.
@@ -29,172 +26,20 @@ Require Import Conventions.
 Require Import LTL.
 Require Import Linear.
 
-(** The typechecker for Linear enforce several properties useful for
-  the proof of the [Stacking] pass:
-- for each instruction, the type of the result register or slot
-  agrees with the type of values produced by the instruction;
-- correctness conditions on the offsets of stack slots
-  accessed through [Lgetstack] and [Lsetstack] Linear instructions.
-*)
-
-(** * Tracking the flow of single-precision floats *)
-
-Module Locset := FSetAVL.Make(OrderedLoc).
-
-(** At each program point, we infer a set of locations that are
-  guaranteed to contain single-precision floats.  [None] means
-  that the program point is not reachable. *)
-
-Definition singlefloats := option Locset.t.
-
-Definition FSbot : singlefloats := None.
-Definition FStop : singlefloats := Some Locset.empty.
-
-Definition setreg (fs: singlefloats) (r: mreg) (t: typ) :=
-  match fs with
-  | None => None
-  | Some s =>
-      Some(if typ_eq t Tsingle then Locset.add (R r) s else Locset.remove (R r) s)
-  end.
-
-Fixpoint setregs (fs: singlefloats) (rl: list mreg) (tl: list typ) :=
-  match rl, tl with
-  | nil, nil => fs
-  | r1 :: rs, t1 :: ts => setregs (setreg fs r1 t1) rs ts
-  | _, _ => fs
-  end.
-
-Definition copyloc (fs: singlefloats) (dst src: loc) :=
-  match fs with
-  | None => None
-  | Some s =>
-      Some(if Locset.mem src s then Locset.add dst s else Locset.remove dst s)
-  end.
-
-Definition destroyed_at_call_regs :=
-  List.fold_right (fun r fs => Locset.add (R r) fs) Locset.empty destroyed_at_call.
-
-Definition callregs (fs: singlefloats) :=
-  match fs with
-  | None => None
-  | Some s => Some (Locset.diff s destroyed_at_call_regs)
-  end.
-
-(** The forward dataflow analysis below records [singlefloats] sets
-  at every label.  Sets at other program points are recomputed when
-  needed. *)
-
-Definition labelmap := PTree.t Locset.t.
-
-(** [update_label lbl fs lm] updates the label map [lm] to reflect the
-  fact that the [singlefloats] set [fs] can flow into label [lbl].
-  It returns the set after the label, an updated label map, and a
-  boolean indicating whether the label map changed. *)
-
-Definition update_label (lbl: label) (fs: singlefloats) (lm: labelmap) : 
-                                              singlefloats * labelmap * bool :=
-  match fs, PTree.get lbl lm with
-  | None, None => (None, lm, false)
-  | None, Some s => (Some s, lm, false)
-  | Some s, None => (Some s, PTree.set lbl s lm, true)
-  | Some s1, Some s2 =>
-      if Locset.subset s2 s1
-      then (Some s2, lm, false)
-      else let s := Locset.inter s1 s2 in (Some s, PTree.set lbl s lm, true)
-  end.
-
-(** [update_labels] is similar, for a list of labels (coming from a 
-    [Ljumptable] instruction). *)
-
-Fixpoint update_labels (lbls: list label) (fs: singlefloats) (lm: labelmap): labelmap * bool :=
-  match lbls with
-  | nil => (lm, false)
-  | lbl1 :: lbls =>
-      let '(_, lm1, changed1) := update_label lbl1 fs lm in
-      let '(lm2, changed2) := update_labels lbls fs lm1 in
-      (lm2, changed1 || changed2)
-  end.
-
-(** One pass of forward analysis over the code [c].  Returns an updated
-  label map and a boolean indicating whether the label map changed. *)
-
-Fixpoint ana_code (lm: labelmap) (ch: bool) (fs: singlefloats) (c: code) : labelmap * bool :=
-  match c with
-  | nil => (lm, ch)
-  | Lgetstack sl ofs ty rd :: c =>
-      ana_code lm ch (copyloc fs (R rd) (S sl ofs ty)) c
-  | Lsetstack rs sl ofs ty :: c =>
-      ana_code lm ch (copyloc fs (S sl ofs ty) (R rs)) c
-  | Lop op args dst :: c =>
-      match is_move_operation op args with
-      | Some src => ana_code lm ch (copyloc fs (R dst) (R src)) c
-      | None     => ana_code lm ch (setreg fs dst (snd (type_of_operation op))) c
-      end
-  | Lload chunk addr args dst :: c =>
-      ana_code lm ch (setreg fs dst (type_of_chunk chunk)) c
-  | Lstore chunk addr args src :: c =>
-      ana_code lm ch fs c
-  | Lcall sg ros :: c =>
-      ana_code lm ch (callregs fs) c
-  | Ltailcall sg ros :: c =>
-      ana_code lm ch None c
-  | Lbuiltin ef args res :: c =>
-      ana_code lm ch (setregs fs res (proj_sig_res' (ef_sig ef))) c
-  | Lannot ef args :: c =>
-      ana_code lm ch fs c
-  | Llabel lbl :: c =>
-      let '(fs1, lm1, ch1) := update_label lbl fs lm in
-      ana_code lm1 (ch || ch1) fs1 c
-  | Lgoto lbl :: c =>
-      let '(_, lm1, ch1) := update_label lbl fs lm in
-      ana_code lm1 (ch || ch1) None c
-  | Lcond cond args lbl :: c =>
-      let '(_, lm1, ch1) := update_label lbl fs lm in
-      ana_code lm1 (ch || ch1) fs c
-  | Ljumptable r lbls :: c =>
-      let '(lm1, ch1) := update_labels lbls fs lm in
-      ana_code lm1 (ch || ch1) None c
-  | Lreturn :: c =>
-      ana_code lm ch None c
-  end.
-
-(** Iterating [ana_code] until the label map is stable. *)
-
-Definition ana_iter (c: code) (lm: labelmap) : labelmap + labelmap :=
-  let '(lm1, ch) := ana_code lm false FStop c in
-  if ch then inr _ lm1 else inl _ lm.
-
-Definition ana_function (f: function): option labelmap :=
-  PrimIter.iterate _ _ (ana_iter f.(fn_code)) (PTree.empty _).
-
-(** * The type-checker *)
-
-(** The typing rules are presented as boolean-valued functions so that we
+(** The rules are presented as boolean-valued functions so that we
   get an executable type-checker for free. *)
 
 Section WT_INSTR.
 
 Variable funct: function.
 
-Variable lm: labelmap.
-
-Definition FSmem (l: loc) (fs: singlefloats) : bool :=
-  match fs with None => true | Some s => Locset.mem l s end.
-
-Definition loc_type (fs: singlefloats) (l: loc) :=
-  let ty := Loc.type l in
-  if typ_eq ty Tfloat && FSmem l fs then Tsingle else ty.
-
 Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   match sl with
   | Local => zle 0 ofs
   | Outgoing => zle 0 ofs
   | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig))
   end &&
-  match ty with
-  | Tint | Tfloat | Tsingle => true
-  | Tlong => false
-  end.
+  match ty with Tlong => false | _ => true end.
 
 Definition slot_writable (sl: slot) : bool :=
   match sl with
@@ -210,475 +55,169 @@ Definition loc_valid (l: loc) : bool :=
   | S _ _ _ => false
   end.
 
-Fixpoint wt_code (fs: singlefloats) (c: code) : bool :=
-  match c with
-  | nil => true
-  | Lgetstack sl ofs ty rd :: c =>
-      subtype ty (mreg_type rd) &&
-      slot_valid sl ofs ty &&
-      wt_code (copyloc fs (R rd) (S sl ofs ty)) c
-  | Lsetstack rs sl ofs ty :: c =>
-      subtype (loc_type fs (R rs)) ty &&
-      slot_valid sl ofs ty && slot_writable sl &&
-      wt_code (copyloc fs (S sl ofs ty) (R rs)) c
-  | Lop op args dst :: c =>
+Definition wt_instr (i: instruction) : bool :=
+  match i with
+  | Lgetstack sl ofs ty r =>
+      subtype ty (mreg_type r) && slot_valid sl ofs ty
+  | Lsetstack r sl ofs ty =>
+      slot_valid sl ofs ty && slot_writable sl
+  | Lop op args res =>
       match is_move_operation op args with
-      | Some src =>
-          typ_eq (mreg_type src) (mreg_type dst) &&
-          wt_code (copyloc fs (R dst) (R src)) c
-      | None =>
-          let (ty_args, ty_res) := type_of_operation op in
-          subtype ty_res (mreg_type dst) &&
-          wt_code (setreg fs dst ty_res) c
+      | Some arg =>
+          subtype (mreg_type arg) (mreg_type res)
+      | None => 
+          let (targs, tres) := type_of_operation op in
+          subtype tres (mreg_type res)
       end
-  | Lload chunk addr args dst :: c =>
-      subtype (type_of_chunk chunk) (mreg_type dst) &&
-      wt_code (setreg fs dst (type_of_chunk chunk)) c
-  | Lstore chunk addr args src :: c =>
-      wt_code fs c
-  | Lcall sg ros :: c =>
-      wt_code (callregs fs) c
-  | Ltailcall sg ros :: c =>
-      zeq (size_arguments sg) 0 &&
-      wt_code None c
-  | Lbuiltin ef args res :: c =>
-      let ty_res := proj_sig_res' (ef_sig ef) in
-      subtype_list ty_res (map mreg_type res) &&
-      wt_code (setregs fs res ty_res) c
-  | Lannot ef args :: c =>
-      forallb loc_valid args &&
-      wt_code fs c
-  | Llabel lbl :: c =>
-      wt_code lm!lbl c
-  | Lgoto lbl :: c =>
-      wt_code None c
-  | Lcond cond args lbl :: c =>
-      wt_code fs c
-  | Ljumptable r lbls :: c =>
-      wt_code None c
-  | Lreturn :: c =>
-      wt_code None c
+  | Lload chunk addr args dst =>
+      subtype (type_of_chunk chunk) (mreg_type dst)
+  | Ltailcall sg ros =>
+      zeq (size_arguments sg) 0
+  | Lbuiltin ef args res =>
+      subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) 
+  | Lannot ef args =>
+      forallb loc_valid args
+  | _ =>
+      true
   end.
 
 End WT_INSTR.
 
-Definition wt_funcode (f: function) (lm: labelmap) : bool :=
-  wt_code f lm FStop f.(fn_code).
+Definition wt_code (f: function) (c: code) : bool :=
+  forallb (wt_instr f) c.
 
 Definition wt_function (f: function) : bool :=
-  match ana_function f with
-  | None => false
-  | Some lm => wt_funcode f lm
-  end.
-
-(** * Properties of the static analysis *)
-
-Inductive FSincl: singlefloats -> singlefloats -> Prop :=
-  | FSincl_none: forall fs,
-      FSincl None fs
-  | FSincl_subset: forall s1 s2,
-      Locset.Subset s2 s1 -> FSincl (Some s1) (Some s2).
-
-Lemma update_label_false:
-  forall lbl fs lm fs' lm',
-  update_label lbl fs lm = (fs', lm', false) ->
-  FSincl fs lm!lbl /\ fs' = lm!lbl /\ lm' = lm.
-Proof.
-  unfold update_label; intros. 
-  destruct fs as [s1|]; destruct lm!lbl as [s2|].
-- destruct (Locset.subset s2 s1) eqn:S; inv H.
-  intuition. constructor. apply Locset.subset_2; auto.
-- inv H.
-- inv H. intuition. constructor. 
-- inv H. intuition. constructor.
-Qed.
-
-Lemma update_labels_false:
-  forall fs lbls lm lm',
-  update_labels lbls fs lm = (lm', false) ->
-  (forall lbl, In lbl lbls -> FSincl fs lm!lbl) /\ lm' = lm.
-Proof.
-  induction lbls; simpl; intros. 
-- inv H. tauto. 
-- destruct (update_label a fs lm) as [[fs1 lm1] changed1] eqn:UL.
-  destruct (update_labels lbls fs lm1) as [lm2 changed2] eqn:ULS.
-  inv H. apply orb_false_iff in H2. destruct H2; subst.
-  exploit update_label_false; eauto. intros (A & B & C).
-  exploit IHlbls; eauto. intros (D & E). subst.
-  split. intros. destruct H. congruence. auto.
-  auto.
-Qed.
-
-Lemma ana_code_false:
-  forall lm' c lm ch fs, ana_code lm ch fs c = (lm', false) -> ch = false /\ lm' = lm.
-Proof.
-  induction c; simpl; intros.
-- inv H; auto. 
-- destruct a; try (eapply IHc; eauto; fail).
-  + destruct (is_move_operation o l); eapply IHc; eauto.
-  + destruct (update_label l fs lm) as [[fs1 lm1] ch1] eqn:UL.
-    exploit IHc; eauto. intros [A B]. apply orb_false_iff in A; destruct A; subst.
-    exploit update_label_false; eauto. intros (C & D & E).
-    auto.
-  + destruct (update_label l fs lm) as [[fs1 lm1] ch1] eqn:UL.
-    exploit IHc; eauto. intros [A B]. apply orb_false_iff in A; destruct A; subst.
-    exploit update_label_false; eauto. intros (C & D & E). 
-    auto.
-  + destruct (update_label l0 fs lm) as [[fs1 lm1] ch1] eqn:UL.
-    exploit IHc; eauto. intros [A B]. apply orb_false_iff in A; destruct A; subst.
-    exploit update_label_false; eauto. intros (C & D & E). 
-    auto.
-  + destruct (update_labels l fs lm) as [lm1 ch1] eqn:UL.
-    exploit IHc; eauto. intros [A B]. apply orb_false_iff in A; destruct A; subst.
-    exploit update_labels_false; eauto. intros (C & D); subst.
-    auto.
-Qed.
-
-Lemma ana_function_inv:
-  forall f lm,
-  ana_function f = Some lm -> ana_code lm false FStop f.(fn_code) = (lm, false).
-Proof.
-  intros. unfold ana_function in H.
-  eapply PrimIter.iterate_prop with
-    (Q := fun lm => ana_code lm false FStop (fn_code f) = (lm, false))
-    (P := fun (lm: labelmap) => True); eauto.
-  intros. unfold ana_iter.
-  destruct (ana_code a false FStop (fn_code f)) as (lm1, ch1) eqn:ANA.
-  destruct ch1. auto. exploit ana_code_false; eauto. intros [A B]. congruence. 
-Qed.
-
-Remark wt_ana_code_cons:
-  forall f lm fs i c,
-  ana_code lm false fs (i :: c) = (lm, false) ->
-  wt_code f lm fs (i :: c) = true ->
-  exists fs', ana_code lm false fs' c = (lm, false) /\ wt_code f lm fs' c = true.
-Proof.
-  simpl; intros; destruct i; InvBooleans; try (econstructor; split; eassumption).
-- destruct (is_move_operation o l).
-  InvBooleans; econstructor; eauto.
-  destruct (type_of_operation o); InvBooleans; econstructor; eauto.
-- destruct (update_label l fs lm) as [[fs1 lm1] ch1] eqn:UL. 
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  exploit update_label_false; eauto. intros (C & D & E); subst.
-  econstructor; eauto.
-- destruct (update_label l fs lm) as [[fs1 lm1] ch1] eqn:UL. 
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  econstructor; eauto.
-- destruct (update_label l0 fs lm) as [[fs1 lm1] ch1] eqn:UL. 
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  econstructor; eauto.
-- destruct (update_labels l fs lm) as [lm1 ch1] eqn:UL. 
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  econstructor; eauto.
-Qed.
-
-Lemma wt_find_label_rec:
-  forall f lm lbl c' c fs,
-  find_label lbl c = Some c' ->
-  ana_code lm false fs c = (lm, false) ->
-  wt_code f lm fs c = true ->
-  ana_code lm false (PTree.get lbl lm) c' = (lm, false) /\ wt_code f lm (PTree.get lbl lm) c' = true.
-Proof.
-  induction c; intros.
-- discriminate.
-- simpl in H. specialize (is_label_correct lbl a). destruct (is_label lbl a); intros IL.
-  + subst a. inv H. simpl in *. 
-    destruct (update_label lbl fs lm) as [[fs1 lm1] ch1] eqn:UL.
-    exploit ana_code_false; eauto. intros [A B]; subst.
-    exploit update_label_false; eauto. intros (C & D & E). subst.
-    InvBooleans. auto.
-  + exploit wt_ana_code_cons; eauto. intros (fs' & A & B).
-    eapply IHc; eauto. 
-Qed.
+  wt_code f f.(fn_code).
 
-Lemma wt_find_label:
-  forall f lm lbl c,
-  ana_function f = Some lm ->
-  wt_funcode f lm = true ->
-  find_label lbl f.(fn_code) = Some c ->
-  ana_code lm false (PTree.get lbl lm) c = (lm, false) /\ wt_code f lm (PTree.get lbl lm) c = true.
-Proof.
-  intros. eapply wt_find_label_rec; eauto. apply ana_function_inv; auto. 
-Qed.
+(** Typing the run-time state. *)
 
-(** * Soundness of the type system *)
-
-Require Import Values.
-Require Import Globalenvs.
-Require Import Memory.
-
-Module LSF := FSetFacts.Facts(Locset).
-
-(** ** Typing the run-time state *)
-
-Inductive wt_locset: singlefloats -> locset -> Prop :=
-  | wt_locset_intro: forall s ls
-      (TY: forall l, Val.has_type (ls l) (Loc.type l))
-      (SINGLE: forall l, Locset.In l s -> Val.has_type (ls l) Tsingle),
-    wt_locset (Some s) ls.
-
-Lemma wt_mreg:
-  forall fs ls r, wt_locset fs ls -> Val.has_type (ls (R r)) (mreg_type r).
-Proof.
-  intros. inv H. apply (TY (R r)). 
-Qed.
-
-Lemma wt_loc_type:
-  forall fs ls l, wt_locset fs ls -> Val.has_type (ls l) (loc_type fs l).
-Proof.
-  intros. inv H. unfold loc_type, FSmem.
-  destruct (typ_eq (Loc.type l) Tfloat); simpl; auto.
-  destruct (Locset.mem l s) eqn:MEM; auto. 
-  apply SINGLE. apply Locset.mem_2; auto.
-Qed.
-
-Lemma loc_type_subtype:
-  forall fs l, subtype (loc_type fs l) (Loc.type l) = true.
-Proof.
-  unfold loc_type; intros. destruct (typ_eq (Loc.type l) Tfloat); simpl.
-  rewrite e. destruct (FSmem l fs); auto. 
-  destruct (Loc.type l); auto.
-Qed.
-
-Lemma wt_locset_top:
-  forall ls,
-  (forall l, Val.has_type (ls l) (Loc.type l)) -> 
-  wt_locset FStop ls.
-Proof.
-  intros; constructor; intros. 
-  auto.
-  eelim Locset.empty_1; eauto.
-Qed.
-
-Lemma wt_locset_mon:
-  forall fs1 fs2 ls,
-  FSincl fs1 fs2 -> wt_locset fs1 ls -> wt_locset fs2 ls.
-Proof.
-  intros. inv H0; inv H. constructor; intros; auto. 
-Qed.
+Definition wt_locset (ls: locset) : Prop :=
+  forall l, Val.has_type (ls l) (Loc.type l).
 
 Lemma wt_setreg:
-  forall fs ls r v ty,
-  Val.has_type v ty -> subtype ty (mreg_type r) = true -> wt_locset fs ls ->
-  wt_locset (setreg fs r ty) (Locmap.set (R r) v ls).
-Proof.
-  intros. inv H1. constructor; intros. 
-- unfold Locmap.set. destruct (Loc.eq (R r) l).
-  subst l; simpl. eapply Val.has_subtype; eauto.
-  destruct (Loc.diff_dec (R r) l); simpl; auto.
-- unfold Locmap.set. destruct (Loc.eq (R r) l).
-  destruct (typ_eq ty Tsingle). congruence. 
-  subst l. rewrite LSF.remove_iff in H1. intuition.
-  destruct (Loc.diff_dec (R r) l); simpl; auto.
-  apply SINGLE. 
-  destruct (typ_eq ty Tsingle).
-  rewrite LSF.add_iff in H1; intuition.
-  rewrite LSF.remove_iff in H1; intuition.
-Qed.
-
-Lemma wt_setregs:
-  forall vl tyl rl fs rs,
-  Val.has_type_list vl tyl ->
-  subtype_list tyl (map mreg_type rl) = true ->
-  wt_locset fs rs ->
-  wt_locset (setregs fs rl tyl) (Locmap.setlist (map R rl) vl rs).
-Proof.
-  induction vl; simpl; intros.
-- destruct tyl; try contradiction. destruct rl; try discriminate. 
-  simpl. auto.
-- destruct tyl as [ | ty tyl]; try contradiction. destruct H.
-  destruct rl as [ | r rl]; simpl in H0; try discriminate. InvBooleans.
-  simpl. eapply IHvl; eauto. eapply wt_setreg; eauto. 
-Qed.
-
-Lemma undef_regs_type:
-  forall ty l rl ls,
-  Val.has_type (ls l) ty -> Val.has_type (undef_regs rl ls l) ty.
+  forall ls r v,
+  Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls).
 Proof.
-  induction rl; simpl; intros.
-- auto.
-- unfold Locmap.set. destruct (Loc.eq (R a) l). red; auto. 
-  destruct (Loc.diff_dec (R a) l); auto. red; auto.
+  intros; red; intros.
+  unfold Locmap.set. 
+  destruct (Loc.eq (R r) l).
+  subst l; auto.
+  destruct (Loc.diff_dec (R r) l). auto. red. auto.
 Qed.
 
-Lemma wt_copyloc_gen:
-  forall fs ls src dst temps,
-  Val.has_type (ls src) (Loc.type dst) ->
-  wt_locset fs ls ->
-  wt_locset (copyloc fs dst src) (Locmap.set dst (ls src) (undef_regs temps ls)).
+Lemma wt_setstack:
+  forall ls sl ofs ty v,
+  wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls).
 Proof.
-  intros. inversion H0; subst. constructor; intros. 
-- unfold Locmap.set. destruct (Loc.eq dst l).
-  subst l. auto.
-  destruct (Loc.diff_dec dst l); simpl; auto.
-  apply undef_regs_type; auto.
-- unfold Locmap.set. destruct (Loc.eq dst l).
-  subst l. destruct (Locset.mem src s) eqn:E.
-  apply SINGLE. apply Locset.mem_2; auto. 
-  rewrite LSF.remove_iff in H1. intuition.
-  destruct (Loc.diff_dec dst l); simpl; auto.
-  apply undef_regs_type; auto.
-  apply SINGLE.
-  destruct (Locset.mem src s).
-  rewrite LSF.add_iff in H1. intuition.
-  rewrite LSF.remove_iff in H1. intuition.
-Qed.
-
-Lemma wt_copyloc:
-  forall fs ls src dst temps,
-  subtype (Loc.type src) (Loc.type dst) = true ->
-  wt_locset fs ls ->
-  wt_locset (copyloc fs dst src) (Locmap.set dst (ls src) (undef_regs temps ls)).
-Proof.
-  intros. eapply wt_copyloc_gen; eauto.
-  eapply Val.has_subtype; eauto. inv H0; auto. 
+  intros; red; intros.
+  unfold Locmap.set. 
+  destruct (Loc.eq (S sl ofs ty) l).
+  subst l. simpl. 
+  generalize (Val.load_result_type (chunk_of_type ty) v). 
+  replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
+  destruct ty; reflexivity.
+  destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto.
 Qed.
 
 Lemma wt_undef_regs:
-  forall fs ls temps, wt_locset fs ls -> wt_locset fs (undef_regs temps ls).
+  forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls).
 Proof.
-  intros. inv H; constructor; intros.
-- apply undef_regs_type; auto. 
-- apply undef_regs_type; auto. 
+  induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto.
 Qed.
 
 Lemma wt_call_regs:
-  forall fs ls, wt_locset fs ls -> wt_locset FStop (call_regs ls).
-Proof.
-  intros. inv H. apply wt_locset_top; intros. 
-  unfold call_regs. 
-  destruct l; auto. 
-  destruct sl; try exact I. 
-  change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)); auto.
-Qed.
-
-Remark destroyed_at_call_regs_charact:
-  forall l,
-  Locset.In l destroyed_at_call_regs <->
-  match l with R r => In r destroyed_at_call | S _ _ _ => False end.
+  forall ls, wt_locset ls -> wt_locset (call_regs ls).
 Proof.
-  intros. unfold destroyed_at_call_regs. generalize destroyed_at_call. 
-  induction l0; simpl.
-- rewrite LSF.empty_iff. destruct l; tauto.
-- rewrite LSF.add_iff. rewrite IHl0. destruct l; intuition congruence.
+  intros; red; intros. unfold call_regs. destruct l. auto.
+  destruct sl.
+  red; auto.
+  change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto.
+  red; auto.
 Qed.
 
 Lemma wt_return_regs:
-  forall fs caller fs' callee,
-  wt_locset fs caller -> wt_locset fs' callee ->
-  wt_locset (callregs fs) (return_regs caller callee).
+  forall caller callee,
+  wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).
 Proof.
-  intros. inv H; inv H0; constructor; intros.
-- unfold return_regs. destruct l; auto. 
+  intros; red; intros.
+  unfold return_regs. destruct l; auto.
   destruct (in_dec mreg_eq r destroyed_at_call); auto.
-- unfold callregs. 
-  rewrite LSF.diff_iff in H. rewrite destroyed_at_call_regs_charact in H. destruct H.
-  unfold return_regs. destruct l.
-+ destruct (in_dec mreg_eq r destroyed_at_call). tauto. auto. 
-+ auto.
 Qed.
 
 Lemma wt_init:
-  forall s, wt_locset (Some s) (Locmap.init Vundef).
+  wt_locset (Locmap.init Vundef).
 Proof.
-  intros; constructor; intros; simpl; auto.
+  red; intros. unfold Locmap.init. red; auto.
 Qed.
 
-Lemma callregs_setregs_result:
-  forall sg fs,
-  FSincl (setregs fs (loc_result sg) (proj_sig_res' sg)) (callregs fs).
+Lemma wt_setlist:
+  forall vl rl rs,
+  Val.has_type_list vl (map mreg_type rl) ->
+  wt_locset rs ->
+  wt_locset (Locmap.setlist (map R rl) vl rs).
 Proof.
-  assert (X: forall rl tyl, setregs None rl tyl = None).
-  {
-    induction rl; destruct tyl; simpl; auto. 
-  }
-  assert (Y: forall rl s tyl,
-             exists s', setregs (Some s) rl tyl = Some s'
-                     /\ forall l, Locset.In l s -> ~In l (map R rl) -> Locset.In l s').
-  {
-    induction rl; simpl; intros.
-  - exists s; split. destruct tyl; auto. tauto.
-  - destruct tyl. exists s; tauto. 
-    destruct (IHrl (if typ_eq t Tsingle
-                    then Locset.add (R a) s
-                    else Locset.remove (R a) s) tyl) as (s1 & A & B).
-    exists s1; split; auto. intros. apply B.
-    destruct (typ_eq t Tsingle). 
-    rewrite LSF.add_iff. tauto. 
-    rewrite LSF.remove_iff. tauto.
-    tauto.
-  }
-  intros. destruct fs as [s|]; simpl.
-  - destruct (Y (loc_result sg) s (proj_sig_res' sg)) as (s' & A & B).
-    rewrite A. constructor. red; intros.
-    rewrite LSF.diff_iff in H. destruct H. apply B. auto. 
-    red; intros. exploit list_in_map_inv; eauto. intros (r & U & V).
-    subst a. elim H0. rewrite destroyed_at_call_regs_charact. 
-    eapply loc_result_caller_save; eauto.
-  - rewrite X. constructor.
+  induction vl; destruct rl; simpl; intros; try contradiction.
+  auto.
+  destruct H. apply IHvl; auto. apply wt_setreg; auto. 
+Qed.
+
+Lemma wt_find_label:
+  forall f lbl c,
+  wt_function f = true ->
+  find_label lbl f.(fn_code) = Some c ->
+  wt_code f c = true.
+Proof.
+  unfold wt_function; intros until c. generalize (fn_code f). induction c0; simpl; intros.
+  discriminate.
+  InvBooleans. destruct (is_label lbl a). 
+  congruence.
+  auto.
 Qed.
 
+(** Soundness of the type system *)
+
 Definition wt_fundef (fd: fundef) :=
   match fd with
   | Internal f => wt_function f = true
   | External ef => True
   end.
 
-Inductive wt_callstack: list stackframe -> singlefloats -> Prop :=
-  | wt_callstack_nil: forall s,
-      wt_callstack nil (Some s)
-  | wt_callstack_cons: forall f sp rs c s fs lm fs0 fs1
-        (WTSTK: wt_callstack s fs0)
-        (ANF: ana_function f = Some lm)
-        (WTF: wt_funcode f lm = true)
-        (ANC: ana_code lm false (callregs fs1) c = (lm, false))
-        (WTC: wt_code f lm (callregs fs1) c = true)
-        (WTRS: wt_locset fs rs)
-        (INCL: FSincl (callregs fs) (callregs fs1)),
-      wt_callstack (Stackframe f sp rs c :: s) fs.
+Inductive wt_callstack: list stackframe -> Prop :=
+  | wt_callstack_nil:
+      wt_callstack nil
+  | wt_callstack_cons: forall f sp rs c s
+        (WTSTK: wt_callstack s)
+        (WTF: wt_function f = true)
+        (WTC: wt_code f c = true)
+        (WTRS: wt_locset rs),
+      wt_callstack (Stackframe f sp rs c :: s).
 
 Lemma wt_parent_locset:
-  forall s fs, wt_callstack s fs -> wt_locset fs (parent_locset s).
+  forall s, wt_callstack s -> wt_locset (parent_locset s).
 Proof.
   induction 1; simpl.
 - apply wt_init.
 - auto.
 Qed.
 
-Lemma wt_callstack_change_fs:
-  forall s fs, wt_callstack s fs -> wt_callstack s (callregs fs).
-Proof.
-  induction 1.
-- constructor. 
-- econstructor; eauto. 
-  apply wt_locset_mon with fs; auto.
-  + destruct fs; simpl; constructor.
-    red; intros. eapply Locset.diff_1; eauto. 
-  + inv INCL; simpl; constructor.
-    destruct fs; simpl in H0; inv H0. 
-    red; intros. exploit H2; eauto. rewrite ! LSF.diff_iff. tauto.
-Qed.
-
 Inductive wt_state: state -> Prop :=
-  | wt_regular_state: forall s f sp c rs m lm fs fs0
-        (WTSTK: wt_callstack s fs0)
-        (ANF: ana_function f = Some lm)
-        (WTF: wt_funcode f lm = true)
-        (ANC: ana_code lm false fs c = (lm, false))
-        (WTC: wt_code f lm fs c = true)
-        (WTRS: wt_locset fs rs),
+  | wt_regular_state: forall s f sp c rs m
+        (WTSTK: wt_callstack s )
+        (WTF: wt_function f = true)
+        (WTC: wt_code f c = true)
+        (WTRS: wt_locset rs),
       wt_state (State s f sp c rs m)
-  | wt_call_state: forall s fd rs m fs
-        (WTSTK: wt_callstack s fs)
+  | wt_call_state: forall s fd rs m
+        (WTSTK: wt_callstack s)
         (WTFD: wt_fundef fd)
-        (WTRS: wt_locset fs rs),
+        (WTRS: wt_locset rs),
       wt_state (Callstate s fd rs m)
-  | wt_return_state: forall s rs m fs
-        (WTSTK: wt_callstack s fs)
-        (WTRS: wt_locset (callregs fs) rs),
+  | wt_return_state: forall s rs m
+        (WTSTK: wt_callstack s)
+        (WTRS: wt_locset rs),
       wt_state (Returnstate s rs m).
 
-(** ** Preservation of state typing by transitions *)
+(** Preservation of state typing by transitions *)
 
 Section SOUNDNESS.
 
@@ -709,129 +248,89 @@ Proof.
 - (* getstack *)
   simpl in *; InvBooleans. 
   econstructor; eauto.
-  apply wt_copyloc; auto.
+  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS. 
+  apply wt_undef_regs; auto.
 - (* setstack *)
   simpl in *; InvBooleans. 
   econstructor; eauto.
-  apply wt_copyloc_gen; auto.
-  eapply Val.has_subtype; eauto. eapply wt_loc_type; eauto.
+  apply wt_setstack. apply wt_undef_regs; auto.
 - (* op *)
   simpl in *. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE.
   + (* move *)
     InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. 
     simpl in H. inv H.
-    econstructor; eauto. 
-    apply wt_copyloc; auto. simpl. rewrite H0. 
-    destruct (mreg_type res); auto.
+    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS. 
+    apply wt_undef_regs; auto.
   + (* other ops *) 
     destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
     econstructor; eauto.
-    apply wt_setreg; auto. 
-    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. 
-    eapply type_of_operation_sound; eauto. 
+    apply wt_setreg; auto. eapply Val.has_subtype; eauto. 
+    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. 
     red; intros; subst op. simpl in ISMOVE. 
     destruct args; try discriminate. destruct args; discriminate. 
     apply wt_undef_regs; auto.
 - (* load *)
   simpl in *; InvBooleans. 
   econstructor; eauto.
-  apply wt_setreg. 
+  apply wt_setreg. eapply Val.has_subtype; eauto. 
   destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
-  auto. 
   apply wt_undef_regs; auto.
 - (* store *)
   simpl in *; InvBooleans. 
-  econstructor; eauto.
+  econstructor. eauto. eauto. eauto. 
   apply wt_undef_regs; auto.
 - (* call *)
   simpl in *; InvBooleans.
   econstructor; eauto. econstructor; eauto.
-  destruct (callregs fs); constructor. red; auto. 
   eapply wt_find_function; eauto.
 - (* tailcall *)
   simpl in *; InvBooleans.
-  econstructor. apply wt_callstack_change_fs; eauto. 
+  econstructor; eauto. 
   eapply wt_find_function; eauto.
-  eapply wt_return_regs. apply wt_parent_locset; auto. eauto.
+  apply wt_return_regs; auto. apply wt_parent_locset; auto. 
 - (* builtin *)
   simpl in *; InvBooleans.
   econstructor; eauto.
-  apply wt_setregs. 
-  eapply external_call_well_typed'; eauto.
-  auto.
+  apply wt_setlist. 
+  eapply Val.has_subtype_list; eauto. eapply external_call_well_typed'; eauto. 
   apply wt_undef_regs; auto.
 - (* annot *)
   simpl in *; InvBooleans.
   econstructor; eauto. 
 - (* label *)
-  simpl in *.
-  destruct (update_label lbl fs lm) as [[fs1 lm1] ch1] eqn:UL.
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  exploit update_label_false; eauto. intros (A & B & C); subst.
-  econstructor; eauto.
-  eapply wt_locset_mon; eauto.
+  simpl in *. econstructor; eauto.
 - (* goto *)
-  simpl in *.
-  destruct (update_label lbl fs lm) as [[fs1 lm1] ch1] eqn:UL.
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  exploit update_label_false; eauto. intros (A & B & C); subst.
-  exploit wt_find_label; eauto. intros [P Q].
-  econstructor; eauto. 
-  eapply wt_locset_mon; eauto.
+  simpl in *. econstructor; eauto. eapply wt_find_label; eauto. 
 - (* cond branch, taken *)
-  simpl in *.
-  destruct (update_label lbl fs lm) as [[fs1 lm1] ch1] eqn:UL.
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  exploit update_label_false; eauto. intros (A & B & C); subst.
-  exploit wt_find_label; eauto. intros [P Q].
-  econstructor; eauto. 
-  eapply wt_locset_mon. eauto. 
+  simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto.
   apply wt_undef_regs; auto.
 - (* cond branch, not taken *)
-  simpl in *.
-  destruct (update_label lbl fs lm) as [[fs1 lm1] ch1] eqn:UL.
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  exploit update_label_false; eauto. intros (A & B & C); subst.
-  econstructor. eauto. eauto. eauto. eauto. eauto.  
+  simpl in *. econstructor. auto. auto. auto. 
   apply wt_undef_regs; auto.
 - (* jumptable *)
-  simpl in *.
-  destruct (update_labels tbl fs lm) as [lm1 ch1] eqn:UL.
-  exploit ana_code_false; eauto. intros [A B]; subst.
-  exploit update_labels_false; eauto. intros (A & B); subst.
-  exploit wt_find_label; eauto. intros [P Q].
-  econstructor; eauto.
-  apply wt_undef_regs. eapply wt_locset_mon; eauto. apply A. eapply list_nth_z_in; eauto. 
+  simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto.
+  apply wt_undef_regs; auto.
 - (* return *)
-  econstructor. eauto. 
-  eapply wt_return_regs. 
-  apply wt_parent_locset; auto.
-  eauto.
+  simpl in *. InvBooleans. 
+  econstructor; eauto.
+  apply wt_return_regs; auto. apply wt_parent_locset; auto.
 - (* internal function *)
-  simpl in WTFD. unfold wt_function in WTFD.
-  destruct (ana_function f) as [lm|] eqn:ANF; try discriminate.
-  econstructor. eauto. eauto. eauto. apply ana_function_inv; auto. exact WTFD. 
-  apply wt_undef_regs. eapply wt_call_regs; eauto. 
+  simpl in WTFD.
+  econstructor. eauto. eauto. eauto.
+  apply wt_undef_regs. apply wt_call_regs. auto. 
 - (* external function *)
-  econstructor. eauto. 
-  eapply wt_locset_mon.
-  eapply callregs_setregs_result. 
-  eapply wt_setregs.
-  eapply external_call_well_typed'; eauto.
-  unfold proj_sig_res', loc_result. destruct (sig_res (ef_sig ef) )as [[] | ]; auto.
-  auto.
+  econstructor. auto. apply wt_setlist; auto.
+  eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto.
 - (* return *)
-  inv WTSTK. econstructor; eauto. 
-  apply wt_locset_mon with (callregs fs); auto. 
+  inv WTSTK. econstructor; eauto.
 Qed.
 
 Theorem wt_initial_state:
   forall S, initial_state prog S -> wt_state S.
 Proof.
-  induction 1. econstructor. 
-  apply wt_callstack_nil with (s := Locset.empty). 
+  induction 1. econstructor. constructor. 
   unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto.
-  intros [id IN]. eapply wt_prog; eauto. 
+  intros [id IN]. eapply wt_prog; eauto.
   apply wt_init.
 Qed.
 
@@ -850,10 +349,9 @@ Qed.
 Lemma wt_state_setstack:
   forall s f sp sl ofs ty r c rs m,
   wt_state (State s f sp (Lsetstack r sl ofs ty :: c) rs m) ->
-  Val.has_type (rs (R r)) ty /\ slot_valid f sl ofs ty = true /\ slot_writable sl = true.
+  slot_valid f sl ofs ty = true /\ slot_writable sl = true.
 Proof.
-  intros. inv H. simpl in WTC; InvBooleans. intuition. 
-  eapply Val.has_subtype; eauto. eapply wt_loc_type; eauto. 
+  intros. inv H. simpl in WTC; InvBooleans. intuition.
 Qed.
 
 Lemma wt_state_tailcall:
@@ -877,5 +375,5 @@ Lemma wt_callstate_wt_regs:
   wt_state (Callstate s f rs m) ->
   forall r, Val.has_type (rs (R r)) (mreg_type r).
 Proof.
-  intros. inv H. eapply wt_mreg; eauto.
+  intros. inv H. apply WTRS. 
 Qed.
diff --git a/backend/Locations.v b/backend/Locations.v
index 96f1eba..5674b93 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -69,7 +69,14 @@ Defined.
 Open Scope Z_scope.
 
 Definition typesize (ty: typ) : Z :=
-  match ty with Tint => 1 | Tlong => 2 | Tfloat => 2 | Tsingle => 1 end.
+  match ty with
+  | Tint => 1
+  | Tlong => 2
+  | Tfloat => 2
+  | Tsingle => 1
+  | Tany32 => 1
+  | Tany64 => 2
+  end.
 
 Lemma typesize_pos:
   forall (ty: typ), typesize ty > 0.
@@ -301,16 +308,29 @@ Module Locmap.
 
   Definition set (l: loc) (v: val) (m: t) : t :=
     fun (p: loc) =>
-      if Loc.eq l p then v
-      else if Loc.diff_dec l p then m p
+      if Loc.eq l p then
+        match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end
+      else if Loc.diff_dec l p then
+        m p
       else Vundef.
 
   Lemma gss: forall l v m,
-    (set l v m) l = v.
+    (set l v m) l = 
+    match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end.
   Proof.
     intros. unfold set. apply dec_eq_true.
   Qed.
 
+  Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v.
+  Proof.
+    intros. unfold set. rewrite dec_eq_true. auto.
+  Qed.
+
+  Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v.
+  Proof.
+    intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto. 
+  Qed.
+
   Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p.
   Proof.
     intros. unfold set. destruct (Loc.eq l p).
@@ -336,10 +356,11 @@ Module Locmap.
   Proof.
     assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef).
       induction ll; simpl; intros. auto. apply IHll. 
-      unfold set. destruct (Loc.eq a l). auto.
+      unfold set. destruct (Loc.eq a l).
+      destruct a. auto. destruct ty; reflexivity. 
       destruct (Loc.diff_dec a l); auto.
     induction ll; simpl; intros. contradiction. 
-    destruct H. apply P. subst a. apply gss.  
+    destruct H. apply P. subst a. apply gss_typed. exact I. 
     auto.
   Qed.
 
@@ -364,10 +385,12 @@ Module IndexedTyp <: INDEXED_TYPE.
   Definition t := typ.
   Definition index (x: t) :=
     match x with
-    | Tint => 1%positive
-    | Tsingle => 2%positive
-    | Tfloat => 3%positive
-    | Tlong => 4%positive
+    | Tany32 => 1%positive
+    | Tint => 2%positive
+    | Tsingle => 3%positive
+    | Tany64 => 4%positive
+    | Tfloat => 5%positive
+    | Tlong => 6%positive
     end.
   Lemma index_inj: forall x y, index x = index y -> x = y.
   Proof. destruct x; destruct y; simpl; congruence. Qed.
@@ -456,7 +479,7 @@ Module OrderedLoc <: OrderedType.
   Definition diff_low_bound (l: loc) : loc :=
     match l with
     | R mr => l
-    | S sl ofs ty => S sl (ofs - 1) Tfloat
+    | S sl ofs ty => S sl (ofs - 1) Tany64
     end.
 
   Definition diff_high_bound (l: loc) : loc :=
@@ -480,9 +503,9 @@ Module OrderedLoc <: OrderedType.
         destruct H. right.
         destruct H0. right. generalize (RANGE ty'); omega. 
         destruct H0. 
-        assert (ty' = Tint \/ ty' = Tsingle). 
+        assert (ty' = Tint \/ ty' = Tsingle \/ ty' = Tany32). 
         { unfold OrderedTyp.lt in H1. destruct ty'; auto; compute in H1; congruence. }
-        right. destruct H2; subst ty'; simpl typesize; omega. 
+        right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; omega. 
       + destruct H. left. apply OrderedSlot.lt_not_eq; auto.
         destruct H. right.
         destruct H0. left; omega.
@@ -502,13 +525,13 @@ Module OrderedLoc <: OrderedType.
       destruct H. contradiction. 
       destruct H.
       right; right; split; auto. left; omega. 
-      left; right; split; auto. destruct ty'; simpl in *.
-      destruct (zlt ofs' (ofs - 1)). left; auto. 
-      right; split. omega. compute. auto. 
+      left; right; split; auto.
+      assert (EITHER: typesize ty' = 1 /\ OrderedTyp.lt ty' Tany64 \/ typesize ty' = 2).
+      { destruct ty'; compute; auto. }
+      destruct (zlt ofs' (ofs - 1)). left; auto.
+      destruct EITHER as [[P Q] | P].
+      right; split; auto. omega.
       left; omega. 
-      left; omega.
-      destruct (zlt ofs' (ofs - 1)). left; auto. 
-      right; split. omega. compute. auto. 
   Qed.
 
 End OrderedLoc.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index f050c72..73b6831 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -33,7 +33,6 @@ Require Import RTL.
 Inductive nval : Type :=
   | Nothing              (**r value is entirely unused *)
   | I (m: int)           (**r only need the bits that are 1 in [m] *)
-  | Fsingle              (**r only need the value after conversion to single float *)
   | All.                 (**r every bit of the value is used *)
 
 Definition eq_nval (x y: nval) : {x=y} + {x<>y}.
@@ -56,12 +55,6 @@ Fixpoint vagree (v w: val) (x: nval) {struct x}: Prop :=
       | Vint p, _ => False
       | _, _ => True                                 
       end
-  | Fsingle =>
-      match v, w with
-      | Vfloat f, Vfloat g => Float.singleoffloat f = Float.singleoffloat g
-      | Vfloat _, _ => False
-      | _, _ => True
-      end
   | All => Val.lessdef v w
   end.
 
@@ -115,9 +108,7 @@ Inductive nge: nval -> nval -> Prop :=
   | nge_all: forall x, nge x Nothing
   | nge_int: forall m1 m2,
       (forall i, 0 <= i < Int.zwordsize -> Int.testbit m2 i = true -> Int.testbit m1 i = true) ->
-      nge (I m1) (I m2)
-  | nge_single:
-      nge Fsingle Fsingle.
+      nge (I m1) (I m2).
 
 Lemma nge_refl: forall x, nge x x.
 Proof.
@@ -145,7 +136,6 @@ Definition nlub (x y: nval) : nval :=
   | Nothing, _ => y
   | _, Nothing => x
   | I m1, I m2 => I (Int.or m1 m2)
-  | Fsingle, Fsingle => Fsingle
   | _, _ => All
   end.
 
@@ -388,14 +378,14 @@ Ltac InvAgree :=
   auto || exact Logic.I ||
   match goal with
   | [ H: False |- _ ] => contradiction
-  | [ H: match ?v with Vundef => _ | Vint _ => _ | Vlong _ => _ | Vfloat _ => _ | Vptr _ _ => _ end |- _ ] => destruct v
+  | [ H: match ?v with Vundef => _ | Vint _ => _ | Vlong _ => _ | Vfloat _ => _ | Vsingle _ => _ | Vptr _ _ => _ end |- _ ] => destruct v
   end).
 
 (** And immediate, or immediate *)
 
 Definition andimm (x: nval) (n: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.and m n)
   | All => I n
   end.
@@ -408,13 +398,12 @@ Proof.
   unfold andimm; intros; destruct x; simpl in *; unfold Val.and.
 - auto.
 - InvAgree. apply iagree_and; auto.
-- destruct v; destruct w; tauto.
 - InvAgree. rewrite iagree_and_eq in H. rewrite H; auto.
 Qed.
 
 Definition orimm (x: nval) (n: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.and m (Int.not n))
   | _ => I (Int.not n)
   end.
@@ -427,21 +416,16 @@ Proof.
   unfold orimm; intros; destruct x; simpl in *.
 - auto.
 - unfold Val.or; InvAgree. apply iagree_or; auto.
-- destruct v; destruct w; tauto.
 - InvAgree. simpl. apply Val.lessdef_same. f_equal. apply iagree_mone. 
   apply iagree_or. rewrite Int.and_commut. rewrite Int.and_mone. auto.
 Qed.
 
 (** Bitwise operations: and, or, xor, not *)
 
-Definition bitwise (x: nval) :=
-  match x with
-  | Fsingle => Nothing
-  | _ => x
-  end.
+Definition bitwise (x: nval) := x.
 
 Remark bitwise_idem: forall nv, bitwise (bitwise nv) = bitwise nv.
-Proof. destruct nv; auto. Qed.
+Proof. auto. Qed.
 
 Lemma vagree_bitwise_binop:
   forall f,
@@ -456,7 +440,6 @@ Proof.
   unfold bitwise; intros. destruct x; simpl in *.
 - auto. 
 - InvAgree. 
-- destruct v1; auto. destruct v2; auto. 
 - inv H0; auto. inv H1; auto. destruct w1; auto.
 Qed.
 
@@ -489,7 +472,7 @@ Qed.
 
 Definition shlimm (x: nval) (n: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.shru m n)
   | All => I (Int.shru Int.mone n)
   end.
@@ -504,14 +487,13 @@ Proof.
   destruct x; simpl in *.
 - auto.
 - InvAgree. apply iagree_shl; auto.
-- destruct v; destruct w; auto.
 - InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. apply iagree_shl; auto.
 - destruct v; auto with na.
 Qed.
 
 Definition shruimm (x: nval) (n: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.shl m n)
   | All => I (Int.shl Int.mone n)
   end.
@@ -526,14 +508,13 @@ Proof.
   destruct x; simpl in *.
 - auto.
 - InvAgree. apply iagree_shru; auto.
-- destruct v; destruct w; auto.
 - InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. apply iagree_shru; auto.
 - destruct v; auto with na.
 Qed.
 
 Definition shrimm (x: nval) (n: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (let m' := Int.shl m n in
               if Int.eq_dec (Int.shru m' n) m
               then m'
@@ -554,14 +535,13 @@ Proof.
   destruct (Int.eq_dec (Int.shru (Int.shl m n) n) m).
   apply iagree_shr_1; auto.
   apply iagree_shr; auto.
-- destruct v; destruct w; auto.
 - InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. apply iagree_shr. auto.
 - destruct v; auto with na.
 Qed.
 
 Definition rolm (x: nval) (amount mask: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.ror (Int.and m mask) amount)
   | _ => I (Int.ror mask amount)
   end.
@@ -575,7 +555,6 @@ Proof.
 - auto.
 - unfold Val.rolm; InvAgree. unfold Int.rolm. 
   apply iagree_and. apply iagree_rol. auto. 
-- unfold Val.rolm; destruct v, w; auto.
 - unfold Val.rolm; InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. 
   unfold Int.rolm. apply iagree_and. apply iagree_rol. rewrite Int.and_commut. 
   rewrite Int.and_mone. auto.
@@ -583,7 +562,7 @@ Qed.
 
 Definition ror (x: nval) (amount: int) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.rol m amount)
   | All => All
   end.
@@ -598,7 +577,6 @@ Proof.
   destruct x; simpl in *.
 - auto.
 - InvAgree. apply iagree_ror; auto. 
-- destruct v, w; auto.
 - inv H; auto.
 - destruct v; auto with na.
 Qed.
@@ -608,7 +586,7 @@ Qed.
 
 Definition modarith (x: nval) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (complete_mask m)
   | All => All
   end.
@@ -621,7 +599,6 @@ Proof.
   unfold modarith; intros. destruct x; simpl in *. 
 - auto.
 - unfold Val.add; InvAgree. apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. 
-- unfold Val.add; destruct v1, w1; auto; destruct v2, w2; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto. 
 Qed.
 
@@ -638,7 +615,6 @@ Proof.
   unfold mul, add; intros. destruct x; simpl in *. 
 - auto.
 - unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto. 
-- unfold Val.mul; destruct v1, w1; auto; destruct v2, w2; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto. 
 Qed.
 
@@ -651,7 +627,6 @@ Proof.
 - auto.
 - unfold Val.neg; InvAgree. 
   apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto. 
-- destruct v, w; simpl; auto. 
 - inv H; simpl; auto.
 Qed.
 
@@ -659,7 +634,7 @@ Qed.
 
 Definition zero_ext (n: Z) (x: nval) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.zero_ext n m)
   | All => I (Int.zero_ext n Int.mone)
   end.
@@ -677,7 +652,6 @@ Proof.
   red; intros. autorewrite with ints; try omega. 
   destruct (zlt i1 n); auto. apply H; auto.
   autorewrite with ints; try omega. rewrite zlt_true; auto.
-- unfold Val.zero_ext; destruct v; destruct w; auto.
 - unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. 
   Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto. 
   autorewrite with ints; try omega. apply zlt_true; auto.
@@ -685,7 +659,7 @@ Qed.
 
 Definition sign_ext (n: Z) (x: nval) :=
   match x with
-  | Nothing | Fsingle => Nothing
+  | Nothing => Nothing
   | I m => I (Int.or (Int.zero_ext n m) (Int.shl Int.one (Int.repr (n - 1))))
   | All => I (Int.zero_ext n Int.mone)
   end.
@@ -710,7 +684,6 @@ Proof.
   right. rewrite Int.unsigned_repr. rewrite zlt_false by omega. 
   replace (n - 1 - (n - 1)) with 0 by omega. reflexivity. 
   generalize Int.wordsize_max_unsigned; omega.
-- unfold Val.sign_ext; destruct v; destruct w; auto.
 - unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. 
   Int.bit_solve; try omega.
   set (j := if zlt i1 n then i1 else n - 1).
@@ -721,31 +694,12 @@ Proof.
   unfold j. destruct (zlt i1 n); omega.
 Qed.
 
-Definition singleoffloat (x: nval) :=
-  match x with
-  | Nothing | I _ => Nothing
-  | Fsingle | All => Fsingle
-  end.
-
-Lemma singleoffloat_sound:
-  forall v w x,
-  vagree v w (singleoffloat x) ->
-  vagree (Val.singleoffloat v) (Val.singleoffloat w) x.
-Proof.
-  unfold singleoffloat; intros. destruct x; simpl in *. 
-- auto.
-- unfold Val.singleoffloat; destruct v, w; auto. 
-- unfold Val.singleoffloat; InvAgree. congruence.
-- unfold Val.singleoffloat; InvAgree; auto. rewrite H; auto. 
-Qed.
-
 (** The needs of a memory store concerning the value being stored. *)
 
 Definition store_argument (chunk: memory_chunk) :=
   match chunk with
   | Mint8signed | Mint8unsigned => I (Int.repr 255)
   | Mint16signed | Mint16unsigned => I (Int.repr 65535)
-  | Mfloat32 => Fsingle
   | _ => All
   end.
 
@@ -781,10 +735,9 @@ Proof.
   change 16 with (Int.size (Int.repr 65535)). apply iagree_eqmod; auto.
 - apply encode_val_inject. rewrite val_inject_id; auto.
 - apply encode_val_inject. rewrite val_inject_id; auto.
-- InvAgree. apply SAME. simpl.
-  rewrite <- (Float.bits_of_singleoffloat f).
-  rewrite <- (Float.bits_of_singleoffloat f0).
-  congruence. 
+- apply encode_val_inject. rewrite val_inject_id; auto.
+- apply encode_val_inject. rewrite val_inject_id; auto.
+- apply encode_val_inject. rewrite val_inject_id; auto.
 - apply encode_val_inject. rewrite val_inject_id; auto.
 Qed.
 
@@ -803,8 +756,6 @@ Proof.
   auto. compute; auto.
 - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16).
   auto. omega.
-- apply singleoffloat_sound with (v := Vfloat f) (w := Vfloat f0) (x := All).
-  auto. 
 Qed.
 
 (** The needs of a comparison *)
@@ -1034,24 +985,6 @@ Proof.
   rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate.
 Qed.
 
-Definition singleoffloat_redundant (x: nval) :=
-  match x with
-  | Nothing => true
-  | Fsingle => true
-  | _ => false
-  end.
-
-Lemma singleoffloat_redundant_sound:
-  forall v w x,
-  singleoffloat_redundant x = true ->
-  vagree v w (singleoffloat x) ->
-  vagree (Val.singleoffloat v) w x.
-Proof.
-  unfold singleoffloat; intros. destruct x; try discriminate.
-- auto.
-- simpl in *; InvAgree. simpl. rewrite Float.singleoffloat_idem; auto. 
-Qed.
-
 (** * Neededness for register environments *)
 
 Module NVal <: SEMILATTICE.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 4c53c5e..51a45b2 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -31,10 +31,10 @@ let rec precedence = function
   | Evar _ -> (16, NA)
   | Econst _ -> (16, NA)
   | Eunop _ -> (15, RtoL)
-  | Ebinop((Omul|Odiv|Odivu|Omod|Omodu|Omulf|Odivf|Omull|Odivl|Odivlu|Omodl|Omodlu), _, _) -> (13, LtoR)
-  | Ebinop((Oadd|Osub|Oaddf|Osubf|Oaddl|Osubl), _, _) -> (12, LtoR)
+  | Ebinop((Omul|Odiv|Odivu|Omod|Omodu|Omulf|Odivf|Omulfs|Odivfs|Omull|Odivl|Odivlu|Omodl|Omodlu), _, _) -> (13, LtoR)
+  | Ebinop((Oadd|Osub|Oaddf|Osubf|Oaddfs|Osubfs|Oaddl|Osubl), _, _) -> (12, LtoR)
   | Ebinop((Oshl|Oshr|Oshru|Oshll|Oshrl|Oshrlu), _, _) -> (11, LtoR)
-  | Ebinop((Ocmp _|Ocmpu _|Ocmpf _|Ocmpl _|Ocmplu _), _, _) -> (10, LtoR)
+  | Ebinop((Ocmp _|Ocmpu _|Ocmpf _|Ocmpfs _|Ocmpl _|Ocmplu _), _, _) -> (10, LtoR)
   | Ebinop((Oand|Oandl), _, _) -> (8, LtoR)
   | Ebinop((Oxor|Oxorl), _, _) -> (7, LtoR)
   | Ebinop((Oor|Oorl), _, _) -> (6, LtoR)
@@ -55,11 +55,18 @@ let name_of_unop = function
   | Onotint -> "~"
   | Onegf -> "-f"
   | Oabsf -> "absf"
+  | Onegfs -> "-s"
+  | Oabsfs -> "abss"
   | Osingleoffloat -> "float32"
+  | Ofloatofsingle -> "float64"
   | Ointoffloat -> "intoffloat"
   | Ointuoffloat -> "intuoffloat"
   | Ofloatofint -> "floatofint"
   | Ofloatofintu -> "floatofintu"
+  | Ointofsingle -> "intofsingle"
+  | Ointuofsingle -> "intuofsingle"
+  | Osingleofint -> "singleofint"
+  | Osingleofintu -> "singleofintu"
   | Onegl -> "-l"
   | Onotl -> "~l"
   | Ointoflong -> "intoflong"
@@ -69,6 +76,8 @@ let name_of_unop = function
   | Olonguoffloat -> "longuoffloat"
   | Ofloatoflong -> "floatoflong"
   | Ofloatoflongu -> "floatoflongu"
+  | Olongofsingle -> "longofsingle"
+  | Olonguofsingle -> "longuofsingle"
   | Osingleoflong -> "singleoflong"
   | Osingleoflongu -> "singleoflongu"
 
@@ -98,6 +107,10 @@ let name_of_binop = function
   | Osubf -> "-f"
   | Omulf -> "*f"
   | Odivf -> "/f"
+  | Oaddfs -> "+s"
+  | Osubfs -> "-s"
+  | Omulfs -> "*s"
+  | Odivfs -> "/s"
   | Oaddl -> "+l"
   | Osubl -> "-l"
   | Omull -> "*l"
@@ -114,6 +127,7 @@ let name_of_binop = function
   | Ocmp c -> comparison_name c
   | Ocmpu c -> comparison_name c ^ "u"
   | Ocmpf c -> comparison_name c ^ "f"
+  | Ocmpfs c -> comparison_name c ^ "s"
   | Ocmpl c -> comparison_name c ^ "l"
   | Ocmplu c -> comparison_name c ^ "lu"
 
@@ -135,6 +149,8 @@ let rec expr p (prec, e) =
       fprintf p "%ld" (camlint_of_coqint n)
   | Econst(Ofloatconst f) ->
       fprintf p "%F" (camlfloat_of_coqfloat f)
+  | Econst(Osingleconst f) ->
+      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
   | Econst(Olongconst n) ->
       fprintf p "%LdLL" (camlint64_of_coqint n)
   | Econst(Oaddrsymbol(id, ofs)) ->
@@ -171,6 +187,8 @@ let name_of_type = function
   | Tfloat -> "float"
   | Tlong -> "long"
   | Tsingle -> "single"
+  | Tany32 -> "any32"
+  | Tany64 -> "any64"
 
 let print_sig p sg =
   List.iter
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index ff45809..08ccf12 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -34,6 +34,8 @@ let short_name_of_type = function
   | Tfloat -> 'f'
   | Tlong -> 'l'
   | Tsingle -> 's'
+  | Tany32 -> 'w'
+  | Tany64 -> 'd'
 
 let loc pp = function
   | R r -> mreg pp r
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index e8ae7ae..5042c77 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -36,8 +36,6 @@ Require Import Conventions.
   is very simple, consisting of the four types [Tint] (for integers
   and pointers), [Tfloat] (for double-precision floats), [Tlong]
   (for 64-bit integers) and [Tsingle] (for single-precision floats).
-  At the RTL level, we simplify things further by equating [Tsingle]
-  with [Tfloat].
 
   Additionally, we impose that each pseudo-register has the same type
   throughout the function.  This requirement helps with register allocation,
@@ -57,11 +55,6 @@ Require Import Conventions.
   which can work over both integers and floats.
 *)
 
-Definition normalize (ty: typ) : typ :=
-  match ty with Tsingle => Tfloat | _ => ty end.
-
-Definition normalize_list (tyl: list typ) : list typ := map normalize tyl.
-
 Definition regenv := reg -> typ.
 
 Section WT_INSTR.
@@ -86,39 +79,39 @@ Inductive wt_instr : instruction -> Prop :=
       forall op args res s,
       op <> Omove ->
       map env args = fst (type_of_operation op) ->
-      env res = normalize (snd (type_of_operation op)) ->
+      env res = snd (type_of_operation op) ->
       valid_successor s ->
       wt_instr (Iop op args res s)
   | wt_Iload:
       forall chunk addr args dst s,
       map env args = type_of_addressing addr ->
-      env dst = normalize (type_of_chunk chunk) ->
+      env dst = type_of_chunk chunk ->
       valid_successor s ->
       wt_instr (Iload chunk addr args dst s)
   | wt_Istore:
       forall chunk addr args src s,
       map env args = type_of_addressing addr ->
-      env src = type_of_chunk_use chunk ->
+      env src = type_of_chunk chunk ->
       valid_successor s ->
       wt_instr (Istore chunk addr args src s)
   | wt_Icall:
       forall sig ros args res s,
       match ros with inl r => env r = Tint | inr s => True end ->
-      map env args = normalize_list sig.(sig_args) ->
-      env res = normalize (proj_sig_res sig) ->
+      map env args = sig.(sig_args) ->
+      env res = proj_sig_res sig ->
       valid_successor s ->
       wt_instr (Icall sig ros args res s)
   | wt_Itailcall:
       forall sig ros args,
       match ros with inl r => env r = Tint | inr s => True end ->
-      map env args = normalize_list sig.(sig_args) ->
+      map env args = sig.(sig_args) ->
       sig.(sig_res) = funct.(fn_sig).(sig_res) ->
       tailcall_possible sig ->
       wt_instr (Itailcall sig ros args)
   | wt_Ibuiltin:
       forall ef args res s,
-      map env args = normalize_list (ef_sig ef).(sig_args) ->
-      env res = normalize (proj_sig_res (ef_sig ef)) ->
+      map env args = (ef_sig ef).(sig_args) ->
+      env res = proj_sig_res (ef_sig ef) ->
       valid_successor s ->
       wt_instr (Ibuiltin ef args res s)
   | wt_Icond:
@@ -139,7 +132,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Ireturn_some:
       forall arg ty,
       funct.(fn_sig).(sig_res) = Some ty ->
-      env arg = normalize ty ->
+      env arg = ty ->
       wt_instr (Ireturn (Some arg)).
 
 End WT_INSTR.
@@ -152,7 +145,7 @@ End WT_INSTR.
 Record wt_function (f: function) (env: regenv): Prop :=
   mk_wt_function {
     wt_params:
-      map env f.(fn_params) = normalize_list f.(fn_sig).(sig_args);
+      map env f.(fn_params) = f.(fn_sig).(sig_args);
     wt_norepet:
       list_norepet f.(fn_params);
     wt_instrs:
@@ -231,23 +224,23 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
         end
       else
        (let (targs, tres) := type_of_operation op in
-        do e1 <- S.set_list e args targs; S.set e1 res (normalize tres))
+        do e1 <- S.set_list e args targs; S.set e1 res tres)
   | Iload chunk addr args dst s =>
       do x <- check_successor s;
       do e1 <- S.set_list e args (type_of_addressing addr);
-      S.set e1 dst (normalize (type_of_chunk chunk))
+      S.set e1 dst (type_of_chunk chunk)
   | Istore chunk addr args src s =>
       do x <- check_successor s;
       do e1 <- S.set_list e args (type_of_addressing addr);
-      S.set e1 src (type_of_chunk_use chunk)
+      S.set e1 src (type_of_chunk chunk)
   | Icall sig ros args res s =>
       do x <- check_successor s;
       do e1 <- type_ros e ros;
-      do e2 <- S.set_list e1 args (normalize_list sig.(sig_args));
-      S.set e2 res (normalize (proj_sig_res sig))
+      do e2 <- S.set_list e1 args sig.(sig_args);
+      S.set e2 res (proj_sig_res sig)
   | Itailcall sig ros args =>
       do e1 <- type_ros e ros;
-      do e2 <- S.set_list e1 args (normalize_list sig.(sig_args));
+      do e2 <- S.set_list e1 args sig.(sig_args);
       if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then
         if tailcall_is_possible sig
         then OK e2
@@ -256,8 +249,8 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
   | Ibuiltin ef args res s =>
       let sig := ef_sig ef in
       do x <- check_successor s;
-      do e1 <- S.set_list e args (normalize_list sig.(sig_args));
-      S.set e1 res (normalize (proj_sig_res sig))
+      do e1 <- S.set_list e args sig.(sig_args);
+      S.set e1 res (proj_sig_res sig)
  | Icond cond args s1 s2 =>
       do x1 <- check_successor s1;
       do x2 <- check_successor s2;
@@ -271,7 +264,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
   | Ireturn optres =>
       match optres, f.(fn_sig).(sig_res) with
       | None, None => OK e
-      | Some r, Some t => S.set e r (normalize t)
+      | Some r, Some t => S.set e r t
       | _, _ => Error(msg "bad return")
       end
   end.
@@ -297,7 +290,7 @@ Definition check_params_norepet (params: list reg): res unit :=
 
 Definition type_function : res regenv :=
   do e1 <- type_code S.initial;
-  do e2 <- S.set_list e1 f.(fn_params) (normalize_list f.(fn_sig).(sig_args));
+  do e2 <- S.set_list e1 f.(fn_params) f.(fn_sig).(sig_args);
   do te <- S.solve e2;
   do x1 <- check_params_norepet f.(fn_params);
   do x2 <- check_successor f.(fn_entrypoint);
@@ -597,7 +590,7 @@ Proof.
   intros. destruct H. 
   destruct (type_code_complete te S.initial) as (e1 & A & B).
   auto. apply S.satisf_initial. 
-  destruct (S.set_list_complete te f.(fn_params) (normalize_list f.(fn_sig).(sig_args)) e1) as (e2 & C & D); auto.
+  destruct (S.set_list_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); auto.
   destruct (S.solve_complete te e2) as (te' & E); auto.
   exists te'; unfold type_function.
   rewrite A; simpl. rewrite C; simpl. rewrite E; simpl. 
@@ -637,23 +630,6 @@ Proof.
   apply H.
 Qed.
 
-Lemma normalize_subtype:
-  forall ty, subtype ty (normalize ty) = true.
-Proof.
-  intros. destruct ty; reflexivity.
-Qed.
-
-Lemma wt_regset_assign2:
-  forall env rs v r ty,
-  wt_regset env rs ->
-  Val.has_type v ty ->
-  env r = normalize ty ->
-  wt_regset env (rs#r <- v).
-Proof.
-  intros. eapply wt_regset_assign; eauto.
-  rewrite H1. eapply Val.has_subtype; eauto. apply normalize_subtype.
-Qed.
-
 Lemma wt_regset_list:
   forall env rs,
   wt_regset env rs ->
@@ -684,9 +660,8 @@ Proof.
   intros. inv H. 
   simpl in H0. inv H0. apply wt_regset_assign; auto.
   rewrite H4; auto.
-  eapply wt_regset_assign2; auto.
-  eapply type_of_operation_sound; eauto.
-  auto.
+  eapply wt_regset_assign; auto.
+  rewrite H8. eapply type_of_operation_sound; eauto.
 Qed.
 
 Lemma wt_exec_Iload:
@@ -697,8 +672,7 @@ Lemma wt_exec_Iload:
   wt_regset env (rs#dst <- v).
 Proof.
   intros. destruct a; simpl in H0; try discriminate. inv H.
-  eapply wt_regset_assign2; eauto.
-  eapply Mem.load_type; eauto.
+  eapply wt_regset_assign; eauto. rewrite H8; eapply Mem.load_type; eauto.
 Qed.
 
 Lemma wt_exec_Ibuiltin:
@@ -709,8 +683,8 @@ Lemma wt_exec_Ibuiltin:
   wt_regset env (rs#res <- vres).
 Proof.
   intros. inv H. 
-  eapply wt_regset_assign2; eauto. 
-  eapply external_call_well_typed; eauto.
+  eapply wt_regset_assign; eauto. 
+  rewrite H7; eapply external_call_well_typed; eauto.
 Qed.
 
 Lemma wt_instr_at:
@@ -728,7 +702,7 @@ Inductive wt_stackframes: list stackframe -> signature -> Prop :=
       forall s res f sp pc rs env sg,
       wt_function f env ->
       wt_regset env rs ->
-      env res = normalize (proj_sig_res sg) ->
+      env res = proj_sig_res sg ->
       wt_stackframes s (fn_sig f) ->
       wt_stackframes (Stackframe res f sp pc rs :: s) sg.
 
@@ -743,12 +717,12 @@ Inductive wt_state: state -> Prop :=
       forall s f args m,
       wt_stackframes s (funsig f) ->
       wt_fundef f ->
-      Val.has_type_list args (normalize_list (sig_args (funsig f))) ->
+      Val.has_type_list args (sig_args (funsig f)) ->
       wt_state (Callstate s f args m)
   | wt_state_return:
       forall s v m sg,
       wt_stackframes s sg ->
-      Val.has_type v (normalize (proj_sig_res sg)) ->
+      Val.has_type v (proj_sig_res sg) ->
       wt_state (Returnstate s v m).
 
 Remark wt_stackframes_change_sig:
@@ -814,15 +788,13 @@ Proof.
   econstructor; eauto.
   (* Ireturn *)
   econstructor; eauto. 
-  inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. rewrite <- H3. auto. 
+  inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. auto. 
   (* internal function *)
   simpl in *. inv H5.
   econstructor; eauto.
   inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. 
   (* external function *)
   econstructor; eauto. simpl.  
-  change (Val.has_type res (normalize (proj_sig_res (ef_sig ef)))).
-  eapply Val.has_subtype. apply normalize_subtype. 
   eapply external_call_well_typed; eauto.
   (* return *)
   inv H1. econstructor; eauto.
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index b736f29..687cbbd 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -92,7 +92,14 @@ let rec constrain_regs vl cl =
   | v1 :: vl', None :: cl' -> v1 :: constrain_regs vl' cl'
 
 let move v1 v2 k =
-  if v1 = v2 then k else Xmove(v1, v2) :: k
+  if v1 = v2 then
+    k
+  else if is_stack_reg v1 then begin
+    let t = new_temp (typeof v2) in Xmove(v1, t) :: Xmove(t, v2) :: k
+  end else if is_stack_reg v2 then begin
+    let t = new_temp (typeof v1) in Xmove(v1, t) :: Xmove(t, v2) :: k
+  end else
+    Xmove(v1, v2) :: k
 
 let rec movelist vl1 vl2 k =
   match vl1, vl2 with
@@ -104,7 +111,7 @@ let xparmove srcs dsts k =
   assert (List.length srcs = List.length dsts);
   match srcs, dsts with
   | [], [] -> k
-  | [src], [dst] -> Xmove(src, dst) :: k
+  | [src], [dst] -> move src dst k
   | _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k
 
 (* Return the XTL basic block corresponding to the given RTL instruction.
@@ -365,9 +372,15 @@ let spill_costs f =
     | L l -> ()
     | V(r, ty) ->
         let st = get_stats r in
-        let c1 = st.cost + amount in
-        let c2 = if c1 >= 0 then c1 else max_int (* overflow *) in
-        st.cost <- c2;
+        if st.cost < 0 then
+          (* the variable must be spilled, don't change its cost *)
+          assert (amount < max_int)
+        else begin
+          (* saturating addition *)
+          let c1 = st.cost + amount in
+          let c2 = if c1 >= 0 then c1 else max_int (* overflow *) in
+          st.cost <- c2
+        end;           
         st.usedefs <- st.usedefs + uses in
 
   let charge_list amount uses vl =
@@ -376,9 +389,23 @@ let spill_costs f =
   let charge_ros amount ros =
     match ros with Coq_inl v -> charge amount 1 v | Coq_inr id -> () in
 
+  let force_stack_allocation v =
+    match v with
+    | L l -> ()
+    | V(r, ty) ->
+        let st = get_stats r in
+        assert (st.cost < max_int);
+        st.cost <- (-1) in
+
   let charge_instr = function
     | Xmove(src, dst) ->
-        charge 1 1 src; charge 1 1 dst
+        if is_stack_reg src then
+          force_stack_allocation dst
+        else if is_stack_reg dst then
+          force_stack_allocation src
+        else begin
+          charge 1 1 src; charge 1 1 dst
+        end
     | Xreload(src, dst) ->
         charge 1 1 src; charge max_int 1 dst
         (* dest must not be spilled! *)
@@ -491,10 +518,13 @@ let add_interfs_instr g instr live =
             add_interfs_list g (vmreg mr) srcs;
             IRC.add_interf g (vmreg mr) ftmp)
           (destroyed_by_setstack Tsingle)
+  | Xop(Ofloatofsingle, arg1::_, res) when Configuration.arch = "powerpc" ->
+      add_interfs_def g res live;
+      IRC.add_pref g arg1 res
   | Xop(op, args, res) ->
       begin match is_two_address op args with
       | None ->
-          add_interfs_def g res live;
+          add_interfs_def g res live
       | Some(arg1, argl) ->
           (* Treat as "res := arg1; res := op(res, argl)" *)
           add_interfs_def g res live;
@@ -502,7 +532,7 @@ let add_interfs_instr g instr live =
           add_interfs_move g arg1 res
             (vset_addlist (res :: argl) (VSet.remove res live))
       end;
-      add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op);
+      add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op)
   | Xload(chunk, addr, args, dst) ->
       add_interfs_def g dst live;
       add_interfs_destroyed g (VSet.remove dst live) 
@@ -576,10 +606,16 @@ let tospill_instr alloc instr ts =
       then ts
       else VSet.add src (VSet.add dst ts)
   | Xreload(src, dst) ->
-      assert (is_reg alloc dst);
+      if not (is_reg alloc dst) then begin
+        printf "Error: %a was spilled\n" PrintXTL.var dst;
+        assert false
+      end;
       ts
   | Xspill(src, dst) ->
-      assert (is_reg alloc src);
+      if not (is_reg alloc src) then begin
+        printf "Error: %a was spilled\n" PrintXTL.var src;
+        assert false
+      end;
       ts
   | Xparmove(srcs, dsts, itmp, ftmp) ->
       assert (is_reg alloc itmp && is_reg alloc ftmp);
@@ -834,7 +870,9 @@ let make_parmove srcs dsts itmp ftmp k =
   assert (Array.length dst = n);
   let status = Array.make n To_move in
   let temp_for =
-    function Tint -> itmp | (Tfloat|Tsingle) -> ftmp | Tlong -> assert false in
+    function (Tint|Tany32) -> itmp
+           | (Tfloat|Tsingle|Tany64) -> ftmp
+           | Tlong -> assert false in
   let code = ref [] in
   let add_move s d =
     match s, d with
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 938ce5d..a275a85 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -182,4 +182,16 @@ Nondetfunction divf (e1: expr) (e2: expr) :=
   | _ => Eop Odivf (e1 ::: e2 ::: Enil)
   end.
 
+Definition divfsimm (e: expr) (n: float32) :=
+  match Float32.exact_inverse n with
+  | Some n' => Eop Omulfs (e ::: Eop (Osingleconst n') Enil ::: Enil)
+  | None    => Eop Odivfs (e ::: Eop (Osingleconst n) Enil ::: Enil)
+  end.
+
+Nondetfunction divfs (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Osingleconst n2) Enil => divfsimm e1 n2
+  | _ => Eop Odivfs (e1 ::: e2 ::: Enil)
+  end.
+
 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 9228cde..d4bd4f5 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -570,4 +570,20 @@ Proof.
 - TrivialExists.
 Qed.
 
+Theorem eval_divfs:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divfs a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros until y. unfold divfs. destruct (divfs_match b); intros.
+- unfold divfsimm. destruct (Float32.exact_inverse n2) as [n2' | ] eqn:EINV.
+  + inv H0. inv H4. simpl in H6. inv H6. econstructor; split.
+    EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. 
+    simpl; eauto. 
+    destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto. 
+  + TrivialExists. 
+- TrivialExists.
+Qed.
+
 End CMCONSTRS.
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index 0c1cbb3..ab4ab8c 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -138,6 +138,10 @@ Definition floatoflong (arg: expr) :=
   Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil).
 Definition floatoflongu (arg: expr) :=
   Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil).
+Definition longofsingle (arg: expr) := 
+  longoffloat (floatofsingle arg).
+Definition longuofsingle (arg: expr) :=
+  longuoffloat (floatofsingle arg).
 Definition singleoflong (arg: expr) :=
   Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil).
 Definition singleoflongu (arg: expr) :=
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index ec0dd2c..c7c7ab2 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -435,6 +435,34 @@ Proof.
   auto.
 Qed.
 
+Theorem eval_longofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.longofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold longofsingle.
+  destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2.
+  exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+  apply Float32.to_long_double in EQ. 
+  eapply eval_longoffloat; eauto. simpl.
+  change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
+Qed.
+
+Theorem eval_longuofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.longuofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold longuofsingle.
+  destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2.
+  exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+  apply Float32.to_longu_double in EQ. 
+  eapply eval_longuoffloat; eauto. simpl.
+  change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
+Qed.
+
 Theorem eval_singleoflong:
   forall le a x y,
   eval_expr ge sp e m le a x ->
diff --git a/backend/Selection.v b/backend/Selection.v
index f62a888..9bd37ef 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -70,6 +70,7 @@ Definition sel_constant (cst: Cminor.constant) : expr :=
   match cst with
   | Cminor.Ointconst n => Eop (Ointconst n) Enil
   | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil
+  | Cminor.Osingleconst f => Eop (Osingleconst f) Enil
   | Cminor.Olongconst n => longconst n
   | Cminor.Oaddrsymbol id ofs => addrsymbol id ofs
   | Cminor.Oaddrstack ofs => addrstack ofs
@@ -85,11 +86,18 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Onotint => notint arg
   | Cminor.Onegf => negf arg
   | Cminor.Oabsf => absf arg
+  | Cminor.Onegfs => negfs arg
+  | Cminor.Oabsfs => absfs arg
   | Cminor.Osingleoffloat => singleoffloat arg
+  | Cminor.Ofloatofsingle => floatofsingle arg
   | Cminor.Ointoffloat => intoffloat arg
   | Cminor.Ointuoffloat => intuoffloat arg
   | Cminor.Ofloatofint => floatofint arg
   | Cminor.Ofloatofintu => floatofintu arg
+  | Cminor.Ointofsingle => intofsingle arg
+  | Cminor.Ointuofsingle => intuofsingle arg
+  | Cminor.Osingleofint => singleofint arg
+  | Cminor.Osingleofintu => singleofintu arg
   | Cminor.Onegl => negl hf arg
   | Cminor.Onotl => notl arg
   | Cminor.Ointoflong => intoflong arg
@@ -99,6 +107,8 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Olonguoffloat => longuoffloat hf arg
   | Cminor.Ofloatoflong => floatoflong hf arg
   | Cminor.Ofloatoflongu => floatoflongu hf arg
+  | Cminor.Olongofsingle => longofsingle hf arg
+  | Cminor.Olonguofsingle => longuofsingle hf arg
   | Cminor.Osingleoflong => singleoflong hf arg
   | Cminor.Osingleoflongu => singleoflongu hf arg
   end.
@@ -122,6 +132,10 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Osubf => subf arg1 arg2
   | Cminor.Omulf => mulf arg1 arg2
   | Cminor.Odivf => divf arg1 arg2
+  | Cminor.Oaddfs => addfs arg1 arg2
+  | Cminor.Osubfs => subfs arg1 arg2
+  | Cminor.Omulfs => mulfs arg1 arg2
+  | Cminor.Odivfs => divfs arg1 arg2
   | Cminor.Oaddl => addl hf arg1 arg2
   | Cminor.Osubl => subl hf arg1 arg2
   | Cminor.Omull => mull hf arg1 arg2
@@ -138,6 +152,7 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Ocmp c => comp c arg1 arg2
   | Cminor.Ocmpu c => compu c arg1 arg2
   | Cminor.Ocmpf c => compf c arg1 arg2
+  | Cminor.Ocmpfs c => compfs c arg1 arg2
   | Cminor.Ocmpl c => cmpl c arg1 arg2
   | Cminor.Ocmplu c => cmplu c arg1 arg2
   end.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 175b025..55977b4 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -191,11 +191,18 @@ Proof.
   apply eval_notint; auto.
   apply eval_negf; auto.
   apply eval_absf; auto.
+  apply eval_negfs; auto.
+  apply eval_absfs; auto.
   apply eval_singleoffloat; auto.
+  apply eval_floatofsingle; auto.
   eapply eval_intoffloat; eauto.
   eapply eval_intuoffloat; eauto.
   eapply eval_floatofint; eauto.
   eapply eval_floatofintu; eauto.
+  eapply eval_intofsingle; eauto.
+  eapply eval_intuofsingle; eauto.
+  eapply eval_singleofint; eauto.
+  eapply eval_singleofintu; eauto.
   eapply eval_negl; eauto.
   eapply eval_notl; eauto.
   eapply eval_intoflong; eauto.
@@ -205,6 +212,8 @@ Proof.
   eapply eval_longuoffloat; eauto.
   eapply eval_floatoflong; eauto.
   eapply eval_floatoflongu; eauto.
+  eapply eval_longofsingle; eauto.
+  eapply eval_longuofsingle; eauto.
   eapply eval_singleoflong; eauto.
   eapply eval_singleoflongu; eauto.
 Qed.
@@ -234,6 +243,10 @@ Proof.
   apply eval_subf; auto.
   apply eval_mulf; auto.
   apply eval_divf; auto.
+  apply eval_addfs; auto.
+  apply eval_subfs; auto.
+  apply eval_mulfs; auto.
+  apply eval_divfs; auto.
   eapply eval_addl; eauto.
   eapply eval_subl; eauto.
   eapply eval_mull; eauto.
@@ -250,6 +263,7 @@ Proof.
   apply eval_comp; auto.
   apply eval_compu; auto.
   apply eval_compf; auto.
+  apply eval_compfs; auto.
   exists v; split; auto. eapply eval_cmpl; eauto.
   exists v; split; auto. eapply eval_cmplu; eauto.
 Qed.
@@ -377,6 +391,7 @@ Proof.
   destruct cst; simpl in *; inv H. 
   exists (Vint i); split; auto. econstructor. constructor. auto. 
   exists (Vfloat f); split; auto. econstructor. constructor. auto.
+  exists (Vsingle f); split; auto. econstructor. constructor. auto. 
   exists (Val.longofwords (Vint (Int64.hiword i)) (Vint (Int64.loword i))); split.
   eapply eval_Eop. constructor. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
   simpl. rewrite Int64.ofwords_recompose. auto.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index f7c16d1..4ee43bb 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -73,12 +73,12 @@ Definition save_callee_save_regs
 Definition save_callee_save_int (fe: frame_env) :=
   save_callee_save_regs 
     fe_num_int_callee_save index_int_callee_save FI_saved_int
-    Tint fe int_callee_save_regs.
+    Tany32 fe int_callee_save_regs.
 
 Definition save_callee_save_float (fe: frame_env) :=
   save_callee_save_regs
     fe_num_float_callee_save index_float_callee_save FI_saved_float 
-    Tfloat fe float_callee_save_regs.
+    Tany64 fe float_callee_save_regs.
 
 Definition save_callee_save (fe: frame_env) (k: Mach.code) :=
   save_callee_save_int fe (save_callee_save_float fe k).
@@ -103,12 +103,12 @@ Definition restore_callee_save_regs
 Definition restore_callee_save_int (fe: frame_env) :=
   restore_callee_save_regs 
     fe_num_int_callee_save index_int_callee_save FI_saved_int
-    Tint fe int_callee_save_regs.
+    Tany32 fe int_callee_save_regs.
 
 Definition restore_callee_save_float (fe: frame_env) :=
   restore_callee_save_regs
     fe_num_float_callee_save index_float_callee_save FI_saved_float 
-    Tfloat fe float_callee_save_regs.
+    Tany64 fe float_callee_save_regs.
 
 Definition restore_callee_save (fe: frame_env) (k: Mach.code) :=
   restore_callee_save_int fe (restore_callee_save_float fe k).
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index b69f1ec..28b155a 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -132,8 +132,8 @@ Definition type_of_index (idx: frame_index) :=
   | FI_retaddr => Tint
   | FI_local x ty => ty
   | FI_arg x ty => ty
-  | FI_saved_int x => Tint
-  | FI_saved_float x => Tfloat
+  | FI_saved_int x => Tany32
+  | FI_saved_float x => Tany64
   end.
 
 (** Non-overlap between the memory areas corresponding to two
@@ -194,8 +194,8 @@ Proof.
   destruct idx1; destruct idx2;
   simpl in V1; simpl in V2; repeat InvIndexValid; simpl in DIFF;
   unfold offset_of_index, type_of_index;
+  change (AST.typesize Tany32) with 4; change (AST.typesize Tany64) with 8;
   change (AST.typesize Tint) with 4;
-  change (AST.typesize Tfloat) with 8;
   omega.
 Qed.
 
@@ -211,8 +211,8 @@ Proof.
   destruct idx;
   simpl in V; repeat InvIndexValid;
   unfold offset_of_index, type_of_index;
+  change (AST.typesize Tany32) with 4; change (AST.typesize Tany64) with 8;
   change (AST.typesize Tint) with 4;
-  change (AST.typesize Tfloat) with 8;
   omega.
 Qed.
 
@@ -254,6 +254,17 @@ Proof.
   auto with align_4.
 Qed.
 
+Lemma offset_of_index_aligned_2:
+  forall idx, index_valid idx ->
+  (align_chunk (chunk_of_type (type_of_index idx)) | offset_of_index fe idx).
+Proof.
+  intros. replace (align_chunk (chunk_of_type (type_of_index idx))) with 4.
+  apply offset_of_index_aligned.
+  assert (type_of_index idx <> Tlong) by
+    (destruct idx; simpl; simpl in H; intuition congruence).
+  destruct (type_of_index idx); auto; congruence.
+Qed.
+
 Lemma fe_stack_data_aligned:
   (8 | fe_stack_data fe).
 Proof.
@@ -271,7 +282,7 @@ Lemma index_local_valid:
 Proof.
   unfold slot_within_bounds, slot_valid, index_valid; intros. 
   InvBooleans. 
-  split. destruct ty; congruence. auto.
+  split. destruct ty; auto || discriminate. auto.
 Qed.
 
 Lemma index_arg_valid:
@@ -281,7 +292,7 @@ Lemma index_arg_valid:
 Proof.
   unfold slot_within_bounds, slot_valid, index_valid; intros. 
   InvBooleans. 
-  split. destruct ty; congruence. auto.
+  split. destruct ty; auto || discriminate. auto. 
 Qed.
 
 Lemma index_saved_int_valid:
@@ -322,8 +333,8 @@ Proof.
   AddPosProps.
   destruct idx; simpl in V; repeat InvIndexValid;
   unfold offset_of_index, type_of_index;
+  change (AST.typesize Tany32) with 4; change (AST.typesize Tany64) with 8;
   change (AST.typesize Tint) with 4;
-  change (AST.typesize Tfloat) with 8;
   omega.
 Qed.
 
@@ -414,7 +425,7 @@ Proof.
   intros. exploit gss_index_contains_base; eauto. intros [v' [A B]].
   assert (v' = v).
     destruct v; destruct (type_of_index idx); simpl in *;
-    try contradiction; auto. rewrite Floats.Float.singleoffloat_of_single in B; auto. 
+    try contradiction; auto.
   subst v'. auto.
 Qed.
 
@@ -479,11 +490,7 @@ Proof.
   rewrite size_type_chunk. 
   apply Mem.range_perm_implies with Freeable; auto with mem.
   apply offset_of_index_perm; auto.
-  replace (align_chunk (chunk_of_type (type_of_index idx))) with 4.
-  apply offset_of_index_aligned; auto.
-  assert (type_of_index idx <> Tlong).
-    destruct idx; simpl in *; tauto || congruence.
-  destruct (type_of_index idx); reflexivity || congruence. 
+  apply offset_of_index_aligned_2; auto.
   exists m'; auto.
 Qed.
 
@@ -514,7 +521,8 @@ Proof.
   intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]].
   exists v''; split; auto.
   inv H2; destruct (type_of_index idx); simpl in *; try contradiction; subst; auto.
-  rewrite Floats.Float.singleoffloat_of_single; auto. 
+  econstructor; eauto.
+  econstructor; eauto.
   econstructor; eauto.
 Qed.
 
@@ -529,6 +537,8 @@ Proof.
   exists v''; split; auto.
   inv H1; destruct (type_of_index idx); simpl in *; try contradiction; subst; auto. 
   econstructor; eauto.
+  econstructor; eauto.
+  econstructor; eauto.
 Qed.
 
 Lemma gso_index_contains_inj:
@@ -576,11 +586,7 @@ Proof.
   rewrite size_type_chunk.
   apply Mem.range_perm_implies with Freeable; auto with mem.
   apply offset_of_index_perm; auto. 
-  replace (align_chunk (chunk_of_type (type_of_index idx))) with 4. 
-  apply offset_of_index_aligned.
-  assert (type_of_index idx <> Tlong).
-    destruct idx; simpl in *; tauto || congruence.
-  destruct (type_of_index idx); reflexivity || congruence. 
+  apply offset_of_index_aligned_2; auto.
   intros [v C]. 
   exists v; split; auto. constructor; auto. 
 Qed.
@@ -844,18 +850,17 @@ Lemma agree_frame_set_local:
   forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
-  Val.has_type v ty ->
   val_inject j v v' ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' ->
   agree_frame j (Locmap.set (S Local ofs ty) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
   intros. inv H. 
-  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H4.
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3.
   constructor; auto; intros.
 (* local *)
   unfold Locmap.set.
   destruct (Loc.eq (S Local ofs ty) (S Local ofs0 ty0)).
-  inv e. eapply gss_index_contains_inj; eauto with stacking.
+  inv e. eapply gss_index_contains_inj'; eauto with stacking.
   destruct (Loc.diff_dec (S Local ofs ty) (S Local ofs0 ty0)).
   eapply gso_index_contains_inj. eauto. eauto with stacking. eauto. 
   simpl. simpl in d. intuition.
@@ -884,20 +889,19 @@ Lemma agree_frame_set_outgoing:
   forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
-  Val.has_type v ty ->
   val_inject j v v' ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' ->
   agree_frame j (Locmap.set (S Outgoing ofs ty) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
   intros. inv H. 
-  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H4.
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3.
   constructor; auto; intros.
 (* local *)
   rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. red; auto.
   red; left; congruence.
 (* outgoing *)
   unfold Locmap.set. destruct (Loc.eq (S Outgoing ofs ty) (S Outgoing ofs0 ty0)).
-  inv e. eapply gss_index_contains_inj; eauto with stacking.
+  inv e. eapply gss_index_contains_inj'; eauto with stacking.
   destruct (Loc.diff_dec (S Outgoing ofs ty) (S Outgoing ofs0 ty0)).
   eapply gso_index_contains_inj; eauto with stacking.
   red. red in d. intuition. 
@@ -1145,12 +1149,6 @@ Proof.
   apply check_mreg_list_incl; compute; auto.
 Qed.
 
-Remark destroyed_by_move_at_function_entry:
-  incl (destroyed_by_op Omove) destroyed_at_function_entry.
-Proof.
-  apply check_mreg_list_incl; compute; auto.
-Qed.
-
 Remark temp_for_parent_frame_caller_save:
   In temp_for_parent_frame destroyed_at_call.
 Proof.
@@ -1164,6 +1162,12 @@ Hint Resolve destroyed_by_op_caller_save destroyed_by_load_caller_save
     destroyed_by_cond_caller_save destroyed_by_jumptable_caller_save
     destroyed_at_function_entry_caller_save: stacking.
 
+Remark destroyed_by_setstack_function_entry:
+  forall ty, incl (destroyed_by_setstack ty) destroyed_at_function_entry.
+Proof.
+  destruct ty; apply check_mreg_list_incl; compute; auto. 
+Qed.
+
 Remark transl_destroyed_by_op:
   forall op e, destroyed_by_op (transl_op e op) = destroyed_by_op op.
 Proof.
@@ -1367,12 +1371,12 @@ Lemma save_callee_save_correct:
   /\ agree_regs j ls rs'.
 Proof.
   intros.
-  assert (UNDEF: forall r, In r (destroyed_by_op Omove) -> ls (R r) = Vundef).
-    intros. unfold ls. apply LTL_undef_regs_same. apply destroyed_by_move_at_function_entry; auto.
+  assert (UNDEF: forall r ty, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef).
+    intros. unfold ls. apply LTL_undef_regs_same. eapply destroyed_by_setstack_function_entry; eauto.
   exploit (save_callee_save_regs_correct 
              fe_num_int_callee_save
              index_int_callee_save
-             FI_saved_int Tint
+             FI_saved_int Tany32
              j cs fb sp int_callee_save_regs ls).
   intros. apply index_int_callee_save_inj; auto. 
   intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption.
@@ -1380,8 +1384,7 @@ Proof.
   intros; congruence.
   intros; simpl. destruct idx; auto. congruence.
   intros. apply int_callee_save_type. auto.
-Local Transparent destroyed_by_setstack.
-  simpl. tauto.
+  eauto.
   auto.
   apply incl_refl. 
   apply int_callee_save_norepet.
@@ -1391,7 +1394,7 @@ Local Transparent destroyed_by_setstack.
   exploit (save_callee_save_regs_correct 
              fe_num_float_callee_save
              index_float_callee_save
-             FI_saved_float Tfloat
+             FI_saved_float Tany64
              j cs fb sp float_callee_save_regs ls).
   intros. apply index_float_callee_save_inj; auto. 
   intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption.
@@ -1399,7 +1402,7 @@ Local Transparent destroyed_by_setstack.
   intros; congruence.
   intros; simpl. destruct idx; auto. congruence.
   intros. apply float_callee_save_type. auto.
-  simpl. tauto. 
+  eauto.
   auto. 
   apply incl_refl. 
   apply float_callee_save_norepet.
@@ -1462,6 +1465,16 @@ Proof.
   left. apply Plt_ne; auto.
 Qed.
 
+Lemma undef_regs_type:
+  forall ty l rl ls,
+  Val.has_type (ls l) ty -> Val.has_type (LTL.undef_regs rl ls l) ty.
+Proof.
+  induction rl; simpl; intros.
+- auto.
+- unfold Locmap.set. destruct (Loc.eq (R a) l). red; auto. 
+  destruct (Loc.diff_dec (R a) l); auto. red; auto.
+Qed.
+
 (** As a corollary of the previous lemmas, we obtain the following
   correctness theorem for the execution of a function prologue
   (allocation of the frame + saving of the link and return address +
@@ -1732,7 +1745,7 @@ Proof.
              fe_num_int_callee_save
              index_int_callee_save
              FI_saved_int
-             Tint
+             Tany32
              int_callee_save_regs
              j cs fb sp' ls0 m'); auto.
   intros. unfold mreg_within_bounds. split; intros.
@@ -1750,7 +1763,7 @@ Proof.
              fe_num_float_callee_save
              index_float_callee_save
              FI_saved_float
-             Tfloat
+             Tany64
              float_callee_save_regs
              j cs fb sp' ls0 m'); auto.
   intros. unfold mreg_within_bounds. split; intros.
@@ -2318,8 +2331,8 @@ Proof.
   unfold parent_sp.
   assert (slot_valid f Outgoing pos ty = true).
     exploit loc_arguments_acceptable; eauto. intros [A B]. 
-    unfold slot_valid. unfold proj_sumbool. rewrite zle_true. 
-    destruct ty; reflexivity || congruence. omega.
+    unfold slot_valid. unfold proj_sumbool. rewrite zle_true by omega.
+    destruct ty; auto; congruence.
   assert (slot_within_bounds (function_bounds f) Outgoing pos ty).
     eauto.
   exploit agree_outgoing; eauto. intros [v [A B]].
@@ -2525,7 +2538,7 @@ Proof.
   apply agree_frame_set_reg; auto.
 
 - (* Lsetstack *)
-  exploit wt_state_setstack; eauto. intros (VTY & SV & SW). 
+  exploit wt_state_setstack; eauto. intros (SV & SW). 
   set (idx := match sl with
               | Local => FI_local ofs ty
               | Incoming => FI_link (*dummy*)
@@ -2552,15 +2565,15 @@ Proof.
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
   eauto with mem. eauto with mem. intros. rewrite <- H1; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. 
-  eauto. eauto. auto. 
+  eauto. eauto. 
   apply agree_regs_set_slot. apply agree_regs_undef_regs; auto. 
   destruct sl.
   + eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto.
-    apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS. 
+    apply destroyed_by_setstack_caller_save. auto. auto. auto.
     assumption. 
   + simpl in SW; discriminate.
   + eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto.
-    apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS.
+    apply destroyed_by_setstack_caller_save. auto. auto. auto.
     assumption.
   + eauto with coqlib.
 
@@ -2613,13 +2626,15 @@ Proof.
   apply plus_one. econstructor. 
   instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   eexact C. eauto.
-  econstructor; eauto with coqlib.
+  econstructor. eauto.
   eapply match_stacks_parallel_stores. eexact MINJ. eexact B. eauto. eauto. auto. 
+  eauto. eauto. 
   rewrite transl_destroyed_by_store. 
   apply agree_regs_undef_regs; auto. 
   apply agree_frame_undef_locs; auto.
   eapply agree_frame_parallel_stores; eauto.
-  apply destroyed_by_store_caller_save. 
+  apply destroyed_by_store_caller_save.
+  eauto with coqlib.
 
 - (* Lcall *)
   exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index e293028..813944d 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -166,7 +166,7 @@ Definition store_init_data (ab: ablock) (p: Z) (id: init_data) : ablock :=
   | Init_int32 n => ablock_store Mint32 ab p (I n)
   | Init_int64 n => ablock_store Mint64 ab p (L n)
   | Init_float32 n => ablock_store Mfloat32 ab p
-                        (if propagate_float_constants tt then F n else ftop)
+                        (if propagate_float_constants tt then FS n else ftop)
   | Init_float64 n => ablock_store Mfloat64 ab p
                         (if propagate_float_constants tt then F n else ftop)
   | Init_addrof symb ofs => ablock_store Mint32 ab p (Ptr (Gl symb ofs))
@@ -922,7 +922,7 @@ Proof.
     eapply VMTOP; eauto.
   - exploit BC'INV; eauto. intros (b'' & delta & J'). 
     exploit Mem.loadbytes_inject. eexact IMEM. eauto. eauto. intros (bytes & A & B).
-    inv B. inv H3. eapply PMTOP; eauto. 
+    inv B. inv H3. inv H7. eapply PMTOP; eauto. 
   }
   (* Conclusions *)
   exists bc'; splitall.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index c8431bb..75dd9d2 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -509,13 +509,13 @@ Inductive aval : Type :=
   | Sgn (n: Z)
   | L (n: int64)
   | F (f: float)
-  | Fsingle
+  | FS (f: float32)
   | Ptr (p: aptr)
   | Ifptr (p: aptr).
 
 Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}.
 Proof.
-  intros. generalize zeq Int.eq_dec Int64.eq_dec Float.eq_dec eq_aptr; intros.
+  intros. generalize zeq Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec eq_aptr; intros.
   decide equality. 
 Defined.
 
@@ -537,14 +537,14 @@ Inductive vmatch : val -> aval -> Prop :=
   | vmatch_Sgn_undef: forall n, vmatch Vundef (Sgn n)
   | vmatch_l: forall i, vmatch (Vlong i) (L i)
   | vmatch_f: forall f, vmatch (Vfloat f) (F f)
-  | vmatch_single: forall f, Float.is_single f -> vmatch (Vfloat f) Fsingle
-  | vmatch_single_undef: vmatch Vundef Fsingle
+  | vmatch_s: forall f, vmatch (Vsingle f) (FS f)
   | vmatch_ptr: forall b ofs p, pmatch b ofs p -> vmatch (Vptr b ofs) (Ptr p)
   | vmatch_ptr_undef: forall p, vmatch Vundef (Ptr p)
   | vmatch_ifptr_undef: forall p, vmatch Vundef (Ifptr p)
   | vmatch_ifptr_i: forall i p, vmatch (Vint i) (Ifptr p)
   | vmatch_ifptr_l: forall i p, vmatch (Vlong i) (Ifptr p)
   | vmatch_ifptr_f: forall f p, vmatch (Vfloat f) (Ifptr p)
+  | vmatch_ifptr_s: forall f p, vmatch (Vsingle f) (Ifptr p)
   | vmatch_ifptr_p: forall b ofs p, pmatch b ofs p -> vmatch (Vptr b ofs) (Ifptr p).
 
 Lemma vmatch_ifptr:
@@ -569,11 +569,14 @@ Proof. constructor. Qed.
 Lemma vmatch_ftop: forall f, vmatch (Vfloat f) ftop.
 Proof. intros; constructor. Qed.
 
+Lemma vmatch_ftop_single: forall f, vmatch (Vsingle f) ftop.
+Proof. intros; constructor. Qed.
+
 Lemma vmatch_undef_ftop: vmatch Vundef ftop.
 Proof. constructor. Qed.    
 
 Hint Constructors vmatch : va.
-Hint Resolve vmatch_itop vmatch_undef_itop vmatch_ftop vmatch_undef_ftop : va.
+Hint Resolve vmatch_itop vmatch_undef_itop vmatch_ftop vmatch_ftop_single vmatch_undef_ftop : va.
 
 (* Some properties about [is_uns] and [is_sgn]. *)
 
@@ -770,22 +773,21 @@ Inductive vge: aval -> aval -> Prop :=
   | vge_i: forall i, vge (I i) (I i)
   | vge_l: forall i, vge (L i) (L i)
   | vge_f: forall f, vge (F f) (F f)
+  | vge_s: forall f, vge (FS f) (FS f)
   | vge_uns_i: forall n i, 0 <= n -> is_uns n i -> vge (Uns n) (I i)
   | vge_uns_uns: forall n1 n2, n1 >= n2 -> vge (Uns n1) (Uns n2)
   | vge_sgn_i: forall n i, 0 < n -> is_sgn n i -> vge (Sgn n) (I i)
   | vge_sgn_sgn: forall n1 n2, n1 >= n2 -> vge (Sgn n1) (Sgn n2)
   | vge_sgn_uns: forall n1 n2, n1 > n2 -> vge (Sgn n1) (Uns n2)
-  | vge_single_f: forall f, Float.is_single f -> vge Fsingle (F f)
-  | vge_single: vge Fsingle Fsingle
   | vge_p_p: forall p q, pge p q -> vge (Ptr p) (Ptr q)
   | vge_ip_p: forall p q, pge p q -> vge (Ifptr p) (Ptr q)
   | vge_ip_ip: forall p q, pge p q -> vge (Ifptr p) (Ifptr q)
   | vge_ip_i: forall p i, vge (Ifptr p) (I i)
   | vge_ip_l: forall p i, vge (Ifptr p) (L i)
   | vge_ip_f: forall p f, vge (Ifptr p) (F f)
+  | vge_ip_s: forall p f, vge (Ifptr p) (FS f)
   | vge_ip_uns: forall p n, vge (Ifptr p) (Uns n)
-  | vge_ip_sgn: forall p n, vge (Ifptr p) (Sgn n)
-  | vge_ip_single: forall p, vge (Ifptr p) Fsingle.
+  | vge_ip_sgn: forall p n, vge (Ifptr p) (Sgn n).
 
 Hint Constructors vge : va.
 
@@ -836,12 +838,9 @@ Definition vlub (v w: aval) : aval :=
   | Sgn n1, Uns n2 => sgn (Z.max n1 (n2 + 1))
   | Sgn n1, Sgn n2 => sgn (Z.max n1 n2)
   | F f1, F f2 =>
-      if Float.eq_dec f1 f2 then v else
-      if Float.is_single_dec f1 && Float.is_single_dec f2 then Fsingle else ftop
-  | F f, Fsingle | Fsingle, F f =>
-      if Float.is_single_dec f then Fsingle else ftop
-  | Fsingle, Fsingle =>
-      Fsingle
+      if Float.eq_dec f1 f2 then v else ftop
+  | FS f1, FS f2 =>
+      if Float32.eq_dec f1 f2 then v else ftop
   | L i1, L i2 =>
       if Int64.eq i1 i2 then v else ltop
   | Ptr p1, Ptr p2 => Ptr(plub p1 p2)
@@ -865,8 +864,8 @@ Proof.
 - f_equal; apply Z.max_comm.
 - f_equal; apply Z.max_comm.
 - rewrite Int64.eq_sym. predSpec Int64.eq Int64.eq_spec n0 n; congruence.
-- rewrite dec_eq_sym. destruct (Float.eq_dec f0 f). congruence. 
-  rewrite andb_comm. auto.
+- rewrite dec_eq_sym. destruct (Float.eq_dec f0 f). congruence. auto.
+- rewrite dec_eq_sym. destruct (Float32.eq_dec f0 f). congruence. auto.
 - f_equal; apply plub_comm.
 - f_equal; apply plub_comm.
 - f_equal; apply plub_comm.
@@ -937,12 +936,8 @@ Proof.
 - eapply vge_trans. apply vge_sgn_sgn'. eauto with va.
 - eapply vge_trans. apply vge_sgn_sgn'. eauto with va.
 - destruct (Int64.eq n n0); constructor.
-- destruct (Float.eq_dec f f0). constructor.
-  destruct (Float.is_single_dec f && Float.is_single_dec f0) eqn:FS.
-  InvBooleans. auto with va.
-  constructor.
-- destruct (Float.is_single_dec f); constructor; auto. 
-- destruct (Float.is_single_dec f); constructor; auto.
+- destruct (Float.eq_dec f f0); constructor.
+- destruct (Float32.eq_dec f f0); constructor.
 - constructor; apply pge_lub_l; auto.
 - constructor; apply pge_lub_l; auto.
 - constructor; apply pge_lub_l; auto.
@@ -1043,8 +1038,7 @@ Definition vincl (v w: aval) : bool :=
   | Sgn n, Sgn m => zle n m
   | L i, L j => Int64.eq_dec i j
   | F i, F j => Float.eq_dec i j
-  | F i, Fsingle => Float.is_single_dec i
-  | Fsingle, Fsingle => true
+  | FS i, FS j => Float32.eq_dec i j
   | Ptr p, Ptr q => pincl p q
   | Ptr p, Ifptr q => pincl p q
   | Ifptr p, Ifptr q => pincl p q
@@ -1063,7 +1057,7 @@ Proof.
   InvBooleans. constructor; auto with va.
   InvBooleans. subst; auto with va.
   InvBooleans. subst; auto with va.
-  InvBooleans. auto with va.
+  InvBooleans. subst; auto with va.
   constructor; apply pincl_ge; auto.
   constructor; apply pincl_ge; auto.
   constructor; apply pincl_ge; auto.
@@ -1154,6 +1148,28 @@ Proof.
   intros. unfold binop_float; inv H; auto with va; inv H0; auto with va.
 Qed.
 
+Definition unop_single (sem: float32 -> float32) (x: aval) :=
+  match x with FS n => FS (sem n) | _ => ftop end.
+
+Lemma unop_single_sound:
+  forall sem v x,
+  vmatch v x ->
+  vmatch (match v with Vsingle i => Vsingle(sem i) | _ => Vundef end) (unop_single sem x).
+Proof.
+  intros. unfold unop_single; inv H; auto with va.
+Qed.
+
+Definition binop_single (sem: float32 -> float32 -> float32) (x y: aval) :=
+  match x, y with FS n, FS m => FS (sem n m) | _, _ => ftop end.
+
+Lemma binop_single_sound:
+  forall sem v x w y,
+  vmatch v x -> vmatch w y ->
+  vmatch (match v, w with Vsingle i, Vsingle j => Vsingle(sem i j) | _, _ => Vundef end) (binop_single sem x y).
+Proof.
+  intros. unfold binop_single; inv H; auto with va; inv H0; auto with va.
+Qed.
+
 (** Logical operations *)
 
 Definition shl (v w: aval) :=
@@ -1636,6 +1652,42 @@ Lemma divf_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divf v w) (divf x y).
 Proof (binop_float_sound Float.div).
 
+Definition negfs := unop_single Float32.neg.
+
+Lemma negfs_sound: 
+  forall v x, vmatch v x -> vmatch (Val.negfs v) (negfs x).
+Proof (unop_single_sound Float32.neg).
+
+Definition absfs := unop_single Float32.abs.
+
+Lemma absfs_sound: 
+  forall v x, vmatch v x -> vmatch (Val.absfs v) (absfs x).
+Proof (unop_single_sound Float32.abs).
+
+Definition addfs := binop_single Float32.add.
+
+Lemma addfs_sound: 
+  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addfs v w) (addfs x y).
+Proof (binop_single_sound Float32.add).
+
+Definition subfs := binop_single Float32.sub.
+
+Lemma subfs_sound: 
+  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subfs v w) (subfs x y).
+Proof (binop_single_sound Float32.sub).
+
+Definition mulfs := binop_single Float32.mul.
+
+Lemma mulfs_sound: 
+  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulfs v w) (mulfs x y).
+Proof (binop_single_sound Float32.mul).
+
+Definition divfs := binop_single Float32.div.
+
+Lemma divfs_sound: 
+  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divfs v w) (divfs x y).
+Proof (binop_single_sound Float32.div).
+
 (** Conversions *)
 
 Definition zero_ext (nbits: Z) (v: aval) :=
@@ -1683,23 +1735,38 @@ Qed.
 
 Definition singleoffloat (v: aval) :=
   match v with
-  | F f => F (Float.singleoffloat f)
-  | _   => Fsingle
+  | F f => FS (Float.to_single f)
+  | _   => ftop
   end.
 
 Lemma singleoffloat_sound:
   forall v x, vmatch v x -> vmatch (Val.singleoffloat v) (singleoffloat x).
 Proof.
-  intros. 
-  assert (DEFAULT: vmatch (Val.singleoffloat v) Fsingle).
-  { destruct v; constructor. apply Float.singleoffloat_is_single. }
+  intros.  
+  assert (DEFAULT: vmatch (Val.singleoffloat v) ftop).
+  { destruct v; constructor. }
+  destruct x; auto. inv H. constructor. 
+Qed.
+
+Definition floatofsingle (v: aval) :=
+  match v with
+  | FS f => F (Float.of_single f)
+  | _   => ftop
+  end.
+
+Lemma floatofsingle_sound:
+  forall v x, vmatch v x -> vmatch (Val.floatofsingle v) (floatofsingle x).
+Proof.
+  intros.  
+  assert (DEFAULT: vmatch (Val.floatofsingle v) ftop).
+  { destruct v; constructor. }
   destruct x; auto. inv H. constructor. 
 Qed.
 
 Definition intoffloat (x: aval) :=
   match x with
   | F f =>
-      match Float.intoffloat f with
+      match Float.to_int f with
       | Some i => I i
       | None => if va_strict tt then Vbot else itop
       end
@@ -1710,14 +1777,14 @@ Lemma intoffloat_sound:
   forall v x w, vmatch v x -> Val.intoffloat v = Some w -> vmatch w (intoffloat x).
 Proof.
   unfold Val.intoffloat; intros. destruct v; try discriminate. 
-  destruct (Float.intoffloat f) as [i|] eqn:E; simpl in H0; inv H0.
+  destruct (Float.to_int f) as [i|] eqn:E; simpl in H0; inv H0.
   inv H; simpl; auto with va. rewrite E; constructor. 
 Qed.
 
 Definition intuoffloat (x: aval) :=
   match x with
   | F f =>
-      match Float.intuoffloat f with
+      match Float.to_intu f with
       | Some i => I i
       | None => if va_strict tt then Vbot else itop
       end
@@ -1728,13 +1795,13 @@ Lemma intuoffloat_sound:
   forall v x w, vmatch v x -> Val.intuoffloat v = Some w -> vmatch w (intuoffloat x).
 Proof.
   unfold Val.intuoffloat; intros. destruct v; try discriminate. 
-  destruct (Float.intuoffloat f) as [i|] eqn:E; simpl in H0; inv H0.
+  destruct (Float.to_intu f) as [i|] eqn:E; simpl in H0; inv H0.
   inv H; simpl; auto with va. rewrite E; constructor. 
 Qed.
 
 Definition floatofint (x: aval) :=
   match x with
-  | I i => F(Float.floatofint i)
+  | I i => F(Float.of_int i)
   | _   => ftop
   end.
 
@@ -1747,7 +1814,7 @@ Qed.
 
 Definition floatofintu (x: aval) :=
   match x with
-  | I i => F(Float.floatofintu i)
+  | I i => F(Float.of_intu i)
   | _   => ftop
   end.
 
@@ -1758,6 +1825,68 @@ Proof.
   inv H; simpl; auto with va.
 Qed.
 
+Definition intofsingle (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_int f with
+      | Some i => I i
+      | None => if va_strict tt then Vbot else itop
+      end
+  | _ => itop
+  end.
+
+Lemma intofsingle_sound:
+  forall v x w, vmatch v x -> Val.intofsingle v = Some w -> vmatch w (intofsingle x).
+Proof.
+  unfold Val.intofsingle; intros. destruct v; try discriminate. 
+  destruct (Float32.to_int f) as [i|] eqn:E; simpl in H0; inv H0.
+  inv H; simpl; auto with va. rewrite E; constructor. 
+Qed.
+
+Definition intuofsingle (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_intu f with
+      | Some i => I i
+      | None => if va_strict tt then Vbot else itop
+      end
+  | _ => itop
+  end.
+
+Lemma intuofsingle_sound:
+  forall v x w, vmatch v x -> Val.intuofsingle v = Some w -> vmatch w (intuofsingle x).
+Proof.
+  unfold Val.intuofsingle; intros. destruct v; try discriminate. 
+  destruct (Float32.to_intu f) as [i|] eqn:E; simpl in H0; inv H0.
+  inv H; simpl; auto with va. rewrite E; constructor. 
+Qed.
+
+Definition singleofint (x: aval) :=
+  match x with
+  | I i => FS(Float32.of_int i)
+  | _   => ftop
+  end.
+
+Lemma singleofint_sound:
+  forall v x w, vmatch v x -> Val.singleofint v = Some w -> vmatch w (singleofint x).
+Proof.
+  unfold Val.singleofint; intros. destruct v; inv H0.
+  inv H; simpl; auto with va.
+Qed.
+
+Definition singleofintu (x: aval) :=
+  match x with
+  | I i => FS(Float32.of_intu i)
+  | _   => ftop
+  end.
+
+Lemma singleofintu_sound:
+  forall v x w, vmatch v x -> Val.singleofintu v = Some w -> vmatch w (singleofintu x).
+Proof.
+  unfold Val.singleofintu; intros. destruct v; inv H0.
+  inv H; simpl; auto with va.
+Qed.
+
 Definition floatofwords (x y: aval) :=
   match x, y with
   | I i, I j => F(Float.from_words i j)
@@ -1862,6 +1991,18 @@ Proof.
   intros. inv H; try constructor; inv H0; constructor. 
 Qed.
 
+Definition cmpfs_bool (c: comparison) (v w: aval) : abool :=
+  match v, w with
+  | FS f1, FS f2 => Just (Float32.cmp c f1 f2)
+  | _, _ => Btop
+  end.
+
+Lemma cmpfs_bool_sound:
+  forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpfs_bool c v w) (cmpfs_bool c x y).
+Proof.
+  intros. inv H; try constructor; inv H0; constructor. 
+Qed.
+
 Definition maskzero (x: aval) (mask: int) : abool :=
   match x with
   | I i => Just (Int.eq (Int.and i mask) Int.zero)
@@ -1939,9 +2080,10 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) :=
   | Mint16unsigned, _ => Uns 16
   | Mint32, (I _ | Ptr _ | Ifptr _) => v
   | Mint64, L _ => v
-  | Mfloat32, F f => F (Float.singleoffloat f)
-  | Mfloat32, _ => Fsingle
+  | Mfloat32, FS f => v
   | Mfloat64, F f => v
+  | Many32, (I _ | Ptr _ | Ifptr _ | FS _) => v
+  | Many64, _ => v
   | _, _ => Ifptr Pbot
   end.
 
@@ -1963,12 +2105,10 @@ Proof.
 - constructor. omega. apply is_zero_ext_uns; auto with va.
 - constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
 - constructor. omega. apply is_zero_ext_uns; auto with va.
-- constructor. apply Float.singleoffloat_is_single.
 - constructor. omega. apply is_sign_ext_sgn; auto with va.
 - constructor. omega. apply is_zero_ext_uns; auto with va.
 - constructor. omega. apply is_sign_ext_sgn; auto with va.
 - constructor. omega. apply is_zero_ext_uns; auto with va.
-- constructor. apply Float.singleoffloat_is_single.
 Qed.
 
 Lemma vnormalize_cast:
@@ -1992,9 +2132,13 @@ Proof.
 - (* int64 *)
   destruct v; try contradiction; constructor.
 - (* float32 *)
-  rewrite H2. destruct v; simpl; constructor. apply Float.singleoffloat_is_single. 
+  destruct v; try contradiction; constructor.
 - (* float64 *)
   destruct v; try contradiction; constructor.
+- (* any32 *)
+  auto.
+- (* any64 *)
+  auto.
 Qed.
 
 Lemma vnormalize_monotone:
@@ -2024,12 +2168,10 @@ Proof.
 - constructor; auto with va. apply is_zero_ext_uns; auto with va.
 - destruct (zlt n2 8); constructor; auto with va.
 - destruct (zlt n2 16); constructor; auto with va.
-- constructor. apply Float.singleoffloat_is_single.
 - constructor; auto with va. apply is_sign_ext_sgn; auto with va.
 - constructor; auto with va. apply is_zero_ext_uns; auto with va.
 - constructor; auto with va. apply is_sign_ext_sgn; auto with va.
 - constructor; auto with va. apply is_zero_ext_uns; auto with va.
-- constructor. apply Float.singleoffloat_is_single.
 - destruct (zlt n 8); constructor; auto with va.
 - destruct (zlt n 16); constructor; auto with va.
 Qed.
@@ -2064,6 +2206,8 @@ Definition chunk_compat (chunk chunk': memory_chunk) : bool :=
   | Mfloat32, Mfloat32 => true
   | Mint64, Mint64 => true
   | Mfloat64, Mfloat64 => true
+  | Many32, Many32 => true
+  | Many64, Many64 => true
   | _, _ => false
   end.
 
@@ -2148,7 +2292,7 @@ Definition ablock_storebytes_anywhere (ab: ablock) (p: aptr) :=
 
 Definition smatch (m: mem) (b: block) (p: aptr) : Prop :=
   (forall chunk ofs v, Mem.load chunk m b ofs = Some v -> vmatch v (Ifptr p))
-/\(forall ofs b' ofs' i, Mem.loadbytes m b ofs 1 = Some (Pointer b' ofs' i :: nil) -> pmatch b' ofs' p).
+/\(forall ofs b' ofs' q i, Mem.loadbytes m b ofs 1 = Some (Fragment (Vptr b' ofs') q i :: nil) -> pmatch b' ofs' p).
 
 Remark loadbytes_load_ext:
   forall b m m',
@@ -2219,10 +2363,10 @@ Proof.
 Qed.
 
 Lemma smatch_loadbytes:
-  forall m b p b' ofs' i n ofs bytes,
+  forall m b p b' ofs' q i n ofs bytes,
   Mem.loadbytes m b ofs n = Some bytes ->
   smatch m b p ->
-  In (Pointer b' ofs' i) bytes ->
+  In (Fragment (Vptr b' ofs') q i) bytes ->
   pmatch b' ofs' p.
 Proof.
   intros. exploit In_loadbytes; eauto. intros (ofs1 & A & B).
@@ -2251,11 +2395,11 @@ Proof.
 Qed.
 
 Lemma storebytes_provenance:
-  forall m b ofs bytes m' b' ofs' b'' ofs'' i,
+  forall m b ofs bytes m' b' ofs' b'' ofs'' q i,
   Mem.storebytes m b ofs bytes = Some m' ->
-  Mem.loadbytes m' b' ofs' 1 = Some (Pointer b'' ofs'' i :: nil) ->
-  In (Pointer b'' ofs'' i) bytes
-  \/ Mem.loadbytes m b' ofs' 1 = Some (Pointer b'' ofs'' i :: nil).
+  Mem.loadbytes m' b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil) ->
+  In (Fragment (Vptr b'' ofs'') q i) bytes
+  \/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil).
 Proof.
   intros. 
   assert (EITHER:
@@ -2275,26 +2419,24 @@ Proof.
 Qed.
 
 Lemma store_provenance:
-  forall chunk m b ofs v m' b' ofs' b'' ofs'' i,
+  forall chunk m b ofs v m' b' ofs' b'' ofs'' q i,
   Mem.store chunk m b ofs v = Some m' ->
-  Mem.loadbytes m' b' ofs' 1 = Some (Pointer b'' ofs'' i :: nil) ->
-  v = Vptr b'' ofs'' /\ chunk = Mint32
-  \/ Mem.loadbytes m b' ofs' 1 = Some (Pointer b'' ofs'' i :: nil).
+  Mem.loadbytes m' b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil) ->
+  v = Vptr b'' ofs'' /\ (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64)
+  \/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil).
 Proof.
   intros. exploit storebytes_provenance; eauto. eapply Mem.store_storebytes; eauto. 
   intros [A|A]; auto. left.
-  assert (IN_ENC_BYTES: forall bl, ~In (Pointer b'' ofs'' i) (inj_bytes bl)).
-  {
-    induction bl; simpl. tauto. red; intros; elim IHbl. destruct H1. congruence. auto. 
-  }
-  assert (IN_REP_UNDEF: forall n, ~In (Pointer b'' ofs'' i) (list_repeat n Undef)).
-  {
-    intros; red; intros. exploit in_list_repeat; eauto. congruence.
-  }
-  unfold encode_val in A; destruct chunk, v;
-  try (eelim IN_ENC_BYTES; eassumption);
-  try (eelim IN_REP_UNDEF; eassumption).
-  simpl in A. split; auto. intuition congruence.
+  generalize (encode_val_shape chunk v). intros ENC; inv ENC.
+- split; auto. rewrite <- H1 in A; destruct A.
+  + congruence.
+  + exploit H5; eauto. intros (j & P & Q); congruence.
+- rewrite <- H1 in A; destruct A. 
+  + congruence.
+  + exploit H3; eauto. intros [byte P]; congruence. 
+- rewrite <- H1 in A; destruct A.
+  + congruence.
+  + exploit H2; eauto. congruence.
 Qed.
 
 Lemma smatch_store:
@@ -2307,7 +2449,7 @@ Proof.
   intros. destruct H0 as [A B]. split.
 - intros chunk' ofs' v' LOAD. destruct v'; auto with va.
   exploit Mem.load_pointer_store; eauto. 
-  intros [(P & Q & R & S & T) | DISJ]. 
+  intros [(P & Q & R & S) | DISJ]. 
 + subst. apply vmatch_vplub_l. auto.
 + apply vmatch_vplub_r. apply A with (chunk := chunk') (ofs := ofs').
   rewrite <- LOAD. symmetry. eapply Mem.load_store_other; eauto.
@@ -2325,17 +2467,20 @@ Lemma smatch_storebytes:
   forall m b ofs bytes m' b' p p',
   Mem.storebytes m b ofs bytes = Some m' ->
   smatch m b' p ->
-  (forall b' ofs' i, In (Pointer b' ofs' i) bytes -> pmatch b' ofs' p') ->
+  (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p') ->
   smatch m' b' (plub p' p).
 Proof.
   intros. destruct H0 as [A B]. split.
 - intros. apply vmatch_ifptr. intros bx ofsx EQ; subst v. 
   exploit Mem.load_loadbytes; eauto. intros (bytes' & P & Q).
-  exploit decode_val_pointer_inv; eauto. intros [U V]. 
-  subst chunk bytes'. 
-  exploit In_loadbytes; eauto.
-  instantiate (1 := Pointer bx ofsx 3%nat). simpl; auto.
-  intros (ofs' & X & Y).
+  destruct bytes' as [ | byte1' bytes']. 
+  exploit Mem.loadbytes_length; eauto. intros. destruct chunk; discriminate.
+  generalize (decode_val_shape chunk byte1' bytes'). rewrite <- Q. 
+  intros DEC; inv DEC; try contradiction.
+  assert (v = Vptr bx ofsx).
+  { destruct H5 as [E|[E|E]]; rewrite E in H4; destruct v; simpl in H4; congruence. }
+  exploit In_loadbytes; eauto. eauto with coqlib. 
+  intros (ofs' & X & Y). subst v. 
   exploit storebytes_provenance; eauto. intros [Z | Z].
   apply pmatch_lub_l. eauto. 
   apply pmatch_lub_r. eauto. 
@@ -2530,10 +2675,10 @@ Proof.
 Qed.
 
 Lemma ablock_loadbytes_sound:
-  forall m b ab b' ofs' i n ofs bytes,
+  forall m b ab b' ofs' q i n ofs bytes,
   Mem.loadbytes m b ofs n = Some bytes ->
   bmatch m b ab ->
-  In (Pointer b' ofs' i) bytes ->
+  In (Fragment (Vptr b' ofs') q i) bytes ->
   pmatch b' ofs' (ablock_loadbytes ab).
 Proof.
   intros. destruct H0. eapply smatch_loadbytes; eauto. 
@@ -2542,7 +2687,7 @@ Qed.
 Lemma ablock_storebytes_anywhere_sound:
   forall m b ofs bytes p m' b' ab,
   Mem.storebytes m b ofs bytes = Some m' ->
-  (forall b' ofs' i, In (Pointer b' ofs' i) bytes -> pmatch b' ofs' p) ->
+  (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p) ->
   bmatch m b' ab ->
   bmatch m' b' (ablock_storebytes_anywhere ab p).
 Proof.
@@ -2566,7 +2711,7 @@ Lemma ablock_storebytes_sound:
   forall m b ofs bytes m' p ab sz,
   Mem.storebytes m b ofs bytes = Some m' ->
   length bytes = nat_of_Z sz ->
-  (forall b' ofs' i, In (Pointer b' ofs' i) bytes -> pmatch b' ofs' p) ->
+  (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p) ->
   bmatch m b ab ->
   bmatch m' b (ablock_storebytes ab p ofs sz).
 Proof.
@@ -3060,7 +3205,7 @@ Theorem loadbytes_sound:
   romatch m rm ->
   mmatch m am ->
   pmatch b ofs p ->
-  forall  b' ofs' i, In (Pointer b' ofs' i) bytes -> pmatch b' ofs' (loadbytes am rm p).
+  forall  b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' (loadbytes am rm p).
 Proof.
   intros. unfold loadbytes; inv H2.
 - (* Gl id ofs *)
@@ -3093,7 +3238,7 @@ Theorem storebytes_sound:
   mmatch m am ->
   pmatch b ofs p ->
   length bytes = nat_of_Z sz ->
-  (forall b' ofs' i, In (Pointer b' ofs' i) bytes -> pmatch b' ofs' q) ->
+  (forall b' ofs' qt i, In (Fragment (Vptr b' ofs') qt i) bytes -> pmatch b' ofs' q) ->
   mmatch m' (storebytes am p sz q).
 Proof.
   intros until q; intros STORE MM PM LENGTH BYTES.
@@ -3403,7 +3548,7 @@ Proof.
     unfold Mem.loadbytes. rewrite pred_dec_true. reflexivity. 
     red; intros. replace ofs0 with ofs by omega. auto.
   }
-  destruct mv; econstructor.
+  destruct mv; econstructor. destruct v; econstructor. 
   apply inj_of_bc_valid.
   assert (PM: pmatch bc b i Ptop).
   { exploit mmatch_top; eauto. intros [P Q].
@@ -3456,7 +3601,7 @@ Proof.
     - exploit Mem.load_inject. eauto. eauto. apply inj_of_bc_valid; auto. 
       intros (v' & A & B). eapply vmatch_inj_top; eauto. 
     - exploit Mem.loadbytes_inject. eauto. eauto. apply inj_of_bc_valid; auto. 
-      intros (bytes' & A & B). inv B. inv H4. eapply pmatch_inj_top; eauto. 
+      intros (bytes' & A & B). inv B. inv H4. inv H8. eapply pmatch_inj_top; eauto. 
   }
   constructor; simpl; intros. 
   - apply ablock_init_sound. apply SM. congruence.
@@ -3701,7 +3846,11 @@ Hint Resolve cnot_sound symbol_address_sound
        divs_sound divu_sound mods_sound modu_sound shrx_sound
        negf_sound absf_sound
        addf_sound subf_sound mulf_sound divf_sound
-       zero_ext_sound sign_ext_sound singleoffloat_sound
+       negfs_sound absfs_sound
+       addfs_sound subfs_sound mulfs_sound divfs_sound
+       zero_ext_sound sign_ext_sound singleoffloat_sound floatofsingle_sound
        intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound
+       intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound
        longofwords_sound loword_sound hiword_sound 
-       cmpu_bool_sound cmp_bool_sound cmpf_bool_sound maskzero_sound : va.
+       cmpu_bool_sound cmp_bool_sound cmpf_bool_sound cmpfs_bool_sound
+       maskzero_sound : va.