From 10cb118e1201268b993973852499d38ce6b8d890 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 17:44:04 +0100 Subject: ported for ppc --- powerpc/CSE2depsproof.v | 39 +++++++++++++++++---------------------- 1 file changed, 17 insertions(+), 22 deletions(-) (limited to 'powerpc/CSE2depsproof.v') diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v index 2112a230..a047b02a 100644 --- a/powerpc/CSE2depsproof.v +++ b/powerpc/CSE2depsproof.v @@ -9,7 +9,7 @@ Require Import CSE2 CSE2deps. Require Import Lia. Lemma ptrofs_size : - Ptrofs.wordsize = 32%nat. + Ptrofs.wordsize = if Archi.ptr64 then 64%nat else 32%nat. Proof. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. @@ -17,7 +17,7 @@ Proof. Qed. Lemma ptrofs_modulus : - Ptrofs.modulus = 4294967296. + Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296. Proof. unfold Ptrofs.modulus. rewrite ptrofs_size. @@ -34,23 +34,22 @@ Section MEMORY_WRITE. Variable chunkw chunkr : memory_chunk. Variable base : val. - Variable addrw addrr valw valr : val. + Variable addrw addrr valw : val. Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. - Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. Section INDEXED_AWAY. - Variable ofsw ofsr : int. + Variable ofsw ofsr : ptrofs. Hypothesis ADDRW : eval_addressing genv sp (Aindexed ofsw) (base :: nil) = Some addrw. Hypothesis ADDRR : eval_addressing genv sp (Aindexed ofsr) (base :: nil) = Some addrr. Lemma load_store_away1 : - forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, - forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, - forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr - \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw, - Mem.loadv chunkr m2 addrr = Some valr. + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intros. @@ -62,28 +61,25 @@ Section MEMORY_WRITE. simpl in *. inv ADDRR. inv ADDRW. - rewrite <- READ. destruct base; try discriminate. eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). exact STORE. right. - all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR]; + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; rewrite OFSR). - all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW]; + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; rewrite OFSW). all: try rewrite ptrofs_modulus in *. - - all: unfold Ptrofs.of_int. all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). all: intuition lia. Qed. Theorem load_store_away : - can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true -> - Mem.loadv chunkr m2 addrr = Some valr. + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intro SWAP. unfold can_swap_accesses_ofs in SWAP. @@ -105,16 +101,15 @@ Section SOUNDNESS. Lemma may_overlap_sound: forall m m' : mem, - forall chunk addr args chunk' addr' args' v a a' vl rs, + forall chunk addr args chunk' addr' args' v a a' 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. + (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a'). Proof. intros until rs. - intros ADDR ADDR' OVERLAP STORE LOAD. + intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. { (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. @@ -122,7 +117,7 @@ Proof. simpl in OVERLAP. destruct (peq base base'). 2: discriminate. subst base'. - destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. 2: discriminate. simpl in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. -- cgit