From 676d1ae6324d3c2f13e20efdcff3fbda9aab1686 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 10:14:13 +0200 Subject: ça avance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asmblockdeps.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'mppa_k1c/Asmblockdeps.v') 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. -- cgit