diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
-rw-r--r-- | backend/CSE3analysisproof.v | 160 |
1 files changed, 40 insertions, 120 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 12048010..66b199cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -478,27 +478,6 @@ Section SOUNDNESS. rewrite negb_true_iff in H. intuition. Qed. - - Lemma reg_min_sound: - forall x y, (reg_min x y) = x \/ (reg_min x y) = y. - Proof. - intros; unfold reg_min. - destruct plt; auto. - Qed. - - Lemma reg_min_rec_sound : - forall (l : list reg) (before : reg), - In (reg_min_rec l before) l \/ - reg_min_rec l before = before. - Proof. - induction l; cbn. - { auto. } - intro bef. - destruct (IHl (reg_min bef a)). - { auto. } - rewrite H. - destruct (reg_min_sound bef a); auto. - Qed. Lemma pick_source_sound : forall (l : list reg), @@ -507,71 +486,47 @@ Section SOUNDNESS. | None => True end. Proof. - destruct l; cbn; trivial. - destruct (reg_min_rec_sound l r); auto. + unfold pick_source. + destruct l; simpl; trivial. + left; trivial. Qed. - + Hint Resolve pick_source_sound : cse3. - Theorem get_sources_sound : - forall l src rs m x, - (forall i eq, - In i l -> - eq_catalog ctx i = Some eq -> - sem_eq eq rs m) -> - (In src (get_sources (ctx := ctx) x l)) -> - rs # src = rs # x. - Proof. - induction l; cbn; intros until x; intros SEM IN. - contradiction. - destruct (eq_catalog ctx a) eqn:CATALOG. - 2: eauto using IHl; fail. - pose proof (SEM a e) as SEMeq. - destruct e; cbn in *. - destruct (is_smove eq_op && peq x eq_lhs) eqn:CORRECT. - 2: eauto using IHl; fail. - destruct eq_args. - eauto using IHl; fail. - destruct eq_args. - 2: eauto using IHl; fail. - cbn in IN. - destruct IN. - 2: eauto using IHl; fail. - rewrite andb_true_iff in CORRECT. - intuition. - destruct (peq x eq_lhs). - 2: discriminate. - subst eq_lhs. - destruct (is_smove eq_op). - 2: discriminate. - subst eq_op. - subst src. - cbn in H2. - symmetry. - assumption. - Qed. - Theorem forward_move_sound : forall rel rs m x, (sem_rel rel rs m) -> rs # (forward_move (ctx := ctx) rel x) = rs # x. Proof. - unfold forward_move. - intros until x; intros REL. - pose proof (pick_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK. - destruct pick_source. + unfold sem_rel, forward_move. + intros until x. + intro REL. + pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT. + destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))). 2: reflexivity. - apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m). - 2: assumption. - intros i eq IN CATALOG. - rewrite PSet.elements_spec in IN. - rewrite PSet.ginter in IN. - rewrite andb_true_iff in IN. - destruct IN. - unfold sem_rel in REL. - apply REL with (i:=i); assumption. + destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. + 2: reflexivity. + specialize REL with (i := r) (eq0 := eq). + destruct (is_smove (eq_op eq)) as [MOVE | ]. + 2: reflexivity. + destruct (peq x (eq_lhs eq)). + 2: reflexivity. + simpl. + subst x. + rewrite PSet.elements_spec in ELEMENT. + rewrite PSet.ginter in ELEMENT. + rewrite andb_true_iff in ELEMENT. + unfold sem_eq in REL. + rewrite MOVE in REL. + simpl in REL. + destruct (eq_args eq) as [ | h t]. + reflexivity. + destruct t. + 2: reflexivity. + simpl in REL. + intuition congruence. Qed. - + Hint Resolve forward_move_sound : cse3. Theorem forward_move_l_sound : @@ -744,28 +699,6 @@ Section SOUNDNESS. + congruence. Qed. - - Lemma arglist_idem_write: - forall { A : Type} args (rs : Regmap.t A) dst, - (rs # dst <- (rs # dst)) ## args = rs ## args. - Proof. - induction args; trivial. - intros. cbn. - f_equal; trivial. - apply Regmap.gsident. - Qed. - - Lemma sem_rhs_idem_write: - forall sop args rs dst m v, - sem_rhs sop args rs m v -> - sem_rhs sop args (rs # dst <- (rs # dst)) m v. - Proof. - intros. - unfold sem_rhs in *. - rewrite arglist_idem_write. - assumption. - Qed. - Theorem oper2_sound: forall no dst sop args rel rs m v, sem_rel rel rs m -> @@ -793,17 +726,6 @@ Section SOUNDNESS. rewrite Regmap.gss. apply sem_rhs_depends_on_args_only; auto. } - intros INi. - destruct (PSet.contains rel e) eqn:CONTAINSe. - { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe. - pose proof (REL i eq CONTAINS INi) as RELi. - unfold sem_eq in *. - cbn in RELe. - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). - rewrite Regmap.gsident. - apply sem_rhs_idem_write. - assumption. - } rewrite PSet.gaddo in CONTAINS by congruence. apply (kill_reg_sound rel rs m dst v REL i eq); auto. Qed. @@ -899,7 +821,11 @@ Section SOUNDNESS. subst. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - - destruct rhs_find as [src |] eqn:RHS_FIND. + - destruct (is_trivial_sym_op sop). + { + apply kill_reg_sound; auto. + } + destruct rhs_find as [src |] eqn:RHS_FIND. + destruct (Compopts.optim_CSE3_glb tt). * apply sem_rel_glb; split. ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. @@ -907,18 +833,12 @@ Section SOUNDNESS. 2: eassumption. rewrite <- (sem_rhs_det SOUND RHS). apply move_sound; auto. - ** apply sem_rel_glb; split. - *** apply oper1_sound; auto. - apply forward_move_rhs_sound; auto. - *** apply oper1_sound; auto. - * apply sem_rel_glb; split. ** apply oper1_sound; auto. apply forward_move_rhs_sound; auto. - ** apply oper1_sound; auto. - + apply sem_rel_glb; split. - * apply oper1_sound; auto. - apply forward_move_rhs_sound; auto. - * apply oper1_sound; auto. + * ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + + apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. Qed. Hint Resolve oper_sound : cse3. |