From fbfbc3c4cbe250a40513e5dabcd6930b39043ea3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 18:14:23 +0100
Subject: playing with offsets

---
 backend/CSE2proof.v | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 67 insertions(+), 1 deletion(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 82fa8a28..4dd8b054 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -14,6 +14,7 @@ Require Import Globalenvs Values.
 Require Import Linking Values Memory Globalenvs Events Smallstep.
 Require Import Registers Op RTL.
 Require Import CSE2.
+Require Import Lia.
 
 Lemma args_unaffected:
   forall rs : regset,
@@ -697,6 +698,71 @@ Proof.
 Qed.
 End SAME_MEMORY.
 
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  Variable ofsw ofsr : Z.
+
+  Hypothesis RANGEW : 0 <= ofsw <= 18446744073709551608.
+  Hypothesis RANGER : 0 <= ofsr <= 18446744073709551608.
+
+  Lemma size_chunk_bounded :
+    forall chunk, 0 <= size_chunk chunk <= 8.
+  Proof.
+    destruct chunk; simpl; lia.
+  Qed.
+  
+  Hypothesis no_overlap:
+         ofsw + size_chunk chunkw <= ofsr
+      \/ ofsr + size_chunk chunkr <= ofsw.
+
+  Variable addrw addrr valw valr : val.
+  
+  Hypothesis ADDRW : eval_addressing genv sp
+                       (Aindexed ofsw) (base :: nil) = Some addrw. 
+  Hypothesis ADDRR : eval_addressing genv sp
+                       (Aindexed ofsr) (base :: nil) = Some addrr.
+  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+  Hypothesis READ : Mem.loadv chunkr m addrr = Some valr.
+
+  Theorem load_store_away :
+    Mem.loadv chunkr m2 addrr = Some valr.
+  Proof.
+    pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded.
+    pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded.
+    
+    destruct addrr ; simpl in * ; try discriminate.
+    unfold eval_addressing in *.
+    destruct Archi.ptr64 eqn:PTR64.
+    {
+      unfold eval_addressing64 in *.
+      inv ADDRW.
+      destruct base; simpl in *; try discriminate.
+      rewrite PTR64 in *.
+      inv ADDRR.
+      rewrite <- READ.
+      eapply Mem.load_store_other.
+      exact STORE.
+      right.
+      destruct (Ptrofs.unsigned_add_either i0
+                  (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR];
+        rewrite OFSR.
+      all: destruct (Ptrofs.unsigned_add_either i0
+                  (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW];
+        rewrite OFSW.
+      all: unfold Ptrofs.of_int64.
+      all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
+      all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
+      all: change Ptrofs.modulus with 18446744073709551616.
+      all: intuition lia.
+    }
+    {
+      destruct base; simpl in *; try discriminate.
+    }
+  Qed.
+End MEMORY_WRITE.
+
 Lemma kill_mem_sound :
   forall m m' : mem,
   forall rel : RELATION.t,
@@ -1305,4 +1371,4 @@ Proof.
   exact step_simulation.
 Qed.
 
-End PRESERVATION.
\ No newline at end of file
+End PRESERVATION.
-- 
cgit 


From 036fc22224c8d171a90b608f6146e742a51e0a25 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 19:10:35 +0100
Subject: works on x86 x86_64

---
 backend/CSE2proof.v | 76 +++++++++++++++++++++++++++++++++--------------------
 1 file changed, 47 insertions(+), 29 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 4dd8b054..55ec653c 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -704,12 +704,18 @@ Section MEMORY_WRITE.
   Variable base : val.
   Variable ofsw ofsr : Z.
 
+  Definition max_chunk_size := 8.
+  (*
   Hypothesis RANGEW : 0 <= ofsw <= 18446744073709551608.
   Hypothesis RANGER : 0 <= ofsr <= 18446744073709551608.
-
+   *)
+  Hypothesis RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size.
+  Hypothesis RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size.
+  
   Lemma size_chunk_bounded :
-    forall chunk, 0 <= size_chunk chunk <= 8.
+    forall chunk, 0 <= size_chunk chunk <= max_chunk_size.
   Proof.
+    unfold max_chunk_size.
     destruct chunk; simpl; lia.
   Qed.
   
@@ -731,35 +737,47 @@ Section MEMORY_WRITE.
   Proof.
     pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded.
     pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded.
-    
+    unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded.
+    try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *.
+    try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *.
     destruct addrr ; simpl in * ; try discriminate.
     unfold eval_addressing in *.
-    destruct Archi.ptr64 eqn:PTR64.
-    {
-      unfold eval_addressing64 in *.
-      inv ADDRW.
-      destruct base; simpl in *; try discriminate.
-      rewrite PTR64 in *.
-      inv ADDRR.
-      rewrite <- READ.
-      eapply Mem.load_store_other.
-      exact STORE.
-      right.
-      destruct (Ptrofs.unsigned_add_either i0
-                  (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR];
-        rewrite OFSR.
-      all: destruct (Ptrofs.unsigned_add_either i0
-                  (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW];
-        rewrite OFSW.
-      all: unfold Ptrofs.of_int64.
-      all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
-      all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
-      all: change Ptrofs.modulus with 18446744073709551616.
-      all: intuition lia.
-    }
-    {
-      destruct base; simpl in *; try discriminate.
-    }
+    destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate.
+    rewrite PTR64 in *.
+    
+    inv ADDRR.
+    inv ADDRW.
+    rewrite <- READ.
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+ 
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW];
+              rewrite OFSW).
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW];
+              rewrite OFSW).
+    
+    all: unfold Ptrofs.of_int64.
+    all: unfold Ptrofs.of_int.
+   
+
+    all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
+    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
+    all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
+    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
+
+    all: try change Ptrofs.modulus with 4294967296.
+    all: try change Ptrofs.modulus with 18446744073709551616.
+   
+    all: intuition lia.
   Qed.
 End MEMORY_WRITE.
 
-- 
cgit 


From f7ea436ac282b6a4a8ddb2281b6e1d86eee46286 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 19:50:21 +0100
Subject: swap predicate

---
 backend/CSE2proof.v | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 55ec653c..6d5496fd 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -704,14 +704,6 @@ Section MEMORY_WRITE.
   Variable base : val.
   Variable ofsw ofsr : Z.
 
-  Definition max_chunk_size := 8.
-  (*
-  Hypothesis RANGEW : 0 <= ofsw <= 18446744073709551608.
-  Hypothesis RANGER : 0 <= ofsr <= 18446744073709551608.
-   *)
-  Hypothesis RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size.
-  Hypothesis RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size.
-  
   Lemma size_chunk_bounded :
     forall chunk, 0 <= size_chunk chunk <= max_chunk_size.
   Proof.
@@ -719,10 +711,6 @@ Section MEMORY_WRITE.
     destruct chunk; simpl; lia.
   Qed.
   
-  Hypothesis no_overlap:
-         ofsw + size_chunk chunkw <= ofsr
-      \/ ofsr + size_chunk chunkr <= ofsw.
-
   Variable addrw addrr valw valr : val.
   
   Hypothesis ADDRW : eval_addressing genv sp
@@ -732,9 +720,15 @@ Section MEMORY_WRITE.
   Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
   Hypothesis READ : Mem.loadv chunkr m addrr = Some valr.
 
-  Theorem load_store_away :
+  Lemma load_store_away1 :
+    forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size,
+    forall RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size,
+    forall SWAPPABLE :    ofsw + size_chunk chunkw <= ofsr
+                       \/ ofsr + size_chunk chunkr <= ofsw,
     Mem.loadv chunkr m2 addrr = Some valr.
   Proof.
+    intros.
+    
     pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded.
     pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded.
     unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded.
@@ -779,6 +773,18 @@ Section MEMORY_WRITE.
    
     all: intuition lia.
   Qed.
+  
+  Theorem load_store_away :
+    can_swap_accesses_ofs ofsr chunkr ofsw chunkw = true ->
+    Mem.loadv chunkr m2 addrr = Some valr.
+  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 load_store_away1; intuition.
+  Qed.
 End MEMORY_WRITE.
 
 Lemma kill_mem_sound :
-- 
cgit 


From cf56eea4e093f25a5c01ccac5ede2a69b568af7a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 20:16:16 +0100
Subject: load_store_away

---
 backend/CSE2proof.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 6d5496fd..c6bb00dd 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -783,7 +783,8 @@ Section MEMORY_WRITE.
     repeat rewrite andb_true_iff in SWAP.
     repeat rewrite orb_true_iff in SWAP.
     repeat rewrite Z.leb_le in SWAP.
-    apply load_store_away1; intuition.
+    apply load_store_away1.
+    all: tauto.
   Qed.
 End MEMORY_WRITE.
 
-- 
cgit 


From 3601929b68ced3777c05cd2861847a111603abee Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 21:34:35 +0100
Subject: kill_store1_sound

---
 backend/CSE2proof.v | 44 +++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 41 insertions(+), 3 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index c6bb00dd..3c42f6e1 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -811,6 +811,44 @@ Proof.
   }
 Qed.
 
+Lemma kill_store1_sound :
+  forall m m' : mem,
+  forall rel : RELATION.t,
+  forall chunk addr args a v rs,
+    (eval_addressing genv sp addr (rs ## args)) = Some a ->
+    (Mem.storev chunk m a v) = Some m' ->
+    sem_rel m rel rs -> sem_rel m' (kill_store1 chunk addr args rel) rs.
+Proof.
+  unfold sem_rel, sem_reg.
+  intros until rs.
+  intros ADDR STORE SEM x.
+  pose proof (SEM x) as SEMx.
+  unfold kill_store1.
+  rewrite PTree.gfilter1.
+  destruct (rel ! x) as [ sv | ].
+  2: reflexivity.
+  destruct sv; simpl in *; trivial.
+  {
+    destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial.
+    rewrite SEMx.
+    apply op_depends_on_memory_correct; auto.
+  }
+  destruct addr; destruct addr0; simpl; trivial.
+  destruct args as [ | base [ | ]]; simpl; trivial.
+  destruct args0 as [ | base0 [ | ]]; simpl; trivial.
+  destruct (peq base base0); simpl; trivial.
+  subst base0.
+  destruct (can_swap_accesses_ofs z0 chunk0 z chunk) eqn:SWAP; simpl; trivial.
+  simpl in *.
+  destruct (eval_addressing genv sp (Aindexed z0) (rs # base :: nil)) eqn:ADDR0; simpl; trivial.
+  symmetry.
+  eapply load_store_away.
+  exact ADDR.
+  exact ADDR0.
+  exact STORE.
+  congruence.
+  assumption.
+Qed. 
 End SOUNDNESS.
 
 Definition match_prog (p tp: RTL.program) :=
@@ -1193,9 +1231,9 @@ Proof.
   unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial.
+  apply sem_rel_b_ge with (rb2 := Some (kill_store chunk addr args mpc)); trivial.
   {
-  replace (Some (kill_mem mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+  replace (Some (kill_store chunk addr args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
   {
     eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
     2: apply apply_instr'_bot.
@@ -1207,7 +1245,7 @@ Proof.
   rewrite H.
   reflexivity.
   }
-  apply (kill_mem_sound' sp m).
+  apply (kill_store_sound' sp m).
   assumption.
   
 (* call *)
-- 
cgit 


From 93bf7e0925b1c11e1874ae5f651970db2bd9823d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 21:55:54 +0100
Subject: kill_store_sound

---
 backend/CSE2proof.v | 35 +++++++++++++++++++++++++----------
 1 file changed, 25 insertions(+), 10 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 3c42f6e1..cd9f5f46 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -502,6 +502,20 @@ Proof.
   destruct s; congruence.
 Qed.
 
+
+Lemma forward_move_rs:
+  forall rel arg rs,
+    sem_rel rel rs ->
+    rs # (forward_move rel arg) = rs # arg.
+Proof.
+  unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
+  intros until rs.
+  intro REL.
+  pose proof (REL arg) as RELarg.
+  destruct (rel ! arg); trivial.
+  destruct s; congruence.
+Qed.
+
 Lemma oper_sound :
   forall rel : RELATION.t,
   forall op : operation,
@@ -811,19 +825,19 @@ Proof.
   }
 Qed.
 
-Lemma kill_store1_sound :
+Lemma kill_store_sound :
   forall m m' : mem,
   forall rel : RELATION.t,
   forall chunk addr args a v rs,
     (eval_addressing genv sp addr (rs ## args)) = Some a ->
     (Mem.storev chunk m a v) = Some m' ->
-    sem_rel m rel rs -> sem_rel m' (kill_store1 chunk addr args rel) rs.
+    sem_rel m rel rs -> sem_rel m' (kill_store chunk addr args rel) rs.
 Proof.
   unfold sem_rel, sem_reg.
   intros until rs.
   intros ADDR STORE SEM x.
   pose proof (SEM x) as SEMx.
-  unfold kill_store1.
+  unfold kill_store, kill_store1.
   rewrite PTree.gfilter1.
   destruct (rel ! x) as [ sv | ].
   2: reflexivity.
@@ -836,18 +850,19 @@ Proof.
   destruct addr; destruct addr0; simpl; trivial.
   destruct args as [ | base [ | ]]; simpl; trivial.
   destruct args0 as [ | base0 [ | ]]; simpl; trivial.
-  destruct (peq base base0); simpl; trivial.
+  destruct (peq (forward_move rel base) base0); simpl; trivial.
   subst base0.
   destruct (can_swap_accesses_ofs z0 chunk0 z chunk) eqn:SWAP; simpl; trivial.
   simpl in *.
-  destruct (eval_addressing genv sp (Aindexed z0) (rs # base :: nil)) eqn:ADDR0; simpl; trivial.
+  erewrite forward_move_rs in * by exact SEM.
+  destruct (eval_addressing genv sp (Aindexed z0) ((rs # base) :: nil)) eqn:ADDR0; simpl; trivial.
   symmetry.
   eapply load_store_away.
-  exact ADDR.
-  exact ADDR0.
-  exact STORE.
-  congruence.
-  assumption.
+  - exact ADDR.
+  - exact ADDR0.
+  - exact STORE.
+  - congruence.
+  - assumption.
 Qed. 
 End SOUNDNESS.
 
-- 
cgit 


From a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 06:13:05 +0100
Subject: with indexed/indexed alias analysis for x86

---
 backend/CSE2proof.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index cd9f5f46..e65d9194 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -951,6 +951,7 @@ Definition fmap_sem' := fmap_sem fundef unit ge.
 Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
 Definition subst_args_ok' := subst_args_ok fundef unit ge.
 Definition kill_mem_sound' := kill_mem_sound fundef unit ge.
+Definition kill_store_sound' := kill_store_sound fundef unit ge.
 
 Lemma sem_rel_b_ge:
   forall rb1 rb2 : RB.t,
@@ -1260,8 +1261,7 @@ Proof.
   rewrite H.
   reflexivity.
   }
-  apply (kill_store_sound' sp m).
-  assumption.
+  eapply (kill_store_sound' sp m); eassumption.
   
 (* call *)
 - econstructor; split.
-- 
cgit 


From c4f88ed5581ffb71e7ed5824c7503e8ce08165df Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 08:58:01 +0100
Subject: globals alias analysis for x86

---
 backend/CSE2proof.v | 67 +++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 57 insertions(+), 10 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index e65d9194..ada0eb00 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -716,7 +716,6 @@ Section MEMORY_WRITE.
   Variable m m2 : mem.
   Variable chunkw chunkr : memory_chunk.
   Variable base : val.
-  Variable ofsw ofsr : Z.
 
   Lemma size_chunk_bounded :
     forall chunk, 0 <= size_chunk chunk <= max_chunk_size.
@@ -726,13 +725,15 @@ Section MEMORY_WRITE.
   Qed.
   
   Variable addrw addrr valw valr : 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 : Z.
   Hypothesis ADDRW : eval_addressing genv sp
                        (Aindexed ofsw) (base :: nil) = Some addrw. 
   Hypothesis ADDRR : eval_addressing genv sp
                        (Aindexed ofsr) (base :: nil) = Some addrr.
-  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
-  Hypothesis READ : Mem.loadv chunkr m addrr = Some valr.
 
   Lemma load_store_away1 :
     forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size,
@@ -800,6 +801,47 @@ Section MEMORY_WRITE.
     apply load_store_away1.
     all: tauto.
   Qed.
+  End INDEXED_AWAY.
+
+  Section DIFFERENT_GLOBALS.
+    Variable ofsw ofsr : ptrofs.
+    Hypothesis symw symr : ident.
+    Hypothesis ADDRW : eval_addressing genv sp
+                                       (Aglobal symw ofsw) nil = Some addrw. 
+    Hypothesis ADDRR : eval_addressing genv sp
+                                       (Aglobal symr ofsr) nil = Some addrr.
+    
+    Lemma load_store_diff_globals :
+      symw <> symr ->
+      Mem.loadv chunkr m2 addrr = Some valr.
+    Proof.
+      intros.
+      unfold eval_addressing in *.
+      destruct Archi.ptr64 eqn:PTR64; simpl in *.
+      rewrite PTR64 in *.
+      2: simpl in *; discriminate.
+      unfold Genv.symbol_address in *.
+      unfold Genv.find_symbol in *.
+      destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW.
+      2: simpl in STORE; discriminate.
+      destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR.
+      2: simpl in READ; discriminate.
+      assert (br <> bw).
+      {
+        intro EQ.
+        subst br.
+        assert (symr = symw).
+        {
+          eapply Genv.genv_vars_inj; eauto.
+        }
+        congruence.
+      }
+      rewrite <- READ.
+      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw).
+      - exact STORE.
+      - left. assumption.
+    Qed.
+  End DIFFERENT_GLOBALS.
 End MEMORY_WRITE.
 
 Lemma kill_mem_sound :
@@ -848,6 +890,7 @@ Proof.
     apply op_depends_on_memory_correct; auto.
   }
   destruct addr; destruct addr0; simpl; trivial.
+  { (* Aindexed / Aindexed *)
   destruct args as [ | base [ | ]]; simpl; trivial.
   destruct args0 as [ | base0 [ | ]]; simpl; trivial.
   destruct (peq (forward_move rel base) base0); simpl; trivial.
@@ -857,12 +900,16 @@ Proof.
   erewrite forward_move_rs in * by exact SEM.
   destruct (eval_addressing genv sp (Aindexed z0) ((rs # base) :: nil)) eqn:ADDR0; simpl; trivial.
   symmetry.
-  eapply load_store_away.
-  - exact ADDR.
-  - exact ADDR0.
-  - exact STORE.
-  - congruence.
-  - assumption.
+  eapply load_store_away; eauto.
+  }
+  { (* Aglobal / Aglobal *)
+    destruct args; destruct args0; simpl; trivial.
+    destruct (peq i i1); simpl; trivial.
+    simpl in *.
+    destruct (eval_addressing genv sp (Aglobal i1 i2) nil) eqn:ADDR1; simpl; trivial.
+    symmetry.
+    eapply load_store_diff_globals; eauto.
+  }
 Qed. 
 End SOUNDNESS.
 
-- 
cgit 


From af7afc0a388986a94f21d2657cc13b823d456781 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 09:39:03 +0100
Subject: offsets in globals for x86

---
 backend/CSE2proof.v | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 78 insertions(+), 1 deletion(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index ada0eb00..5acffc71 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -842,6 +842,74 @@ Section MEMORY_WRITE.
       - left. assumption.
     Qed.
   End DIFFERENT_GLOBALS.
+
+  Section SAME_GLOBALS.
+    Variable ofsw ofsr : ptrofs.
+    Hypothesis sym : ident.
+    Hypothesis ADDRW : eval_addressing genv sp
+                                       (Aglobal sym ofsw) nil = Some addrw. 
+    Hypothesis ADDRR : eval_addressing genv sp
+                                       (Aglobal sym ofsr) nil = Some addrr.
+    
+  Lemma load_store_glob_away1 :
+    forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - max_chunk_size,
+    forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - max_chunk_size,
+    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 = Some valr.
+  Proof.
+    intros.
+    
+    pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded.
+    pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded.
+    unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded.
+    try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *.
+    try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *.
+    unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
+    destruct Archi.ptr64 eqn:PTR64.
+
+    {
+      unfold Genv.symbol_address in *.
+      inv ADDRR.
+      inv ADDRW.
+      destruct (Genv.find_symbol genv sym).
+      2: discriminate.
+      
+      rewrite <- READ.
+      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+      exact STORE.
+      right.
+      tauto.
+    }
+
+    {
+      unfold Genv.symbol_address in *.
+      inv ADDRR.
+      inv ADDRW.
+      destruct (Genv.find_symbol genv sym).
+      2: discriminate.
+      
+      rewrite <- READ.
+      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+      exact STORE.
+      right.
+      tauto.
+    }
+  Qed.
+
+  Lemma load_store_glob_away :
+    (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw) = true ->
+    Mem.loadv chunkr m2 addrr = Some valr.
+  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 load_store_glob_away1.
+    all: tauto.
+  Qed.
+  End SAME_GLOBALS.
 End MEMORY_WRITE.
 
 Lemma kill_mem_sound :
@@ -904,7 +972,16 @@ Proof.
   }
   { (* Aglobal / Aglobal *)
     destruct args; destruct args0; simpl; trivial.
-    destruct (peq i i1); simpl; trivial.
+    destruct (peq i i1).
+    {
+      subst i1.
+      destruct (can_swap_accesses_ofs (Ptrofs.unsigned i2) chunk0
+                                      (Ptrofs.unsigned i0) chunk) eqn:SWAP; simpl; trivial.
+      simpl in *.
+      destruct (eval_addressing genv sp (Aglobal i i2) nil) eqn:ADDR1; simpl; trivial.
+      symmetry.
+      eapply load_store_glob_away; eauto.
+    }
     simpl in *.
     destruct (eval_addressing genv sp (Aglobal i1 i2) nil) eqn:ADDR1; simpl; trivial.
     symmetry.
-- 
cgit 


From b11cbccf7eb4a6696c5285cb0bcde57dd0c0447e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 10:41:33 +0100
Subject: starting to move x86 stuff to x86

---
 backend/CSE2proof.v | 202 +---------------------------------------------------
 1 file changed, 1 insertion(+), 201 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 5acffc71..eeb9442f 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -13,7 +13,7 @@ Require Import Memory Registers Op RTL Maps.
 Require Import Globalenvs Values.
 Require Import Linking Values Memory Globalenvs Events Smallstep.
 Require Import Registers Op RTL.
-Require Import CSE2.
+Require Import CSE2 CSE2depsproof.
 Require Import Lia.
 
 Lemma args_unaffected:
@@ -712,206 +712,6 @@ Proof.
 Qed.
 End SAME_MEMORY.
 
-Section MEMORY_WRITE.
-  Variable m m2 : mem.
-  Variable chunkw chunkr : memory_chunk.
-  Variable base : val.
-
-  Lemma size_chunk_bounded :
-    forall chunk, 0 <= size_chunk chunk <= max_chunk_size.
-  Proof.
-    unfold max_chunk_size.
-    destruct chunk; simpl; lia.
-  Qed.
-  
-  Variable addrw addrr valw valr : 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 : Z.
-  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 <= ofsw <= Ptrofs.modulus - max_chunk_size,
-    forall RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size,
-    forall SWAPPABLE :    ofsw + size_chunk chunkw <= ofsr
-                       \/ ofsr + size_chunk chunkr <= ofsw,
-    Mem.loadv chunkr m2 addrr = Some valr.
-  Proof.
-    intros.
-    
-    pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded.
-    pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded.
-    unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded.
-    try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *.
-    try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *.
-    destruct addrr ; simpl in * ; try discriminate.
-    unfold eval_addressing in *.
-    destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate.
-    rewrite PTR64 in *.
-    
-    inv ADDRR.
-    inv ADDRW.
-    rewrite <- READ.
-    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
-    exact STORE.
-    right.
- 
-    all: try (destruct (Ptrofs.unsigned_add_either i0
-                (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR];
-              rewrite OFSR).
-    all: try (destruct (Ptrofs.unsigned_add_either i0
-                (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR];
-              rewrite OFSR).
-    all: try (destruct (Ptrofs.unsigned_add_either i0
-                (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW];
-              rewrite OFSW).
-    all: try (destruct (Ptrofs.unsigned_add_either i0
-                (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW];
-              rewrite OFSW).
-    
-    all: unfold Ptrofs.of_int64.
-    all: unfold Ptrofs.of_int.
-   
-
-    all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
-    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
-    all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
-    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
-
-    all: try change Ptrofs.modulus with 4294967296.
-    all: try change Ptrofs.modulus with 18446744073709551616.
-   
-    all: intuition lia.
-  Qed.
-  
-  Theorem load_store_away :
-    can_swap_accesses_ofs ofsr chunkr ofsw chunkw = true ->
-    Mem.loadv chunkr m2 addrr = Some valr.
-  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 load_store_away1.
-    all: tauto.
-  Qed.
-  End INDEXED_AWAY.
-
-  Section DIFFERENT_GLOBALS.
-    Variable ofsw ofsr : ptrofs.
-    Hypothesis symw symr : ident.
-    Hypothesis ADDRW : eval_addressing genv sp
-                                       (Aglobal symw ofsw) nil = Some addrw. 
-    Hypothesis ADDRR : eval_addressing genv sp
-                                       (Aglobal symr ofsr) nil = Some addrr.
-    
-    Lemma load_store_diff_globals :
-      symw <> symr ->
-      Mem.loadv chunkr m2 addrr = Some valr.
-    Proof.
-      intros.
-      unfold eval_addressing in *.
-      destruct Archi.ptr64 eqn:PTR64; simpl in *.
-      rewrite PTR64 in *.
-      2: simpl in *; discriminate.
-      unfold Genv.symbol_address in *.
-      unfold Genv.find_symbol in *.
-      destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW.
-      2: simpl in STORE; discriminate.
-      destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR.
-      2: simpl in READ; discriminate.
-      assert (br <> bw).
-      {
-        intro EQ.
-        subst br.
-        assert (symr = symw).
-        {
-          eapply Genv.genv_vars_inj; eauto.
-        }
-        congruence.
-      }
-      rewrite <- READ.
-      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw).
-      - exact STORE.
-      - left. assumption.
-    Qed.
-  End DIFFERENT_GLOBALS.
-
-  Section SAME_GLOBALS.
-    Variable ofsw ofsr : ptrofs.
-    Hypothesis sym : ident.
-    Hypothesis ADDRW : eval_addressing genv sp
-                                       (Aglobal sym ofsw) nil = Some addrw. 
-    Hypothesis ADDRR : eval_addressing genv sp
-                                       (Aglobal sym ofsr) nil = Some addrr.
-    
-  Lemma load_store_glob_away1 :
-    forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - max_chunk_size,
-    forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - max_chunk_size,
-    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 = Some valr.
-  Proof.
-    intros.
-    
-    pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded.
-    pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded.
-    unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded.
-    try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *.
-    try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *.
-    unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
-    destruct Archi.ptr64 eqn:PTR64.
-
-    {
-      unfold Genv.symbol_address in *.
-      inv ADDRR.
-      inv ADDRW.
-      destruct (Genv.find_symbol genv sym).
-      2: discriminate.
-      
-      rewrite <- READ.
-      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
-      exact STORE.
-      right.
-      tauto.
-    }
-
-    {
-      unfold Genv.symbol_address in *.
-      inv ADDRR.
-      inv ADDRW.
-      destruct (Genv.find_symbol genv sym).
-      2: discriminate.
-      
-      rewrite <- READ.
-      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
-      exact STORE.
-      right.
-      tauto.
-    }
-  Qed.
-
-  Lemma load_store_glob_away :
-    (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw) = true ->
-    Mem.loadv chunkr m2 addrr = Some valr.
-  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 load_store_glob_away1.
-    all: tauto.
-  Qed.
-  End SAME_GLOBALS.
-End MEMORY_WRITE.
-
 Lemma kill_mem_sound :
   forall m m' : mem,
   forall rel : RELATION.t,
-- 
cgit 


From 44811b4917b69e9a33efe5ab75ceb3b01f6594fc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 11:21:27 +0100
Subject: may_overlap_sound

---
 backend/CSE2proof.v | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index eeb9442f..206dbf30 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -735,6 +735,44 @@ Proof.
   }
 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,
   forall rel : RELATION.t,
-- 
cgit 


From 3fc937ddc8f82525081bca67818ca87f448f618e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 11:27:59 +0100
Subject: modularize proof

---
 backend/CSE2proof.v | 39 ++++++++++-----------------------------
 1 file changed, 10 insertions(+), 29 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 206dbf30..90179f82 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -795,36 +795,17 @@ Proof.
     rewrite SEMx.
     apply op_depends_on_memory_correct; auto.
   }
-  destruct addr; destruct addr0; simpl; trivial.
-  { (* Aindexed / Aindexed *)
-  destruct args as [ | base [ | ]]; simpl; trivial.
-  destruct args0 as [ | base0 [ | ]]; simpl; trivial.
-  destruct (peq (forward_move rel base) base0); simpl; trivial.
-  subst base0.
-  destruct (can_swap_accesses_ofs z0 chunk0 z chunk) eqn:SWAP; simpl; trivial.
-  simpl in *.
-  erewrite forward_move_rs in * by exact SEM.
-  destruct (eval_addressing genv sp (Aindexed z0) ((rs # base) :: nil)) eqn:ADDR0; simpl; trivial.
+  destruct may_overlap eqn:OVERLAP; simpl; trivial.
+  destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0.
   symmetry.
-  eapply load_store_away; eauto.
-  }
-  { (* Aglobal / Aglobal *)
-    destruct args; destruct args0; simpl; trivial.
-    destruct (peq i i1).
-    {
-      subst i1.
-      destruct (can_swap_accesses_ofs (Ptrofs.unsigned i2) chunk0
-                                      (Ptrofs.unsigned i0) chunk) eqn:SWAP; simpl; trivial.
-      simpl in *.
-      destruct (eval_addressing genv sp (Aglobal i i2) nil) eqn:ADDR1; simpl; trivial.
-      symmetry.
-      eapply load_store_glob_away; eauto.
-    }
-    simpl in *.
-    destruct (eval_addressing genv sp (Aglobal i1 i2) nil) eqn:ADDR1; simpl; trivial.
-    symmetry.
-    eapply load_store_diff_globals; eauto.
-  }
+  eapply may_overlap_sound with (args := (map (forward_move rel) args)).
+  erewrite forward_move_map by eassumption.
+  exact ADDR.
+  exact ADDR0.
+  exact OVERLAP.
+  exact STORE.
+  symmetry; assumption.
+  assumption.
 Qed. 
 End SOUNDNESS.
 
-- 
cgit 


From 577d3dbeb54aaf23db19dddf149c48764e20c58d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
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 


From 74efac13484e4767f793cf9ccc94835825ca30ba Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 12:27:58 +0100
Subject: CSE2 alias analysis for Risc-V

---
 backend/CSE2proof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 8cc87275..09490c4d 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -13,7 +13,7 @@ Require Import Memory Registers Op RTL Maps.
 Require Import Globalenvs Values.
 Require Import Linking Values Memory Globalenvs Events Smallstep.
 Require Import Registers Op RTL.
-Require Import CSE2 CSE2depsproof.
+Require Import CSE2 CSE2deps CSE2depsproof.
 Require Import Lia.
 
 Lemma args_unaffected:
-- 
cgit