From e66be6e05b190c51b38d628884ef3e015ebf73fd Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 24 Feb 2020 19:59:43 +0100
Subject: Make single arg alignment depend on toolchain.

GCC does passes single arguments as singles on the stack but diab
and the eabi say single arguments should be passed as double on
the stack.

This commit changes the alignment of single arguments to 4 for
gcc based backends.
---
 powerpc/Archi.v             |  3 +++
 powerpc/Conventions1.v      | 17 ++++++++++++++---
 powerpc/extractionMachdep.v |  3 +++
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index ab348c14..88fff302 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -30,6 +30,9 @@ Definition align_float64 := 8%Z.
 (** Can we use the 64-bit extensions to the PowerPC architecture? *)
 Parameter ppc64 : bool.
 
+(** Should singles be passed as single or double *)
+Parameter single_passed_as_single : bool.
+
 Definition splitlong := negb ppc64.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 1f048694..5639ff8d 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -208,7 +208,16 @@ Fixpoint loc_arguments_rec
       | Some ireg =>
           One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs
       end
-  | (Tfloat | Tsingle | Tany64) as ty :: tys =>
+  | Tsingle as ty :: tys =>
+      match list_nth_z float_param_regs fr with
+      | None =>
+          let ty := if Archi.single_passed_as_single then Tsingle else Tfloat in
+          let ofs := align ofs (typesize ty) in
+          One (S Outgoing ofs Tsingle) :: loc_arguments_rec tys ir fr (ofs + (typesize ty))
+      | Some freg =>
+          One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs
+      end
+  | (Tfloat | Tany64) as ty :: tys =>
       match list_nth_z float_param_regs fr with
       | None =>
           let ofs := align ofs 2 in
@@ -295,12 +304,14 @@ Opaque list_nth_z.
   apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l.
   eapply Y; eauto. omega.
 - (* single *)
+  assert (ofs <= align ofs 1) by (apply align_le; omega).
   assert (ofs <= align ofs 2) by (apply align_le; omega).
   destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. omega. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. split. destruct Archi.single_passed_as_single; simpl; omega.
+  destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l.
+  eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega.
 - (* any32 *)
   destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
   subst. left. eapply list_nth_z_in; eauto.
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index 7482435f..a3e945bf 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -34,3 +34,6 @@ Extract Constant Archi.ppc64 =>
    | ""e5500"" -> true
    | _ -> false
    end".
+
+(* Choice of passing of single *)
+Extract Constant Archi.single_passed_as_single => "Configuration.gnu_toolchain".
-- 
cgit 


From 78d76b65b417b2724cc54a7e5fc5d434d8fc57b5 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 27 Feb 2020 10:04:43 +0100
Subject: Define IRC.class_of_type for types Tany32, Tany64

Until now the types Tany32 and Tany64 were not used prior to register
allocation, so IRC.class_of_type did not need to be defined for
those types.

However, there are possible uses of stack slots of type Tany32 and Tany64
to specify calling conventions.  For this purpose, we need to define
class_of_type for Tany32 and Tany64.  We follow the informal convention
that Tany32 goes in integer registers and Tany64 goes into integer
registers if 64-bit wide, or FP registers otherwise.
---
 backend/IRC.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/backend/IRC.ml b/backend/IRC.ml
index 43955897..b359da35 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -240,7 +240,8 @@ type graph = {
 let class_of_type = function
   | Tint | Tlong -> 0
   | Tfloat | Tsingle -> 1
-  | Tany32 | Tany64 -> assert false
+  | Tany32 -> 0
+  | Tany64 -> if Archi.ptr64 then 0 else 1
 
 let class_of_reg r =
   if Conventions1.is_float_reg r then 1 else 0
-- 
cgit 


From 9190ca38b3ae098186421a7cc21a087666a6a677 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 27 Feb 2020 10:10:23 +0100
Subject: In strict PPC ABI mode, pass single FP on stack in double FP format

The EABI and the SVR4 ABI state that single-precision FP arguments passed
on stack are passed as a 64-bit word, extended to double-precision.

This commit implements this behavior by using a stack slot of type Tany64.
Not only this ensures that the slot is of size and alignment 8 bytes,
but it also ensures that it is accessed by stfd and lfd instructions,
using single-extended-to-double format.
---
 powerpc/Conventions1.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 5639ff8d..5c9cbd4f 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -211,9 +211,9 @@ Fixpoint loc_arguments_rec
   | Tsingle as ty :: tys =>
       match list_nth_z float_param_regs fr with
       | None =>
-          let ty := if Archi.single_passed_as_single then Tsingle else Tfloat in
+          let ty := if Archi.single_passed_as_single then Tsingle else Tany64 in
           let ofs := align ofs (typesize ty) in
-          One (S Outgoing ofs Tsingle) :: loc_arguments_rec tys ir fr (ofs + (typesize ty))
+          One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + (typesize ty))
       | Some freg =>
           One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs
       end
-- 
cgit 


From 35ba7f373963d8a1f0094abd457809d1e3c3cdb4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 27 Feb 2020 10:15:40 +0100
Subject: Documentation comment for single_passed_as_single

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

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 88fff302..10f38391 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -30,7 +30,8 @@ Definition align_float64 := 8%Z.
 (** Can we use the 64-bit extensions to the PowerPC architecture? *)
 Parameter ppc64 : bool.
 
-(** Should singles be passed as single or double *)
+(** Should single-precision FP arguments passed on stack be passed 
+    as singles or use double FP format. *)
 Parameter single_passed_as_single : bool.
 
 Definition splitlong := negb ppc64.
-- 
cgit 


From 8587b8310a91702e2635a689e1622a87b7bf8985 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Mon, 2 Mar 2020 10:32:07 +0100
Subject: Weaker ec_readonly condition over external calls (#225)

Currently we require the memory to be unchanged on readonly locations.
This is too strong.  For example, current permissions could decrease
from readonly to none.

This commit weakens the ec_readonly condition to the strict minimum
needed to show the correctness of value analysis for const globals.
---
 backend/ValueAnalysis.v |  5 ++---
 common/Events.v         | 48 +++++++++++++++++++++++++++++++++---------------
 2 files changed, 35 insertions(+), 18 deletions(-)

diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 2b233900..b0ce019c 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1039,9 +1039,8 @@ Proof.
   red; simpl; intros. destruct (plt b (Mem.nextblock m)).
   exploit RO; eauto. intros (R & P & Q).
   split; auto.
-  split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto.
-  intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto.
-  auto. intros; red. apply Q.
+  split. apply bmatch_incr with bc; auto. apply bmatch_ext with m; auto.
+  intros. eapply external_call_readonly with (m2 := m'); eauto.
   intros; red; intros; elim (Q ofs).
   eapply external_call_max_perm with (m2 := m'); eauto.
   destruct (j' b); congruence.
diff --git a/common/Events.v b/common/Events.v
index 10e0c232..4431b0b7 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -649,9 +649,12 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
 (** External call cannot modify memory unless they have [Max, Writable]
    permissions. *)
   ec_readonly:
-    forall ge vargs m1 t vres m2,
+    forall ge vargs m1 t vres m2 b ofs n bytes,
     sem ge vargs m1 t vres m2 ->
-    Mem.unchanged_on (loc_not_writable m1) m1 m2;
+    Mem.valid_block m1 b ->
+    Mem.loadbytes m2 b ofs n = Some bytes ->
+    (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) ->
+    Mem.loadbytes m1 b ofs n = Some bytes;
 
 (** External calls must commute with memory extensions, in the
   following sense. *)
@@ -784,7 +787,7 @@ Proof.
 (* max perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H. inv H1. inv H6. inv H4.
   exploit volatile_load_extends; eauto. intros [v' [A B]].
@@ -833,14 +836,27 @@ Proof.
   rewrite C; auto.
 Qed.
 
+Lemma unchanged_on_readonly:
+  forall m1 m2 b ofs n bytes,
+  Mem.unchanged_on (loc_not_writable m1) m1 m2 ->
+  Mem.valid_block m1 b ->
+  Mem.loadbytes m2 b ofs n = Some bytes ->
+  (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) ->
+  Mem.loadbytes m1 b ofs n = Some bytes.
+Proof.
+  intros.
+  rewrite <- H1. symmetry.
+  apply Mem.loadbytes_unchanged_on_1 with (P := loc_not_writable m1); auto.
+Qed.
+
 Lemma volatile_store_readonly:
   forall ge chunk1 m1 b1 ofs1 v t m2,
   volatile_store ge chunk1 m1 b1 ofs1 v t m2 ->
   Mem.unchanged_on (loc_not_writable m1) m1 m2.
 Proof.
   intros. inv H.
-  apply Mem.unchanged_on_refl.
-  eapply Mem.store_unchanged_on; eauto.
+- apply Mem.unchanged_on_refl.
+- eapply Mem.store_unchanged_on; eauto.
   exploit Mem.store_valid_access_3; eauto. intros [P Q].
   intros. unfold loc_not_writable. red; intros. elim H2.
   apply Mem.perm_cur_max. apply P. auto.
@@ -934,7 +950,7 @@ Proof.
 (* perms *)
 - inv H. inv H2. auto. eauto with mem.
 (* readonly *)
-- inv H. eapply volatile_store_readonly; eauto.
+- inv H. eapply unchanged_on_readonly; eauto. eapply volatile_store_readonly; eauto.
 (* mem extends*)
 - inv H. inv H1. inv H6. inv H7. inv H4.
   exploit volatile_store_extends; eauto. intros [m2' [A [B C]]].
@@ -994,7 +1010,7 @@ Proof.
   rewrite dec_eq_false. auto.
   apply Mem.valid_not_valid_diff with m1; eauto with mem.
 (* readonly *)
-- inv H. eapply UNCHANGED; eauto.
+- inv H. eapply unchanged_on_readonly; eauto. 
 (* mem extends *)
 - inv H. inv H1. inv H7.
   assert (SZ: v2 = Vptrofs sz).
@@ -1065,8 +1081,9 @@ Proof.
 (* perms *)
 - inv H. eapply Mem.perm_free_3; eauto.
 (* readonly *)
-- inv H. eapply Mem.free_unchanged_on; eauto.
-  intros. red; intros. elim H3.
+- inv H. eapply unchanged_on_readonly; eauto. 
+  eapply Mem.free_unchanged_on; eauto.
+  intros. red; intros. elim H6.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.free_range_perm; eauto.
 (* mem extends *)
@@ -1159,8 +1176,9 @@ Proof.
 - (* perms *)
   intros. inv H. eapply Mem.perm_storebytes_2; eauto.
 - (* readonly *)
-  intros. inv H. eapply Mem.storebytes_unchanged_on; eauto.
-  intros; red; intros. elim H8.
+  intros. inv H. eapply unchanged_on_readonly; eauto. 
+  eapply Mem.storebytes_unchanged_on; eauto.
+  intros; red; intros. elim H11.
   apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto.
 - (* extensions *)
   intros. inv H.
@@ -1271,7 +1289,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H.
   exists Vundef; exists m1'; intuition.
@@ -1316,7 +1334,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H. inv H1. inv H6.
   exists v2; exists m1'; intuition.
@@ -1359,7 +1377,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H.
   exists Vundef; exists m1'; intuition.
@@ -1406,7 +1424,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H. fold bsem in H2. apply val_inject_list_lessdef in H1.
   specialize (bs_inject _ bsem _ _ _ H1).
-- 
cgit 


From f8d3d265f6ef967acf6eea017cb472809096a135 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Mon, 2 Mar 2020 10:41:11 +0100
Subject: Define the semantics of `free(NULL)` (#226)

According to ISO C, `free(NULL)` is correct and does nothing.
This commit updates accordingly the formal semantics of the `free`
external function and the reference interpreter.

Closes: #334
---
 cfrontend/Cexec.v | 73 +++++++++++++++++++++++++++++++++----------------------
 common/Events.v   | 44 ++++++++++++++++++++++-----------
 2 files changed, 74 insertions(+), 43 deletions(-)

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 2942080b..b08c3ad7 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -460,6 +460,14 @@ Definition do_ef_free
       check (zlt 0 (Ptrofs.unsigned sz));
       do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz);
       Some(w, E0, Vundef, m')
+  | Vint n :: nil =>
+      if Int.eq_dec n Int.zero && negb Archi.ptr64
+      then Some(w, E0, Vundef, m)
+      else None
+  | Vlong n :: nil =>
+      if Int64.eq_dec n Int64.zero && Archi.ptr64
+      then Some(w, E0, Vundef, m)
+      else None
   | _ => None
   end.
 
@@ -544,45 +552,51 @@ Proof with try congruence.
   - eapply do_external_function_sound; eauto.
   }
   destruct ef; simpl.
-(* EF_external *)
+- (* EF_external *)
   eapply do_external_function_sound; eauto.
-(* EF_builtin *)
+- (* EF_builtin *)
   eapply BF_EX; eauto.
-(* EF_runtime *)
+- (* EF_runtime *)
   eapply BF_EX; eauto.
-(* EF_vload *)
+- (* EF_vload *)
   unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
   exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto.
-  auto.
-(* EF_vstore *)
+- (* EF_vstore *)
   unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs...
   mydestr. destruct p as [[w'' t''] m'']. mydestr.
   exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
-  auto.
-(* EF_malloc *)
+- (* EF_malloc *)
   unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr.
   destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr.
   split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor.
-(* EF_free *)
-  unfold do_ef_free. destruct vargs... destruct v... destruct vargs...
-  mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor.
-(* EF_memcpy *)
+- (* EF_free *)
+  unfold do_ef_free. destruct vargs... destruct v... 
++ destruct vargs... mydestr; InvBooleans; subst i.
+  replace (Vint Int.zero) with Vnullptr. split; constructor.
+  apply negb_true_iff in H0. unfold Vnullptr; rewrite H0; auto.
++ destruct vargs... mydestr; InvBooleans; subst i.
+  replace (Vlong Int64.zero) with Vnullptr. split; constructor.
+  unfold Vnullptr; rewrite H0; auto.
++ destruct vargs... mydestr.
+  split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega.
+  constructor.
+- (* EF_memcpy *)
   unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
   destruct v... destruct vargs... mydestr. 
   apply Decidable_sound in Heqb1. red in Heqb1.
   split. econstructor; eauto; tauto. constructor.
-(* EF_annot *)
+- (* EF_annot *)
   unfold do_ef_annot. mydestr.
   split. constructor. apply list_eventval_of_val_sound; auto.
   econstructor. constructor; eauto. constructor.
-(* EF_annot_val *)
+- (* EF_annot_val *)
   unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr.
   split. constructor. apply eventval_of_val_sound; auto.
   econstructor. constructor; eauto. constructor.
-(* EF_inline_asm *)
+- (* EF_inline_asm *)
   eapply do_inline_assembly_sound; eauto.
-(* EF_debug *)
+- (* EF_debug *)
   unfold do_ef_debug. mydestr. split; constructor.
 Qed.
 
@@ -605,37 +619,38 @@ Proof.
   - eapply do_external_function_complete; eauto.
   }
   destruct ef; simpl in *.
-(* EF_external *)
+- (* EF_external *)
   eapply do_external_function_complete; eauto.
-(* EF_builtin *)
+- (* EF_builtin *)
   eapply BF_EX; eauto.
-(* EF_runtime *)
+- (* EF_runtime *)
   eapply BF_EX; eauto.
-(* EF_vload *)
+- (* EF_vload *)
   inv H; unfold do_ef_volatile_load.
   exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
-(* EF_vstore *)
+- (* EF_vstore *)
   inv H; unfold do_ef_volatile_store.
   exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
-(* EF_malloc *)
+- (* EF_malloc *)
   inv H; unfold do_ef_malloc.
   inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto.
-(* EF_free *)
+- (* EF_free *)
   inv H; unfold do_ef_free.
-  inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
-(* EF_memcpy *)
++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
++ inv H0. unfold Vnullptr; destruct Archi.ptr64; auto.
+- (* EF_memcpy *)
   inv H; unfold do_ef_memcpy.
   inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto.
   red. tauto.
-(* EF_annot *)
+- (* EF_annot *)
   inv H; unfold do_ef_annot. inv H0. inv H6. inv H4.
   rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
-(* EF_annot_val *)
+- (* EF_annot_val *)
   inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4.
   rewrite (eventval_of_val_complete _ _ _ H1). auto.
-(* EF_inline_asm *)
+- (* EF_inline_asm *)
   eapply do_inline_assembly_complete; eauto.
-(* EF_debug *)
+- (* EF_debug *)
   inv H. inv H0. reflexivity.
 Qed.
 
diff --git a/common/Events.v b/common/Events.v
index 4431b0b7..022adaef 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1061,11 +1061,13 @@ Qed.
 
 Inductive extcall_free_sem (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_free_sem_intro: forall b lo sz m m',
+  | extcall_free_sem_ptr: forall b lo sz m m',
       Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) ->
       Ptrofs.unsigned sz > 0 ->
       Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' ->
-      extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.
+      extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'
+  | extcall_free_sem_null: forall m,
+      extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m.
 
 Lemma extcall_free_ok:
   extcall_properties extcall_free_sem
@@ -1073,27 +1075,29 @@ Lemma extcall_free_ok:
 Proof.
   constructor; intros.
 (* well typed *)
-- inv H. simpl. auto.
+- inv H; simpl; auto.
 (* symbols preserved *)
 - inv H0; econstructor; eauto.
 (* valid block *)
-- inv H. eauto with mem.
+- inv H; eauto with mem.
 (* perms *)
-- inv H. eapply Mem.perm_free_3; eauto.
+- inv H; eauto using Mem.perm_free_3.
 (* readonly *)
-- inv H. eapply unchanged_on_readonly; eauto. 
-  eapply Mem.free_unchanged_on; eauto.
+- eapply unchanged_on_readonly; eauto. inv H.
++ eapply Mem.free_unchanged_on; eauto.
   intros. red; intros. elim H6.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.free_range_perm; eauto.
++ apply Mem.unchanged_on_refl.
 (* mem extends *)
-- inv H. inv H1. inv H8. inv H6.
+- inv H.
++ inv H1. inv H8. inv H6.
   exploit Mem.load_extends; eauto. intros [v' [A B]].
   assert (v' = Vptrofs sz).
   { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
   subst v'.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
-  exists Vundef; exists m2'; intuition.
+  exists Vundef; exists m2'; intuition auto.
   econstructor; eauto.
   eapply Mem.free_unchanged_on; eauto.
   unfold loc_out_of_bounds; intros.
@@ -1101,8 +1105,14 @@ Proof.
   { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
     eapply Mem.free_range_perm. eexact H4. eauto. }
   tauto.
++ inv H1. inv H5. replace v2 with Vnullptr.
+  exists Vundef; exists m1'; intuition auto.
+  constructor.
+  apply Mem.unchanged_on_refl.
+  unfold Vnullptr in *; destruct Archi.ptr64; inv H3; auto.
 (* mem inject *)
-- inv H0. inv H2. inv H7. inv H9.
+- inv H0.
++ inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [v' [A B]].
   assert (v' = Vptrofs sz).
   { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
@@ -1116,7 +1126,7 @@ Proof.
   intro EQ.
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
   exists f, Vundef, m2'; split.
-  apply extcall_free_sem_intro with (sz := sz) (m' := m2').
+  apply extcall_free_sem_ptr with (sz := sz) (m' := m2').
     rewrite EQ. rewrite <- A. f_equal. omega.
     auto. auto.
     rewrite ! EQ. rewrite <- C. f_equal; omega.
@@ -1129,14 +1139,19 @@ Proof.
     apply P. omega.
   split. auto.
   red; intros. congruence.
++ inv H2. inv H6. replace v' with Vnullptr.
+  exists f, Vundef, m1'; intuition auto using Mem.unchanged_on_refl.
+  constructor.
+  red; intros; congruence.
+  unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto.
 (* trace length *)
 - inv H; simpl; omega.
 (* receptive *)
-- assert (t1 = t2). inv H; inv H0; auto. subst t2.
+- assert (t1 = t2) by (inv H; inv H0; auto). subst t2.
   exists vres1; exists m1; auto.
 (* determ *)
-- inv H; inv H0.
-  assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
+- inv H; inv H0; try (unfold Vnullptr in *; discriminate).
++ assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
   assert (EQ2: sz0 = sz).
   { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF.
     rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
@@ -1144,6 +1159,7 @@ Proof.
   }
   subst sz0.
   split. constructor. intuition congruence.
++ split. constructor. intuition auto.
 Qed.
 
 (** ** Semantics of [memcpy] operations. *)
-- 
cgit 


From 94558ecb3e48261f12c644045d40c7d0784415e0 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 2 Mar 2020 11:39:06 +0100
Subject: Define the semantics of `free(NULL)`, continued

The proof script for Events.excall_free_ok was incomplete
if Archi.ptr64 is unknown (as in the RISC-V case).
---
 common/Events.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/common/Events.v b/common/Events.v
index 022adaef..28bb992a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1150,7 +1150,7 @@ Proof.
 - assert (t1 = t2) by (inv H; inv H0; auto). subst t2.
   exists vres1; exists m1; auto.
 (* determ *)
-- inv H; inv H0; try (unfold Vnullptr in *; discriminate).
+- inv H; inv H0; try (unfold Vnullptr in *; destruct Archi.ptr64; discriminate).
 + assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
   assert (EQ2: sz0 = sz).
   { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF.
-- 
cgit 


From 6af8f4275f7f9572d4d0783818cbfb85357807c6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 13:17:54 +0100
Subject: loadv_storev_same

---
 common/Memory.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/common/Memory.v b/common/Memory.v
index b68a5049..89b920b3 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1169,6 +1169,24 @@ Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
 Local Hint Resolve store_valid_access_1 store_valid_access_2
              store_valid_access_3: mem.
 
+
+Section STOREV.
+Variable chunk: memory_chunk.
+Variable m1: mem.
+Variables addr v: val.
+Variable m2: mem.
+Hypothesis STORE: storev chunk m1 addr v = Some m2.
+
+
+Theorem loadv_storev_same:
+  loadv chunk m2 addr = Some (Val.load_result chunk v).
+Proof.
+  destruct addr; simpl in *; try discriminate.
+  eapply load_store_same.
+  eassumption.
+Qed.
+End STOREV.
+
 Lemma load_store_overlap:
   forall chunk m1 b ofs v m2 chunk' ofs' v',
   store chunk m1 b ofs v = Some m2 ->
-- 
cgit 


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(-)

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(-)

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/CSE2.v      |  8 ++++++++
 backend/CSE2proof.v | 32 +++++++++++++++++++-------------
 2 files changed, 27 insertions(+), 13 deletions(-)

diff --git a/backend/CSE2.v b/backend/CSE2.v
index b7665097..a03e02a4 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -266,6 +266,14 @@ Definition kill_reg (dst : reg) (rel : RELATION.t) :=
   PTree.filter1 (fun x => negb (kill_sym_val dst x))
                 (PTree.remove dst rel).
 
+Definition max_chunk_size := 8.
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - max_chunk_size))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - max_chunk_size))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+  
 Definition kill_sym_val_mem (sv: sym_val) :=
   match sv with
   | SMove _ => false
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(-)

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(-)

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(-)

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/CSE2.v           | 26 ++++++++++++++++++++++++--
 backend/CSE2proof.v      |  4 ++--
 test/cse2/indexed_addr.c |  6 ++++++
 3 files changed, 32 insertions(+), 4 deletions(-)
 create mode 100644 test/cse2/indexed_addr.c

diff --git a/backend/CSE2.v b/backend/CSE2.v
index a03e02a4..f5ff8748 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -281,16 +281,38 @@ Definition kill_sym_val_mem (sv: sym_val) :=
   | SLoad _ _ _ => true
   end.
 
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
+    else true
+  | _, _, _, _ => true
+  end.
+
+Definition kill_sym_val_store chunk addr args (sv: sym_val) :=
+  match sv with
+  | SMove _ => false
+  | SOp op _ => op_depends_on_memory op
+  | SLoad chunk' addr' args' => may_overlap chunk addr args chunk' addr' args'
+  end.
+
 Definition kill_mem (rel : RELATION.t) :=
   PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel.
 
-
 Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
   match rel ! x with
   | Some (SMove org) => org
   | _ => x
   end.
 
+Definition kill_store1 chunk addr args rel :=
+  PTree.filter1 (fun x => negb (kill_sym_val_store chunk addr args x)) rel.
+
+Definition kill_store chunk addr args rel :=
+  kill_store1 chunk addr (List.map (forward_move rel) args) rel.
+
 Definition move (src dst : reg) (rel : RELATION.t) :=
   PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel).
 
@@ -403,7 +425,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   | Inop _
   | Icond _ _ _ _
   | Ijumptable _ _ => Some rel
-  | Istore _ _ _ _ _ => Some (kill_mem rel)
+  | Istore chunk addr args _ _ => Some (kill_store chunk addr args rel)
   | Iop op args dst _ => Some (gen_oper op dst args rel)
   | Iload chunk addr args dst _ => Some (load chunk addr dst args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
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.
diff --git a/test/cse2/indexed_addr.c b/test/cse2/indexed_addr.c
new file mode 100644
index 00000000..30a7c571
--- /dev/null
+++ b/test/cse2/indexed_addr.c
@@ -0,0 +1,6 @@
+void foo(int *t) {
+  if (t[0] > 4) {
+    t[1] ++;
+    t[0] --;
+  }
+}
-- 
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/CSE2.v      |  2 ++
 backend/CSE2proof.v | 67 +++++++++++++++++++++++++++++++++++++++++++++--------
 test/cse2/globals.c |  8 +++++++
 3 files changed, 67 insertions(+), 10 deletions(-)
 create mode 100644 test/cse2/globals.c

diff --git a/backend/CSE2.v b/backend/CSE2.v
index f5ff8748..5b0556aa 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -288,6 +288,8 @@ Definition may_overlap chunk addr args chunk' addr' args' :=
     if peq base base'
     then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
     else true
+  | (Aglobal symb ofs), (Aglobal symb' ofs'),
+    nil, nil => peq symb symb'
   | _, _, _, _ => true
   end.
 
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.
 
diff --git a/test/cse2/globals.c b/test/cse2/globals.c
new file mode 100644
index 00000000..c6dd59cd
--- /dev/null
+++ b/test/cse2/globals.c
@@ -0,0 +1,8 @@
+int glob1, glob2;
+
+void toto() {
+  if (glob1 > 4) {
+    glob2 ++;
+    glob1 --;
+  }
+}
-- 
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/CSE2.v      |  5 +++-
 backend/CSE2proof.v | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 82 insertions(+), 2 deletions(-)

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 5b0556aa..9c45b476 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -289,7 +289,10 @@ Definition may_overlap chunk addr args chunk' addr' args' :=
     then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
     else true
   | (Aglobal symb ofs), (Aglobal symb' ofs'),
-    nil, nil => peq symb symb'
+    nil, nil =>
+    if peq symb symb'
+    then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+    else false
   | _, _, _, _ => true
   end.
 
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 +-----------------------------------------------
 x86/CSE2depsproof.v | 215 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 216 insertions(+), 201 deletions(-)
 create mode 100644 x86/CSE2depsproof.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,
diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v
new file mode 100644
index 00000000..f4eace6f
--- /dev/null
+++ b/x86/CSE2depsproof.v
@@ -0,0 +1,215 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+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 Lia.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+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.
+End SOUNDNESS.
-- 
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(+)

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(-)

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 --------------------------------------
 x86/CSE2depsproof.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 38 deletions(-)

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,
diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v
index f4eace6f..84b22c69 100644
--- a/x86/CSE2depsproof.v
+++ b/x86/CSE2depsproof.v
@@ -213,3 +213,49 @@ Section MEMORY_WRITE.
   End SAME_GLOBALS.
 End MEMORY_WRITE.
 End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+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.
+
+End SOUNDNESS.
-- 
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/CSE2.v        |  25 +---------
 backend/CSE2proof.v   |   2 +-
 backend/ValueDomain.v |   5 --
 common/Memdata.v      |   7 +++
 riscV/CSE2deps.v      |  20 ++++++++
 riscV/CSE2depsproof.v | 129 ++++++++++++++++++++++++++++++++++++++++++++++++++
 6 files changed, 158 insertions(+), 30 deletions(-)
 create mode 100644 riscV/CSE2deps.v
 create mode 100644 riscV/CSE2depsproof.v

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 9c45b476..8142ee5d 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -6,7 +6,7 @@ David Monniaux, CNRS, VERIMAG
 
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
-Require Import Memory Registers Op RTL Maps.
+Require Import Memory Registers Op RTL Maps CSE2deps.
 
 (* Static analysis *)
 
@@ -265,14 +265,6 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) :=
 Definition kill_reg (dst : reg) (rel : RELATION.t) :=
   PTree.filter1 (fun x => negb (kill_sym_val dst x))
                 (PTree.remove dst rel).
-
-Definition max_chunk_size := 8.
-
-Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
-     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - max_chunk_size))
-  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - max_chunk_size))
-  && ((ofsw + size_chunk chunkw <=? ofsr) ||
-      (ofsr + size_chunk chunkr <=? ofsw)).
   
 Definition kill_sym_val_mem (sv: sym_val) :=
   match sv with
@@ -281,21 +273,6 @@ Definition kill_sym_val_mem (sv: sym_val) :=
   | SLoad _ _ _ => true
   end.
 
-Definition may_overlap chunk addr args chunk' addr' args' :=
-  match addr, addr', args, args' with
-  | (Aindexed ofs), (Aindexed ofs'),
-    (base :: nil), (base' :: nil) =>
-    if peq base base'
-    then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
-    else true
-  | (Aglobal symb ofs), (Aglobal symb' ofs'),
-    nil, nil =>
-    if peq symb symb'
-    then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
-    else false
-  | _, _, _, _ => true
-  end.
-
 Definition kill_sym_val_store chunk addr args (sv: sym_val) :=
   match sv with
   | SMove _ => false
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:
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index c132ce7c..779e7bb9 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -3502,11 +3502,6 @@ Proof.
 - omegaContradiction.
 Qed.
 
-Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
-Proof.
-  destruct chunk; simpl; omega.
-Qed.
-
 Remark inval_before_contents:
   forall i c chunk' av' j,
   (inval_before i (i - 7) c)##j = Some (ACval chunk' av') ->
diff --git a/common/Memdata.v b/common/Memdata.v
index f3016efe..a09b90f5 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -44,6 +44,13 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
   | Many64 => 8
   end.
 
+Definition largest_size_chunk := 8.
+
+Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
+Proof.
+  destruct chunk; simpl; omega.
+Qed.
+
 Lemma size_chunk_pos:
   forall chunk, size_chunk chunk > 0.
 Proof.
diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v
new file mode 100644
index 00000000..8ab9242a
--- /dev/null
+++ b/riscV/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+    else true  | _, _, _, _ => true
+  end.
diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v
new file mode 100644
index 00000000..ee500965
--- /dev/null
+++ b/riscV/CSE2depsproof.v
@@ -0,0 +1,129 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+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 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = (if Archi.ptr64 then 64 else 32)%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296.
+Proof.
+  unfold Ptrofs.modulus.
+  rewrite ptrofs_size.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  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 : 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 <= 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 = Some valr.
+  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 *.
+
+    rewrite ptrofs_modulus in *.
+    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 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 load_store_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_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+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 (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.
+  }
+Qed.
+
+End SOUNDNESS.
-- 
cgit 


From 4096e8c1b1e3d4fcdb44e81844d65a74f881aa47 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 13:33:54 +0100
Subject: better 32/64-bit handling

---
 x86/CSE2deps.v      | 24 ++++++++++++++++++++++++
 x86/CSE2depsproof.v | 53 +++++++++++++++++++++++++++--------------------------
 2 files changed, 51 insertions(+), 26 deletions(-)
 create mode 100644 x86/CSE2deps.v

diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v
new file mode 100644
index 00000000..f4d9e254
--- /dev/null
+++ b/x86/CSE2deps.v
@@ -0,0 +1,24 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
+    else true
+  | (Aglobal symb ofs), (Aglobal symb' ofs'), nil, nil =>
+    if peq symb symb'
+    then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+    else false
+  | _, _, _, _ => true
+  end.
diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v
index 84b22c69..37e16dfe 100644
--- a/x86/CSE2depsproof.v
+++ b/x86/CSE2depsproof.v
@@ -5,7 +5,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 CSE2deps.
 Require Import Lia.
 
 Section SOUNDNESS.
@@ -17,13 +17,6 @@ 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.
@@ -37,19 +30,18 @@ Section MEMORY_WRITE.
                        (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 RANGEW : 0 <= ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk,
     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 *.
+    pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+    pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+    try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *.
+    try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *.
     destruct addrr ; simpl in * ; try discriminate.
     unfold eval_addressing in *.
     destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate.
@@ -111,16 +103,25 @@ Section MEMORY_WRITE.
                                        (Aglobal symw ofsw) nil = Some addrw. 
     Hypothesis ADDRR : eval_addressing genv sp
                                        (Aglobal symr ofsr) nil = Some addrr.
-    
+
+    Lemma ptr64_cases:
+      forall {T : Type},
+      forall b : bool,
+      forall x y : T,
+        (if b then (if b then x else y) else (if b then y else x)) = x.
+    Proof.
+      destruct b; reflexivity.
+    Qed.
+
     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.
+      simpl in *.
+      rewrite ptr64_cases in ADDRR.
+      rewrite ptr64_cases in ADDRW.
       unfold Genv.symbol_address in *.
       unfold Genv.find_symbol in *.
       destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW.
@@ -153,19 +154,19 @@ Section MEMORY_WRITE.
                                        (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 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 = 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 *.
+    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 size_chunkr_bounded, size_chunkw_bounded.
+    try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *.
+    try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *.
     unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
     destruct Archi.ptr64 eqn:PTR64.
 
-- 
cgit 


From 091e00ed16d4189c27a05ad7056eab47bd29f5b7 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 14:39:31 +0100
Subject: CSE2 for ARM

---
 arm/CSE2depsproof.v | 132 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 132 insertions(+)
 create mode 100644 arm/CSE2depsproof.v

diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v
new file mode 100644
index 00000000..2112a230
--- /dev/null
+++ b/arm/CSE2depsproof.v
@@ -0,0 +1,132 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+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 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = 32%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = 4294967296.
+Proof.
+  unfold Ptrofs.modulus.
+  rewrite ptrofs_size.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  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 : int.
+  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.
+  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 *.
+
+    rewrite ptrofs_modulus in *.
+    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];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int 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.
+  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.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+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 (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+  }
+Qed.
+
+End SOUNDNESS.
-- 
cgit 


From a2b5e7c85dbbc6a27d941dcd931b36c4aa747fb5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 14:57:20 +0100
Subject: aarch64

---
 aarch64/CSE2deps.v      |  20 ++++++++
 aarch64/CSE2depsproof.v | 130 ++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 150 insertions(+)
 create mode 100644 aarch64/CSE2deps.v
 create mode 100644 aarch64/CSE2depsproof.v

diff --git a/aarch64/CSE2deps.v b/aarch64/CSE2deps.v
new file mode 100644
index 00000000..90b514a2
--- /dev/null
+++ b/aarch64/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs (Int64.unsigned ofs') chunk' (Int64.unsigned ofs) chunk)
+    else true  | _, _, _, _ => true
+  end.
diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v
new file mode 100644
index 00000000..e20824e3
--- /dev/null
+++ b/aarch64/CSE2depsproof.v
@@ -0,0 +1,130 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+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 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = 64%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = 18446744073709551616.
+Proof.
+  reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  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 : int64.
+  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 <= Int64.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= Int64.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE :    Int64.unsigned ofsw + size_chunk chunkw <= Int64.unsigned ofsr
+                       \/ Int64.unsigned ofsr + size_chunk chunkr <= Int64.unsigned ofsw,
+    Mem.loadv chunkr m2 addrr = Some valr.
+  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 *.
+
+    rewrite ptrofs_modulus in *.
+    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: unfold Ptrofs.of_int64.
+
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.repr (Int64.unsigned ofsr))) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.repr (Int64.unsigned ofsw))) as [OFSW | OFSW];
+              rewrite OFSW).
+    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
+
+    all: try rewrite ptrofs_modulus in *.
+
+    all: intuition lia.
+  Qed.
+  
+  Theorem load_store_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_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+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 (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.
+  }
+Qed.
+
+End SOUNDNESS.
-- 
cgit 


From 63c878610c5ef531731f5d9f83570f19c8c1acbc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 15:08:43 +0100
Subject: CSE2 for powerpc

---
 powerpc/CSE2deps.v      |  20 ++++++++
 powerpc/CSE2depsproof.v | 132 ++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 152 insertions(+)
 create mode 100644 powerpc/CSE2deps.v
 create mode 100644 powerpc/CSE2depsproof.v

diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v
new file mode 100644
index 00000000..9db51bbb
--- /dev/null
+++ b/powerpc/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (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
+  end.
diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v
new file mode 100644
index 00000000..2112a230
--- /dev/null
+++ b/powerpc/CSE2depsproof.v
@@ -0,0 +1,132 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+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 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = 32%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = 4294967296.
+Proof.
+  unfold Ptrofs.modulus.
+  rewrite ptrofs_size.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  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 : int.
+  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.
+  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 *.
+
+    rewrite ptrofs_modulus in *.
+    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];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int 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.
+  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.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+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 (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+  }
+Qed.
+
+End SOUNDNESS.
-- 
cgit 


From 3b640f041be480b82f1b3a1f695ed8a57193bf28 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 15:28:27 +0100
Subject: CSE2 with alias analysis

---
 arm/CSE2deps.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 arm/CSE2deps.v

diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v
new file mode 100644
index 00000000..9db51bbb
--- /dev/null
+++ b/arm/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (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
+  end.
-- 
cgit