From 5909a0340ad0fe871dede1eaead855fb4b68fb0e Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Aug 2011 06:31:10 +0000 Subject: IA32 port: more faithful treatment of pseudoregister ST0. Related general change: support for destroyed_at_moves. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Linear.v | 9 ++- backend/Lineartyping.v | 19 ++++- backend/Mach.v | 24 +++++- backend/Machsem.v | 2 +- backend/Parallelmove.v | 25 ++++--- backend/Reloadproof.v | 141 ++++++++++++++++++++++------------- backend/Stackingproof.v | 194 +++++++++++++++++++++++++++++++----------------- 7 files changed, 272 insertions(+), 142 deletions(-) (limited to 'backend') diff --git a/backend/Linear.v b/backend/Linear.v index 3553ced..b218531 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -169,8 +169,8 @@ Definition return_regs (caller callee: locset) : locset := Definition undef_op (op: operation) (rs: locset) := match op with - | Omove => rs - | _ => undef_temps rs + | Omove => Locmap.undef destroyed_at_move rs + | _ => Locmap.undef temporaries rs end. Definition undef_getstack (s: slot) (rs: locset) := @@ -179,6 +179,9 @@ Definition undef_getstack (s: slot) (rs: locset) := | _ => rs end. +Definition undef_setstack (rs: locset) := + Locmap.undef destroyed_at_move rs. + (** Linear execution states. *) Inductive stackframe: Type := @@ -261,7 +264,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lsetstack: forall s f sp r sl b rs m, step (State s f sp (Lsetstack r sl :: b) rs m) - E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) rs) m) + E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) (undef_setstack rs)) m) | exec_Lop: forall s f sp op args res b rs m v, eval_operation ge sp op (reglist rs args) m = Some v -> diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 390b630..3930da3 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -153,18 +153,23 @@ Proof. auto. Qed. +Lemma wt_undef_locs: + forall locs ls, wt_locset ls -> wt_locset (Locmap.undef locs ls). +Proof. + induction locs; simpl; intros. auto. apply IHlocs. apply wt_setloc; auto. red; auto. +Qed. + Lemma wt_undef_temps: forall ls, wt_locset ls -> wt_locset (undef_temps ls). Proof. - unfold undef_temps. generalize temporaries. induction l; simpl; intros. - auto. - apply IHl. apply wt_setloc; auto. red; auto. + intros; unfold undef_temps. apply wt_undef_locs; auto. Qed. Lemma wt_undef_op: forall op ls, wt_locset ls -> wt_locset (undef_op op ls). Proof. - intros. generalize (wt_undef_temps ls H); intro. case op; simpl; auto. + intros. generalize (wt_undef_temps ls H); intro. + unfold undef_op; destruct op; auto; apply wt_undef_locs; auto. Qed. Lemma wt_undef_getstack: @@ -173,6 +178,12 @@ Proof. intros. unfold undef_getstack. destruct s; auto. apply wt_setloc; auto. red; auto. Qed. +Lemma wt_undef_setstack: + forall ls, wt_locset ls -> wt_locset (undef_setstack ls). +Proof. + intros. unfold undef_setstack. apply wt_undef_locs; auto. +Qed. + Lemma wt_call_regs: forall ls, wt_locset ls -> wt_locset (call_regs ls). Proof. diff --git a/backend/Mach.v b/backend/Mach.v index 3210a9e..5c9cff5 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -117,15 +117,35 @@ Fixpoint undef_regs (rl: list mreg) (rs: regset) {struct rl} : regset := | r1 :: rl' => undef_regs rl' (Regmap.set r1 Vundef rs) end. +Lemma undef_regs_other: + forall r rl rs, ~In r rl -> undef_regs rl rs r = rs r. +Proof. + induction rl; simpl; intros. auto. rewrite IHrl. apply Regmap.gso. intuition. intuition. +Qed. + +Lemma undef_regs_same: + forall r rl rs, In r rl \/ rs r = Vundef -> undef_regs rl rs r = Vundef. +Proof. + induction rl; simpl; intros. tauto. + destruct H. destruct H. apply IHrl. right. subst; apply Regmap.gss. + auto. + apply IHrl. right. unfold Regmap.set. destruct (RegEq.eq r a); auto. +Qed. + Definition undef_temps (rs: regset) := - undef_regs (int_temporaries ++ float_temporaries) rs. + undef_regs temporary_regs rs. + +Definition undef_move (rs: regset) := + undef_regs destroyed_at_move_regs rs. Definition undef_op (op: operation) (rs: regset) := match op with - | Omove => rs + | Omove => undef_move rs | _ => undef_temps rs end. +Definition undef_setstack (rs: regset) := undef_move rs. + Definition is_label (lbl: label) (instr: instruction) : bool := match instr with | Mlabel lbl' => if peq lbl lbl' then true else false diff --git a/backend/Machsem.v b/backend/Machsem.v index 853e8a7..a802323 100644 --- a/backend/Machsem.v +++ b/backend/Machsem.v @@ -149,7 +149,7 @@ Inductive step: state -> trace -> state -> Prop := forall s f sp src ofs ty c rs m m', store_stack m sp ty ofs (rs src) = Some m' -> step (State s f sp (Msetstack src ofs ty :: c) rs m) - E0 (State s f sp c rs m') + E0 (State s f sp c (undef_setstack rs) m') | exec_Mgetparam: forall s fb f sp ofs ty dst c rs m v, Genv.find_funct_ptr ge fb = Some (Internal f) -> diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index 44eb399..d7a4217 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -238,11 +238,13 @@ Proof. Qed. Lemma source_not_temp1: - forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> Loc.diff s (R IT1) /\ Loc.diff s (R FT1). + forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> + Loc.diff s (R IT1) /\ Loc.diff s (R FT1) /\ Loc.notin s destroyed_at_move. Proof. - intros. elim H; intro. - split; apply NO_SRCS_TEMP; auto; simpl; tauto. - elim H0; intro; subst s; simpl; split; congruence. + intros. destruct H. + exploit Loc.disjoint_notin. eexact NO_SRCS_TEMP. eauto. + simpl; tauto. + destruct H; subst s; simpl; intuition congruence. Qed. Lemma dest_noteq_diff: @@ -265,16 +267,16 @@ Qed. Definition locmap_equiv (e1 e2: Locmap.t): Prop := forall l, - no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> e2 l = e1 l. + no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e2 l = e1 l. (** The following predicates characterize the effect of one move move ([effect_move]) and of a sequence of elementary moves ([effect_seqmove]). We allow the code generated for one move - to use the temporaries [IT1] and [FT1] in any way it needs. *) + to use the temporaries [IT1] and [FT1] and [destroyed_at_move] in any way it needs. *) Definition effect_move (src dst: loc) (e e': Locmap.t): Prop := e' dst = e src /\ - forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> e' l = e l. + forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e' l = e l. Inductive effect_seqmove: list (loc * loc) -> Locmap.t -> Locmap.t -> Prop := | effect_seqmove_nil: forall e, @@ -299,7 +301,7 @@ Lemma effect_move_equiv: Proof. intros. destruct H2. red; intros. unfold Parmov.update. destruct (Loc.eq l d). - subst l. elim (source_not_temp1 _ H); intros. + subst l. destruct (source_not_temp1 _ H) as [A [B C]]. rewrite H2. apply H1; auto. apply source_no_overlap_dests; auto. rewrite H3; auto. apply dest_noteq_diff; auto. Qed. @@ -345,15 +347,16 @@ Proof. generalize (parmove_prop_1 srcs dsts LENGTH NOREPET NO_SRCS_TEMP NO_DSTS_TEMP e). fold mu. intros [A B]. (* e' dsts = e srcs *) - split. rewrite <- A. apply list_map_exten; intros. + split. rewrite <- A. apply list_map_exten; intros. + exploit Loc.disjoint_notin. eexact NO_DSTS_TEMP. eauto. simpl; intros. apply H1. apply dests_no_overlap_dests; auto. - apply NO_DSTS_TEMP; auto; simpl; tauto. - apply NO_DSTS_TEMP; auto; simpl; tauto. + tauto. tauto. simpl; tauto. (* other locations *) intros. transitivity (exec_seq mu e l). symmetry. apply H1. apply notin_dests_no_overlap_dests; auto. eapply Loc.in_notin_diff; eauto. simpl; tauto. eapply Loc.in_notin_diff; eauto. simpl; tauto. + simpl in H3; simpl; tauto. apply B. apply Loc.notin_not_in; auto. apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto. apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index f0a0b97..6ee9263 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -228,16 +228,17 @@ Lemma add_reload_correct: forall l, Loc.diff (R dst) l -> loc_acceptable src \/ Loc.diff (R IT1) l -> + Loc.notin l destroyed_at_move -> rs' l = rs l. Proof. intros. unfold add_reload. destruct src. - case (mreg_eq m0 dst); intro. + destruct (mreg_eq m0 dst). subst dst. exists rs. split. apply star_refl. tauto. - exists (Locmap.set (R dst) (rs (R m0)) rs). - split. apply star_one; apply exec_Lop. reflexivity. - split. apply Locmap.gss. - intros; apply Locmap.gso; auto. - exists (Locmap.set (R dst) (rs (S s)) (undef_getstack s rs)). + econstructor. + split. apply star_one; apply exec_Lop. simpl; reflexivity. + unfold undef_op. split. apply Locmap.gss. + intros. rewrite Locmap.gso; auto; apply Locmap.guo; auto. + econstructor. split. apply star_one; apply exec_Lgetstack. split. apply Locmap.gss. intros. rewrite Locmap.gso; auto. @@ -279,19 +280,31 @@ Lemma add_spill_correct: star step ge (State stk f sp (add_spill src dst k) rs m) E0 (State stk f sp k rs' m) /\ rs' dst = rs (R src) /\ - forall l, Loc.diff dst l -> rs' l = rs l. + forall l, Loc.diff dst l -> Loc.notin l destroyed_at_move -> rs' l = rs l. Proof. intros. unfold add_spill. destruct dst. - case (mreg_eq src m0); intro. + destruct (mreg_eq src m0). subst src. exists rs. split. apply star_refl. tauto. - exists (Locmap.set (R m0) (rs (R src)) rs). - split. apply star_one. apply exec_Lop. reflexivity. + econstructor. + split. apply star_one. apply exec_Lop. simpl; reflexivity. split. apply Locmap.gss. - intros; apply Locmap.gso; auto. - exists (Locmap.set (S s) (rs (R src)) rs). + intros. rewrite Locmap.gso; auto; unfold undef_op; apply Locmap.guo; auto. + econstructor. split. apply star_one. apply exec_Lsetstack. split. apply Locmap.gss. - intros; apply Locmap.gso; auto. + intros. rewrite Locmap.gso; auto; unfold undef_setstack; apply Locmap.guo; auto. +Qed. + +Remark notin_destroyed_move_1: + forall r, ~In r destroyed_at_move_regs -> Loc.notin (R r) destroyed_at_move. +Proof. + intros. simpl in *. intuition congruence. +Qed. + +Remark notin_destroyed_move_2: + forall s, Loc.notin (S s) destroyed_at_move. +Proof. + intros. simpl in *. destruct s; auto. Qed. Lemma add_reloads_correct_rec: @@ -300,21 +313,26 @@ Lemma add_reloads_correct_rec: enough_temporaries_rec srcs itmps ftmps = true -> (forall r, In (R r) srcs -> In r itmps -> False) -> (forall r, In (R r) srcs -> In r ftmps -> False) -> + (forall r, In (R r) srcs -> ~In r destroyed_at_move_regs) -> list_disjoint itmps ftmps -> list_norepet itmps -> list_norepet ftmps -> + list_disjoint itmps destroyed_at_move_regs -> + list_disjoint ftmps destroyed_at_move_regs -> exists rs', star step ge (State stk f sp (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m) E0 (State stk f sp k rs' m) /\ reglist rs' (regs_for_rec srcs itmps ftmps) = map rs srcs /\ - (forall r, ~(In r itmps) -> ~(In r ftmps) -> rs' (R r) = rs (R r)) /\ + (forall r, ~(In r itmps) -> ~(In r ftmps) -> ~(In r destroyed_at_move_regs) -> rs' (R r) = rs (R r)) /\ (forall s, rs' (S s) = rs (S s)). Proof. +Opaque destroyed_at_move_regs. induction srcs; simpl; intros. (* base case *) exists rs. split. apply star_refl. tauto. (* inductive case *) + simpl in H0. assert (ACC1: loc_acceptable a) by (auto with coqlib). assert (ACC2: locs_acceptable srcs) by (red; auto with coqlib). destruct a as [r | s]. @@ -323,41 +341,53 @@ Proof. exploit IHsrcs; eauto. intros [rs' [EX [RES [OTH1 OTH2]]]]. exists rs'. split. eauto. - split. simpl. decEq. apply OTH1. red; intros; eauto. red; intros; eauto. auto. + split. simpl. decEq. + apply OTH1. red; intros; eauto. red; intros; eauto. auto. + auto. auto. (* a is a stack slot *) destruct (slot_type s). (* ... of integer type *) - destruct itmps as [ | it1 itmps ]. discriminate. inv H4. + destruct itmps as [ | it1 itmps ]. discriminate. inv H5. destruct (add_reload_correct (S s) it1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m) as [rs1 [A [B C]]]. - exploit IHsrcs; eauto. - intros. apply H1 with r. tauto. simpl. tauto. eapply list_disjoint_cons_left; eauto. + exploit IHsrcs; eauto with coqlib. + eapply list_disjoint_cons_left; eauto. + eapply list_disjoint_cons_left; eauto. intros [rs' [P [Q [T U]]]]. exists rs'. split. eapply star_trans; eauto. - split. simpl. decEq. rewrite <- B. apply T. auto. - eapply list_disjoint_notin; eauto with coqlib. + split. simpl. decEq. rewrite <- B. apply T. + auto. + eapply list_disjoint_notin. eexact H4. eauto with coqlib. + eapply list_disjoint_notin. eapply H7. auto with coqlib. rewrite Q. apply list_map_exten. intros. symmetry. apply C. simpl. destruct x; auto. red; intro; subst m0. apply H1 with it1; auto with coqlib. auto. + destruct x. apply notin_destroyed_move_1. auto. apply notin_destroyed_move_2. split. simpl. intros. transitivity (rs1 (R r)). - apply T; tauto. apply C. simpl. tauto. auto. - intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto. + apply T; tauto. apply C. simpl. tauto. auto. + apply notin_destroyed_move_1; auto. + intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto. apply notin_destroyed_move_2. (* ... of float type *) - destruct ftmps as [ | ft1 ftmps ]. discriminate. inv H5. + destruct ftmps as [ | ft1 ftmps ]. discriminate. inv H6. destruct (add_reload_correct (S s) ft1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m) as [rs1 [A [B C]]]. - exploit IHsrcs; eauto. - intros. apply H2 with r. tauto. simpl. tauto. eapply list_disjoint_cons_right; eauto. + exploit IHsrcs; eauto with coqlib. + eapply list_disjoint_cons_right; eauto. + eapply list_disjoint_cons_left; eauto. intros [rs' [P [Q [T U]]]]. - exists rs'. split. eapply star_trans; eauto. - split. simpl. decEq. rewrite <- B. apply T; auto. - eapply list_disjoint_notin; eauto. apply list_disjoint_sym. eauto. auto with coqlib. + exists rs'. split. eapply star_trans; eauto. + split. simpl. decEq. rewrite <- B. apply T. + eapply list_disjoint_notin; eauto. apply list_disjoint_sym. apply H4. auto with coqlib. + auto. + eapply list_disjoint_notin. eexact H8. auto with coqlib. rewrite Q. apply list_map_exten. intros. symmetry. apply C. simpl. destruct x; auto. red; intro; subst m0. apply H2 with ft1; auto with coqlib. auto. + destruct x. apply notin_destroyed_move_1. auto. apply notin_destroyed_move_2. split. simpl. intros. transitivity (rs1 (R r)). - apply T; tauto. apply C. simpl. tauto. auto. - intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto. + apply T; tauto. apply C. simpl. tauto. auto. + apply notin_destroyed_move_1; auto. + intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto. apply notin_destroyed_move_2; auto. Qed. Lemma add_reloads_correct: @@ -370,22 +400,26 @@ Lemma add_reloads_correct: reglist rs' (regs_for srcs) = List.map rs srcs /\ forall l, Loc.notin l temporaries -> rs' l = rs l. Proof. +Transparent destroyed_at_move_regs. intros. unfold enough_temporaries in H. - exploit add_reloads_correct_rec; eauto. - intros. generalize (H0 _ H1). unfold loc_acceptable. generalize H2. + exploit add_reloads_correct_rec. eauto. eauto. + intros. generalize (H0 _ H1). unfold loc_acceptable. generalize H2. simpl. intuition congruence. intros. generalize (H0 _ H1). unfold loc_acceptable. generalize H2. simpl. intuition congruence. - red; intros r1 r2; simpl. intuition congruence. + intros. generalize (H0 _ H1). unfold loc_acceptable. + simpl. intuition congruence. + red; simpl; intros. intuition congruence. unfold int_temporaries. NoRepet. unfold float_temporaries. NoRepet. + red; simpl; intros. intuition congruence. + red; simpl; intros. intuition congruence. intros [rs' [EX [RES [OTH1 OTH2]]]]. exists rs'. split. eexact EX. split. exact RES. - intros. destruct l. apply OTH1. - generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence. - generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence. + intros. destruct l. generalize (Loc.notin_not_in _ _ H1); simpl; intro. + apply OTH1; simpl; intuition congruence. apply OTH2. Qed. @@ -395,19 +429,21 @@ Lemma add_move_correct: star step ge (State stk f sp (add_move src dst k) rs m) E0 (State stk f sp k rs' m) /\ rs' dst = rs src /\ - forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> rs' l = rs l. + forall l, + Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> + rs' l = rs l. Proof. intros; unfold add_move. - case (Loc.eq src dst); intro. + destruct (Loc.eq src dst). subst dst. exists rs. split. apply star_refl. tauto. destruct src. (* src is a register *) generalize (add_spill_correct m0 dst k rs m); intros [rs' [EX [RES OTH]]]. - exists rs'; intuition. apply OTH; apply Loc.diff_sym; auto. + exists rs'; intuition. apply OTH. apply Loc.diff_sym; auto. auto. destruct dst. (* src is a stack slot, dst a register *) generalize (add_reload_correct (S s) m0 k rs m); intros [rs' [EX [RES OTH]]]. - exists rs'; intuition. apply OTH. apply Loc.diff_sym; auto. right; apply Loc.diff_sym; auto. + exists rs'; intuition. apply OTH. apply Loc.diff_sym; auto. right; apply Loc.diff_sym; auto. auto. (* src and dst are stack slots *) set (tmp := match slot_type s with Tint => IT1 | Tfloat => FT1 end). generalize (add_reload_correct (S s) tmp (add_spill tmp (S s0) k) rs m); @@ -419,8 +455,8 @@ Proof. split. congruence. intros. rewrite OTH2. apply OTH1. apply Loc.diff_sym. unfold tmp; case (slot_type s); auto. - right. apply Loc.diff_sym; auto. - apply Loc.diff_sym; auto. + right. apply Loc.diff_sym; auto. auto. + apply Loc.diff_sym; auto. auto. Qed. Lemma effect_move_sequence: @@ -440,7 +476,7 @@ Proof. destruct (add_move_correct src dst k1 rs m) as [rs1 [A [B C]]]. destruct (IHmoves rs1 m) as [rs' [D E]]. exists rs'; split. - eapply star_trans; eauto. traceEq. + eapply star_trans; eauto. econstructor; eauto. red. tauto. Qed. @@ -566,7 +602,7 @@ Remark undef_op_others: Loc.notin l temporaries -> undef_op op rs l = rs l. Proof. intros. generalize (undef_temps_others rs l H); intro. - destruct op; simpl; auto. + unfold undef_op; destruct op; auto; apply Locmap.guo; simpl in *; tauto. Qed. Lemma agree_undef_temps: @@ -1006,7 +1042,7 @@ Proof. apply agree_set2 with ls; auto. rewrite B. simpl in H; inversion H. auto. intros. apply C. apply Loc.diff_sym; auto. - simpl in H7; tauto. simpl in H7; tauto. + simpl in H7; tauto. simpl in H7; tauto. simpl in *; tauto. (* other ops *) assert (is_move_operation op args = None). caseEq (is_move_operation op args); intros. @@ -1032,7 +1068,7 @@ Proof. apply agree_set2 with ls; auto. rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_op_others; auto. - apply reg_for_diff; auto. + apply reg_for_diff; auto. simpl in *; tauto. (* Lload *) ExploitWT; inv WTI. @@ -1056,7 +1092,7 @@ Proof. apply agree_set2 with ls; auto. rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. - apply reg_for_diff; auto. + apply reg_for_diff; auto. simpl in *; tauto. (* Lstore *) ExploitWT; inv WTI. @@ -1212,10 +1248,12 @@ Proof. (map ls3 (loc_arguments sig))). replace (map ls3 (loc_arguments sig)) with (map ls2 (loc_arguments sig)). rewrite B. apply agree_locs; auto. - apply list_map_exten; intros. apply F. - apply Loc.diff_sym. - apply (loc_arguments_not_temporaries sig x (R IT1)); simpl; auto. + apply list_map_exten; intros. + exploit Loc.disjoint_notin. apply loc_arguments_not_temporaries. eauto. simpl; intros. + apply F. + apply Loc.diff_sym; tauto. auto. + simpl; tauto. left; econstructor; split. eapply star_plus_trans. eexact A. eapply plus_right. eexact D. eapply exec_Ltailcall; eauto. @@ -1273,7 +1311,7 @@ Proof. apply agree_set with ls; auto. rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. - apply reg_for_diff; auto. + apply reg_for_diff; auto. simpl in *; tauto. (* no reload *) exploit external_call_mem_extends; eauto. apply agree_locs; eauto. @@ -1401,6 +1439,7 @@ Proof. econstructor; eauto. apply agree_set with ls; auto. rewrite B. auto. + intros. apply C; auto. simpl in *; tauto. unfold parent_locset in PRES. apply agree_postcall_2 with ls0; auto. Qed. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index a2c8ecd..2ec14aa 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -673,17 +673,44 @@ Proof. rewrite Locmap.gso; auto. red. auto. Qed. +Lemma agree_regs_exten: + forall j ls rs ls' rs', + agree_regs j ls rs -> + (forall r, ls' (R r) = Vundef \/ ls' (R r) = ls (R r) /\ rs' r = rs r) -> + agree_regs j ls' rs'. +Proof. + intros; red; intros. + destruct (H0 r) as [A | [A B]]. + rewrite A. constructor. + rewrite A; rewrite B; auto. +Qed. + +Lemma agree_regs_undef_list: + forall j rl ls rs, + agree_regs j ls rs -> + agree_regs j (Locmap.undef (List.map R rl) ls) (undef_regs rl rs). +Proof. + induction rl; simpl; intros. + auto. + apply IHrl. apply agree_regs_set_reg; auto. +Qed. + Lemma agree_regs_undef_temps: forall j ls rs, agree_regs j ls rs -> agree_regs j (LTL.undef_temps ls) (undef_temps rs). Proof. - unfold LTL.undef_temps, undef_temps. - change temporaries with (List.map R (int_temporaries ++ float_temporaries)). - generalize (int_temporaries ++ float_temporaries). - induction l; simpl; intros. - auto. - apply IHl. apply agree_regs_set_reg; auto. + unfold LTL.undef_temps, undef_temps, temporaries. + intros; apply agree_regs_undef_list; auto. +Qed. + +Lemma agree_regs_undef_setstack: + forall j ls rs, + agree_regs j ls rs -> + agree_regs j (Linear.undef_setstack ls) (undef_setstack rs). +Proof. + intros. unfold Linear.undef_setstack, undef_setstack, destroyed_at_move. + apply agree_regs_undef_list; auto. Qed. Lemma agree_regs_undef_op: @@ -691,9 +718,9 @@ Lemma agree_regs_undef_op: agree_regs j ls rs -> agree_regs j (Linear.undef_op op ls) (undef_op (transl_op fe op) rs). Proof. - intros. - generalize (agree_regs_undef_temps _ _ _ H). - destruct op; simpl; auto. + intros. generalize (agree_regs_undef_temps _ _ _ H); intro A. +Opaque destroyed_at_move_regs. + destruct op; auto; simpl; apply agree_regs_undef_setstack; auto. Qed. (** Preservation under assignment of stack slot *) @@ -740,7 +767,7 @@ 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)) -> + 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. @@ -767,25 +794,36 @@ Proof. contradiction. Qed. -Lemma agree_frame_undef_temps: - forall j ls ls0 m sp m' sp' parent ra, +Lemma agree_frame_undef_locs: + forall j ls0 m sp m' sp' parent ra regs ls, agree_frame j ls ls0 m sp m' sp' parent ra -> - agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra. + incl (List.map R regs) temporaries -> + agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra. Proof. - intros until ra. - assert (forall regs ls, - incl (List.map R regs) temporaries -> - agree_frame j ls ls0 m sp m' sp' parent ra -> - agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra). induction regs; simpl; intros. auto. apply IHregs; eauto with coqlib. apply agree_frame_set_reg; auto. apply temporary_within_bounds; eauto with coqlib. red; auto. - intros. unfold LTL.undef_temps. - change temporaries with (List.map R (int_temporaries ++ float_temporaries)). - apply H; auto. apply incl_refl. +Qed. + +Lemma agree_frame_undef_temps: + forall j ls ls0 m sp m' sp' parent ra, + agree_frame j ls ls0 m sp m' sp' parent ra -> + agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra. +Proof. + intros. unfold temporaries. apply agree_frame_undef_locs; auto. apply incl_refl. +Qed. + +Lemma agree_frame_undef_setstack: + forall j ls ls0 m sp m' sp' parent ra, + agree_frame j ls ls0 m sp m' sp' parent ra -> + agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent ra. +Proof. + intros. unfold Linear.undef_setstack, destroyed_at_move. + apply agree_frame_undef_locs; auto. + red; simpl; tauto. Qed. Lemma agree_frame_undef_op: @@ -794,7 +832,8 @@ Lemma agree_frame_undef_op: agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent ra. Proof. intros. - exploit agree_frame_undef_temps; eauto. destruct op; simpl; auto. + exploit agree_frame_undef_temps; eauto. + destruct op; simpl; auto; intros; apply agree_frame_undef_setstack; auto. Qed. (** Preservation by assignment to local slot *) @@ -1083,7 +1122,6 @@ Variable fb: block. Variable sp: block. Variable csregs: list mreg. Variable ls: locset. -Variable rs: regset. Inductive stores_in_frame: mem -> mem -> Prop := | stores_in_frame_refl: forall m, @@ -1116,19 +1154,22 @@ Hypothesis mkindex_diff: Hypothesis csregs_typ: forall r, In r csregs -> mreg_type r = ty. -Hypothesis agree: agree_regs j ls rs. +Hypothesis ls_temp_undef: + forall r, In r destroyed_at_move_regs -> ls (R r) = Vundef. + Hypothesis wt_ls: wt_locset ls. Lemma save_callee_save_regs_correct: - forall l k m, + forall l k rs m, incl l csregs -> list_norepet l -> frame_perm_freeable m sp -> - exists m', + agree_regs j ls rs -> + exists rs', exists m', star step tge (State cs fb (Vptr sp Int.zero) (save_callee_save_regs bound number mkindex ty fe l k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs m') + E0 (State cs fb (Vptr sp Int.zero) k rs' m') /\ (forall r, In r l -> number r < bound fe -> index_contains_inj j m' sp (mkindex (number r)) (ls (R r))) @@ -1139,12 +1180,13 @@ Lemma save_callee_save_regs_correct: index_contains m sp idx v -> index_contains m' sp idx v) /\ stores_in_frame m m' - /\ frame_perm_freeable m' sp. + /\ frame_perm_freeable m' sp + /\ agree_regs j ls rs'. Proof. induction l; intros; simpl save_callee_save_regs. (* base case *) - exists m. split. apply star_refl. - split. intros. elim H2. + exists rs; exists m. split. apply star_refl. + split. intros. elim H3. split. auto. split. constructor. auto. @@ -1156,20 +1198,24 @@ Proof. (* a store takes place *) exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. eauto. instantiate (1 := rs a). intros [m1 ST]. - exploit (IHl k m1). auto with coqlib. auto. + exploit (IHl k (undef_setstack rs) m1). auto with coqlib. auto. red; eauto with mem. - intros [m' [A [B [C [D E]]]]]. - exists m'. - split. eapply star_left; eauto. constructor. + apply agree_regs_exten with ls rs. auto. + intros. destruct (In_dec mreg_eq r destroyed_at_move_regs). + left. apply ls_temp_undef; auto. + right; split. auto. unfold undef_setstack, undef_move. apply undef_regs_other; auto. + intros [rs' [m' [A [B [C [D [E F]]]]]]]. + exists rs'; exists m'. + split. eapply star_left; eauto. econstructor. rewrite <- (mkindex_typ (number a)). apply store_stack_succeeds; auto with coqlib. traceEq. split; intros. - simpl in H2. destruct (mreg_eq a r). subst r. + 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. - destruct H4 as [v' [P Q]]. + destruct H5 as [v' [P Q]]. exists v'; split; auto. apply C; auto. intros. apply mkindex_inj. apply number_inj; auto with coqlib. inv H0. intuition congruence. @@ -1182,44 +1228,49 @@ Proof. rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; eauto with coqlib. auto. (* no store takes place *) - exploit (IHl k m); auto with coqlib. - intros [m' [A [B [C [D E]]]]]. - exists m'; intuition. - simpl in H2. destruct H2. subst r. omegaContradiction. apply B; auto. + exploit (IHl k rs m); auto with coqlib. + intros [rs' [m' [A [B [C [D [E F]]]]]]]. + exists rs'; exists m'; intuition. + simpl in H3. destruct H3. subst r. omegaContradiction. apply B; auto. apply C; auto with coqlib. - intros. eapply H3; eauto. auto with coqlib. + intros. eapply H4; eauto. auto with coqlib. Qed. End SAVE_CALLEE_SAVE. Lemma save_callee_save_correct: forall j ls rs sp cs fb k m, - agree_regs j ls rs -> wt_locset ls -> + agree_regs j (call_regs ls) rs -> wt_locset (call_regs ls) -> frame_perm_freeable m sp -> - exists m', + exists rs', exists m', star step tge (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs m') + E0 (State cs fb (Vptr sp Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) -> - index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (ls (R r))) + index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (call_regs ls (R r))) /\ (forall r, In r float_callee_save_regs -> index_float_callee_save r < b.(bound_float_callee_save) -> - index_contains_inj j m' sp (FI_saved_float (index_float_callee_save r)) (ls (R r))) + index_contains_inj j m' sp (FI_saved_float (index_float_callee_save r)) (call_regs ls (R r))) /\ (forall idx v, index_valid idx -> match idx with FI_saved_int _ => False | FI_saved_float _ => False | _ => True end -> index_contains m sp idx v -> index_contains m' sp idx v) /\ stores_in_frame sp m m' - /\ frame_perm_freeable m' sp. + /\ frame_perm_freeable m' sp + /\ agree_regs j (call_regs ls) rs'. Proof. intros. + assert (ls_temp_undef: forall r, In r destroyed_at_move_regs -> call_regs ls (R r) = Vundef). + intros; unfold call_regs. apply pred_dec_true. +Transparent destroyed_at_move_regs. + simpl in *; intuition congruence. exploit (save_callee_save_regs_correct fe_num_int_callee_save index_int_callee_save FI_saved_int Tint - j cs fb sp int_callee_save_regs ls rs). + j cs fb sp int_callee_save_regs (call_regs ls)). intros. apply index_int_callee_save_inj; auto. intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption. auto. @@ -1231,12 +1282,13 @@ Proof. apply incl_refl. apply int_callee_save_norepet. eauto. - intros [m1 [A [B [C [D E]]]]]. + eauto. + intros [rs1 [m1 [A [B [C [D [E F]]]]]]]. exploit (save_callee_save_regs_correct fe_num_float_callee_save index_float_callee_save FI_saved_float Tfloat - j cs fb sp float_callee_save_regs ls rs). + j cs fb sp float_callee_save_regs (call_regs ls)). intros. apply index_float_callee_save_inj; auto. intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption. simpl; auto. @@ -1248,8 +1300,9 @@ Proof. apply incl_refl. apply float_callee_save_norepet. eexact E. - intros [m2 [P [Q [R [S T]]]]]. - exists m2. + eexact F. + intros [rs2 [m2 [P [Q [R [S [T U]]]]]]]. + exists rs2; exists m2. split. unfold save_callee_save, save_callee_save_int, save_callee_save_float. eapply star_trans; eauto. split; intros. @@ -1318,14 +1371,14 @@ Lemma function_prologue_correct: Mem.inject j m1 m1' -> Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) -> Val.has_type parent Tint -> Val.has_type ra Tint -> - exists j', exists m2', exists sp', exists m3', exists m4', exists m5', + exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5', Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp') /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3' /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4' /\ star step tge (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4') - E0 (State cs fb (Vptr sp' Int.zero) k (undef_temps rs) m5') - /\ agree_regs j' (call_regs ls) (undef_temps rs) + E0 (State cs fb (Vptr sp' Int.zero) k rs' m5') + /\ agree_regs j' (call_regs ls) rs' /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent ra /\ inject_incr j j' /\ inject_separated j j' m1 m1' @@ -1368,11 +1421,10 @@ Proof. assert (PERM4: frame_perm_freeable m4' sp'). red; intros. eauto with mem. exploit save_callee_save_correct. - apply agree_regs_undef_temps. - eapply agree_regs_inject_incr; eauto. - apply wt_undef_temps. auto. + apply agree_regs_call_regs. eapply agree_regs_inject_incr; eauto. + apply wt_call_regs. auto. eexact PERM4. - intros [m5' [STEPS [ICS [FCS [OTHERS [STORES PERM5]]]]]]. + intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. (* stores in frames *) assert (SIF: stores_in_frame sp' m2' m5'). econstructor; eauto. @@ -1388,7 +1440,7 @@ Proof. assert (~Mem.valid_block m1' sp') by eauto with mem. contradiction. (* Conclusions *) - exists j'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'. + exists j'; exists rs'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'. split. auto. (* store parent *) split. change Tint with (type_of_index FI_link). @@ -1401,7 +1453,7 @@ Proof. (* saving of registers *) split. eexact STEPS. (* agree_regs *) - split. apply agree_regs_call_regs. apply agree_regs_inject_incr with j; auto. + split. auto. (* agree frame *) split. constructor; intros. (* unused regs *) @@ -1423,15 +1475,15 @@ Proof. apply OTHERS; auto. red; auto. eapply gss_index_contains; eauto. red; auto. (* int callee save *) - rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)). + rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)). apply ICS; auto. - unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. + unfold call_regs. apply pred_dec_false. red; intros; exploit int_callee_save_not_destroyed; eauto. auto. (* float callee save *) - rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)). + rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)). apply FCS; auto. - unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. + unfold call_regs. apply pred_dec_false. red; intros; exploit float_callee_save_not_destroyed; eauto. auto. (* inj *) @@ -2350,7 +2402,7 @@ Proof. econstructor; eauto with coqlib. econstructor; eauto. apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. congruence. eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. - apply temporary_within_bounds. unfold temporaries; auto with coqlib. + apply temporary_within_bounds. simpl; auto. simpl; auto. simpl; rewrite <- H1. eapply agree_wt_ls; eauto. (* Lgetstack, outgoing *) exploit agree_outgoing; eauto. intros [v [A B]]. @@ -2389,11 +2441,13 @@ Proof. omega. apply match_stacks_change_mach_mem with m'; auto. eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega. - apply agree_regs_set_slot; auto. + apply agree_regs_set_slot. apply agree_regs_undef_setstack; auto. destruct sl. - eapply agree_frame_set_local; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. + eapply agree_frame_set_local. eapply agree_frame_undef_setstack; eauto. auto. auto. + simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. auto. simpl in H3; contradiction. - eapply agree_frame_set_outgoing; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. + eapply agree_frame_set_outgoing. apply agree_frame_undef_setstack; eauto. auto. auto. + simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. auto. (* Lop *) assert (Val.has_type v (mreg_type res)). @@ -2611,7 +2665,7 @@ Proof. exploit function_prologue_correct; eauto. eapply match_stacks_type_sp; eauto. eapply match_stacks_type_retaddr; eauto. - intros [j' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]. + intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]]. econstructor; split. eapply plus_left. econstructor; eauto. rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body. -- cgit v1.2.3