diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 11:27:59 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 11:27:59 +0100 |
| commit | 3fc937ddc8f82525081bca67818ca87f448f618e (patch) | |
| tree | 42c8081afdbb150477fd043095d5cff942764cf1 /backend/CSE2proof.v | |
| parent | 44811b4917b69e9a33efe5ab75ceb3b01f6594fc (diff) | |
| download | compcert-kvx-3fc937ddc8f82525081bca67818ca87f448f618e.tar.gz compcert-kvx-3fc937ddc8f82525081bca67818ca87f448f618e.zip | |
modularize proof
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 39 |
1 files changed, 10 insertions, 29 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 206dbf30..90179f82 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -795,36 +795,17 @@ Proof. rewrite SEMx. apply op_depends_on_memory_correct; auto. } - destruct addr; destruct addr0; simpl; trivial. - { (* Aindexed / Aindexed *) - destruct args as [ | base [ | ]]; simpl; trivial. - destruct args0 as [ | base0 [ | ]]; simpl; trivial. - destruct (peq (forward_move rel base) base0); simpl; trivial. - subst base0. - destruct (can_swap_accesses_ofs z0 chunk0 z chunk) eqn:SWAP; simpl; trivial. - simpl in *. - erewrite forward_move_rs in * by exact SEM. - destruct (eval_addressing genv sp (Aindexed z0) ((rs # base) :: nil)) eqn:ADDR0; simpl; trivial. + destruct may_overlap eqn:OVERLAP; simpl; trivial. + destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0. symmetry. - eapply load_store_away; eauto. - } - { (* Aglobal / Aglobal *) - destruct args; destruct args0; simpl; trivial. - destruct (peq i i1). - { - subst i1. - destruct (can_swap_accesses_ofs (Ptrofs.unsigned i2) chunk0 - (Ptrofs.unsigned i0) chunk) eqn:SWAP; simpl; trivial. - simpl in *. - destruct (eval_addressing genv sp (Aglobal i i2) nil) eqn:ADDR1; simpl; trivial. - symmetry. - eapply load_store_glob_away; eauto. - } - simpl in *. - destruct (eval_addressing genv sp (Aglobal i1 i2) nil) eqn:ADDR1; simpl; trivial. - symmetry. - eapply load_store_diff_globals; eauto. - } + eapply may_overlap_sound with (args := (map (forward_move rel) args)). + erewrite forward_move_map by eassumption. + exact ADDR. + exact ADDR0. + exact OVERLAP. + exact STORE. + symmetry; assumption. + assumption. Qed. End SOUNDNESS. |