Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass

2 files changed, 73 insertions, 3 deletions

diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v
index d48dabf3..4592f408 100644
--- a/powerpc/CSE2deps.v
+++ b/powerpc/CSE2deps.v
@@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' :=
     (base :: nil), (base' :: nil) =>
     if peq base base'
     then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk)
-    else true  | _, _, _, _ => true
+    else true
+  | (Ainstack ofs), (Ainstack ofs'), _, _ =>
+    negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+  | _, _, _, _ => true
   end.
diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v
index 123341da..ede09dd6 100644
--- a/powerpc/CSE2depsproof.v
+++ b/powerpc/CSE2depsproof.v
@@ -111,6 +111,66 @@ Section MEMORY_WRITE.
   Qed.
   End INDEXED_AWAY.
 End MEMORY_WRITE.
+
+Section STACK_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  
+  Variable addrw addrr valw : val.
+  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+  Section INDEXED_AWAY.
+  Variable ofsw ofsr : ptrofs.
+  Hypothesis ADDRW : eval_addressing genv sp
+                       (Ainstack ofsw) nil = Some addrw.
+  Hypothesis ADDRR : eval_addressing genv sp
+                       (Ainstack ofsr) nil = Some addrr.
+
+  Lemma stack_load_store_away1 :
+    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.
+    
+    pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+    pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+    unfold largest_size_chunk in *.
+
+    inv ADDRR.
+    inv ADDRW.
+
+    destruct sp; 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 ofsr) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW];
+              rewrite OFSW).
+    all: try rewrite ptrofs_modulus in *.
+    all: destruct Archi.ptr64.
+
+    all: intuition lia.
+  Qed.
+  
+  Theorem stack_load_store_away :
+    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.
+    repeat rewrite andb_true_iff in SWAP.
+    repeat rewrite orb_true_iff in SWAP.
+    repeat rewrite Z.leb_le in SWAP.
+    apply stack_load_store_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End STACK_WRITE.
 End SOUNDNESS.
 
 
@@ -131,7 +191,7 @@ Proof.
   intros until rs.
   intros ADDR ADDR' OVERLAP STORE.
   destruct addr; destruct addr'; try discriminate.
-  { (* Aindexed / Aindexed *)
+- (* Aindexed / Aindexed *)
   destruct args as [ | base [ | ]]. 1,3: discriminate.
   destruct args' as [ | base' [ | ]]. 1,3: discriminate.
   simpl in OVERLAP.
@@ -141,7 +201,14 @@ Proof.
   2: discriminate.
   simpl in *.
   eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
-  }
+- (* Ainstack / Ainstack *)
+  destruct args. 2: discriminate.
+  destruct args'. 2: discriminate.
+  cbn in OVERLAP.
+  destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  cbn in *.
+  eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
 Qed.
 
 End SOUNDNESS.