From f37a87e35850e57febba0a39ce3cb526e7886c10 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 28 Mar 2014 08:08:46 +0000 Subject: Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping): the new Lineartyping can't keep track of single floats that were spilled. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stackingproof.v | 206 +++++++++++++++++++++++++++--------------------- 1 file changed, 117 insertions(+), 89 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index cea2e0b4..9b144cb8 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -664,12 +664,17 @@ 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' + frame_perm_freeable m' sp'; + + (** Current locset is well-typed *) + agree_wt_ls: + wt_locset ls }. 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: stacking. + agree_valid_linear agree_valid_mach agree_perm + agree_wt_ls: stacking. (** Auxiliary predicate used at call points *) @@ -788,16 +793,19 @@ 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. @@ -813,7 +821,7 @@ Lemma agree_frame_undef_regs: Proof. induction regs; simpl; intros. auto. - apply agree_frame_set_reg; auto. + apply agree_frame_set_reg; auto. red; auto. Qed. Lemma caller_save_reg_within_bounds: @@ -844,18 +852,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. @@ -876,6 +883,8 @@ 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 *) @@ -884,20 +893,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. @@ -915,6 +923,8 @@ 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. *) @@ -1041,6 +1051,7 @@ 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. @@ -1236,7 +1247,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 Regset.empty ls. +Hypothesis wt_ls: wt_locset ls. Lemma save_callee_save_regs_correct: forall l k rs m, @@ -1293,8 +1304,7 @@ 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). eapply wt_mreg; eauto. - auto with coqlib. + rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. 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. @@ -1344,7 +1354,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 Regset.empty ls -> + agree_regs j ls rs -> wt_locset ls -> frame_perm_freeable m sp -> exists rs', exists m', star step tge @@ -1470,7 +1480,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 Regset.empty ls -> + wt_locset 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' -> @@ -1530,7 +1540,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. eapply wt_call_regs. eauto. + apply wt_undef_regs. apply wt_call_regs. auto. eexact PERM4. rewrite <- LS1. intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. @@ -1612,6 +1622,8 @@ 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 *) @@ -1854,6 +1866,7 @@ 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') @@ -2042,6 +2055,16 @@ 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' -> @@ -2434,6 +2457,7 @@ 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)), @@ -2445,6 +2469,7 @@ 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) @@ -2453,6 +2478,7 @@ 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) @@ -2460,40 +2486,37 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := Theorem transf_step_correct: forall s1 t s2, Linear.step ge s1 t s2 -> - forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'), + forall 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. - exploit wt_state_getstack; eauto. intros SV. - unfold destroyed_by_getstack; destruct sl. -+ (* Lgetstack, local *) + (* Lgetstack *) + destruct BOUND. 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. -+ (* Lgetstack, incoming *) - unfold slot_valid in SV. InvBooleans. + 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. exploit incoming_slot_in_parameters; eauto. intros IN_ARGS. inversion STACKS; clear STACKS. - elim (H6 _ IN_ARGS). + elim (H7 _ IN_ARGS). subst bound bound' s cs'. exploit agree_outgoing. eexact FRM. eapply ARGS; eauto. exploit loc_arguments_acceptable; eauto. intros [A B]. @@ -2514,7 +2537,8 @@ 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. -+ (* Lgetstack, outgoing *) + simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto. + (* Lgetstack, outgoing *) exploit agree_outgoing; eauto. intros [v [A B]]. econstructor; split. apply plus_one. apply exec_Mgetstack. @@ -2522,55 +2546,66 @@ 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 *) - exploit wt_state_setstack; eauto. intros (VTY & SV & SW). + (* Lsetstack *) 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 SW. + apply plus_one. destruct sl; simpl in H0. 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 H2. + rewrite size_type_chunk in H4. 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 <- H1; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. + eauto with mem. eauto with mem. intros. rewrite <- H3; 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. auto. apply AGREGS. + 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. 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. - assumption. - + eauto with coqlib. + eauto with coqlib. -- (* Lop *) + (* 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. 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 H0 as [v' [A B]]. + destruct H1 as [v' [A B]]. econstructor; split. apply plus_one. econstructor. instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved. @@ -2581,7 +2616,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'). @@ -2598,8 +2633,9 @@ 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'). @@ -2620,7 +2656,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. @@ -2636,9 +2672,10 @@ 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]]]]. @@ -2651,13 +2688,14 @@ 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 <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. + intros. rewrite <- H3. 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. eapply wt_state_tailcall; eauto. + apply zero_size_arguments_tailcall_possible; auto. + apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. -- (* Lbuiltin *) + (* Lbuiltin *) exploit external_call_mem_inject'; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_reglist; eauto. @@ -2679,9 +2717,12 @@ 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. eapply wt_state_annot; eauto. + (* Lannot *) + exploit transl_annot_params_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_inject'; eauto. eapply match_stacks_preserves_globals; eauto. @@ -2702,49 +2743,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. + econstructor. eauto. 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. + econstructor. eauto. 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. + econstructor. eauto. 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. @@ -2760,12 +2801,13 @@ 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. eapply wt_callstate_wt_locset; eauto. + exploit function_prologue_correct; 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]]]]]]]]]]]]]]]]. @@ -2786,9 +2828,10 @@ 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. @@ -2803,10 +2846,11 @@ 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. @@ -2835,6 +2879,7 @@ 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. @@ -2848,31 +2893,14 @@ 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. - 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. + eapply forward_simulation_plus. + eexact symbols_preserved. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. Qed. End PRESERVATION. -- cgit