fixed CSE2 for mppa_k1c

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

5 files changed, 213 insertions, 784 deletions

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