ported for ppc

1 files changed, 17 insertions, 22 deletions

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.