fixed CSE2 for mppa_k1c

Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2

24 files changed, 1266 insertions, 843 deletions

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.
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.
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.
diff --git a/backend/CSE2.v b/backend/CSE2.v
index 41adba7b..be72405b 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 *)
 
@@ -29,30 +29,13 @@ Proof.
   decide equality.
 Defined.
 
-Definition pset := PTree.t unit.
-
-Definition pset_inter : pset -> pset -> pset :=
-  PTree.combine_null
-    (fun ov1 ov2 => Some tt).
-
-Definition pset_empty : pset := PTree.empty unit.
-Definition pset_add (i : positive) (s : pset) := PTree.set i tt s.
-Definition pset_remove (i : positive) (s : pset) := PTree.remove i s.
-
-Record relmap := mkrel {
-   var_to_sym : PTree.t sym_val ;
-   mem_used : pset ;
-   reg_used : PTree.t pset
- }.
-
 Module RELATION.
-
-Definition t := relmap.
-
+  
+Definition t := (PTree.t sym_val).
 Definition eq (r1 r2 : t) :=
-  forall x, (PTree.get x (var_to_sym r1)) = (PTree.get x (var_to_sym r2)).
+  forall x, (PTree.get x r1) = (PTree.get x r2).
 
-Definition top : t := mkrel (PTree.empty sym_val) pset_empty (PTree.empty pset).
+Definition top : t := PTree.empty sym_val.
 
 Lemma eq_refl: forall x, eq x x.
 Proof.
@@ -75,27 +58,27 @@ Qed.
 Definition sym_val_beq (x y : sym_val) :=
   if eq_sym_val x y then true else false.
 
-Definition beq (r1 r2 : t) := PTree.beq sym_val_beq (var_to_sym r1) (var_to_sym r2).
+Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2.
 
 Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2.
 Proof.
   unfold beq, eq. intros r1 r2 EQ x.
-  pose proof (PTree.beq_correct sym_val_beq (var_to_sym r1) (var_to_sym r2)) as CORRECT.
+  pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT.
   destruct CORRECT as [CORRECTF CORRECTB].
   pose proof (CORRECTF EQ x) as EQx.
   clear CORRECTF CORRECTB EQ.
   unfold sym_val_beq in *.
-  destruct ((var_to_sym r1) ! x) as [R1x | ] in *;
-    destruct ((var_to_sym r2) ! x) as [R2x | ] in *;
+  destruct (r1 ! x) as [R1x | ] in *;
+    destruct (r2 ! x) as [R2x | ] in *;
     trivial; try contradiction.
   destruct (eq_sym_val R1x R2x) in *; congruence.
 Qed.
 
 Definition ge (r1 r2 : t) :=
   forall x,
-    match PTree.get x (var_to_sym r1) with
+    match PTree.get x r1 with
     | None => True
-    | Some v => (PTree.get x (var_to_sym r2)) = Some v
+    | Some v => (PTree.get x r2) = Some v
     end.
 
 Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2.
@@ -104,7 +87,7 @@ Proof.
   intros r1 r2 EQ x.
   pose proof (EQ x) as EQx.
   clear EQ.
-  destruct ((var_to_sym r1) ! x).
+  destruct (r1 ! x).
   - congruence.
   - trivial.
 Qed.
@@ -115,13 +98,12 @@ Proof.
   intros r1 r2 r3 GE12 GE23 x.
   pose proof (GE12 x) as GE12x; clear GE12.
   pose proof (GE23 x) as GE23x; clear GE23.
-  destruct ((var_to_sym r1) ! x); trivial.
-  destruct ((var_to_sym r2) ! x); congruence.
+  destruct (r1 ! x); trivial.
+  destruct (r2 ! x); congruence.
 Qed.
 
 Definition lub (r1 r2 : t) :=
-  mkrel
-  (PTree.combine
+  PTree.combine
     (fun ov1 ov2 =>
        match ov1, ov2 with
        | (Some v1), (Some v2) =>
@@ -131,19 +113,12 @@ Definition lub (r1 r2 : t) :=
        | None, _
        | _, None => None
        end)
-    (var_to_sym r1) (var_to_sym r2))
-  (pset_inter (mem_used r1) (mem_used r2))
-  (PTree.combine_null
-     (fun x y => let r := pset_inter x y in
-                 if PTree.bempty_canon r
-                 then None
-                 else Some r)
-     (reg_used r1) (reg_used r2)).
+    r1 r2.
 
 Lemma ge_lub_left: forall x y, ge (lub x y) x.
 Proof.
   unfold ge, lub.
-  intros r1 r2 x. simpl.
+  intros r1 r2 x.
   rewrite PTree.gcombine by reflexivity.
   destruct (_ ! _); trivial.
   destruct (_ ! _); trivial.
@@ -153,7 +128,7 @@ Qed.
 Lemma ge_lub_right: forall x y, ge (lub x y) y.
 Proof.
   unfold ge, lub.
-  intros r1 r2 x. simpl.
+  intros r1 r2 x.
   rewrite PTree.gcombine by reflexivity.
   destruct (_ ! _); trivial.
   destruct (_ ! _); trivial.
@@ -275,79 +250,53 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM).
     - apply L.ge_refl.
       apply L.eq_refl.
   Qed.
-
-  Definition top := Some RELATION.top.
 End ADD_BOTTOM.
 
 Module RB := ADD_BOTTOM(RELATION).
 Module DS := Dataflow_Solver(RB)(NodeSetForward).
 
-Definition kill_sym_val (dst : reg) (sv : sym_val) : bool :=
+Definition kill_sym_val (dst : reg) (sv : sym_val) :=
   match sv with
   | SMove src => if peq dst src then true else false
   | SOp op args => List.existsb (peq dst) args
   | SLoad chunk addr args => List.existsb (peq dst) args
   end.
-
-Definition referenced_by sv :=
+                                                 
+Definition kill_reg (dst : reg) (rel : RELATION.t) :=
+  PTree.filter1 (fun x => negb (kill_sym_val dst x))
+                (PTree.remove dst rel).
+  
+Definition kill_sym_val_mem (sv: sym_val) :=
   match sv with
-  | SMove src => src :: nil
-  | SOp op args => args
-  | SLoad chunk addr args => args
-  end.
-           
-Definition referenced_by' osv :=
-  match osv with
-  | None => nil
-  | Some sv => referenced_by sv
+  | SMove _ => false
+  | SOp op _ => op_depends_on_memory op
+  | SLoad _ _ _ => true
   end.
 
-Definition remove_from_sets
-           (to_remove : reg) :
-           list reg -> PTree.t pset -> PTree.t pset :=
-  List.fold_left
-    (fun sets reg =>
-       match PTree.get reg sets with
-       | None => sets
-       | Some xset =>
-         let xset' := PTree.remove to_remove xset in
-         if PTree.bempty_canon xset'
-         then PTree.remove reg sets
-         else PTree.set reg xset' sets
-       end).
-
-Definition kill_reg (dst : reg) (rel : RELATION.t) : RELATION.t :=
-  let rel' := PTree.remove dst (var_to_sym rel) in
-  mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x)) rel')
-        (pset_remove dst (mem_used rel))
-        (remove_from_sets dst (referenced_by' (PTree.get dst (var_to_sym rel)))
-                          (PTree.remove dst (reg_used rel))).
-
-Definition kill_sym_val_mem (sv: sym_val) :=
+Definition kill_sym_val_store chunk addr args (sv: sym_val) :=
   match sv with
   | SMove _ => false
   | SOp op _ => op_depends_on_memory op
-  | SLoad _ _ _ => true
+  | SLoad chunk' addr' args' => may_overlap chunk addr args chunk' addr' args'
   end.
 
 Definition kill_mem (rel : RELATION.t) :=
-  mkrel
-    (PTree.remove_t (var_to_sym rel) (mem_used rel))
-    pset_empty
-    (reg_used rel). (* FIXME *)
-
+  PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel.
 
 Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
-  match (var_to_sym rel) ! x with
+  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) :=
-  let rel0 := kill_reg dst rel in
-  mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym rel0))
-        (mem_used rel0)
-        (reg_used rel0). (* FIXME *)
+  PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel).
 
 Definition find_op_fold op args (already : option reg) x sv :=
                 match already with
@@ -363,7 +312,7 @@ Definition find_op_fold op args (already : option reg) x sv :=
                 end.
 
 Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) :=
-  PTree.fold (find_op_fold op args) (var_to_sym rel) None.
+  PTree.fold (find_op_fold op args) rel None.
 
 Definition find_load_fold chunk addr args (already : option reg) x sv :=
                 match already with
@@ -381,42 +330,37 @@ Definition find_load_fold chunk addr args (already : option reg) x sv :=
                 end.
 
 Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) :=
-  PTree.fold (find_load_fold chunk addr args) (var_to_sym rel) None.
+  PTree.fold (find_load_fold chunk addr args) rel None.
 
 Definition oper2 (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) : RELATION.t :=
+           (rel : RELATION.t) :=
   let rel' := kill_reg dst rel in
-  mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel'))
-        (if op_depends_on_memory op then (pset_add dst (mem_used rel'))
-         else mem_used rel')
-        (reg_used rel'). (* FIXME *)
+  PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'.
 
 Definition oper1 (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) : RELATION.t :=
+           (rel : RELATION.t) :=
   if List.in_dec peq dst args
   then kill_reg dst rel
   else oper2 op dst args rel.
 
 Definition oper (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) : RELATION.t :=
+           (rel : RELATION.t) :=
   match find_op rel op (List.map (forward_move rel) args) with
   | Some r => move r dst rel
   | None => oper1 op dst args rel
   end.
 
 Definition gen_oper (op: operation) (dst : reg) (args : list reg)
-           (rel : RELATION.t) : RELATION.t :=
+           (rel : RELATION.t) :=
   match op, args with
   | Omove, src::nil => move src dst rel
   | _, _ => oper op dst args rel
   end.
 
 Definition load2 (chunk: memory_chunk) (addr : addressing)
-           (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t :=
+           (dst : reg) (args : list reg) (rel : RELATION.t) :=
   let rel' := kill_reg dst rel in
-  mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel'))
-        (pset_add dst (mem_used rel'))
-        (reg_used rel'). (* FIXME *)
+  PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'.
 
 Definition load1 (chunk: memory_chunk) (addr : addressing)
            (dst : reg) (args : list reg) (rel : RELATION.t) :=
@@ -463,7 +407,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 trap chunk addr args dst _ => Some (load chunk addr dst args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
@@ -483,7 +427,7 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
 
 Definition forward_map (f : RTL.function) := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
-  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) RB.top.
+  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
 
 Definition forward_move_b (rb : RB.t) (x : reg) :=
   match rb with
@@ -525,7 +469,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t))
   match instr with
   | Iop op args dst s =>
     let args' := subst_args fmap pc args in
-    match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with
+    match find_op_in_fmap fmap pc op args' with
     | None => Iop op args' dst s
     | Some src => Iop Omove (src::nil) dst s
     end
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 577b1e69..7e1dd430 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -13,7 +13,8 @@ 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 CSE2depsproof.
+Require Import Lia.
 
 Lemma args_unaffected:
   forall rs : regset,
@@ -37,515 +38,6 @@ Proof.
   assumption.
 Qed.
 
-Lemma gpset_inter_none: forall a b i,
-    (pset_inter a b) ! i = None <->
-    (a ! i = None) \/ (b ! i = None).
-Proof.
-  intros. unfold pset_inter.
-  rewrite PTree.gcombine_null.
-  destruct (a ! i); destruct (b ! i); intuition discriminate.
-Qed.
-
-Lemma some_some:
-  forall x : option unit,
-    x <> None <-> x = Some tt.
-Proof.
-  destruct x as [[] | ]; split; congruence.
-Qed.  
-
-Lemma gpset_inter_some: forall a b i,
-    (pset_inter a b) ! i = Some tt <->
-    (a ! i = Some tt) /\ (b ! i = Some tt).
-Proof.
-  intros. unfold pset_inter.
-  rewrite PTree.gcombine_null.
-  destruct (a ! i) as [[] | ]; destruct (b ! i) as [[] | ]; intuition congruence.
-Qed.
-
-Definition wellformed_mem (rel : RELATION.t) : Prop :=
-  forall i sv,
-  (var_to_sym rel) ! i = Some sv ->
-  kill_sym_val_mem sv = true ->
-  (mem_used rel) ! i = Some tt.
-
-Definition wellformed_reg (rel : RELATION.t) : Prop :=
-  forall i j sv,
-  (var_to_sym rel) ! i = Some sv ->
-  kill_sym_val j sv = true ->
-  match (reg_used rel) ! j with
-  | Some uses => uses ! i = Some tt
-  | None => False
-  end.
-
-Lemma wellformed_mem_top : wellformed_mem RELATION.top.
-Proof.
-  unfold wellformed_mem, RELATION.top, pset_empty.
-  simpl.
-  intros.
-  rewrite PTree.gempty in *.
-  discriminate.
-Qed.
-Local Hint Resolve wellformed_mem_top : wellformed.
-
-Lemma wellformed_reg_top : wellformed_reg RELATION.top.
-Proof.
-  unfold wellformed_reg, RELATION.top, pset_empty.
-  simpl.
-  intros.
-  rewrite PTree.gempty in *.
-  discriminate.
-Qed.
-Local Hint Resolve wellformed_reg_top : wellformed.
-
-Lemma wellformed_mem_lub : forall a b,
-    (wellformed_mem a) -> (wellformed_mem b) -> (wellformed_mem (RELATION.lub a b)).
-Proof.
-  unfold wellformed_mem, RELATION.lub.
-  simpl.
-  intros a b Ha Hb.
-  intros i sv COMBINE KILLABLE.
-  rewrite PTree.gcombine in *.
-  2: reflexivity.
-  destruct (var_to_sym a) ! i as [syma | ] eqn:SYMA;
-    destruct (var_to_sym b) ! i as [symb | ] eqn:SYMB;
-    try discriminate.
-  destruct (eq_sym_val syma symb); try discriminate.
-  subst syma.
-  inv COMBINE.
-  apply gpset_inter_some.
-  split; eauto.
-Qed.
-Local Hint Resolve wellformed_mem_lub : wellformed.
-
-Lemma wellformed_reg_lub : forall a b,
-    (wellformed_reg a) -> (wellformed_reg b) -> (wellformed_reg (RELATION.lub a b)).
-Proof.
-  unfold wellformed_reg, RELATION.lub.
-  simpl.
-  intros a b Ha Hb.
-  intros i j sv COMBINE KILLABLE.
-  specialize Ha with (i := i) (j := j).
-  specialize Hb with (i := i) (j := j).
-  rewrite PTree.gcombine in *.
-  2: reflexivity.
-  destruct (var_to_sym a) ! i as [syma | ] eqn:SYMA;
-    destruct (var_to_sym b) ! i as [symb | ] eqn:SYMB;
-    try discriminate.
-  specialize Ha with (sv := syma).
-  specialize Hb with (sv := symb).
-  destruct (eq_sym_val syma symb); try discriminate.
-  subst syma.
-  inv COMBINE.
-  rewrite PTree.gcombine_null.
-  destruct ((reg_used a) ! j) as [uA| ]; destruct ((reg_used b) ! j) as [uB | ]; auto.
-  { pose proof (PTree.bempty_canon_correct (pset_inter uA uB) i) as EMPTY.
-    destruct PTree.bempty_canon.
-  - rewrite gpset_inter_none in EMPTY.
-    intuition congruence.
-  - rewrite gpset_inter_some.
-    auto.
-  }
-Qed.
-Local Hint Resolve wellformed_reg_lub : wellformed.
-
-Lemma wellformed_mem_kill_reg:
-  forall dst rel,
-    (wellformed_mem rel) -> (wellformed_mem (kill_reg dst rel)).
-Proof.
-  unfold wellformed_mem, kill_reg, pset_remove.
-  simpl.
-  intros dst rel Hrel.
-  intros i sv KILLREG KILLABLE.
-  rewrite PTree.gfilter1 in KILLREG.
-  destruct (peq dst i).
-  { subst i.
-    rewrite PTree.grs in *.
-    discriminate.
-  }
-  rewrite PTree.gro in * by congruence.
-  specialize Hrel with (i := i).
-  eapply Hrel.
-  2: eassumption.  
-  destruct (_ ! i); try discriminate.
-  destruct negb; congruence.
-Qed.
-Local Hint Resolve wellformed_mem_kill_reg : wellformed.
-
-Lemma kill_sym_val_referenced:
-  forall dst,
-  forall sv,
-    (kill_sym_val dst sv)=true <-> In dst (referenced_by sv).
-Proof.
-  intros.
-  destruct sv; simpl.
-  - destruct peq; intuition congruence.
-  - rewrite existsb_exists.
-    split.
-    + intros [x [IN EQ]].
-      destruct peq.
-      * subst x; trivial.
-      * discriminate.
-    + intro.
-      exists dst.
-      split; trivial.
-      destruct peq; trivial.
-      congruence.
-  - rewrite existsb_exists.
-    split.
-    + intros [x [IN EQ]].
-      destruct peq.
-      * subst x; trivial.
-      * discriminate.
-    + intro.
-      exists dst.
-      split; trivial.
-      destruct peq; trivial.
-      congruence.
-Qed.
-Local Hint Resolve kill_sym_val_referenced : wellformed.
-
-Lemma remove_from_sets_notin:
-  forall dst l sets j,
-    not (In j l) ->
-    (remove_from_sets dst l sets) ! j = sets ! j.
-Proof.
-  induction l; simpl; trivial.
-  intros.
-  rewrite IHl by tauto.
-  destruct (@PTree.get (PTree.t unit) a sets) eqn:SETSA; trivial.
-  pose proof (PTree.bempty_canon_correct (PTree.remove dst t)) as CORRECT.
-  destruct (PTree.bempty_canon (PTree.remove dst t)).
-  - apply PTree.gro.
-    intuition.
-  - rewrite PTree.gso by intuition.
-    trivial.
-Qed.
-
-Lemma remove_from_sets_pass:
-  forall dst l sets i j,
-    i <> dst ->
-    match sets ! j with
-    | Some uses => uses ! i = Some tt
-    | None => False
-    end ->
-    match (remove_from_sets dst l sets) ! j with
-    | Some uses => uses ! i = Some tt
-    | None => False
-    end.
-Proof.
-  induction l; simpl; trivial.
-  intros.
-  apply IHl; trivial.
-  destruct (@PTree.get (PTree.t unit) a sets) eqn:SETSA; trivial.
-  pose proof (PTree.bempty_canon_correct (PTree.remove dst t)) as CORRECT.
-  specialize CORRECT with (i := i).
-  destruct (PTree.bempty_canon (PTree.remove dst t)).
-  - rewrite PTree.gro in CORRECT by congruence.
-    destruct (peq a j).
-    + subst a.
-      rewrite SETSA in *.
-      intuition congruence.
-    + rewrite PTree.gro by congruence.
-      assumption.
-  - destruct (peq a j).
-    + subst a.
-      rewrite SETSA in *.
-      rewrite PTree.gss.
-      rewrite PTree.gro by congruence.
-      assumption.
-    + rewrite PTree.gso by congruence.
-      assumption.
-Qed.
-Local Hint Resolve remove_from_sets_pass : wellformed.
-
-Lemma rem_comes_from:
-  forall A x y (tr: PTree.t A) v,
-    (PTree.remove x tr) ! y = Some v -> tr ! y = Some v.
-Proof.
-  intros.
-  destruct (peq x y).
-  - subst y.
-    rewrite PTree.grs in *.
-    discriminate.
-  - rewrite PTree.gro in * by congruence.
-    assumption.
-Qed.
-Local Hint Resolve rem_comes_from : wellformed.
-
-Lemma rem_ineq:
-  forall A x y (tr: PTree.t A) v,
-    (PTree.remove x tr) ! y = Some v -> x<>y.
-Proof.
-  intros.
-  intro.
-  subst y.
-  rewrite PTree.grs in *.
-  discriminate.
-Qed.
-Local Hint Resolve rem_ineq : wellformed.
-
-Lemma wellformed_reg_kill_reg:
-  forall dst rel,
-    (wellformed_reg rel) -> (wellformed_reg (kill_reg dst rel)).
-Proof.
-  unfold wellformed_reg, kill_reg.
-  simpl.
-  intros dst rel Hrel.
-  intros i j sv KILLREG KILLABLE.
-
-  rewrite PTree.gfilter1 in KILLREG.
-  destruct PTree.get eqn:REMi in KILLREG.
-  2: discriminate.
-  destruct negb eqn:NEGB in KILLREG.
-  2: discriminate.
-  inv KILLREG.
-
-  assert ((var_to_sym rel) ! i = Some sv) as RELi by eauto with wellformed.
-  
-  destruct (peq dst j).
-  { (* absurd case *)
-    subst j.
-    rewrite KILLABLE in NEGB.
-    simpl in NEGB.
-    discriminate.
-  }
-  specialize Hrel with (i := i) (j := j) (sv := sv).
-  destruct ((var_to_sym rel) ! dst) eqn:DST; simpl.
-  {
-    assert (dst <> i) by eauto with wellformed.
-    apply remove_from_sets_pass.
-    congruence.
-    rewrite PTree.gro by congruence.
-    apply Hrel; trivial.
-  }
-  rewrite PTree.gro by congruence.
-  apply Hrel; trivial.
-Qed.
-Local Hint Resolve wellformed_reg_kill_reg : wellformed.
-
-Lemma wellformed_mem_kill_mem:
-  forall rel,
-    (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)).
-Proof.
-  unfold wellformed_mem, kill_mem.
-  simpl.
-  intros rel Hrel.
-  intros i sv KILLMEM KILLABLE.
-  rewrite PTree.gremove_t in KILLMEM.
-  exfalso.
-  specialize Hrel with (i := i).
-  destruct ((var_to_sym rel) ! i) eqn:RELi.
-  - specialize Hrel with (sv := s).
-    destruct ((mem_used rel) ! i) eqn:USEDi.
-    discriminate.
-    inv KILLMEM.
-    intuition congruence.
- - destruct ((mem_used rel) ! i); discriminate.
-Qed.
-Local Hint Resolve wellformed_mem_kill_mem : wellformed.
-
-Lemma wellformed_reg_kill_mem:
-  forall rel,
-    (wellformed_reg rel) -> (wellformed_reg (kill_mem rel)).
-Proof.
-  unfold wellformed_reg, kill_mem.
-  simpl.
-  intros rel Hrel.
-  intros i j sv KILLMEM KILLABLE.
-  apply Hrel with (sv := sv); trivial.
-  rewrite PTree.gremove_t in KILLMEM.
-  destruct ((mem_used rel) ! i) in KILLMEM.
-  discriminate.
-  assumption.
-Qed.
-Local Hint Resolve wellformed_reg_kill_mem : wellformed.
-
-Lemma wellformed_mem_move:
-  forall r dst rel,
-    (wellformed_mem rel) -> (wellformed_mem (move r dst rel)).
-Proof.
-  Local Opaque kill_reg.
-  intros; unfold move, wellformed_mem; simpl.
-  intros i sv MOVE KILL.
-  destruct (peq i dst).
-  { subst i.
-    rewrite PTree.gss in MOVE.
-    inv MOVE.
-    simpl in KILL.
-    discriminate.
-  }
-  rewrite PTree.gso in MOVE by congruence.
-  eapply wellformed_mem_kill_reg; eauto.
-Qed.
-Local Hint Resolve wellformed_mem_move : wellformed.
-
-Lemma wellformed_mem_oper2:
-  forall op dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (oper2 op dst args rel)).
-Proof.
-  intros until rel. intro WELLFORMED.
-  unfold oper2.
-  intros i sv MOVE OPER.
-  simpl in *.
-  destruct (peq i dst).
-  { subst i.
-    rewrite PTree.gss in MOVE.
-    inv MOVE.
-    simpl in OPER.
-    rewrite OPER.
-    apply PTree.gss.
-  }
-  unfold pset_add.
-  rewrite PTree.gso in MOVE by congruence.
-  destruct op_depends_on_memory.
-  - rewrite PTree.gso by congruence.
-    eapply wellformed_mem_kill_reg; eauto.
-  - eapply wellformed_mem_kill_reg; eauto.
-Qed.
-Local Hint Resolve wellformed_mem_oper2 : wellformed.
-
-Lemma wellformed_mem_oper1:
-  forall op dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (oper1 op dst args rel)).
-Proof.
-  unfold oper1. intros.
-  destruct in_dec ; auto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_oper1 : wellformed.
-
-Lemma wellformed_mem_oper:
-  forall op dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (oper op dst args rel)).
-Proof.
-  unfold oper. intros.
-  destruct find_op ; auto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_oper : wellformed.
-
-Lemma wellformed_mem_gen_oper:
-  forall op dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (gen_oper op dst args rel)).
-Proof.
-  intros.
-  unfold gen_oper.
-  destruct op; auto with wellformed.
-  destruct args; auto with wellformed.
-  destruct args; auto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_gen_oper : wellformed.
-
-Lemma wellformed_mem_load2 :
-  forall chunk addr dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (load2 chunk addr dst args rel)).
-Proof.
-  intros.
-  unfold load2, wellformed_mem.
-  simpl.
-  intros i sv LOAD KILL.
-  destruct (peq i dst).
-  { subst i.
-    apply PTree.gss.
-  }
-  unfold pset_add.
-  rewrite PTree.gso in * by congruence.
-  eapply wellformed_mem_kill_reg; eauto.
-Qed.
-Local Hint Resolve wellformed_mem_load2 : wellformed.
-
-Lemma wellformed_mem_load1 :
-  forall chunk addr dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (load1 chunk addr dst args rel)).
-Proof.
-  intros.
-  unfold load1.
-  destruct in_dec; eauto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_load1 : wellformed.
-
-Lemma wellformed_mem_load :
-  forall chunk addr dst args rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem (load chunk addr dst args rel)).
-Proof.
-  intros.
-  unfold load.
-  destruct find_load; eauto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_load : wellformed.
-
-Definition wellformed_mem_rb (rb : RB.t) :=
-  match rb with
-  | None => True
-  | Some r => wellformed_mem r
-  end.
-
-Lemma wellformed_mem_apply_instr:
-  forall instr rel,
-    (wellformed_mem rel) ->
-    (wellformed_mem_rb (apply_instr instr rel)).
-Proof.
-  destruct instr; simpl; auto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_apply_instr : wellformed.
-
-Lemma wellformed_mem_rb_bot :
-  wellformed_mem_rb RB.bot.
-Proof.
-  simpl.
-  trivial.
-Qed.
-Local Hint Resolve wellformed_mem_rb_bot: wellformed.
-
-Lemma wellformed_mem_rb_top :
-  wellformed_mem_rb RB.top.
-Proof.
-  simpl.
-  auto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_rb_top: wellformed.
-
-Lemma wellformed_mem_rb_apply_instr':
-  forall code pc rel,
-    (wellformed_mem_rb rel) ->
-    (wellformed_mem_rb (apply_instr' code pc rel)).
-Proof.
-  destruct rel; simpl; trivial.
-  intro.
-  destruct (code ! pc);
-  eauto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_rb_apply_instr' : wellformed.
-
-Lemma wellformed_mem_rb_lub : forall a b,
-    (wellformed_mem_rb a) -> (wellformed_mem_rb b) -> (wellformed_mem_rb (RB.lub a b)).
-Proof.
-  destruct a; destruct b; simpl; auto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_rb_lub: wellformed.
-
-Definition wellformed_mem_fmap fmap :=
-  forall i, wellformed_mem_rb (fmap !! i).
-
-Theorem wellformed_mem_forward_map : forall f,
-    forall fmap, (forward_map f) = Some fmap ->
-    wellformed_mem_fmap fmap.
-Proof.
-  intros.
-  unfold forward_map in *.
-  unfold wellformed_mem_fmap.
-  intro.
-  eapply DS.fixpoint_invariant with (ev := Some RELATION.top); eauto with wellformed.
-Qed.
-Local Hint Resolve wellformed_mem_forward_map: wellformed.
-
-Local Transparent kill_reg.
-
 Section SOUNDNESS.
   Variable F V : Type.
   Variable genv: Genv.t F V.
@@ -570,7 +62,7 @@ Definition sem_sym_val sym rs (v : option val) : Prop :=
   end.
     
 Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop :=
-  match (var_to_sym rel) ! x with
+  match rel ! x with
   | None => True
   | Some sym => sem_sym_val sym rs (Some (rs # x)) 
   end.
@@ -610,7 +102,7 @@ Proof.
   pose proof (SEM arg) as SEMarg.
   simpl. unfold forward_move.
   unfold sem_sym_val in *.
-  destruct (_ ! arg); trivial.
+  destruct (t ! arg); trivial.
   destruct s; congruence.
 Qed.
 
@@ -639,7 +131,7 @@ Lemma kill_reg_sound :
 Proof.
   unfold sem_rel, kill_reg, sem_reg, sem_sym_val.
   intros until v.
-  intros REL x. simpl.
+  intros REL x.
   rewrite PTree.gfilter1.
   destruct (Pos.eq_dec dst x).
   {
@@ -649,7 +141,7 @@ Proof.
   }
   rewrite PTree.gro by congruence.
   rewrite Regmap.gso by congruence.
-  destruct (_ ! x) as [relx | ] eqn:RELx; trivial.
+  destruct (rel ! x) as [relx | ] eqn:RELx; trivial.
   unfold kill_sym_val.
   pose proof (REL x) as RELinstx.
   rewrite RELx in RELinstx.
@@ -702,13 +194,12 @@ Proof.
   {
     subst x.
     unfold sem_reg.
-    simpl.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     unfold sem_reg in *.
     simpl.
     unfold forward_move.
-    destruct (_ ! src) as [ sv |]; simpl.
+    destruct (rel ! src) as [ sv |]; simpl.
     destruct sv eqn:SV; simpl in *.
     {
       destruct (peq dst src0).
@@ -724,7 +215,6 @@ Proof.
   }
   rewrite Regmap.gso by congruence.
   unfold sem_reg.
-  simpl.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -737,10 +227,9 @@ Lemma move_cases_neq:
 Proof.
   intros until a. intro NEQ.
   unfold kill_reg, forward_move.
-  simpl.
   rewrite PTree.gfilter1.
   rewrite PTree.gro by congruence.
-  destruct (_ ! a); simpl.
+  destruct (rel ! a); simpl.
   2: congruence.
   destruct s.
   {
@@ -774,10 +263,9 @@ Proof.
   unfold kill_reg.
   unfold sem_reg in RELa.
   unfold forward_move.
-  simpl.
   rewrite PTree.gfilter1.
   rewrite PTree.gro by auto.
-  destruct (_ ! a); simpl; trivial.
+  destruct (rel ! a); simpl; trivial.
   destruct s; simpl in *; destruct negb; simpl; congruence.
 Qed.
 
@@ -801,7 +289,6 @@ Proof.
   {
     subst x.
     unfold sem_reg.
-    simpl.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
@@ -811,7 +298,6 @@ Proof.
   }
   rewrite Regmap.gso by congruence.
   unfold sem_reg.
-  simpl.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -859,13 +345,13 @@ Proof.
              | Some src => eval_operation genv sp op rs ## args m = Some rs # src
              end -> fold_left
     (fun (a : option reg) (p : positive * sym_val) =>
-     find_op_fold op args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start =
+     find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start =
                     Some src ->
              eval_operation genv sp op rs ## args m = Some rs # src) as REC.
   {
     unfold sem_rel, sem_reg in REL.
-    generalize (PTree.elements_complete (var_to_sym rel)).
-    generalize (PTree.elements (var_to_sym rel)).
+    generalize (PTree.elements_complete rel).
+    generalize (PTree.elements rel).
     induction l; simpl.
     {
       intros.
@@ -890,7 +376,7 @@ Proof.
     destruct eq_args; trivial.
     subst args0.
     simpl.
-    assert (((var_to_sym rel) ! r) = Some (SOp op args)) as RELatr.
+    assert ((rel ! r) = Some (SOp op args)) as RELatr.
     {
       apply COMPLETE.
       left.
@@ -905,6 +391,7 @@ Proof.
   apply REC; auto.
 Qed.
 
+
 Lemma find_load_sound :
   forall rel : RELATION.t,
   forall chunk : memory_chunk,
@@ -941,7 +428,7 @@ Proof.
              end ->
     fold_left
     (fun (a : option reg) (p : positive * sym_val) =>
-     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start =
+     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start =
     Some src ->
     match eval_addressing genv sp addr rs##args with
                | Some a => match Mem.loadv chunk m a with
@@ -953,8 +440,8 @@ Proof.
   
   {
     unfold sem_rel, sem_reg in REL.
-    generalize (PTree.elements_complete (var_to_sym rel)).
-    generalize (PTree.elements (var_to_sym rel)).
+    generalize (PTree.elements_complete rel).
+    generalize (PTree.elements rel).
     induction l; simpl.
     {
       intros.
@@ -981,7 +468,7 @@ Proof.
     destruct eq_args; trivial.
     subst args0.
     simpl.
-    assert (((var_to_sym rel) ! r) = Some (SLoad chunk addr args)) as RELatr.
+    assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr.
     {
       apply COMPLETE.
       left.
@@ -1077,7 +564,21 @@ Proof.
   2: (apply IHargs; assumption).
   unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
   pose proof (REL a) as RELa.
-  destruct (_ ! a); trivial.
+  destruct (rel ! a); trivial.
+  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.
 
@@ -1160,7 +661,6 @@ Proof.
   {
     subst x.
     unfold sem_reg.
-    simpl.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
@@ -1173,7 +673,7 @@ Proof.
     discriminate.
   }
   rewrite Regmap.gso by congruence.
-  unfold sem_reg. simpl.
+  unfold sem_reg.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -1198,7 +698,7 @@ Proof.
   destruct (peq x dst).
   {
     subst x.
-    unfold sem_reg. simpl.
+    unfold sem_reg.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
@@ -1208,7 +708,7 @@ Proof.
     trivial.
   }
   rewrite Regmap.gso by congruence.
-  unfold sem_reg. simpl.
+  unfold sem_reg.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -1235,7 +735,7 @@ Proof.
   destruct (peq x dst).
   {
     subst x.
-    unfold sem_reg. simpl.
+    unfold sem_reg.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
@@ -1245,8 +745,7 @@ Proof.
     right; trivial.
   }
   rewrite Regmap.gso by congruence.
-  unfold sem_reg. simpl.
-  simpl.
+  unfold sem_reg.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -1443,7 +942,6 @@ Proof.
   intros REL x.
   pose proof (REL x) as RELx.
   unfold kill_reg, sem_reg in *.
-  simpl.
   rewrite PTree.gfilter1.
   destruct (peq res x).
   { subst x.
@@ -1451,7 +949,7 @@ Proof.
     reflexivity.
   }
   rewrite PTree.gro by congruence.
-  destruct (_ ! x) as [sv | ]; trivial.
+  destruct (mpc ! x) as [sv | ]; trivial.
   destruct negb; trivial.
 Qed.
 
@@ -1474,8 +972,8 @@ Proof.
   pose proof (RE x) as REx.
   pose proof (GE x) as GEx.
   unfold sem_reg in *.
-  destruct ((var_to_sym r1) ! x) as [r1x | ] in *;
-    destruct ((var_to_sym r2) ! x) as [r2x | ] in *;
+  destruct (r1 ! x) as [r1x | ] in *;
+    destruct (r2 ! x) as [r2x | ] in *;
     congruence.
 Qed.
 End SAME_MEMORY.
@@ -1484,35 +982,58 @@ Lemma kill_mem_sound :
   forall m m' : mem,
   forall rel : RELATION.t,
   forall rs,
-    wellformed_mem rel ->
     sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs.
 Proof.
   unfold sem_rel, sem_reg.
   intros until rs.
-  intros WELLFORMED SEM x.
-  unfold wellformed_mem in *.
-  specialize SEM with (x := x).
-  specialize WELLFORMED with (i := x).
+  intros SEM x.
+  pose proof (SEM x) as SEMx.
   unfold kill_mem.
-  simpl.
-  rewrite PTree.gremove_t.
+  rewrite PTree.gfilter1.
   unfold kill_sym_val_mem.
-  destruct ((var_to_sym rel) ! x) as [ sv | ] eqn:VAR.
-  - specialize WELLFORMED with (sv0 := sv).
-    destruct ((mem_used rel) ! x) eqn:USED; trivial.
-    unfold sem_sym_val in *.
-    destruct sv; simpl in *; trivial.
-    + rewrite op_depends_on_memory_correct with (m2 := m).
-      assumption.
-      destruct op_depends_on_memory; intuition congruence.
-    + intuition discriminate.
-  - replace (match (mem_used rel) ! x with
-        | Some _ | _ => None
-             end) with (@None sym_val) by
-        (destruct ((mem_used rel) ! x); trivial).
-    trivial.
+  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.
+  }
 Qed.
-
+  
+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_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_store, 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 may_overlap eqn:OVERLAP; simpl; trivial.
+  destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0.
+  {
+    erewrite may_overlap_sound with (args := (map (forward_move rel) args)).
+    all: try eassumption.
+    
+    erewrite forward_move_map by eassumption.
+    assumption.
+  }
+  intuition congruence.
+Qed. 
 End SOUNDNESS.
 
 Definition match_prog (p tp: RTL.program) :=
@@ -1600,6 +1121,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,
@@ -1651,39 +1173,6 @@ Ltac TR_AT :=
         generalize (transf_function_at _ _ _ A); intros
   end.
 
-Lemma wellformed_mem_mpc:
-  forall f map pc mpc,
-    (forward_map f) = Some map ->
-    map # pc = Some mpc ->
-    wellformed_mem mpc.
-Proof.
-  intros.
-  assert (wellformed_mem_fmap map) by eauto with wellformed.
-  unfold wellformed_mem_fmap, wellformed_mem_rb in *.
-  specialize H1 with (i := pc).
-  rewrite H0 in H1.
-  assumption.
-Qed.
-Hint Resolve wellformed_mem_mpc : wellformed.
-
-Lemma match_same_option :
-  forall { A B : Type},
-  forall x : option A,
-  forall y : B,
-    (match x with Some _ => y | None => y end) = y.
-Proof.
-  destruct x; trivial.
-Qed.
-
-Lemma match_same_bool :
-  forall { B : Type},
-  forall x : bool,
-  forall y : B,
-    (if x then y else y) = y.
-Proof.
-  destruct x; trivial.
-Qed.
-
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
@@ -1711,9 +1200,8 @@ Proof.
   reflexivity.
 - (* op *)
   unfold transf_instr in *.
-  destruct (if is_trivial_op op then None else find_op_in_fmap (forward_map f)  pc op (subst_args (forward_map f) pc args)) eqn:FIND_OP.
+  destruct find_op_in_fmap eqn:FIND_OP.
   {
-    destruct is_trivial_op. discriminate.
     unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
     destruct (forward_map f) as [map |] eqn:MAP.
     2: discriminate.
@@ -1803,9 +1291,9 @@ Proof.
       {
         f_equal.
         symmetry.
-        apply find_load_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial.
         rewrite MAP in H0.
-        assumption.
+        eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+        all: eassumption.
       }
       unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
     }
@@ -1830,36 +1318,37 @@ Proof.
     apply load_sound with (a := a); auto.
   }
   {  
-    econstructor; split.
-    assert (eval_addressing tge sp addr rs ## args = Some a).
-    rewrite <- H0.
-    apply eval_addressing_preserved. exact symbols_preserved.
-    eapply exec_Iload; eauto.
-    rewrite (subst_args_ok' sp m); assumption.
-    constructor; auto.
-    
-    simpl in *.
-    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 (load chunk addr dst args mpc)).
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0.
+  apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload; eauto.
+  rewrite (subst_args_ok' sp m); assumption.
+  constructor; auto.
+
+  simpl in *.
+  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 (load chunk addr dst args mpc)).
+  {
+    replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
-      replace (Some (load chunk addr dst 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.
-        simpl. tauto.
-      }
-      unfold apply_instr'.
-      rewrite H.
-      rewrite MPC.
-      simpl.
-      reflexivity.
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
     }
-    apply load_sound with (a := a); assumption.
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    simpl.
+    reflexivity.
+  }
+  apply load_sound with (a := a); assumption.
   }
   
--  unfold transf_instr in *.
+- (* load notrap1 *)
+  unfold transf_instr in *.
   destruct find_load_in_fmap eqn:FIND_LOAD.
   {
     unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
@@ -1868,16 +1357,16 @@ Proof.
     change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
     destruct (map # pc) as [mpc | ] eqn:MPC.
     2: discriminate.
-
     econstructor; split.
     {
       eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto.
+      simpl.
       rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
-      { simpl.
+      {
         f_equal.
-        apply find_load_notrap1_sound' with (chunk := chunk) (m := m) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial.
         rewrite MAP in H0.
-        assumption.
+        eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+        all: eassumption.
       }
       unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
     }
@@ -1901,37 +1390,38 @@ Proof.
     unfold sem_rel_b', sem_rel_b.
     apply load_notrap1_sound; auto.
   }
-  {
-    econstructor; split.
-    assert (eval_addressing tge sp addr rs ## args = None).
-    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-    eapply exec_Iload_notrap1; eauto.
-    rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m) ; assumption.
-    constructor; auto.
+  {  
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = None).
+  rewrite <- H0.
+  apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap1; eauto.
+  rewrite (subst_args_ok' sp m); assumption.
+  constructor; auto.
 
-    simpl in *.
-    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 (load chunk addr dst args mpc)).
+  simpl in *.
+  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 (load chunk addr dst args mpc)).
+  {
+    replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
-      replace (Some (load chunk addr dst 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.
-        simpl. tauto.
-      }
-      unfold apply_instr'.
-      rewrite H.
-      rewrite MPC.
-      simpl.
-      reflexivity.
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
     }
-    apply load_notrap1_sound; trivial.
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    simpl.
+    reflexivity.
+  }
+  apply load_notrap1_sound; assumption.
   }
   
-- (* load notrap2 *)
-   unfold transf_instr in *.
+(* load notrap2 *)
+- unfold transf_instr in *.
   destruct find_load_in_fmap eqn:FIND_LOAD.
   {
     unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
@@ -1947,9 +1437,9 @@ Proof.
       rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
       {
         f_equal.
-        apply find_load_notrap2_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial.
         rewrite MAP in H0.
-        assumption.
+        eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+        all: try eassumption.
       }
       unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
     }
@@ -1973,19 +1463,20 @@ Proof.
     unfold sem_rel_b', sem_rel_b.
     apply load_notrap2_sound with (a := a); auto.
   }
-  {
+  {  
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  rewrite <- H0.
+  apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Iload_notrap2; eauto.
-  rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption.
+  rewrite (subst_args_ok' sp m); assumption.
   constructor; auto.
 
   simpl in *.
   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  (load chunk addr dst args mpc)).
+  apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
   {
     replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
@@ -2016,9 +1507,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.
@@ -2030,7 +1521,7 @@ Proof.
   rewrite H.
   reflexivity.
   }
-  apply (kill_mem_sound' sp m); eauto with wellformed.
+  eapply (kill_store_sound' sp m); eassumption.
   
 (* call *)
 - econstructor; split.
@@ -2060,7 +1551,8 @@ Proof.
       reflexivity.
     }
     apply kill_reg_sound.
-    apply (kill_mem_sound' sp m); eauto with wellformed.
+    apply (kill_mem_sound' sp m).
+    assumption.
   }
   
 (* tailcall *)
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 67da47da..785b0a2d 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -238,7 +238,6 @@ type graph = {
    according to their types.  A variable can be forced into class 2
    by giving it a negative spill cost. *)
 
-
 let class_of_reg r =
   if Conventions1.is_float_reg r then 1 else 0
 
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 9a33768c..e25d2e5f 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1044,9 +1044,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/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/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 10e0c232..28bb992a 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).
@@ -1045,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
@@ -1057,26 +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 Mem.free_unchanged_on; eauto.
-  intros. red; intros. elim H3.
+- 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.
@@ -1084,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. }
@@ -1099,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.
@@ -1112,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 *; 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.
     rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
@@ -1127,6 +1159,7 @@ Proof.
   }
   subst sz0.
   split. constructor. intuition congruence.
++ split. constructor. intuition auto.
 Qed.
 
 (** ** Semantics of [memcpy] operations. *)
@@ -1159,8 +1192,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 +1305,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 +1350,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 +1393,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 +1440,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).
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/common/Memory.v b/common/Memory.v
index f21d99af..cd8a2001 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1307,6 +1307,23 @@ Proof.
   }
 Qed.
     
+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 ->
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index ab348c14..10f38391 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -30,6 +30,10 @@ Definition align_float64 := 8%Z.
 (** Can we use the 64-bit extensions to the PowerPC architecture? *)
 Parameter ppc64 : bool.
 
+(** 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.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
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.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 1f048694..5c9cbd4f 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 Tany64 in
+          let ofs := align ofs (typesize ty) in
+          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
+  | (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".
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.
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 --;
+  }
+}
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] --;
+  }
+}
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
new file mode 100644
index 00000000..37e16dfe
--- /dev/null
+++ b/x86/CSE2depsproof.v
@@ -0,0 +1,262 @@
+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.
+
+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 : 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 - 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 (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.
+    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 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 *.
+      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.
+      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 - 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 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.
+
+    {
+      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.
+
+
+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.