diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-27 15:21:11 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-27 15:21:11 +0100 |
| commit | f59c540aa7cf85c89ee0cb07c20374c8ad76a46c (patch) | |
| tree | de0849bc8c130598ce39ac472bc90f282ba4ab7b /backend/CSE3analysisproof.v | |
| parent | 9646053ba537d24f973e104aebd80500381ce11d (diff) | |
| download | compcert-kvx-f59c540aa7cf85c89ee0cb07c20374c8ad76a46c.tar.gz compcert-kvx-f59c540aa7cf85c89ee0cb07c20374c8ad76a46c.zip | |
new CSE3
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 53 |
1 files changed, 44 insertions, 9 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 66b199cc..ea4d37ca 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -699,6 +699,28 @@ 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 -> @@ -726,6 +748,17 @@ 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. @@ -821,11 +854,7 @@ Section SOUNDNESS. subst. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - - destruct (is_trivial_sym_op sop). - { - apply kill_reg_sound; auto. - } - destruct rhs_find as [src |] eqn:RHS_FIND. + - 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. @@ -833,12 +862,18 @@ 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 forward_move_rhs_sound; auto. - + 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. Qed. Hint Resolve oper_sound : cse3. |