Merge of branch linear-typing:

1) Revised division of labor between RTLtyping and Lineartyping:
- RTLtyping no longer keeps track of single-precision floats,
  switches from subtype-based inference to unification-based inference.
- Unityping: new library for unification-based inference.
- Locations: don't normalize at assignment in a stack slot
- Allocation, Allocproof: simplify accordingly.
- Lineartyping: add inference of locations that contain
  a single-precision float.
- Stackingproof: adapted accordingly.

This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c).

This corresponds to commits 2435+2436 plus improvements in Lineartyping.

2) Add -dtimings option to measure compilation times.
Moved call to C parser from Elab to Parse, to make it easier to
measure parsing time independently of elaboration time.


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

1 files changed, 116 insertions, 138 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 4c39fee..9303878 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) tyl ->
+  Val.has_type_list (rs##rl) (normalize_list 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.
@@ -648,7 +648,7 @@ Lemma loc_unconstrained_satisf:
 Proof.
   intros; red; intros. 
   destruct (OrderedEquation.eq_dec q (Eq k r l)). 
-  subst q; simpl. unfold l; rewrite Locmap.gss_reg. auto.
+  subst q; simpl. unfold l; rewrite Locmap.gss. auto.
   assert (EqSet.In q (remove_equation (Eq k r l) e)).
     simpl. ESD.fsetdec.  
   rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. 
@@ -674,7 +674,7 @@ Lemma parallel_assignment_satisf:
 Proof.
   intros; red; intros.
   destruct (OrderedEquation.eq_dec q (Eq k r l)).
-  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss_reg; auto.
+  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto.
   assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)).
     simpl. ESD.fsetdec.
   exploit reg_loc_unconstrained_sound; eauto. intros [A B].
@@ -702,11 +702,11 @@ Proof.
   rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl.
   destruct (OrderedEquation.eq_dec q (Eq Low res l2)).
   subst q; simpl. rewrite Regmap.gss.
-  destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg.
+  destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
   apply Val.loword_lessdef; auto. 
   destruct (OrderedEquation.eq_dec q (Eq High res l1)).
   subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto.
-  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg.
+  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
   apply Val.hiword_lessdef; auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. 
   rewrite Regmap.gso. rewrite ! Locmap.gso. auto. 
@@ -719,7 +719,7 @@ Proof.
   set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *.
   destruct (OrderedEquation.eq_dec q (Eq Full res l1)). 
   subst q; simpl. rewrite Regmap.gss.
-  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg.
+  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
   auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. 
   simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto.
@@ -969,6 +969,7 @@ 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 ->
@@ -1008,7 +1009,8 @@ 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' ->
@@ -1016,23 +1018,19 @@ 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.
-  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). 
+  subst dst. rewrite Locmap.gss. apply (H1 _ B).
   rewrite Locmap.gso; auto.
 Qed.
 
@@ -1079,22 +1077,18 @@ Proof.
 Qed.
 
 Lemma subst_loc_undef_satisf:
-  forall env src dst rs ls ml e e',
+  forall 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 *.
-  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). 
+  destruct q as [k r l]; simpl in *. apply (H1 _ B). 
   rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. 
   eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto.
 Qed.
@@ -1336,27 +1330,27 @@ Qed.
 (** * Properties of the dataflow analysis *)
 
 Lemma analyze_successors:
-  forall f env bsh an pc bs s e,
-  analyze f env bsh = Some an ->
+  forall f bsh an pc bs s e,
+  analyze f bsh = Some an ->
   bsh!pc = Some bs ->
   In s (successors_block_shape bs) ->
   an!!pc = OK e ->
-  exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e.
+  exists e', transfer f 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 env bsh s an#s); intros.
+  rewrite H2. unfold DS.L.ge. destruct (transfer f bsh s an#s); intros.
   exists e0; auto. 
   contradiction.
 Qed.
 
 Lemma satisf_successors:
-  forall f env bsh an pc bs s e rs ls,
-  analyze f env bsh = Some an ->
+  forall f bsh an pc bs s e rs ls,
+  analyze f 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 env bsh s an!!s = OK e' /\ satisf rs ls e'.
+  exists e', transfer f 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.
@@ -1366,13 +1360,12 @@ Qed.
 
 Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop :=
   | transf_function_spec_intro:  
-      forall env an mv k e1 e2,
-      wt_function f env ->
-      analyze f env (pair_codes f tf) = Some an ->
+      forall an mv k e1 e2,
+      analyze f (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 env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
-      track_moves env mv e1 = Some e2 ->
+      transfer f (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
+      track_moves 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 ->
@@ -1387,36 +1380,33 @@ 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 env) as [] eqn:?; inv H.
+  destruct (check_function f f0) as [] eqn:?; inv H.
   unfold check_function in Heqr. 
-  destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate.
+  destruct (analyze f (pair_codes f tf)) as [an|] eqn:?; try discriminate.
   monadInv Heqr. 
-  destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate.
+  destruct (check_entrypoints_aux f tf 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. eapply type_function_correct; eauto. congruence. 
+  econstructor; eauto. congruence. 
 Qed.
 
 Lemma invert_code:
-  forall f env tf pc i opte e,
-  wt_function f env ->
+  forall f tf pc i opte e,
   (RTL.fn_code f)!pc = Some i ->
-  transfer f env (pair_codes f tf) pc opte = OK e ->
+  transfer f (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 env bsh eafter = Some e /\
-  wt_instr f env i.
+  transfer_aux f bsh eafter = Some e.
 Proof.
-  intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter.
+  intros. destruct opte as [eafter|]; simpl in H0; 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 env bsh eafter) as [e1|] eqn:?; inv H1. 
-  exists bb. exploit wt_instr_at; eauto.
-  tauto. 
+  destruct (transfer_aux f bsh eafter) as [e1|] eqn:?; inv H0. 
+  exists bb. tauto. 
 Qed.
 
 (** * Semantic preservation *)
@@ -1490,11 +1480,10 @@ Proof.
 Qed.
 
 Lemma exec_moves:
-  forall mv env rs s f sp bb m e e' ls,
-  track_moves env mv e = Some e' ->
+  forall mv rs s f sp bb m e e' ls,
+  track_moves 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)
@@ -1506,7 +1495,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 env mv e) as [e1|] eqn:?; MonadInv.
+  destruct (track_moves 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 *)
@@ -1532,17 +1521,13 @@ 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 env
+      forall res f sp pc rs s tf bb ls ts sg an e
         (STACKS: match_stackframes s ts (fn_sig tf))
         (FUN: transf_function f = OK tf)
-        (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: subtype (proj_sig_res sg) (env res) = true)
+        (ANL: analyze f (pair_codes f tf) = Some an)
+        (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e)
         (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)
@@ -1555,15 +1540,13 @@ 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 env
+      forall s f sp pc rs m ts tf ls m' an e
         (STACKS: match_stackframes s ts (fn_sig tf))
         (FUN: transf_function f = OK tf)
-        (ANL: analyze f env (pair_codes f tf) = Some an)
-        (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e)
+        (ANL: analyze f (pair_codes f tf) = Some an)
+        (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e)
         (SAT: satisf rs ls e)
-        (MEM: Mem.extends m m')
-        (WTF: wt_function f env)
-        (WTRS: wt_regset env rs),
+        (MEM: Mem.extends m m'),
       match_states (RTL.State s f sp pc rs m)
                    (LTL.State ts tf sp pc ls m')
   | match_states_call:
@@ -1572,8 +1555,7 @@ 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')
-        (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
+        (MEM: Mem.extends m m'),
       match_states (RTL.Callstate s f args m)
                    (LTL.Callstate ts tf ls m')
   | match_states_return:
@@ -1581,8 +1563,7 @@ 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')
-        (WTRES: Val.has_type res (proj_sig_res sg)),
+        (MEM: Mem.extends m m'),
       match_states (RTL.Returnstate s res m)
                    (LTL.Returnstate ts ls m').
 
@@ -1595,14 +1576,13 @@ 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
-  | [ 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); 
+  | [ CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ = OK _ |- _ ] =>
+      destruct (invert_code _ _ _ _ _ _ CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR); 
       inv EBS; unfold transfer_aux in TR; MonadInv
   end.
 
@@ -1619,10 +1599,8 @@ Proof.
   { generalize args (type_of_addressing addr) H0 H1 H5.
     induction args0; simpl; intros.
     contradiction.
-    destruct l. discriminate. InvBooleans. 
-    destruct H2. subst a. 
-    assert (t = Tint) by auto with coqlib. subst t. 
-    destruct (env r); auto || discriminate. 
+    destruct l. discriminate. inv H4. 
+    destruct H2. subst a. apply H3; auto with coqlib. 
     eauto with coqlib. 
   }
   red; intros; subst r. rewrite H in H8; discriminate.
@@ -1632,11 +1610,11 @@ Qed.
     "plus" kind. *)
 
 Lemma step_simulation:
-  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 ->
   forall S1', match_states S1 S1' ->
   exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'.
 Proof.
-  induction 1; intros S1' MS; inv MS; try UseShape.
+  induction 1; intros WT S1' MS; inv MS; try UseShape.
 
 (* nop *)
   exploit exec_moves; eauto. intros [ls1 [X Y]]. 
@@ -1648,8 +1626,7 @@ Proof.
   econstructor; eauto. 
 
 (* op move *)
-- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
-  simpl in H0. inv H0.  
+- simpl in H0. inv H0.  
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1660,8 +1637,7 @@ Proof.
   econstructor; eauto.
 
 (* op makelong *)
-- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
-  simpl in H0. inv H0. 
+- simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1673,8 +1649,7 @@ Proof.
   econstructor; eauto.
 
 (* op lowlong *)
-- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
-  simpl in H0. inv H0. 
+- simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1686,8 +1661,7 @@ Proof.
   econstructor; eauto.
 
 (* op highlong *)
-- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
-  simpl in H0. inv H0. 
+- simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1699,8 +1673,7 @@ Proof.
   econstructor; eauto.
 
 (* op regular *)
-- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- 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]].
@@ -1724,11 +1697,9 @@ Proof.
   eapply reg_unconstrained_satisf; eauto. 
   intros [enext [U V]]. 
   econstructor; eauto.
-  eapply wt_exec_Iop; eauto. 
 
 (* load regular *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- 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]]. 
@@ -1744,8 +1715,7 @@ Proof.
   econstructor; eauto.
 
 (* load pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
-  exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
   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]]. 
@@ -1766,7 +1736,8 @@ Proof.
   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. 
+    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.
@@ -1798,8 +1769,7 @@ Proof.
   econstructor; eauto.
 
 (* load first word of a pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
-  exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
   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]]. 
@@ -1829,8 +1799,7 @@ Proof.
   econstructor; eauto.
 
 (* load second word of a pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
-  exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
   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]]. 
@@ -1870,7 +1839,6 @@ 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]].
@@ -1950,21 +1918,19 @@ Proof.
   exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]].
   econstructor; eauto.
   econstructor; eauto.
-  inv WTI. rewrite SIG. auto. 
   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.
-  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
+  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
+  inv WTI. rewrite <- H7. apply wt_regset_list; auto. 
   simpl. red; auto.
-  inv WTI. rewrite SIG. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
 
 (* tailcall *)
 - set (sg := RTL.funsig fd) in *.
@@ -1985,16 +1951,16 @@ 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.
-  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
+  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. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
 
 (* builtin *)
-- assert (WTRS': wt_regset env (rs#res <- v)) by (eapply wt_exec_Ibuiltin; eauto).
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit external_call_mem_extends; eauto.
   eapply add_equations_args_lessdef; eauto.
-  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
+  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').
   { unfold reglist. rewrite list_map_compose. auto. }
@@ -2024,7 +1990,8 @@ Proof.
 (* annot *)
 - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. 
   exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto.
-  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
+  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.
   econstructor; split.
@@ -2042,7 +2009,6 @@ 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]].
@@ -2074,45 +2040,43 @@ Proof.
 
 (* return *)
 - destruct (transf_function_inv _ _ FUN). 
-  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.
-  unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto.
-  apply return_regs_agree_callee_save.
-  constructor.
+  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]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto. rewrite <- H11.
+  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.
   apply return_regs_agree_callee_save.
-  unfold proj_sig_res. rewrite <- H11; rewrite H13. 
-  eapply Val.has_subtype; eauto. 
+
+  (* without an argument *)
++ assert (SG: f.(RTL.fn_sig).(sig_res) = None).
+  { exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
+    inv WTI; auto. }
+  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.
+  apply return_regs_agree_callee_save.
 
 (* internal function *)
 - monadInv FUN. simpl in *.
   destruct (transf_function_inv _ _ EQ). 
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. 
+  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H7; apply Zle_refl. 
   intros [m'' [U V]].
-  assert (WTRS: wt_regset env (init_regs args (fn_params f))).
-  { apply wt_init_regs. inv H0. eapply Val.has_subtype_list; eauto. congruence. }
   exploit (exec_moves mv). eauto. eauto.
     eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. 
-    rewrite call_regs_param_values. rewrite H9. eexact ARGS.
-    exact WTRS.
+    rewrite call_regs_param_values. rewrite H8. eexact ARGS.
   intros [ls1 [A B]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -2144,15 +2108,13 @@ 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. eapply Val.has_subtype; eauto. intros [ls2 [A B]].
+  exploit STEPS; eauto. intros [ls2 [A B]].
   econstructor; split.
   eapply plus_left. constructor. eexact A. traceEq.
   econstructor; eauto.
-  apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. 
 Qed.
 
 Lemma initial_states_simulation:
@@ -2173,7 +2135,6 @@ Proof.
   rewrite SIG; rewrite H3; simpl; auto.
   red; auto.
   apply Mem.extends_refl.
-  rewrite SIG; rewrite H3; simpl; auto.
 Qed.
 
 Lemma final_states_simulation:
@@ -2185,14 +2146,31 @@ Proof.
   unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto. 
 Qed.
 
+Lemma wt_prog: wt_program prog.
+Proof.
+  red; intros. exploit transform_partial_program_succeeds; eauto. 
+  intros [tfd TF]. destruct f; simpl in *. 
+- monadInv TF. unfold transf_function in EQ.
+  destruct (type_function f) as [env|] eqn:TF; try discriminate.
+  econstructor. eapply type_function_correct; eauto.
+- constructor.
+Qed.
+
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (LTL.semantics tprog).
 Proof.
-  eapply forward_simulation_plus.
-  eexact symbols_preserved.
-  eexact initial_states_simulation.
-  eexact final_states_simulation.
-  exact step_simulation. 
+  set (ms := fun s s' => wt_state s /\ match_states s s').
+  eapply forward_simulation_plus with (match_states := ms). 
+- exact symbols_preserved.
+- intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. 
+  exists st2; split; auto. split; auto.
+  apply wt_initial_state with (p := prog); auto. exact wt_prog. 
+- intros. destruct H. eapply final_states_simulation; eauto. 
+- intros. destruct H0. 
+  exploit step_simulation; eauto. intros [s2' [A B]].
+  exists s2'; split. exact A. split.
+  eapply subject_reduction; eauto. eexact wt_prog. eexact H. 
+  auto.
 Qed.
 
 End PRESERVATION.