From 577d3dbeb54aaf23db19dddf149c48764e20c58d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 11:30:23 +0100 Subject: moved away x86-dependent parts --- backend/CSE2proof.v | 38 -------------------------------------- 1 file changed, 38 deletions(-) (limited to 'backend/CSE2proof.v') diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 90179f82..8cc87275 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -734,44 +734,6 @@ Proof. apply op_depends_on_memory_correct; auto. } Qed. - -Lemma may_overlap_sound: - forall m m' : mem, - forall chunk addr args chunk' addr' args' v a a' vl rs, - (eval_addressing genv sp addr (rs ## args)) = Some a -> - (eval_addressing genv sp addr' (rs ## args')) = Some a' -> - (may_overlap chunk addr args chunk' addr' args') = false -> - (Mem.storev chunk m a v) = Some m' -> - (Mem.loadv chunk' m a') = Some vl -> - (Mem.loadv chunk' m' a') = Some vl. -Proof. - intros until rs. - intros ADDR ADDR' OVERLAP STORE LOAD. - destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) - destruct args as [ | base [ | ]]. 1,3: discriminate. - destruct args' as [ | base' [ | ]]. 1,3: discriminate. - simpl in OVERLAP. - destruct (peq base base'). 2: discriminate. - subst base'. - destruct (can_swap_accesses_ofs z0 chunk' z chunk) eqn:SWAP. - 2: discriminate. - simpl in *. - eapply load_store_away; eassumption. - } - { (* Aglobal / Aglobal *) - destruct args. 2: discriminate. - destruct args'. 2: discriminate. - simpl in *. - destruct (peq i i1). - { - subst i1. - rewrite negb_false_iff in OVERLAP. - eapply load_store_glob_away; eassumption. - } - eapply load_store_diff_globals; eassumption. - } -Qed. Lemma kill_store_sound : forall m m' : mem, -- cgit