From c98440cad6b7a9c793aded892ec61a8ed50cac28 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 2 Mar 2007 15:43:35 +0000 Subject: Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de Lattice pour utiliser une notion d'egalite possiblement differente de =. Adaptation de Kildall et de ses utilisateurs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocproof.v | 87 ++++++++++++++++++++++++++++------------------------ 1 file changed, 47 insertions(+), 40 deletions(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 0b252d5..f0b2968 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2,6 +2,8 @@ RTL to LTL). *) Require Import Relations. +Require Import FSets. +Require Import SetoidList. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -83,7 +85,7 @@ Lemma analyze_correct: f.(fn_code)!n <> None -> f.(fn_code)!s <> None -> In s (successors f n) -> - Regset.ge live!!n (transfer f s live!!s). + RegsetLat.ge live!!n (transfer f s live!!s). Proof. intros. eapply DS.fixpoint_solution. @@ -188,6 +190,7 @@ End REGALLOC_PROPERTIES. (** * Semantic agreement between RTL registers and LTL locations *) Require Import LTL. +Module RegsetP := Properties(Regset). Section AGREE. @@ -212,7 +215,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign. of [assign r] can be arbitrary. *) Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := - forall (r: reg), Regset.mem r live = true -> ls (assign r) = rs#r. + forall (r: reg), Regset.In r live -> ls (assign r) = rs#r. (** What follows is a long list of lemmas expressing properties of the [agree_live_regs] predicate that are useful for the @@ -222,7 +225,7 @@ Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := Lemma agree_increasing: forall live1 live2 rs ls, - Regset.ge live1 live2 -> agree live1 rs ls -> + RegsetLat.ge live1 live2 -> agree live1 rs ls -> agree live2 rs ls. Proof. unfold agree; intros. @@ -231,14 +234,13 @@ Qed. (** Some useful special cases of [agree_increasing]. *) + Lemma agree_reg_live: forall r live rs ls, agree (reg_live r live) rs ls -> agree live rs ls. Proof. - intros. apply agree_increasing with (reg_live r live). - red; intros. case (Reg.eq r r0); intro. - subst r0. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. auto. + intros. apply agree_increasing with (reg_live r live); auto. + red. apply RegsetP.subset_add_2. apply RegsetP.subset_refl. Qed. Lemma agree_reg_list_live: @@ -266,7 +268,7 @@ Lemma agree_eval_reg: forall r live rs ls, agree (reg_live r live) rs ls -> ls (assign r) = rs#r. Proof. - intros. apply H. apply Regset.mem_add_same. + intros. apply H. apply Regset.add_1. auto. Qed. (** Same, for a list of registers. *) @@ -304,13 +306,13 @@ Qed. Lemma agree_assign_dead: forall live r rs ls v, - Regset.mem r live = false -> + ~Regset.In r live -> agree live rs ls -> agree live (rs#r <- v) ls. Proof. unfold agree; intros. case (Reg.eq r r0); intro. - subst r0. congruence. + subst r0. contradiction. rewrite Regmap.gso; auto. Qed. @@ -322,7 +324,7 @@ Qed. Lemma agree_assign_live: forall live r rs ls ls' v, (forall s, - Regset.mem s live = true -> s <> r -> assign s <> assign r) -> + Regset.In s live -> s <> r -> assign s <> assign r) -> ls' (assign r) = v -> (forall l, Loc.diff l (assign r) -> Loc.notin l temporaries -> ls' l = ls l) -> agree (reg_dead r live) rs ls -> @@ -332,8 +334,8 @@ Proof. case (Reg.eq r r0); intro. subst r0. rewrite Regmap.gss. assumption. rewrite Regmap.gso; auto. - rewrite H1. apply H2. rewrite Regset.mem_remove_other. auto. - auto. eapply regalloc_noteq_diff. eauto. apply H. auto. auto. + rewrite H1. apply H2. apply Regset.remove_2; auto. + eapply regalloc_noteq_diff. eauto. apply H. auto. auto. eapply regalloc_not_temporary; eauto. Qed. @@ -347,7 +349,7 @@ Qed. Lemma agree_move_live: forall live arg res rs (ls ls': locset), (forall r, - Regset.mem r live = true -> r <> res -> r <> arg -> + Regset.In r live -> r <> res -> r <> arg -> assign r <> assign res) -> ls' (assign res) = ls (assign arg) -> (forall l, Loc.diff l (assign res) -> Loc.notin l temporaries -> ls' l = ls l) -> @@ -357,17 +359,16 @@ Proof. unfold agree; intros. case (Reg.eq res r); intro. subst r. rewrite Regmap.gss. rewrite H0. apply H2. - apply Regset.mem_add_same. + apply Regset.add_1; auto. rewrite Regmap.gso; auto. case (Loc.eq (assign r) (assign res)); intro. rewrite e. rewrite H0. case (Reg.eq arg r); intro. - subst r. apply H2. apply Regset.mem_add_same. + subst r. apply H2. apply Regset.add_1; auto. elim (H r); auto. rewrite H1. apply H2. - case (Reg.eq arg r); intro. subst r. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. - rewrite Regset.mem_remove_other; auto. + case (Reg.eq arg r); intro. subst r. apply Regset.add_1; auto. + apply Regset.add_2. apply Regset.remove_2. auto. auto. eapply regalloc_noteq_diff; eauto. eapply regalloc_not_temporary; eauto. Qed. @@ -379,11 +380,10 @@ Qed. Lemma agree_call: forall live args ros res rs v (ls ls': locset), (forall r, - Regset.mem r live = true -> - r <> res -> + Regset.In r live -> r <> res -> ~(In (assign r) Conventions.destroyed_at_call)) -> (forall r, - Regset.mem r live = true -> r <> res -> assign r <> assign res) -> + Regset.In r live -> r <> res -> assign r <> assign res) -> ls' (assign res) = v -> (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) -> @@ -399,7 +399,7 @@ Proof. case (Reg.eq r res); intro. subst r. rewrite Regmap.gss. assumption. rewrite Regmap.gso; auto. rewrite H2. apply H4. - rewrite Regset.mem_remove_other; auto. + apply Regset.remove_2; auto. eapply regalloc_notin_notin; eauto. eapply regalloc_acceptable; eauto. eapply regalloc_noteq_diff; eauto. @@ -411,7 +411,7 @@ Qed. Lemma agree_init_regs: forall rl vl ls live, (forall r1 r2, - In r1 rl -> Regset.mem r2 live = true -> r1 <> r2 -> + In r1 rl -> Regset.In r2 live -> r1 <> r2 -> assign r1 <> assign r2) -> List.map ls (List.map assign rl) = vl -> agree (reg_list_dead rl live) (Regmap.init Vundef) ls -> @@ -421,15 +421,13 @@ Proof. assumption. destruct vl. discriminate. assert (agree (reg_dead a live) (init_regs vl rl) ls). - apply IHrl. intros. apply H. tauto. - case (Reg.eq a r2); intro. subst r2. - rewrite Regset.mem_remove_same in H3. discriminate. - rewrite Regset.mem_remove_other in H3; auto. + apply IHrl. intros. apply H. tauto. + eapply Regset.remove_3; eauto. auto. congruence. assumption. red; intros. case (Reg.eq a r); intro. subst r. rewrite Regmap.gss. congruence. - rewrite Regmap.gso; auto. apply H2. - rewrite Regset.mem_remove_other; auto. + rewrite Regmap.gso; auto. apply H2. + apply Regset.remove_2; auto. Qed. Lemma agree_parameters: @@ -437,7 +435,7 @@ Lemma agree_parameters: let params := f.(RTL.fn_params) in List.map ls (List.map assign params) = vl -> (forall r, - Regset.mem r (reg_list_dead params (live0 f flive)) = true -> + Regset.In r (reg_list_dead params (live0 f flive)) -> ls (assign r) = Vundef) -> agree (live0 f flive) (init_regs vl params) ls. Proof. @@ -1373,6 +1371,7 @@ Proof. intros; red; intros; CleanupHyps. caseEq (Regset.mem res live!!pc); intro LV; rewrite LV in AG. + generalize (Regset.mem_2 _ _ LV). intro LV'. assert (LL: (List.length (List.map assign args) <= 3)%nat). rewrite list_length_map. inversion WTI. simpl; omega. simpl; omega. @@ -1409,7 +1408,8 @@ Proof. exists ls. split. CleanupGoal. rewrite LV. apply exec_Bgoto; apply exec_refl. - apply agree_assign_dead; assumption. + apply agree_assign_dead; auto. + red; intro. exploit Regset.mem_1; eauto. congruence. Qed. Lemma transl_Iload_correct: @@ -1426,6 +1426,7 @@ Proof. caseEq (Regset.mem dst live!!pc); intro LV; rewrite LV in AG. (* dst is live *) + exploit Regset.mem_2; eauto. intro LV'. assert (LL: (List.length (List.map assign args) <= 2)%nat). rewrite list_length_map. inversion WTI. @@ -1453,6 +1454,7 @@ Proof. CleanupGoal. rewrite LV. apply exec_Bgoto; apply exec_refl. apply agree_assign_dead; auto. + red; intro; exploit Regset.mem_1; eauto. congruence. Qed. Lemma transl_Istore_correct: @@ -1681,16 +1683,15 @@ Qed. Remark regset_mem_reg_list_dead: forall rl r live, - Regset.mem r (reg_list_dead rl live) = true -> - ~(In r rl) /\ Regset.mem r live = true. + Regset.In r (reg_list_dead rl live) -> + ~(In r rl) /\ Regset.In r live. Proof. induction rl; simpl; intros. tauto. elim (IHrl r (reg_dead a live) H). intros. - assert (a <> r). red; intro; subst r. - rewrite Regset.mem_remove_same in H1. discriminate. - rewrite Regset.mem_remove_other in H1; auto. - tauto. + assert (a <> r). red; intro; subst r. + exploit Regset.remove_1; eauto. + intuition. eapply Regset.remove_3; eauto. Qed. Lemma transf_entrypoint_correct: @@ -1733,7 +1734,9 @@ Proof. intros [p [AP INP]]. clear INAP; subst ap. generalize (list_in_map_inv _ _ _ INAU). intros [u [AU INU]]. clear INAU; subst au. - generalize (Regset.elements_complete _ _ INU). intro. + assert (INU': InA Regset.E.eq u undefs). + rewrite InA_alt. exists u; intuition. + generalize (Regset.elements_2 _ _ INU'). intro. generalize (regset_mem_reg_list_dead _ _ _ H4). intros [A B]. eapply regalloc_noteq_diff; eauto. @@ -1761,7 +1764,11 @@ Proof. rewrite PARAMS1. assumption. fold oldentry; fold params. intros. apply UNDEFS1. apply in_map. - unfold undefs; apply Regset.elements_correct; auto. + unfold undefs. + change (transfer f oldentry live!!oldentry) + with (live0 f live). + exploit Regset.elements_1; eauto. + rewrite InA_alt. intros [r' [C D]]. hnf in C. subst r'. auto. Qed. Lemma transl_function_correct: -- cgit v1.2.3