diff options
Diffstat (limited to 'backend/Allocproof_aux.v')
| -rw-r--r-- | backend/Allocproof_aux.v | 850 |
1 files changed, 850 insertions, 0 deletions
diff --git a/backend/Allocproof_aux.v b/backend/Allocproof_aux.v new file mode 100644 index 0000000..d1b213e --- /dev/null +++ b/backend/Allocproof_aux.v @@ -0,0 +1,850 @@ +(** Correctness results for the [parallel_move] function defined in + file [Allocation]. + + The present file, contributed by Laurence Rideau, glues the general + results over the parallel move algorithm (see file [Parallelmove]) + with the correctness proof for register allocation (file [Allocproof]). +*) + +Require Import Coqlib. +Require Import Values. +Require Import Parallelmove. +Require Import Allocation. +Require Import LTL. +Require Import Locations. +Require Import Conventions. + +Section parallel_move_correction. +Variable ge : LTL.genv. +Variable sp : val. +Hypothesis + add_move_correct : + forall src dst k rs m, + (exists rs' , + exec_instrs ge sp (add_move src dst k) rs m 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)) ). + +Lemma exec_instr_update: + forall a1 a2 k e m, + (exists rs' , + exec_instrs ge sp (add_move a1 a2 k) e m k rs' m /\ + (rs' a2 = update e a2 (e a1) a2 /\ + (forall l, + Loc.diff l a2 -> + Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> rs' l = (update e a2 (e a1)) l)) + ). +Proof. +intros; destruct (add_move_correct a1 a2 k e m) as [rs' [Hf [R1 R2]]]. +exists rs'; (repeat split); auto. +generalize (get_update_id e a2); unfold get, Locmap.get; intros H; rewrite H; + auto. +intros l H0; generalize (get_update_diff e a2); unfold get, Locmap.get; + intros H; rewrite H; auto. +apply Loc.diff_sym; assumption. +Qed. + +Lemma map_inv: + forall (A B : Set) (f f' : A -> B) l, + map f l = map f' l -> forall x, In x l -> f x = f' x. +Proof. +induction l; simpl; intros Hmap x Hin. +elim Hin. +inversion Hmap. +elim Hin; intros H; [subst a | apply IHl]; auto. +Qed. + +Fixpoint reswellFormed (p : Moves) : Prop := + match p with + nil => True + | (s, d) :: l => Loc.notin s (getdst l) /\ reswellFormed l + end. + +Definition temporaries1 := R IT1 :: (R FT1 :: nil). + +Lemma no_overlap_list_pop: + forall p m, no_overlap_list (m :: p) -> no_overlap_list p. +Proof. +induction p; unfold no_overlap_list, no_overlap; destruct m as [m1 m2]; simpl; + auto. +Qed. + +Lemma exec_instrs_pmov: + forall p k rs m, + no_overlap_list p -> + Loc.disjoint (getdst p) temporaries1 -> + Loc.disjoint (getsrc p) temporaries1 -> + (exists rs' , + exec_instrs + ge sp + (fold_left + (fun (k0 : block) => fun (p0 : loc * loc) => add_move (fst p0) (snd p0) k0) + p k) rs m k rs' m /\ + (forall l, + (forall r, In r (getdst p) -> r = l \/ Loc.diff r l) -> + Loc.diff l (Locations.R IT1) -> + Loc.diff l (Locations.R FT1) -> rs' l = (sexec p rs) l) ). +Proof. +induction p; intros k rs m. +simpl; exists rs; (repeat split); auto; apply exec_refl. +destruct a as [a1 a2]; simpl; intros Hno_O Hdisd Hdiss; + elim (IHp (add_move a1 a2 k) rs m); + [idtac | apply no_overlap_list_pop with (a1, a2) | + apply (Loc.disjoint_cons_left a2) | apply (Loc.disjoint_cons_left a1)]; + (try assumption). +intros rs' Hexec; + destruct (add_move_correct a1 a2 k rs' m) as [rs'' [Hexec2 [R1 R2]]]. +exists rs''; elim Hexec; intros; (repeat split). +apply exec_trans with ( b2 := add_move a1 a2 k ) ( rs2 := rs' ) ( m2 := m ); + auto. +intros l Heqd Hdi Hdf; case (Loc.eq a2 l); intro. +subst l; generalize get_update_id; unfold get, Locmap.get; intros Hgui; + rewrite Hgui; rewrite R1. +apply H0; auto. +unfold no_overlap_list, no_overlap in Hno_O |-; simpl in Hno_O |-; intros; + generalize (Hno_O a1). +intros H8; elim H8 with ( s := r ); + [intros H9; left | intros H9; right; apply Loc.diff_sym | left | right]; auto. +unfold Loc.disjoint in Hdiss |-; apply Hdiss; simpl; left; trivial. +apply Hdiss; simpl; [left | right; left]; auto. +elim (Heqd a2); + [intros H7; absurd (a2 = l); auto | intros H7; auto | left; trivial]. +generalize get_update_diff; unfold get, Locmap.get; intros H6; rewrite H6; auto. +rewrite R2; auto. +apply Loc.diff_sym; auto. +Qed. + +Definition p_move := + fun (l : list (loc * loc)) => + fun (k : block) => + fold_left + (fun (k0 : block) => fun (p : loc * loc) => add_move (fst p) (snd p) k0) + (P_move l) k. + +Lemma norepet_SD: forall p, Loc.norepet (getdst p) -> simpleDest p. +Proof. +induction p; (simpl; auto). +destruct a as [a1 a2]. +intro; inversion H. +split. +apply notindst_nW; auto. +apply IHp; auto. +Qed. + +Theorem SDone_stepf: + forall S1, StateDone (stepf S1) = nil -> StateDone S1 = nil. +Proof. +destruct S1 as [[t b] d]; destruct t. +destruct b; auto. +destruct m as [m1 m2]; simpl. +destruct b. +simpl; intro; discriminate. +case (Loc.eq m2 (fst (last (m :: b)))); simpl; intros; discriminate. +destruct m as [a1 a2]; simpl. +destruct b. +case (Loc.eq a1 a2); simpl; intros; auto. +destruct m as [m1 m2]; case (Loc.eq a1 m2); intro; (try (simpl; auto; fail)). +case (split_move t m2). +(repeat destruct p); simpl; intros; auto. +destruct b; (try (simpl; intro; discriminate)); auto. +case (Loc.eq m2 (fst (last (m :: b)))); intro; simpl; intro; discriminate. +Qed. + +Theorem SDone_Pmov: forall S1, StateDone (Pmov S1) = nil -> StateDone S1 = nil. +Proof. +intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). +clear S1; intros S1; intros Hrec. +destruct S1 as [[t b] d]. +rewrite Pmov_equation. +destruct t. +destruct b; auto. +intro; assert (StateDone (stepf (nil, m :: b, d)) = nil); + [apply Hrec; auto; apply stepf1_dec | apply SDone_stepf]; auto. +intro; assert (StateDone (stepf (m :: t, b, d)) = nil); + [apply Hrec; auto; apply stepf1_dec | apply SDone_stepf]; auto. +Qed. + +Lemma no_overlap_temp: forall r s, In s temporaries -> r = s \/ Loc.diff r s. +Proof. +intros r s H; case (Loc.eq r s); intros e; [left | right]; (try assumption). +unfold Loc.diff; destruct r. +destruct s; trivial. +red; intro; elim e; rewrite H0; auto. +destruct s0; destruct s; trivial; + (elim H; [intros H1 | intros [H1|[H1|[H1|[H1|[H1|H1]]]]]]; (try discriminate); + inversion H1). +Qed. + +Lemma getsrcdst_app: + forall l1 l2, + getdst l1 ++ getdst l2 = getsrc l1 ++ getsrc l2 -> + getdst l1 = getsrc l1 /\ getdst l2 = getsrc l2. +Proof. +induction l1; simpl; auto. +destruct a as [a1 a2]; intros; inversion H. +subst a1; inversion H; + (elim IHl1 with ( l2 := l2 ); + [intros H0 H3; (try clear IHl1); (try exact H0) | idtac]; auto). +rewrite H0; auto. +Qed. + +Lemma In_norepet: + forall r x l, Loc.norepet l -> In x l -> In r l -> r = x \/ Loc.diff r x. +Proof. +induction l; simpl; intros. +elim H1. +inversion H. +subst hd. +elim H1; intros H2; clear H1; elim H0; intros H1. +rewrite <- H1; rewrite <- H2; auto. +subst a; right; apply Loc.in_notin_diff with l; auto. +subst a; right; apply Loc.diff_sym; apply Loc.in_notin_diff with l; auto. +apply IHl; auto. +Qed. + +Definition no_overlap_stateD (S : State) := + no_overlap + (getsrc (StateToMove S ++ (StateBeing S ++ StateDone S))) + (getdst (StateToMove S ++ (StateBeing S ++ StateDone S))). + +Ltac +incl_tac_rec := +(auto with datatypes; fail) + || + (apply in_cons; incl_tac_rec) + || + (apply in_or_app; left; incl_tac_rec) + || + (apply in_or_app; right; incl_tac_rec) + || + (apply incl_appl; incl_tac_rec) || + (apply incl_appr; incl_tac_rec) || (apply incl_tl; incl_tac_rec). + +Ltac incl_tac := (repeat (apply incl_cons || apply incl_app)); incl_tac_rec. + +Ltac +in_tac := +match goal with +| |- In ?x ?L1 => +match goal with +| H:In x ?L2 |- _ => +let H1 := fresh "H" in +(assert (H1: incl L2 L1); [incl_tac | apply (H1 x)]); auto; fail +| _ => fail end end. + +Lemma in_cons_noteq: + forall (A : Set) (a b : A) (l : list A), In a (b :: l) -> a <> b -> In a l. +Proof. +intros A a b l; simpl; intros. +elim H; intros H1; (try assumption). +absurd (a = b); auto. +Qed. + +Lemma no_overlapD_inv: + forall S1 S2, step S1 S2 -> no_overlap_stateD S1 -> no_overlap_stateD S2. +Proof. +intros S1 S2 STEP; inversion STEP; unfold no_overlap_stateD, no_overlap; simpl; + auto; (repeat (rewrite getsrc_app; rewrite getdst_app; simpl)); intros. +apply H1; in_tac. +destruct m as [m1 m2]; apply H1; in_tac. +apply H1; in_tac. +case (Loc.eq r (T r0)); intros e. +elim (no_overlap_temp s0 r); + [intro; left; auto | intro; right; apply Loc.diff_sym; auto | unfold T in e |-]. +destruct (Loc.type r0); simpl; [right; left | right; right; right; right; left]; + auto. +case (Loc.eq s0 (T r0)); intros es. +apply (no_overlap_temp r s0); unfold T in es |-; destruct (Loc.type r0); simpl; + [right; left | right; right; right; right; left]; auto. +apply H1; apply in_cons_noteq with ( b := T r0 ); auto; in_tac. +apply H3; in_tac. +Qed. + +Lemma no_overlapD_invpp: + forall S1 S2, stepp S1 S2 -> no_overlap_stateD S1 -> no_overlap_stateD S2. +Proof. +intros; induction H as [r|r1 r2 r3 H H1 HrecH]; auto. +apply HrecH; auto. +apply no_overlapD_inv with r1; auto. +Qed. + +Lemma no_overlapD_invf: + forall S1, stepInv S1 -> no_overlap_stateD S1 -> no_overlap_stateD (stepf S1). +Proof. +intros; destruct S1 as [[t1 b1] d1]. +destruct t1; destruct b1; auto. +set (S1:=(nil (A:=Move), m :: b1, d1)). +apply (no_overlapD_invpp S1); [apply dstep_step; auto | assumption]. +apply f2ind; [unfold S1 | idtac | idtac]; auto. +generalize H0; clear H0; unfold no_overlap_stateD; destruct m as [m1 m2]. +intros; apply no_overlap_noOverlap. +unfold no_overlap_state; simpl. +generalize H0; clear H0; unfold no_overlap; (repeat rewrite getdst_app); + (repeat rewrite getsrc_app); simpl; intros. +apply H0. +elim H1; intros H4; [left; assumption | right; in_tac]. +elim H2; intros H4; [left; assumption | right; in_tac]. +set (S1:=(m :: t1, nil (A:=Move), d1)). +apply (no_overlapD_invpp S1); [apply dstep_step; auto | assumption]. +apply f2ind; [unfold S1 | idtac | idtac]; auto. +generalize H0; clear H0; unfold no_overlap_stateD; destruct m as [m1 m2]. +intros; apply no_overlap_noOverlap. +unfold no_overlap_state; simpl. +generalize H0; clear H0; unfold no_overlap; (repeat rewrite getdst_app); + (repeat rewrite getsrc_app); simpl; (repeat rewrite app_nil); intros. +apply H0. +elim H1; intros H4; [left; assumption | right; (try in_tac)]. +elim H2; intros H4; [left; assumption | right; in_tac]. +set (S1:=(m :: t1, m0 :: b1, d1)). +apply (no_overlapD_invpp S1); [apply dstep_step; auto | assumption]. +apply f2ind; [unfold S1 | idtac | idtac]; auto. +generalize H0; clear H0; unfold no_overlap_stateD; destruct m as [m1 m2]. +intros; apply no_overlap_noOverlap. +unfold no_overlap_state; simpl. +generalize H0; clear H0; unfold no_overlap; (repeat rewrite getdst_app); + (repeat rewrite getsrc_app); destruct m0; simpl; intros. +apply H0. +elim H1; intros H4; [left; assumption | right; in_tac]. +elim H2; intros H4; [left; assumption | right; in_tac]. +Qed. + +Lemma no_overlapD_res: + forall S1, stepInv S1 -> no_overlap_stateD S1 -> no_overlap_stateD (Pmov S1). +Proof. +intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). +clear S1; intros S1 Hrec. +destruct S1 as [[t b] d]. +rewrite Pmov_equation. +destruct t; auto. +destruct b; auto. +intros; apply Hrec. +apply stepf1_dec; auto. +apply (dstep_inv (nil, m :: b, d)); auto. +apply f2ind'; auto. +apply no_overlap_noOverlap. +generalize H0; unfold no_overlap_stateD, no_overlap_state, no_overlap; simpl. +destruct m; (repeat rewrite getdst_app); (repeat rewrite getsrc_app). +intros H1 r1 H2 s H3; (try assumption). +apply H1; in_tac. +apply no_overlapD_invf; auto. +intros; apply Hrec. +apply stepf1_dec; auto. +apply (dstep_inv (m :: t, b, d)); auto. +apply f2ind'; auto. +apply no_overlap_noOverlap. +generalize H0; destruct m; + unfold no_overlap_stateD, no_overlap_state, no_overlap; simpl; + (repeat (rewrite getdst_app; simpl)); (repeat (rewrite getsrc_app; simpl)). +simpl; intros H1 r1 H2 s H3; (try assumption). +apply H1. +elim H2; intros H4; [left; (try assumption) | right; in_tac]. +elim H3; intros H4; [left; (try assumption) | right; in_tac]. +apply no_overlapD_invf; auto. +Qed. + +Definition temporaries1_3 := R IT1 :: (R FT1 :: (R IT3 :: nil)). + +Definition temporaries2 := R IT2 :: (R FT2 :: nil). + +Definition no_tmp13_state (S1 : State) := + Loc.disjoint (getsrc (StateDone S1)) temporaries1_3 /\ + Loc.disjoint (getdst (StateDone S1)) temporaries1_3. + +Definition Done_well_formed (S1 S2 : State) := + forall x, + (In x (getsrc (StateDone S2)) -> + In x temporaries2 \/ In x (getsrc (StateToMove S1 ++ StateBeing S1))) /\ + (In x (getdst (StateDone S2)) -> + In x temporaries2 \/ In x (getdst (StateToMove S1 ++ StateBeing S1))). + +Lemma Done_notmp3_inv: + forall S1 S2, + step S1 S2 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT3)) -> + forall x, + In x (getdst (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + Loc.diff x (R IT3). +Proof. +intros S1 S2 STEP; inversion STEP; (try (simpl; trivial; fail)); + simpl StateDone; simpl StateToMove; simpl StateBeing; simpl getdst; + (repeat (rewrite getdst_app; simpl)); intros. +apply H1; in_tac. +destruct m; apply H1; in_tac. +apply H1; in_tac. +case (Loc.eq x (T r0)); intros e. +unfold T in e |-; destruct (Loc.type r0); rewrite e; simpl; red; intro; + discriminate. +apply H1; apply in_cons_noteq with ( b := T r0 ); auto; in_tac. +apply H3; in_tac. +Qed. + +Lemma Done_notmp3_invpp: + forall S1 S2, + stepp S1 S2 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT3)) -> + forall x, + In x (getdst (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + Loc.diff x (R IT3). +Proof. +intros S1 S2 H H0; (try assumption). +induction H as [r|r1 r2 r3 H1 H2 Hrec]; auto. +apply Hrec; auto. +apply Done_notmp3_inv with r1; auto. +Qed. + +Lemma Done_notmp3_invf: + forall S1, + stepInv S1 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT3)) -> + forall x, + In + x + (getdst + (StateToMove (stepf S1) ++ (StateBeing (stepf S1) ++ StateDone (stepf S1)))) -> + Loc.diff x (R IT3). +Proof. +intros S1 H H0; (try assumption). +generalize H; unfold stepInv; intros [Hpath [HSD [HnoO [Hnotmp HnotmpL]]]]. +destruct S1 as [[t1 b1] d1]; set (S1:=(t1, b1, d1)); destruct t1; destruct b1; + auto; apply (Done_notmp3_invpp S1); auto; apply dstep_step; auto; apply f2ind; + unfold S1; auto. +Qed. + +Lemma Done_notmp3_res: + forall S1, + stepInv S1 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT3)) -> + forall x, + In + x + (getdst + (StateToMove (Pmov S1) ++ (StateBeing (Pmov S1) ++ StateDone (Pmov S1)))) -> + Loc.diff x (R IT3). +Proof. +intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). +clear S1; intros S1 Hrec. +destruct S1 as [[t b] d]; set (S1:=(t, b, d)). +unfold S1; rewrite Pmov_equation. +intros H; generalize H; intros [Hpath [HSD [HnoO [Htmp HtmpL]]]]. +destruct t; [destruct b; auto | idtac]; + (intro; apply Hrec; + [apply stepf1_dec | apply (dstep_inv S1); auto; apply f2ind' + | apply Done_notmp3_invf]; auto). +Qed. + +Lemma Done_notmp1_inv: + forall S1 S2, + step S1 S2 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In x (getdst (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1 S2 STEP; inversion STEP; (try (simpl; trivial; fail)); + (repeat (rewrite getdst_app; simpl)); intros. +apply H1; in_tac. +destruct m; apply H1; in_tac. +apply H1; in_tac. +case (Loc.eq x (T r0)); intro. +rewrite e; unfold T; case (Loc.type r0); simpl; split; red; intro; discriminate. +apply H1; apply in_cons_noteq with ( b := T r0 ); (try assumption); in_tac. +apply H3; in_tac. +Qed. + +Lemma Done_notmp1_invpp: + forall S1 S2, + stepp S1 S2 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In x (getdst (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1 S2 H H0; (try assumption). +induction H as [r|r1 r2 r3 H1 H2 Hrec]; auto. +apply Hrec; auto. +apply Done_notmp1_inv with r1; auto. +Qed. + +Lemma Done_notmp1_invf: + forall S1, + stepInv S1 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In + x + (getdst + (StateToMove (stepf S1) ++ (StateBeing (stepf S1) ++ StateDone (stepf S1)))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1 H H0; (try assumption). +generalize H; unfold stepInv; intros [Hpath [HSD [HnoO [Hnotmp HnotmpL]]]]. +destruct S1 as [[t1 b1] d1]; set (S1:=(t1, b1, d1)); destruct t1; destruct b1; + auto; apply (Done_notmp1_invpp S1); auto; apply dstep_step; auto; apply f2ind; + unfold S1; auto. +Qed. + +Lemma Done_notmp1_res: + forall S1, + stepInv S1 -> + (forall x, + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In + x + (getdst + (StateToMove (Pmov S1) ++ (StateBeing (Pmov S1) ++ StateDone (Pmov S1)))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). +clear S1; intros S1 Hrec. +destruct S1 as [[t b] d]; set (S1:=(t, b, d)). +intros H; generalize H; intros [Hpath [HSD [HnoO [Htmp HtmpL]]]]. +unfold S1; rewrite Pmov_equation. +destruct t; [destruct b; auto | idtac]; + (intro; apply Hrec; + [apply stepf1_dec | apply (dstep_inv S1); auto; apply f2ind' + | apply Done_notmp1_invf]; auto). +Qed. + +Lemma Done_notmp1src_inv: + forall S1 S2, + step S1 S2 -> + (forall x, + In x (getsrc (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In x (getsrc (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1 S2 STEP; inversion STEP; (try (simpl; trivial; fail)); + (repeat (rewrite getsrc_app; simpl)); intros. +apply H1; in_tac. +destruct m; apply H1; in_tac. +apply H1; in_tac. +case (Loc.eq x (T r0)); intro. +rewrite e; unfold T; case (Loc.type r0); simpl; split; red; intro; discriminate. +apply H1; apply in_cons_noteq with ( b := T r0 ); (try assumption); in_tac. +apply H3; in_tac. +Qed. + +Lemma Done_notmp1src_invpp: + forall S1 S2, + stepp S1 S2 -> + (forall x, + In x (getsrc (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In x (getsrc (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1 S2 H H0; (try assumption). +induction H as [r|r1 r2 r3 H1 H2 Hrec]; auto. +apply Hrec; auto. +apply Done_notmp1src_inv with r1; auto. +Qed. + +Lemma Done_notmp1src_invf: + forall S1, + stepInv S1 -> + (forall x, + In x (getsrc (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In + x + (getsrc + (StateToMove (stepf S1) ++ (StateBeing (stepf S1) ++ StateDone (stepf S1)))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1 H H0. +generalize H; unfold stepInv; intros [Hpath [HSD [HnoO [Hnotmp HnotmpL]]]]. +destruct S1 as [[t1 b1] d1]; set (S1:=(t1, b1, d1)); destruct t1; destruct b1; + auto; apply (Done_notmp1src_invpp S1); auto; apply dstep_step; auto; + apply f2ind; unfold S1; auto. +Qed. + +Lemma Done_notmp1src_res: + forall S1, + stepInv S1 -> + (forall x, + In x (getsrc (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1)) -> + forall x, + In + x + (getsrc + (StateToMove (Pmov S1) ++ (StateBeing (Pmov S1) ++ StateDone (Pmov S1)))) -> + Loc.diff x (R IT1) /\ Loc.diff x (R FT1). +Proof. +intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). +clear S1; intros S1 Hrec. +destruct S1 as [[t b] d]; set (S1:=(t, b, d)). +intros H; generalize H; intros [Hpath [HSD [HnoO [Htmp HtmpL]]]]. +unfold S1; rewrite Pmov_equation. +destruct t; [destruct b; auto | idtac]; + (intro; apply Hrec; + [apply stepf1_dec | apply (dstep_inv S1); auto; apply f2ind' + | apply Done_notmp1src_invf]; auto). +Qed. + +Lemma dst_tmp2_step: + forall S1 S2, + step S1 S2 -> + forall x, + In x (getdst (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + In x temporaries2 \/ + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))). +Proof. +intros S1 S2 STEP; inversion STEP; (repeat (rewrite getdst_app; simpl)); intros; + (try (right; in_tac)). +destruct m; right; in_tac. +case (Loc.eq x (T r0)); intro. +rewrite e; unfold T; case (Loc.type r0); left; [left | right; left]; trivial. +right; apply in_cons_noteq with ( b := T r0 ); auto; in_tac. +Qed. + +Lemma dst_tmp2_stepp: + forall S1 S2, + stepp S1 S2 -> + forall x, + In x (getdst (StateToMove S2 ++ (StateBeing S2 ++ StateDone S2))) -> + In x temporaries2 \/ + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))). +Proof. +intros S1 S2 H. +induction H as [r|r1 r2 r3 H1 H2 Hrec]; auto. +intros. +elim Hrec with ( x := x ); + [intros H0; (try clear Hrec); (try exact H0) | intros H0; (try clear Hrec) + | try clear Hrec]; auto. +generalize (dst_tmp2_step r1 r2); auto. +Qed. + +Lemma dst_tmp2_stepf: + forall S1, + stepInv S1 -> + forall x, + In + x + (getdst + (StateToMove (stepf S1) ++ (StateBeing (stepf S1) ++ StateDone (stepf S1)))) -> + In x temporaries2 \/ + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))). +Proof. +intros S1 H H0. +generalize H; unfold stepInv; intros [Hpath [HSD [HnoO [Hnotmp HnotmpL]]]]. +destruct S1 as [[t1 b1] d1]; set (S1:=(t1, b1, d1)); destruct t1; destruct b1; + auto; apply (dst_tmp2_stepp S1); auto; apply dstep_step; auto; apply f2ind; + unfold S1; auto. +Qed. + +Lemma dst_tmp2_res: + forall S1, + stepInv S1 -> + forall x, + In + x + (getdst + (StateToMove (Pmov S1) ++ (StateBeing (Pmov S1) ++ StateDone (Pmov S1)))) -> + In x temporaries2 \/ + In x (getdst (StateToMove S1 ++ (StateBeing S1 ++ StateDone S1))). +Proof. +intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). +clear S1; intros S1 Hrec. +destruct S1 as [[t b] d]; set (S1:=(t, b, d)). +intros H; generalize H; intros [Hpath [HSD [HnoO [Htmp HtmpL]]]]. +unfold S1; rewrite Pmov_equation; intros. +destruct t; auto. +destruct b; auto. +elim Hrec with ( y := stepf S1 ) ( x := x ); + [intros H1 | intros H1 | try clear Hrec | try clear Hrec | try assumption]. +left; (try assumption). +apply dst_tmp2_stepf; auto. +apply stepf1_dec; auto. +apply (dstep_inv S1); auto; unfold S1; apply f2ind'; auto. +elim Hrec with ( y := stepf S1 ) ( x := x ); + [intro; left; (try assumption) | intros H1; apply dst_tmp2_stepf; auto | + apply stepf1_dec; auto | + apply (dstep_inv S1); auto; unfold S1; apply f2ind'; auto | try assumption]. +Qed. + +Lemma getdst_lists2moves: + forall srcs dsts, + length srcs = length dsts -> + getsrc (listsLoc2Moves srcs dsts) = srcs /\ + getdst (listsLoc2Moves srcs dsts) = dsts. +Proof. +induction srcs; intros dsts; destruct dsts; simpl; auto; intro; + (try discriminate). +inversion H. +elim IHsrcs with ( dsts := dsts ); auto; intros. +rewrite H2; rewrite H0; auto. +Qed. + +Lemma stepInv_pnilnil: + forall p, + simpleDest p -> + Loc.disjoint (getsrc p) temporaries -> + Loc.disjoint (getdst p) temporaries -> + no_overlap_list p -> stepInv (p, nil, nil). +Proof. +unfold stepInv; simpl; (repeat split); auto. +rewrite app_nil; auto. +generalize (no_overlap_noOverlap (p, nil, nil)). +simpl; (intros H3; apply H3). +generalize H2; unfold no_overlap_state, no_overlap_list; simpl; intro. +rewrite app_nil; auto. +apply disjoint_tmp__noTmp; auto. +Qed. + +Lemma noO_list_pnilnil: + forall (p : Moves), + simpleDest p -> + Loc.disjoint (getsrc p) temporaries -> + Loc.disjoint (getdst p) temporaries -> + no_overlap_list p -> no_overlap_list (StateDone (Pmov (p, nil, nil))). +Proof. +intros; generalize (no_overlapD_res (p, nil, nil)); + unfold no_overlap_stateD, no_overlap_list. +rewrite STM_Pmov; rewrite SB_Pmov; simpl; rewrite app_nil; intro. +apply H3; auto. +apply stepInv_pnilnil; auto. +Qed. + +Lemma dis_srctmp1_pnilnil: + forall (p : Moves), + simpleDest p -> + Loc.disjoint (getsrc p) temporaries -> + Loc.disjoint (getdst p) temporaries -> + no_overlap_list p -> + Loc.disjoint (getsrc (StateDone (Pmov (p, nil, nil)))) temporaries1. +Proof. +intros; generalize (Done_notmp1src_res (p, nil, nil)); simpl. +rewrite STM_Pmov; rewrite SB_Pmov; simpl; rewrite app_nil; intro. +unfold temporaries1. +apply Loc.notin_disjoint; auto. +simpl; intros. +assert (HsI: stepInv (p, nil, nil)); (try apply stepInv_pnilnil); auto. +elim H3 with x; (try assumption). +intros; (repeat split); auto. +intros; split; + (apply Loc.in_notin_diff with ( ll := temporaries ); + [apply Loc.disjoint_notin with (getsrc p) | simpl]; auto). +Qed. + +Lemma dis_dsttmp1_pnilnil: + forall (p : Moves), + simpleDest p -> + Loc.disjoint (getsrc p) temporaries -> + Loc.disjoint (getdst p) temporaries -> + no_overlap_list p -> + Loc.disjoint (getdst (StateDone (Pmov (p, nil, nil)))) temporaries1. +Proof. +intros; generalize (Done_notmp1_res (p, nil, nil)); simpl. +rewrite STM_Pmov; rewrite SB_Pmov; simpl; rewrite app_nil; intro. +unfold temporaries1. +apply Loc.notin_disjoint; auto. +simpl; intros. +assert (HsI: stepInv (p, nil, nil)); (try apply stepInv_pnilnil); auto. +elim H3 with x; (try assumption). +intros; (repeat split); auto. +intros; split; + (apply Loc.in_notin_diff with ( ll := temporaries ); + [apply Loc.disjoint_notin with (getdst p) | simpl]; auto). +Qed. + +Lemma parallel_move_correct': + forall p k rs m, + Loc.norepet (getdst p) -> + no_overlap_list p -> + Loc.disjoint (getsrc p) temporaries -> + Loc.disjoint (getdst p) temporaries -> + (exists rs' , + exec_instrs ge sp (p_move p k) rs m k rs' m /\ + (List.map rs' (getdst p) = List.map rs (getsrc p) /\ + (rs' (R IT3) = rs (R IT3) /\ + (forall l, + Loc.notin l (getdst p) -> Loc.notin l temporaries -> rs' l = rs l))) + ). +Proof. +unfold p_move, P_move. +intros p k rs m Hnorepet HnoOverlap Hdisjointsrc Hdisjointdst. +assert (HsD: simpleDest p); (try (apply norepet_SD; assumption)). +assert (HsI: stepInv (p, nil, nil)); (try (apply stepInv_pnilnil; assumption)). +generalize HsI; unfold stepInv; simpl StateToMove; simpl StateBeing; + (repeat rewrite app_nil); intros [_ [_ [HnoO [Hnotmp _]]]]. +elim (exec_instrs_pmov (StateDone (Pmov (p, nil, nil))) k rs m); auto; + (try apply noO_list_pnilnil); (try apply dis_dsttmp1_pnilnil); + (try apply dis_srctmp1_pnilnil); auto. +intros rs' [Hexec R]; exists rs'; (repeat split); auto. +rewrite <- (Fpmov_correct_map p rs); auto. +apply list_map_exten; intros; rewrite <- R; auto; + (try + (apply Loc.in_notin_diff with ( ll := temporaries ); + [apply Loc.disjoint_notin with (getdst p) | simpl]; auto)). +generalize (dst_tmp2_res (p, nil, nil)); intros. +elim H0 with ( x := r ); + [intros H2; right | + simpl; rewrite app_nil; intros H2; apply In_norepet with (getdst p); auto | + try assumption | rewrite STM_Pmov; rewrite SB_Pmov; auto]. +apply Loc.diff_sym; apply Loc.in_notin_diff with ( ll := temporaries ); + (try assumption). +apply Loc.disjoint_notin with (getdst p); auto. +generalize H2; unfold temporaries, temporaries2; intros; in_tac. +rewrite <- (Fpmov_correct_IT3 p rs); auto; rewrite <- R; + (try (simpl; intro; discriminate)); auto. +intros r H; right; apply (Done_notmp3_res (p, nil, nil)); auto; + (try (rewrite STM_Pmov; rewrite SB_Pmov; auto)). +simpl; rewrite app_nil; intros; apply Loc.in_notin_diff with temporaries; auto. +apply Loc.disjoint_notin with (getdst p); auto. +simpl; right; right; left; trivial. +intros; rewrite <- (Fpmov_correct_ext p rs); auto; rewrite <- R; auto; + (try (apply Loc.in_notin_diff with temporaries; simpl; auto)). +intros r H1; right; generalize (dst_tmp2_res (p, nil, nil)); intros. +elim H2 with ( x := r ); + [intros H3 | simpl; rewrite app_nil; intros H3 | assumption + | rewrite STM_Pmov; rewrite SB_Pmov; auto]. +apply Loc.diff_sym; apply Loc.in_notin_diff with temporaries; auto. +generalize H3; unfold temporaries, temporaries2; intros; in_tac. +apply Loc.diff_sym; apply Loc.in_notin_diff with ( ll := getdst p ); auto. +Qed. + +Lemma parallel_move_correctX: + forall srcs dsts k rs m, + List.length srcs = List.length dsts -> + no_overlap srcs dsts -> + Loc.norepet dsts -> + Loc.disjoint srcs temporaries -> + Loc.disjoint dsts temporaries -> + (exists rs' , + exec_instrs ge sp (parallel_move srcs dsts k) rs m k rs' m /\ + (List.map rs' dsts = List.map rs srcs /\ + (rs' (R IT3) = rs (R IT3) /\ + (forall l, Loc.notin l dsts -> Loc.notin l temporaries -> rs' l = rs l))) ). +Proof. +intros; unfold parallel_move, parallel_move_order; + generalize (parallel_move_correct' (listsLoc2Moves srcs dsts) k rs m). +elim (getdst_lists2moves srcs dsts); auto. +intros heq1 heq2; rewrite heq1; rewrite heq2; unfold p_move. +intros H4; apply H4; auto. +unfold no_overlap_list; rewrite heq1; rewrite heq2; auto. +Qed. + +End parallel_move_correction. |