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 machine registers that contain
  a single-precision float.
- Stackingproof: adapted accordingly.

This addresses a defect report by D. Dickman whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats.



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

1 files changed, 89 insertions, 117 deletions

diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 9b144cb..cea2e0b 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -664,17 +664,12 @@ Record agree_frame (j: meminj) (ls ls0: locset)
 
     (** Permissions on the frame part of the Mach stack block *)
     agree_perm:
-      frame_perm_freeable m' sp';
-
-    (** Current locset is well-typed *)
-    agree_wt_ls:
-      wt_locset ls
+      frame_perm_freeable m' sp'
   }.
 
 Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming
              agree_link agree_retaddr agree_saved_int agree_saved_float
-             agree_valid_linear agree_valid_mach agree_perm
-             agree_wt_ls: stacking.
+             agree_valid_linear agree_valid_mach agree_perm: stacking.
 
 (** Auxiliary predicate used at call points *)
 
@@ -793,19 +788,16 @@ Lemma agree_frame_set_reg:
   forall j ls ls0 m sp m' sp' parent ra r v,
   agree_frame j ls ls0 m sp m' sp' parent ra ->
   mreg_within_bounds b r ->
-   Val.has_type v (Loc.type (R r)) ->
   agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. inv H; constructor; auto; intros.
   rewrite Locmap.gso. auto. red. intuition congruence.
-  apply wt_setreg; auto.
 Qed.
 
 Lemma agree_frame_set_regs:
   forall j ls0 m sp m' sp' parent ra rl vl ls,
   agree_frame j ls ls0 m sp m' sp' parent ra ->
   (forall r, In r rl -> mreg_within_bounds b r) ->
-  Val.has_type_list vl (map Loc.type (map R rl)) ->
   agree_frame j (Locmap.setlist (map R rl) vl ls) ls0 m sp m' sp' parent ra.
 Proof.
   induction rl; destruct vl; simpl; intros; intuition.
@@ -821,7 +813,7 @@ Lemma agree_frame_undef_regs:
 Proof.
   induction regs; simpl; intros.
   auto.
-  apply agree_frame_set_reg; auto. red; auto.
+  apply agree_frame_set_reg; auto.
 Qed.
 
 Lemma caller_save_reg_within_bounds:
@@ -852,17 +844,18 @@ 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 H3.
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H4.
   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.
@@ -883,8 +876,6 @@ Proof.
   eauto with mem.
 (* perm *)
   red; intros. eapply Mem.perm_store_1; eauto.
-(* wt *)
-  apply wt_setstack; auto. 
 Qed.
 
 (** Preservation by assignment to outgoing slot *)
@@ -893,19 +884,20 @@ 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 H3.
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H4.
   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. 
@@ -923,8 +915,6 @@ Proof.
   eauto with mem stacking.
 (* perm *)
   red; intros. eapply Mem.perm_store_1; eauto.
-(* wt *)
-  apply wt_setstack; auto. 
 Qed.
 
 (** General invariance property with respect to memory changes. *)
@@ -1051,7 +1041,6 @@ Lemma agree_frame_return:
   forall j ls ls0 m sp m' sp' parent retaddr ls',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   agree_callee_save ls' ls ->
-  wt_locset ls' ->
   agree_frame j ls' ls0 m sp m' sp' parent retaddr.
 Proof.
   intros. red in H0. inv H; constructor; auto; intros.
@@ -1247,7 +1236,7 @@ Hypothesis csregs_typ:
 Hypothesis ls_temp_undef:
   forall r, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef.
 
-Hypothesis wt_ls: wt_locset ls.
+Hypothesis wt_ls: wt_locset Regset.empty ls.
 
 Lemma save_callee_save_regs_correct:
   forall l k rs m,
@@ -1304,7 +1293,8 @@ Proof.
   simpl in H3. destruct (mreg_eq a r). subst r.
   assert (index_contains_inj j m1 sp (mkindex (number a)) (ls (R a))).
     eapply gss_index_contains_inj; eauto.
-    rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. auto with coqlib.
+    rewrite mkindex_typ. rewrite <- (csregs_typ a). eapply wt_mreg; eauto. 
+    auto with coqlib.
   destruct H5 as [v' [P Q]].
   exists v'; split; auto. apply C; auto. 
   intros. apply mkindex_inj. apply number_inj; auto with coqlib. 
@@ -1354,7 +1344,7 @@ Qed.
 Lemma save_callee_save_correct:
   forall j ls0 rs sp cs fb k m,
   let ls := LTL.undef_regs destroyed_at_function_entry ls0 in
-  agree_regs j ls rs -> wt_locset ls ->
+  agree_regs j ls rs -> wt_locset Regset.empty ls ->
   frame_perm_freeable m sp ->
   exists rs', exists m',
     star step tge 
@@ -1480,7 +1470,7 @@ Lemma function_prologue_correct:
   forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k,
   agree_regs j ls rs ->
   agree_callee_save ls ls0 ->
-  wt_locset ls ->
+  wt_locset Regset.empty ls ->
   ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) ->
   rs1 = undef_regs destroyed_at_function_entry rs ->
   Mem.inject j m1 m1' ->
@@ -1540,7 +1530,7 @@ Proof.
     instantiate (1 := rs1). instantiate (1 := call_regs ls). instantiate (1 := j').
     subst rs1. apply agree_regs_undef_regs. 
     apply agree_regs_call_regs. eapply agree_regs_inject_incr; eauto.
-    apply wt_undef_regs. apply wt_call_regs. auto.
+    apply wt_undef_regs. eapply wt_call_regs. eauto.
     eexact PERM4.
   rewrite <- LS1.
   intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]].
@@ -1622,8 +1612,6 @@ Proof.
     exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto.
     (* perms *)
     auto.
-    (* wt *)
-    rewrite LS1. apply wt_undef_regs. apply wt_call_regs; auto.
   (* incr *)
   split. auto.
   (* separated *)
@@ -1866,7 +1854,6 @@ Inductive match_stacks (j: meminj) (m m': mem):
       match_stacks j m m' nil nil sg bound bound'
   | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf
         (TAIL: is_tail c (Linear.fn_code f))
-        (WTF: wt_function f = true)
         (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf))
         (TRF: transf_function f = OK trf)
         (TRC: transl_code (make_env (function_bounds f)) c = c')
@@ -2055,16 +2042,6 @@ Qed.
 
 (** Typing properties of [match_stacks]. *)
 
-Lemma match_stacks_wt_locset:
-  forall j m m' cs cs' sg bound bound',
-  match_stacks j m m' cs cs' sg bound bound' ->
-  wt_locset (parent_locset cs).
-Proof.
-  induction 1; simpl.
-  unfold Locmap.init; red; intros; red; auto.
-  inv FRM; auto.
-Qed.
-
 Lemma match_stacks_type_sp:
   forall j m m' cs cs' sg bound bound',
   match_stacks j m m' cs cs' sg bound bound' ->
@@ -2457,7 +2434,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
         (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp')
         (TRANSL: transf_function f = OK tf)
         (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf))
-        (WTF: wt_function f = true)
         (AGREGS: agree_regs j ls rs)
         (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
         (TAIL: is_tail c (Linear.fn_code f)),
@@ -2469,7 +2445,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
         (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m'))
         (TRANSL: transf_fundef f = OK tf)
         (FIND: Genv.find_funct_ptr tge fb = Some tf)
-        (WTLS: wt_locset ls)
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Callstate cs f ls m)
@@ -2478,7 +2453,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
       forall cs ls m cs' rs m' j sg 
         (MINJ: Mem.inject j m m')
         (STACKS: match_stacks j m m' cs cs' sg (Mem.nextblock m) (Mem.nextblock m'))
-        (WTLS: wt_locset ls)
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Returnstate cs ls m)
@@ -2486,37 +2460,40 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
 
 Theorem transf_step_correct:
   forall s1 t s2, Linear.step ge s1 t s2 ->
-  forall s1' (MS: match_states s1 s1'),
+  forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'),
   exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
+(*
   assert (USEWTF: forall f i c,
           wt_function f = true -> is_tail (i :: c) (Linear.fn_code f) ->
           wt_instr f i = true).
     intros. unfold wt_function, wt_code in H. rewrite forallb_forall in H.
     apply H. eapply is_tail_in; eauto. 
+*)
   induction 1; intros;
   try inv MS;
   try rewrite transl_code_eq;
-  try (generalize (USEWTF _ _ _ WTF TAIL); intro WTI; simpl in WTI; InvBooleans);
   try (generalize (function_is_within_bounds f _ (is_tail_in TAIL));
        intro BOUND; simpl in BOUND);
   unfold transl_instr.
 
-  (* Lgetstack *)
-  destruct BOUND. unfold destroyed_by_getstack; destruct sl.
-  (* Lgetstack, local *)
+- (* Lgetstack *)
+  destruct BOUND.
+  exploit wt_state_getstack; eauto. intros SV.
+  unfold destroyed_by_getstack; destruct sl.
++ (* Lgetstack, local *)
   exploit agree_locals; eauto. intros [v [A B]].
   econstructor; split.
   apply plus_one. apply exec_Mgetstack. 
   eapply index_contains_load_stack; eauto.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
-  apply agree_frame_set_reg; auto. simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto.
-  (* Lgetstack, incoming *)
-  unfold slot_valid in H0. InvBooleans.
+  apply agree_frame_set_reg; auto.
++ (* Lgetstack, incoming *)
+  unfold slot_valid in SV. InvBooleans.
   exploit incoming_slot_in_parameters; eauto. intros IN_ARGS.
   inversion STACKS; clear STACKS.
-  elim (H7 _ IN_ARGS).
+  elim (H6 _ IN_ARGS).
   subst bound bound' s cs'.
   exploit agree_outgoing. eexact FRM. eapply ARGS; eauto.
   exploit loc_arguments_acceptable; eauto. intros [A B].
@@ -2537,8 +2514,7 @@ Proof.
   eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. 
   apply caller_save_reg_within_bounds. 
   apply temp_for_parent_frame_caller_save.
-  simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto.
-  (* Lgetstack, outgoing *)
++ (* Lgetstack, outgoing *)
   exploit agree_outgoing; eauto. intros [v [A B]].
   econstructor; split.
   apply plus_one. apply exec_Mgetstack. 
@@ -2546,66 +2522,55 @@ Proof.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
   apply agree_frame_set_reg; auto.
-  simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto.
 
-  (* Lsetstack *)
+- (* Lsetstack *)
+  exploit wt_state_setstack; eauto. intros (VTY & SV & SW). 
   set (idx := match sl with
               | Local => FI_local ofs ty
               | Incoming => FI_link (*dummy*)
               | Outgoing => FI_arg ofs ty
               end).
   assert (index_valid f idx).
-    unfold idx; destruct sl.
+  { unfold idx; destruct sl.
     apply index_local_valid; auto.
     red; auto.
-    apply index_arg_valid; auto.
+    apply index_arg_valid; auto. }
   exploit store_index_succeeds; eauto. eapply agree_perm; eauto.
   instantiate (1 := rs0 src). intros [m1' STORE].
   econstructor; split.
-  apply plus_one. destruct sl; simpl in H0.
+  apply plus_one. destruct sl; simpl in SW.
     econstructor. eapply store_stack_succeeds with (idx := idx); eauto. eauto.
     discriminate.
     econstructor. eapply store_stack_succeeds with (idx := idx); eauto. auto. 
   econstructor. 
   eapply Mem.store_outside_inject; eauto. 
     intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta.
-    rewrite size_type_chunk in H4.
+    rewrite size_type_chunk in H2.
     exploit offset_of_index_disj_stack_data_2; eauto.
     exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. 
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
-  eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. 
+  eauto with mem. eauto with mem. intros. rewrite <- H1; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. 
   eauto. eauto. auto. 
   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. apply AGREGS. 
-    assumption. 
-    simpl in H0; discriminate.
-    eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto.
-    apply destroyed_by_setstack_caller_save. auto. auto. apply AGREGS.
+  + eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto.
+    apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS. 
     assumption. 
-  eauto with coqlib.
+  + 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.
+    assumption.
+  + eauto with coqlib.
 
-  (* Lop *)
-  assert (Val.has_type v (mreg_type res)).
-    destruct (is_move_operation op args) as [arg|] eqn:?.
-    exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst op args. 
-    eapply Val.has_subtype; eauto. simpl in H; inv H. eapply agree_wt_ls; eauto. 
-    destruct (type_of_operation op) as [targs tres] eqn:TYOP. 
-    eapply Val.has_subtype; eauto. 
-    replace tres with (snd (type_of_operation op)).
-    eapply type_of_operation_sound; eauto.
-    red; intros. subst op. simpl in Heqo.
-    destruct args; simpl in H. discriminate. destruct args. discriminate. simpl in H. discriminate.
-    rewrite TYOP; auto. 
+- (* Lop *)
   assert (exists v',
           eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
        /\ val_inject j v v').
   eapply eval_operation_inject; eauto.
   eapply match_stacks_preserves_globals; eauto.
   eapply agree_inj; eauto. eapply agree_reglist; eauto.
-  destruct H1 as [v' [A B]].
+  destruct H0 as [v' [A B]].
   econstructor; split. 
   apply plus_one. econstructor. 
   instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved. 
@@ -2616,7 +2581,7 @@ Proof.
   apply agree_frame_set_reg; auto. apply agree_frame_undef_locs; auto.
   apply destroyed_by_op_caller_save.
 
-  (* Lload *)
+- (* Lload *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
        /\ val_inject j a a').
@@ -2633,9 +2598,8 @@ Proof.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. 
   apply agree_frame_set_reg. apply agree_frame_undef_locs; auto.
   apply destroyed_by_load_caller_save. auto. 
-  simpl. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
 
-  (* Lstore *)
+- (* Lstore *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
        /\ val_inject j a a').
@@ -2656,7 +2620,7 @@ Proof.
   eapply agree_frame_parallel_stores; eauto.
   apply destroyed_by_store_caller_save. 
 
-  (* Lcall *)
+- (* Lcall *)
   exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
   exploit is_tail_transf_function; eauto. intros IST.
   rewrite transl_code_eq in IST. simpl in IST.
@@ -2672,10 +2636,9 @@ Proof.
     apply loc_arguments_bounded; auto.
   eapply agree_valid_linear; eauto.
   eapply agree_valid_mach; eauto.
-  eapply agree_wt_ls; eauto. 
   simpl; red; auto.
 
-  (* Ltailcall *)
+- (* Ltailcall *)
   exploit function_epilogue_correct; eauto.
   intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]].
   exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
@@ -2688,14 +2651,13 @@ Proof.
   apply match_stacks_change_mach_mem with m'0.
   auto. 
   eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. 
-  intros. rewrite <- H3. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. 
+  intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. 
   eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
   apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
-  apply zero_size_arguments_tailcall_possible; auto. 
-  apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
+  apply zero_size_arguments_tailcall_possible. eapply wt_state_tailcall; eauto. 
 
-  (* Lbuiltin *)
+- (* Lbuiltin *)
   exploit external_call_mem_inject'; eauto. 
     eapply match_stacks_preserves_globals; eauto.
     eapply agree_reglist; eauto. 
@@ -2717,12 +2679,9 @@ Proof.
   intros. inv H; eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto.
   eapply external_call_valid_block'; eauto.
   eapply agree_valid_mach; eauto.
-  simpl. rewrite list_map_compose.
-  change (fun x => Loc.type (R x)) with mreg_type.
-  eapply Val.has_subtype_list; eauto. eapply external_call_well_typed'; eauto.
 
-  (* Lannot *)
-  exploit transl_annot_params_correct; eauto.
+- (* Lannot *)
+  exploit transl_annot_params_correct; eauto. eapply wt_state_annot; eauto.
   intros [vargs' [P Q]]. 
   exploit external_call_mem_inject'; eauto. 
     eapply match_stacks_preserves_globals; eauto.
@@ -2743,49 +2702,49 @@ Proof.
   eapply external_call_valid_block'; eauto.
   eapply agree_valid_mach; eauto.
 
-  (* Llabel *)
+- (* Llabel *)
   econstructor; split.
   apply plus_one; apply exec_Mlabel.
   econstructor; eauto with coqlib.
 
-  (* Lgoto *)
+- (* Lgoto *)
   econstructor; split.
   apply plus_one; eapply exec_Mgoto; eauto.
   apply transl_find_label; eauto.
   econstructor; eauto. 
   eapply find_label_tail; eauto.
 
-  (* Lcond, true *)
+- (* Lcond, true *)
   econstructor; split.
   apply plus_one. eapply exec_Mcond_true; eauto.
   eapply eval_condition_inject; eauto. eapply agree_reglist; eauto.
   eapply transl_find_label; eauto.
-  econstructor. eauto. eauto. eauto. eauto. eauto. 
+  econstructor. eauto. eauto. eauto. eauto.
   apply agree_regs_undef_regs; auto. 
   apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. 
   eapply find_label_tail; eauto.
 
-  (* Lcond, false *)
+- (* Lcond, false *)
   econstructor; split.
   apply plus_one. eapply exec_Mcond_false; eauto.
   eapply eval_condition_inject; eauto. eapply agree_reglist; eauto.
-  econstructor. eauto. eauto. eauto. eauto. eauto. 
+  econstructor. eauto. eauto. eauto. eauto.
   apply agree_regs_undef_regs; auto. 
   apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. 
   eauto with coqlib.
 
-  (* Ljumptable *)
+- (* Ljumptable *)
   assert (rs0 arg = Vint n).
-    generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto.
+  { generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto. }
   econstructor; split.
   apply plus_one; eapply exec_Mjumptable; eauto. 
   apply transl_find_label; eauto.
-  econstructor. eauto. eauto. eauto. eauto. eauto.
+  econstructor. eauto. eauto. eauto. eauto.
   apply agree_regs_undef_regs; auto.
   apply agree_frame_undef_locs; auto. apply destroyed_by_jumptable_caller_save.
   eapply find_label_tail; eauto.
 
-  (* Lreturn *)
+- (* Lreturn *)
   exploit function_epilogue_correct; eauto.
   intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]].
   econstructor; split.
@@ -2801,13 +2760,12 @@ Proof.
   eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
   apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
-  apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
-  (* internal function *)
+- (* internal function *)
   revert TRANSL. unfold transf_fundef, transf_partial_fundef.
   caseEq (transf_function f); simpl; try congruence.
   intros tfn TRANSL EQ. inversion EQ; clear EQ; subst tf.
-  exploit function_prologue_correct; eauto.
+  exploit function_prologue_correct; eauto. eapply wt_callstate_wt_locset; eauto.
   eapply match_stacks_type_sp; eauto. 
   eapply match_stacks_type_retaddr; eauto.
   intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]].
@@ -2828,10 +2786,9 @@ Proof.
   intros. eapply stores_in_frame_perm; eauto with mem.
   intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto.
   eapply Mem.load_alloc_unchanged; eauto. red. congruence.
-  eapply transf_function_well_typed; eauto.
   auto with coqlib.
 
-  (* external function *)
+- (* external function *)
   simpl in TRANSL. inversion TRANSL; subst tf.
   exploit transl_external_arguments; eauto. intros [vl [ARGS VINJ]].
   exploit external_call_mem_inject'; eauto. 
@@ -2846,11 +2803,10 @@ Proof.
   inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. 
   eapply external_call_nextblock'; eauto.
   eapply external_call_nextblock'; eauto.
-  inv H0. apply wt_setlist_result. eapply external_call_well_typed; eauto. auto.
   apply agree_regs_set_regs; auto. apply agree_regs_inject_incr with j; auto. 
   apply agree_callee_save_set_result; auto. 
 
-  (* return *)
+- (* return *)
   inv STACKS. simpl in AGLOCS.  
   econstructor; split.
   apply plus_one. apply exec_return. 
@@ -2879,7 +2835,6 @@ Proof.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
   rewrite H3. red; intros. contradiction.
-  apply wt_init.
   unfold Locmap.init. red; intros; auto.
   unfold parent_locset. red; auto.
 Qed.
@@ -2893,14 +2848,31 @@ Proof.
   econstructor; eauto. 
 Qed.
 
+Lemma wt_prog:
+  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
+Proof.
+  intros. exploit transform_partial_program_succeeds; eauto. 
+  intros [tfd TF]. destruct fd; simpl in *. 
+- monadInv TF. unfold transf_function in EQ.
+  destruct (wt_function f). auto. discriminate.  
+- auto.
+Qed.
+
 Theorem transf_program_correct:
   forward_simulation (Linear.semantics prog) (Mach.semantics return_address_offset tprog).
 Proof.
-  eapply forward_simulation_plus.
-  eexact symbols_preserved.
-  eexact transf_initial_states.
-  eexact transf_final_states.
-  eexact transf_step_correct. 
+  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 transf_initial_states; eauto. intros [st2 [A B]]. 
+  exists st2; split; auto. split; auto.
+  apply wt_initial_state with (prog := prog); auto. exact wt_prog. 
+- intros. destruct H. eapply transf_final_states; eauto. 
+- intros. destruct H0. 
+  exploit transf_step_correct; eauto. intros [s2' [A B]].
+  exists s2'; split. exact A. split.
+  eapply step_type_preservation; eauto. eexact wt_prog. eexact H. 
+  auto.
 Qed.
 
 End PRESERVATION.