diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 10:14:13 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 10:14:13 +0200 |
| commit | 676d1ae6324d3c2f13e20efdcff3fbda9aab1686 (patch) | |
| tree | 7efc457b9692980163c7b2b5324f4b2580429465 | |
| parent | da32340a8c063c9dc0847d01e7ec5c77ce75f3b1 (diff) | |
| download | compcert-kvx-676d1ae6324d3c2f13e20efdcff3fbda9aab1686.tar.gz compcert-kvx-676d1ae6324d3c2f13e20efdcff3fbda9aab1686.zip | |
ça avance
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 2b6a8450..b2fa79d1 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -890,8 +890,35 @@ Proof. intros rr; destruct rr; Simpl. + unfold parexec_store_q_offset. + simpl. destruct (gpreg_q_expand rs) as [s0 s1]. simpl. + unfold exec_store_deps_offset. + repeat rewrite H0. + repeat rewrite H. + destruct Ge. + destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ] eqn:MEML0; simpl. + ++ rewrite MEML0. + destruct (Mem.storev _ _ _ (rsr s1)) as [mem1 | ] eqn:MEML1; simpl. + * rewrite (assign_diff sr _ (# s1)) by apply ppos_pmem_discr. + rewrite (assign_diff sr _ (# ra)) by apply ppos_pmem_discr. + repeat rewrite H0. + rewrite MEML1. + eexists; split. + reflexivity. + rewrite (assign_eq _ pmem). + split; trivial. + intro r. + rewrite (assign_diff _ _ (# r)) by apply ppos_pmem_discr. + rewrite (assign_diff _ _ (# r)) by apply ppos_pmem_discr. + congruence. + * rewrite (assign_diff sr pmem (# s1)) by apply ppos_pmem_discr. + rewrite (assign_diff sr pmem (# ra)) by apply ppos_pmem_discr. + repeat rewrite H0. + rewrite MEML1. + reflexivity. + ++ rewrite MEML0. + reflexivity. (* Allocframe *) - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. * eexists; repeat split. |