From 56579f8ade21cb0a880ffbd6d5e28f152e951be8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 6 Apr 2014 07:11:12 +0000 Subject: 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 --- backend/Stackingproof.v | 207 +++++++++++++++++++++--------------------------- 1 file changed, 90 insertions(+), 117 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 9b144cb..b69f1ec 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: forall r, Val.has_type (ls (R r)) (mreg_type r). 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). 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. @@ -1354,7 +1344,8 @@ 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 -> + (forall r, Val.has_type (ls (R r)) (mreg_type r)) -> frame_perm_freeable m sp -> exists rs', exists m', star step tge @@ -1480,7 +1471,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 -> + (forall r, Val.has_type (ls (R r)) (mreg_type r)) -> 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 +1531,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. + intros. apply undef_regs_type. simpl. apply WTREGS. eexact PERM4. rewrite <- LS1. intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. @@ -1622,8 +1613,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 +1855,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 +2043,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 +2435,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 +2446,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 +2454,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 +2461,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 +2515,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 +2523,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 +2582,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 +2599,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 +2621,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 +2637,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 +2652,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 +2680,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 +2703,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 +2761,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_regs; 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 +2787,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 +2804,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 +2836,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 +2849,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. -- cgit v1.2.3