Merge remote-tracking branch 'origin/kvx-work' into kvx-work-dirty

25 files changed, 1406 insertions, 538 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index dc1f025f..5f109224 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -201,8 +201,8 @@ Inductive instruction: Type :=
   | Pstrx_a (rs: ireg) (a: addressing)                                (**r store int64 as any64 *)
   | Pstrb (rs: ireg) (a: addressing)                                  (**r store int8 *)
   | Pstrh (rs: ireg) (a: addressing)                                  (**r store int16 *)
-  | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)                              (**r store two int64 *)
-  | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)                              (**r store two int64 *)
+  | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two int64 *)
+  | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two int64 *)
   (** Integer arithmetic, immediate *)
   | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r addition *)
   | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r subtraction *)
@@ -273,9 +273,13 @@ Inductive instruction: Type :=
   | Pldrs (rd: freg) (a: addressing)                                  (**r load float32 (single precision) *)
   | Pldrd (rd: freg) (a: addressing)                                  (**r load float64 (double precision) *)
   | Pldrd_a (rd: freg) (a: addressing)                                (**r load float64 as any64 *)
+  | Pldps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two float32 *)
+  | Pldpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two float64 *)
   | Pstrs (rs: freg) (a: addressing)                                  (**r store float32 *)
   | Pstrd (rs: freg) (a: addressing)                                  (**r store float64 *)
   | Pstrd_a (rs: freg) (a: addressing)                                (**r store float64 as any64 *)
+  | Pstps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two float32 *)
+  | Pstpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two float64 *)
   (** Floating-point move *)
   | Pfmov (rd r1: freg)
   | Pfmovimms (rd: freg) (f: float32)                                 (**r load float32 constant *)
@@ -798,7 +802,7 @@ Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
                      (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
-    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
+    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
         match Mem.loadv chk1 m addr with
         | None => Stuck
@@ -824,7 +828,7 @@ Definition exec_store_double (chk1 chk2: memory_chunk)
                       (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
-    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
+    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
       match Mem.storev chk1 m addr v1 with
       | None => Stuck
@@ -1258,17 +1262,27 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | _ => Stuck
       end
   | Pbuiltin ef args res => Stuck    (**r treated specially below *)
-  (** The following instructions and directives are not generated directly
-      by Asmgen, so we do not model them. *)
+  (** loads and stores pairs int/int64 *)
   | Pldpw rd1 rd2 chk1 chk2 a =>
       exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
   | Pldpx rd1 rd2 chk1 chk2 a =>
       exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
-  | Pnop => Next (nextinstr rs) m
   | Pstpw rs1 rs2 chk1 chk2 a =>
       exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
   | Pstpx rs1 rs2 chk1 chk2 a =>
       exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
+  (** loads and stores pairs floating-point *)
+  | Pldps rd1 rd2 chk1 chk2 a =>
+      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
+  | Pldpd rd1 rd2 chk1 chk2 a =>
+      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
+  | Pstps rs1 rs2 chk1 chk2 a =>
+      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
+  | Pstpd rs1 rs2 chk1 chk2 a =>
+      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
+  | Pnop => Next (nextinstr rs) m
+  (** The following instructions and directives are not generated directly
+      by Asmgen, so we do not model them. *)
   | Pcls _ _ _
   | Pclz _ _ _
   | Prev _ _ _
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index ed84b7d8..c606002a 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -110,11 +110,13 @@ Inductive load_rd_a: Type :=
 Inductive load_rd1_rd2_a: Type :=
   | Pldpw
   | Pldpx
+  | Pldps
+  | Pldpd
   .
 
 Inductive ld_instruction: Type :=
   | PLd_rd_a (ld: load_rd_a) (rd: dreg) (a: addressing)
-  | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int64 *)
+  | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: dreg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int64 *)
   .
 
 Inductive store_rs_a : Type :=
@@ -134,11 +136,13 @@ Inductive store_rs_a : Type :=
 Inductive store_rs1_rs2_a : Type :=
   | Pstpw
   | Pstpx
+  | Pstps
+  | Pstpd
   .
 
 Inductive st_instruction : Type :=
   | PSt_rs_a (st: store_rs_a) (rs: dreg) (a: addressing)
-  | Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)  (**r store two int64 *)
+  | Pstp (st: store_rs1_rs2_a) (rs1 rs2: dreg) (chk1 chk2: memory_chunk) (a: addressing)  (**r store two int64 *)
   .
 
 Inductive arith_p : Type :=
@@ -481,7 +485,7 @@ Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
                      (a: addressing) (rd1 rd2: dreg) (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
-    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
+    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
         match Mem.loadv chk1 m addr with
         | None => Stuck
@@ -505,7 +509,7 @@ Definition exec_store_double (chk1 chk2: memory_chunk)
                       (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
-    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
+    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
       match Mem.storev chk1 m addr v1 with
       | None => Stuck
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index e1d591df..5cd049c5 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1150,20 +1150,32 @@ Definition eval_addressing_rlocs_ld (ld: load_rd_a) (chunk: memory_chunk) (a: ad
   | ADpostincr base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
   end.
 
-Definition trans_ldp_chunk (chunk: memory_chunk): load_rd_a :=
+Definition trans_ldp_chunk (chunk: memory_chunk) (r: dreg): load_rd_a :=
   match chunk with
-  | Many32 => Pldrw_a
+  | Mint32 => Pldrw
   | Mint64 => Pldrx
-  | Many64 => Pldrx_a
-  | _ => Pldrw
+  | Mfloat32 => Pldrs
+  | Mfloat64 => Pldrd
+  | Many32 => Pldrw_a
+  | _ => (* This case should always correspond to Many64 *)
+    match r with
+    | IR _ => Pldrx_a
+    | FR _ => Pldrd_a
+    end
   end.
 
-Definition trans_stp_chunk (chunk: memory_chunk): store_rs_a :=
+Definition trans_stp_chunk (chunk: memory_chunk) (r: dreg): store_rs_a :=
   match chunk with
-  | Many32 => Pstrw_a
+  | Mint32 => Pstrw
   | Mint64 => Pstrx
-  | Many64 => Pstrx_a
-  | _ => Pstrw
+  | Mfloat32 => Pstrs
+  | Mfloat64 => Pstrd
+  | Many32 => Pstrw_a
+  | _ => (* This case should always correspond to Many64 *)
+    match r with
+    | IR _ => Pstrx_a
+    | FR _ => Pstrd_a
+    end
   end.
 
 Definition trans_load (ldi: ld_instruction) :=
@@ -1171,10 +1183,10 @@ Definition trans_load (ldi: ld_instruction) :=
   | PLd_rd_a ld r a =>
       let lr := eval_addressing_rlocs_ld ld (chunk_load ld) a in [(#r, lr)]
   | Pldp ld r1 r2 chk1 chk2 a =>
-      let ldi1 := trans_ldp_chunk chk1 in
-      let ldi2 := trans_ldp_chunk chk2 in
+      let ldi1 := trans_ldp_chunk chk1 r1 in
+      let ldi2 := trans_ldp_chunk chk2 r1 in
       let lr := eval_addressing_rlocs_ld ldi1 chk1 a in
-      let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in
+      let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4%Z | _ => 8%Z end in
       match a with
       | ADimm base n =>
         let a' := (get_offset_addr a ofs) in
@@ -1190,10 +1202,10 @@ Definition trans_store (sti: st_instruction) :=
   | PSt_rs_a st r a =>
       let lr := eval_addressing_rlocs_st st (chunk_store st) r a in [(pmem, lr)]
   | Pstp st r1 r2 chk1 chk2 a =>
-      let sti1 := trans_stp_chunk chk1 in
-      let sti2 := trans_stp_chunk chk2 in
+      let sti1 := trans_stp_chunk chk1 r1 in
+      let sti2 := trans_stp_chunk chk2 r1 in
       let lr := eval_addressing_rlocs_st sti1 chk1 r1 a in
-      let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in
+      let ofs := match chk1 with | Mint32 | Mfloat32| Many32 => 4%Z | _ => 8%Z end in
       match a with
       | ADimm base n =>
         let a' := (get_offset_addr a ofs) in
@@ -1356,6 +1368,14 @@ Proof.
   intros; destruct r; discriminate.
 Qed.
 
+Lemma dreg_not_pmem: forall (r: dreg),
+  (# r) <> pmem.
+Proof.
+  intros; destruct r as [i|f].
+  - destruct i. apply ireg_not_pmem. discriminate.
+  - apply freg_not_pmem.
+Qed.
+
 Ltac DPRM pr :=
   destruct pr as [drDPRF|crDPRF|]; 
       [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
@@ -1463,6 +1483,7 @@ Ltac discriminate_ppos :=
   try apply ireg_not_pmem;
   try apply ireg_not_pc;
   try apply freg_not_pmem;
+  try apply dreg_not_pmem;
   try apply ireg_not_CN;
   try apply ireg_not_CZ;
   try apply ireg_not_CC;
@@ -1706,10 +1727,10 @@ Proof.
   econstructor.
 Qed.
 
-Lemma load_chunk_neutral: forall chk v,
-  interp_load (trans_ldp_chunk chk) v = v.
+Lemma load_chunk_neutral: forall chk v r,
+  interp_load (trans_ldp_chunk chk r) v = v.
 Proof.
-  intros; destruct chk; simpl; reflexivity.
+  intros; destruct chk; destruct r; simpl; reflexivity.
 Qed.
 
 Theorem bisimu_basic rsr mr sr bi:
@@ -1749,8 +1770,10 @@ Local Ltac preg_eq_discr r rd :=
       try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr;
       rewrite !load_chunk_neutral;
       try (rewrite !assign_diff; discriminate_ppos; reflexivity);
-      try (destruct base; discriminate_ppos);
-      repeat (try fold (ppos r); intros; Simpl_update).
+      try (destruct rd1 as [ir1|fr1]; try destruct ir1; destruct rd2 as [ir2|fr2]; try destruct ir2;
+      destruct base; discriminate_ppos);
+      repeat (try fold (ppos r); try fold (ppos r0);
+      try fold (ppos fr1); try fold (ppos fr2); intros; Simpl_update).
   - (* Store *)
     destruct st.
     + unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval;
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index a720c11c..45205158 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -326,10 +326,16 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
 
   | PLoad (Pldp Pldpw rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1;
                                     do rd2' <- ireg_of_preg rd2;
-                                    OK (Asm.Pldpw rd1 rd2 chk1 chk2 a)
+                                    OK (Asm.Pldpw rd1' rd2' chk1 chk2 a)
   | PLoad (Pldp Pldpx rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1;
                                     do rd2' <- ireg_of_preg rd2;
-                                    OK (Asm.Pldpx rd1 rd2 chk1 chk2 a)
+                                    OK (Asm.Pldpx rd1' rd2' chk1 chk2 a)
+  | PLoad (Pldp Pldps rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1;
+                                    do rd2' <- freg_of_preg rd2;
+                                    OK (Asm.Pldps rd1' rd2' chk1 chk2 a)
+  | PLoad (Pldp Pldpd rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1;
+                                    do rd2' <- freg_of_preg rd2;
+                                    OK (Asm.Pldpd rd1' rd2' chk1 chk2 a)
 
   | PStore (PSt_rs_a Pstrw   r a) => do r'  <- ireg_of_preg r; OK (Asm.Pstrw   r' a)
   | PStore (PSt_rs_a Pstrw_a r a) => do r'  <- ireg_of_preg r; OK (Asm.Pstrw_a r' a)
@@ -344,10 +350,16 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
 
   | PStore (Pstp Pstpw rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
                                     do rs2' <- ireg_of_preg rs2;
-                                    OK (Asm.Pstpw rs1 rs2 chk1 chk2 a)
+                                    OK (Asm.Pstpw rs1' rs2' chk1 chk2 a)
   | PStore (Pstp Pstpx rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
                                     do rs2' <- ireg_of_preg rs2;
-                                    OK (Asm.Pstpx rs1 rs2 chk1 chk2 a)
+                                    OK (Asm.Pstpx rs1' rs2' chk1 chk2 a)
+  | PStore (Pstp Pstps rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
+                                    do rs2' <- freg_of_preg rs2;
+                                    OK (Asm.Pstps rs1' rs2' chk1 chk2 a)
+  | PStore (Pstp Pstpd rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
+                                    do rs2' <- freg_of_preg rs2;
+                                    OK (Asm.Pstpd rs1' rs2' chk1 chk2 a)
 
   | Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs)
   | Pfreeframe  sz linkofs => OK (Asm.Pfreeframe  sz linkofs)
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index a33f90b3..d27b3f8c 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1100,7 +1100,7 @@ Proof.
   destruct (Mem.loadv chk2 m2
       (eval_addressing lk
          (get_offset_addr a match chk1 with
-                            | Mint32 | Many32 => 4
+                            | Mint32 | Mfloat32| Many32 => 4
                             | _ => 8
                             end) rs1));
   inversion HLOAD; auto.
@@ -1150,7 +1150,7 @@ Proof.
              (eval_addressing lk
                 (get_offset_addr a
                    match chk1 with
-                   | Mint32 | Many32 => 4
+                   | Mint32 | Mfloat32 | Many32 => 4
                    | _ => 8
                    end) rs1) v2);
   inversion HSTORE; auto.
@@ -1331,12 +1331,14 @@ Proof.
     destruct ld.
     - destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_rd_a_preserved; eauto;
       intros; simpl in *; destruct sz; eauto.
-    - destruct ld; monadInv TRANSBI; exploit load_double_preserved; eauto. }
+    - destruct ld; monadInv TRANSBI; destruct rd1 as [[rd1'|]|]; destruct rd2 as [[rd2'|]|];
+      inv EQ; inv EQ1; exploit load_double_preserved; eauto. }
   { (* PStore *)
     destruct st.
     - destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_rs_a_preserved; eauto;
       simpl in *; inv_matchi; find_rwrt_ag.
-    - destruct st; monadInv TRANSBI; exploit store_double_preserved; eauto;
+    - destruct st; monadInv TRANSBI; destruct rs0 as [[rs0'|]|]; destruct rs3 as [[rs3'|]|];
+      inv EQ; inv EQ1; exploit store_double_preserved; eauto;
       simpl in *; inv_matchi; find_rwrt_ag. }
   { (* Pallocframe *)
     monadInv TRANSBI;
@@ -2224,8 +2226,7 @@ Proof.
   - apply senv_preserved.
   - eexact transf_initial_states.
   - eexact transf_final_states.
-  - (* TODO step_simulation *)
-    unfold match_states.
+  - unfold match_states.
     simpl; intros; subst; eexists; split; eauto.
     eapply step_simulation; eauto.
 Qed.
diff --git a/aarch64/Op.v b/aarch64/Op.v
index f2a8e6fb..40f6ebf0 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -1202,18 +1202,26 @@ Proof.
   rewrite (cond_depends_on_memory_correct cond args m1 m2 H). auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+    
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op eqn:OP; simpl; try congruence.
-  - intros MEM; destruct cond; simpl; try congruence;
+  intros until m2. intro MEM. destruct op eqn:OP; simpl; try congruence.
+  - f_equal; f_equal; auto using cond_valid_pointer_eq.
+  - destruct cond; simpl; try congruence;
     repeat (destruct args; simpl; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intro MEM; destruct cond; simpl; try congruence;
-      repeat (destruct args; simpl; try congruence);
-      erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index a6945b9f..18f41fed 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -27,37 +27,37 @@ let is_valid_immofs_64 z =
   if z <= 504 && z >= -512 && z mod 8 = 0 then true else false
 
 (* Functions to check if a ldp/stp replacement is valid according to args *)
-let is_valid_ldrw rd1 rd2 b1 b2 n1 n2 =
+let is_valid_ldr32 rd1 rd2 b1 b2 n1 n2 =
   let z1 = to_int (camlint64_of_coqint n1) in
   let z2 = to_int (camlint64_of_coqint n2) in
   if
-    (not (ireg_eq rd1 rd2))
+    (not (dreg_eq rd1 rd2))
     && iregsp_eq b1 b2
-    && (not (iregsp_eq (RR1 rd1) b2))
+    && (not (dreg_eq rd1 (IR b2)))
     && (z2 = z1 + 4 || z2 = z1 - 4)
     && is_valid_immofs_32 z1
   then true
   else false
 
-let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
+let is_valid_ldr64 rd1 rd2 b1 b2 n1 n2 =
   let z1 = to_int (camlint64_of_coqint n1) in
   let z2 = to_int (camlint64_of_coqint n2) in
   if
-    (not (ireg_eq rd1 rd2))
+    (not (dreg_eq rd1 rd2))
     && iregsp_eq b1 b2
-    && (not (iregsp_eq (RR1 rd1) b2))
+    && (not (dreg_eq rd1 (IR b2)))
     && (z2 = z1 + 8 || z2 = z1 - 8)
     && is_valid_immofs_64 z1
   then true
   else false
 
-let is_valid_strw b1 b2 n1 n2 =
+let is_valid_str32 b1 b2 n1 n2 =
   let z1 = to_int (camlint64_of_coqint n1) in
   let z2 = to_int (camlint64_of_coqint n2) in
   if iregsp_eq b1 b2 && z2 = z1 + 4 && is_valid_immofs_32 z1 then true
   else false
 
-let is_valid_strx b1 b2 n1 n2 =
+let is_valid_str64 b1 b2 n1 n2 =
   let z1 = to_int (camlint64_of_coqint n1) in
   let z2 = to_int (camlint64_of_coqint n2) in
   if iregsp_eq b1 b2 && z2 = z1 + 8 && is_valid_immofs_64 z1 then true
@@ -65,29 +65,45 @@ let is_valid_strx b1 b2 n1 n2 =
 
 let dreg_of_ireg r = IR (RR1 r)
 
+let dreg_of_freg r = FR r
+
 (* Return true if an intermediate
  * affectation eliminates the potential
  * candidate *)
 let verify_load_affect reg rd b rev =
   let b = IR b in
-  let rd = dreg_of_ireg rd in
   if not rev then dreg_eq reg b else dreg_eq reg b || dreg_eq reg rd
 
 (* Return true if an intermediate
  * read eliminates the potential
  * candidate *)
-let verify_load_read reg rd b rev =
-  let rd = dreg_of_ireg rd in
-  dreg_eq reg rd
+let verify_load_read reg rd b rev = dreg_eq reg rd
 
 (* Return true if an intermediate
  * affectation eliminates the potential
  * candidate *)
 let verify_store_affect reg rs b rev =
   let b = IR b in
-  let rs = dreg_of_ireg rs in
   dreg_eq reg b || dreg_eq reg rs
 
+type ph_type = P32 | P32f | P64 | P64f
+
+type inst_type = Ldr of ph_type | Str of ph_type
+
+let ph_ty_to_string = function
+  | Ldr P32 -> "ldr32"
+  | Ldr P32f -> "ldr32f"
+  | Ldr P64 -> "ldr64"
+  | Ldr P64f -> "ldr64f"
+  | Str P32 -> "str32"
+  | Str P32f -> "str32f"
+  | Str P64 -> "str64"
+  | Str P64f -> "str64f"
+
+let print_ph_ty chan v = output_string chan (ph_ty_to_string v)
+
+let symb_mem = Hashtbl.create 9
+
 (* Affect a symbolic memory list of potential replacements
  * for a given write in reg *)
 let rec affect_symb_mem reg insta pot_rep stype rev =
@@ -95,11 +111,11 @@ let rec affect_symb_mem reg insta pot_rep stype rev =
   | [] -> []
   | h0 :: t0 -> (
       match (insta.(h0), stype) with
-      | PLoad (PLd_rd_a (_, IR (RR1 rd), ADimm (b, n))), "ldr" ->
+      | PLoad (PLd_rd_a (_, rd, ADimm (b, n))), Ldr _ ->
           if verify_load_affect reg rd b rev then
             affect_symb_mem reg insta t0 stype rev
           else h0 :: affect_symb_mem reg insta t0 stype rev
-      | PStore (PSt_rs_a (_, IR (RR1 rs), ADimm (b, n))), "str" ->
+      | PStore (PSt_rs_a (_, rs, ADimm (b, n))), Str _ ->
           if verify_store_affect reg rs b rev then
             affect_symb_mem reg insta t0 stype rev
           else h0 :: affect_symb_mem reg insta t0 stype rev
@@ -113,11 +129,11 @@ let rec read_symb_mem reg insta pot_rep stype rev =
   | [] -> []
   | h0 :: t0 -> (
       match (insta.(h0), stype) with
-      | PLoad (PLd_rd_a (_, IR (RR1 rd), ADimm (b, n))), "ldr" ->
+      | PLoad (PLd_rd_a (_, rd, ADimm (b, n))), Ldr _ ->
           if verify_load_read reg rd b rev then
             read_symb_mem reg insta t0 stype rev
           else h0 :: read_symb_mem reg insta t0 stype rev
-      | PStore (PSt_rs_a (_, IR (RR1 rs), ADimm (b, n))), "str" ->
+      | PStore (PSt_rs_a (_, rs, ADimm (b, n))), Str _ ->
           h0 :: read_symb_mem reg insta t0 stype rev
       | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep")
 
@@ -146,8 +162,9 @@ let update_pot_rep_addressing a insta pot_rep stype rev =
 
 (* Update a symbolic memory list of potential replacements
  * for any basic instruction *)
-let update_pot_rep_basic inst insta pot_rep stype rev =
-  match inst with
+let update_pot_rep_basic inst insta stype rev =
+  let pot_rep = Hashtbl.find symb_mem stype in
+  (match inst with
   | PArith i -> (
       match i with
       | PArithP (_, rd) ->
@@ -197,7 +214,8 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
           pot_rep := read_symb_mem rs1 insta !pot_rep stype rev
       | Pcset (rd, _) ->
           pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
-      | Pfmovi (_, _, rs) -> (
+      | Pfmovi (_, rd, rs) -> (
+          pot_rep := affect_symb_mem (dreg_of_freg rd) insta !pot_rep stype rev;
           match rs with
           | RR0 rs ->
               pot_rep :=
@@ -207,28 +225,29 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
           pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
           pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
           pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
-      | Pfnmul (_, rd, rs1, rs2) -> ())
+      | Pfnmul (_, rd, rs1, rs2) ->
+          pot_rep := affect_symb_mem (dreg_of_freg rd) insta !pot_rep stype rev;
+          pot_rep := read_symb_mem (dreg_of_freg rs1) insta !pot_rep stype rev;
+          pot_rep := read_symb_mem (dreg_of_freg rs2) insta !pot_rep stype rev)
   | PLoad i -> (
       (* Here, we consider a different behavior for load and store potential candidates:
          * a load does not obviously cancel the ldp candidates, but it does for any stp candidate. *)
       match stype with
-      | "ldr" -> (
+      | Ldr _ -> (
           match i with
           | PLd_rd_a (_, rd, a) ->
               pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
               update_pot_rep_addressing a insta pot_rep stype rev
           | Pldp (_, rd1, rd2, _, _, a) ->
-              pot_rep :=
-                affect_symb_mem (dreg_of_ireg rd1) insta !pot_rep stype rev;
-              pot_rep :=
-                affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype rev;
+              pot_rep := affect_symb_mem rd1 insta !pot_rep stype rev;
+              pot_rep := affect_symb_mem rd2 insta !pot_rep stype rev;
               update_pot_rep_addressing a insta pot_rep stype rev)
       | _ -> pot_rep := [])
   | PStore _ -> (
       (* Here, we consider that a store cancel all ldp candidates, but it is far more complicated for stp ones :
          * if we cancel stp candidates here, we would prevent ourselves to apply the non-consec store peephole.
          * To solve this issue, the store candidates cleaning is managed directly in the peephole function below. *)
-      match stype with "ldr" -> pot_rep := [] | _ -> ())
+      match stype with Ldr _ -> pot_rep := [] | _ -> ())
   | Pallocframe (_, _) -> pot_rep := []
   | Pfreeframe (_, _) -> pot_rep := []
   | Ploadsymbol (rd, _) ->
@@ -242,60 +261,8 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
   | Pcvtx2w rd ->
       pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
       pot_rep := read_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
-  | Pnop -> ()
-
-(* Try to find the index of the first previous compatible
- * replacement in a given symbolic memory *)
-let rec search_compat_rep r2 b2 n2 insta pot_rep stype =
-  match pot_rep with
-  | [] -> None
-  | h0 :: t0 -> (
-      match (insta.(h0), stype) with
-      | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
-          if is_valid_ldrw rd1 r2 b1 b2 n1 n2 then
-            Some (h0, chunk_load ld1, rd1, b1, n1)
-          else search_compat_rep r2 b2 n2 insta t0 stype
-      | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" ->
-          if is_valid_ldrx rd1 r2 b1 b2 n1 n2 then
-            Some (h0, chunk_load ld1, rd1, b1, n1)
-          else search_compat_rep r2 b2 n2 insta t0 stype
-      | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strw" ->
-          if is_valid_strw b1 b2 n1 n2 then
-            Some (h0, chunk_store st1, rs1, b1, n1)
-          else search_compat_rep r2 b2 n2 insta t0 stype
-      | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strx" ->
-          if is_valid_strx b1 b2 n1 n2 then
-            Some (h0, chunk_store st1, rs1, b1, n1)
-          else search_compat_rep r2 b2 n2 insta t0 stype
-      | _, _ ->
-          failwith "search_compat_rep: Found an inconsistent inst in pot_rep")
-
-(* Try to find the index of the first previous compatible
- * replacement in a given symbolic memory (when iterating in the reversed list) *)
-let rec search_compat_rep_inv r2 b2 n2 insta pot_rep stype =
-  match pot_rep with
-  | [] -> None
-  | h0 :: t0 -> (
-      match (insta.(h0), stype) with
-      | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
-          if is_valid_ldrw r2 rd1 b2 b1 n2 n1 then
-            Some (h0, chunk_load ld1, rd1, b1, n1)
-          else search_compat_rep_inv r2 b2 n2 insta t0 stype
-      | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" ->
-          if is_valid_ldrx r2 rd1 b2 b1 n2 n1 then
-            Some (h0, chunk_load ld1, rd1, b1, n1)
-          else search_compat_rep_inv r2 b2 n2 insta t0 stype
-      | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strw" ->
-          if is_valid_strw b2 b1 n2 n1 then
-            Some (h0, chunk_store st1, rs1, b1, n1)
-          else search_compat_rep_inv r2 b2 n2 insta t0 stype
-      | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strx" ->
-          if is_valid_strx b2 b1 n2 n1 then
-            Some (h0, chunk_store st1, rs1, b1, n1)
-          else search_compat_rep_inv r2 b2 n2 insta t0 stype
-      | _, _ ->
-          failwith
-            "search_compat_rep_inv: Found an inconsistent inst in pot_rep")
+  | Pnop -> ());
+  Hashtbl.replace symb_mem stype pot_rep
 
 (* This is useful to manage the case were the immofs
  * of the first ldr/str is greater than the second one *)
@@ -310,82 +277,150 @@ let trans_ldi (ldi : load_rd_a) : load_rd1_rd2_a =
   match ldi with
   | Pldrw | Pldrw_a -> Pldpw
   | Pldrx | Pldrx_a -> Pldpx
+  | Pldrs -> Pldps
+  | Pldrd | Pldrd_a -> Pldpd
   | _ -> failwith "trans_ldi: Found a non compatible load to translate"
 
 let trans_sti (sti : store_rs_a) : store_rs1_rs2_a =
   match sti with
   | Pstrw | Pstrw_a -> Pstpw
   | Pstrx | Pstrx_a -> Pstpx
+  | Pstrs -> Pstps
+  | Pstrd | Pstrd_a -> Pstpd
   | _ -> failwith "trans_sti: Found a non compatible store to translate"
 
 let is_compat_load (ldi : load_rd_a) =
-  match ldi with Pldrw | Pldrw_a | Pldrx | Pldrx_a -> true | _ -> false
+  match ldi with
+  | Pldrw | Pldrw_a | Pldrx | Pldrx_a | Pldrs | Pldrd | Pldrd_a -> true
+  | _ -> false
 
 let are_compat_load (ldi1 : load_rd_a) (ldi2 : load_rd_a) =
   match ldi1 with
   | Pldrw | Pldrw_a -> ( match ldi2 with Pldrw | Pldrw_a -> true | _ -> false)
   | Pldrx | Pldrx_a -> ( match ldi2 with Pldrx | Pldrx_a -> true | _ -> false)
+  | Pldrs -> ( match ldi2 with Pldrs -> true | _ -> false)
+  | Pldrd | Pldrd_a -> ( match ldi2 with Pldrd | Pldrd_a -> true | _ -> false)
   | _ -> false
 
 let is_compat_store (sti : store_rs_a) =
-  match sti with Pstrw | Pstrw_a | Pstrx | Pstrx_a -> true | _ -> false
+  match sti with
+  | Pstrw | Pstrw_a | Pstrx | Pstrx_a | Pstrs | Pstrd | Pstrd_a -> true
+  | _ -> false
 
 let are_compat_store (sti1 : store_rs_a) (sti2 : store_rs_a) =
   match sti1 with
   | Pstrw | Pstrw_a -> ( match sti2 with Pstrw | Pstrw_a -> true | _ -> false)
   | Pstrx | Pstrx_a -> ( match sti2 with Pstrx | Pstrx_a -> true | _ -> false)
+  | Pstrs -> ( match sti2 with Pstrs -> true | _ -> false)
+  | Pstrd | Pstrd_a -> ( match sti2 with Pstrd | Pstrd_a -> true | _ -> false)
   | _ -> false
 
-let get_load_string (ldi : load_rd_a) =
+let get_load_pht (ldi : load_rd_a) =
   match ldi with
-  | Pldrw | Pldrw_a -> "ldrw"
-  | Pldrx | Pldrx_a -> "ldrx"
+  | Pldrw | Pldrw_a -> Ldr P32
+  | Pldrs -> Ldr P32f
+  | Pldrx | Pldrx_a -> Ldr P64
+  | Pldrd | Pldrd_a -> Ldr P64f
   | _ -> failwith "get_load_string: Found a non compatible load to translate"
 
-let get_store_string (sti : store_rs_a) =
+let get_store_pht (sti : store_rs_a) =
   match sti with
-  | Pstrw | Pstrw_a -> "strw"
-  | Pstrx | Pstrx_a -> "strx"
+  | Pstrw | Pstrw_a -> Str P32
+  | Pstrs -> Str P32f
+  | Pstrx | Pstrx_a -> Str P64
+  | Pstrd | Pstrd_a -> Str P64f
   | _ -> failwith "get_store_string: Found a non compatible store to translate"
 
 let is_valid_ldr rd1 rd2 b1 b2 n1 n2 stype =
   match stype with
-  | "ldrw" -> is_valid_ldrw rd1 rd2 b1 b2 n1 n2
-  | _ -> is_valid_ldrx rd1 rd2 b1 b2 n1 n2
+  | Ldr P32 | Ldr P32f -> is_valid_ldr32 rd1 rd2 b1 b2 n1 n2
+  | _ -> is_valid_ldr64 rd1 rd2 b1 b2 n1 n2
 
 let is_valid_str b1 b2 n1 n2 stype =
   match stype with
-  | "strw" -> is_valid_strw b1 b2 n1 n2
-  | _ -> is_valid_strx b1 b2 n1 n2
+  | Str P32 | Str P32f -> is_valid_str32 b1 b2 n1 n2
+  | _ -> is_valid_str64 b1 b2 n1 n2
+
+(* Try to find the index of the first previous compatible
+ * replacement in a given symbolic memory *)
+let rec search_compat_rep r2 b2 n2 insta pot_rep stype =
+  match pot_rep with
+  | [] -> None
+  | h0 :: t0 -> (
+      match insta.(h0) with
+      | PLoad (PLd_rd_a (ld1, rd1, ADimm (b1, n1))) ->
+          if is_valid_ldr rd1 r2 b1 b2 n1 n2 stype then
+            Some (h0, chunk_load ld1, rd1, b1, n1)
+          else search_compat_rep r2 b2 n2 insta t0 stype
+      | PStore (PSt_rs_a (st1, rs1, ADimm (b1, n1))) ->
+          if is_valid_str b1 b2 n1 n2 stype then
+            Some (h0, chunk_store st1, rs1, b1, n1)
+          else search_compat_rep r2 b2 n2 insta t0 stype
+      | _ -> failwith "search_compat_rep: Found an inconsistent inst in pot_rep"
+      )
+
+(* Try to find the index of the first previous compatible
+ * replacement in a given symbolic memory (when iterating in the reversed list) *)
+let rec search_compat_rep_inv r2 b2 n2 insta pot_rep stype =
+  match pot_rep with
+  | [] -> None
+  | h0 :: t0 -> (
+      match insta.(h0) with
+      | PLoad (PLd_rd_a (ld1, rd1, ADimm (b1, n1))) ->
+          if is_valid_ldr r2 rd1 b2 b1 n2 n1 stype then
+            Some (h0, chunk_load ld1, rd1, b1, n1)
+          else search_compat_rep_inv r2 b2 n2 insta t0 stype
+      | PStore (PSt_rs_a (st1, rs1, ADimm (b1, n1))) ->
+          if is_valid_str b2 b1 n2 n1 stype then
+            Some (h0, chunk_store st1, rs1, b1, n1)
+          else search_compat_rep_inv r2 b2 n2 insta t0 stype
+      | _ ->
+          failwith
+            "search_compat_rep_ldst_inv: Found an inconsistent inst in pot_rep")
+
+let init_symb_mem () =
+  Hashtbl.clear symb_mem;
+  Hashtbl.add symb_mem (Ldr P32) (ref []);
+  Hashtbl.add symb_mem (Ldr P64) (ref []);
+  Hashtbl.add symb_mem (Ldr P32f) (ref []);
+  Hashtbl.add symb_mem (Ldr P64f) (ref []);
+  Hashtbl.add symb_mem (Str P32) (ref []);
+  Hashtbl.add symb_mem (Str P64) (ref []);
+  Hashtbl.add symb_mem (Str P32f) (ref []);
+  Hashtbl.add symb_mem (Str P64f) (ref [])
+
+let reset_str_symb_mem () =
+  Hashtbl.replace symb_mem (Str P32) (ref []);
+  Hashtbl.replace symb_mem (Str P64) (ref []);
+  Hashtbl.replace symb_mem (Str P32f) (ref []);
+  Hashtbl.replace symb_mem (Str P64f) (ref [])
 
 (* Main peephole function in backward style *)
 let pair_rep_inv insta =
   (* Each list below is a symbolic mem representation
    * for one type of inst. Lists contains integers which
    * are the indices of insts in the main array "insta". *)
-  let pot_ldrw_rep = ref [] in
-  let pot_ldrx_rep = ref [] in
-  let pot_strw_rep = ref [] in
-  let pot_strx_rep = ref [] in
+  init_symb_mem ();
   for i = Array.length insta - 1 downto 1 do
     let h0 = insta.(i) in
     let h1 = insta.(i - 1) in
     (* Here we need to update every symbolic memory according to the matched inst *)
-    update_pot_rep_basic h0 insta pot_ldrw_rep "ldr" true;
-    update_pot_rep_basic h0 insta pot_ldrx_rep "ldr" true;
-    update_pot_rep_basic h0 insta pot_strw_rep "str" true;
-    update_pot_rep_basic h0 insta pot_strx_rep "str" true;
+    update_pot_rep_basic h0 insta (Ldr P32) true;
+    update_pot_rep_basic h0 insta (Ldr P64) true;
+    update_pot_rep_basic h0 insta (Ldr P32f) true;
+    update_pot_rep_basic h0 insta (Ldr P64f) true;
+    update_pot_rep_basic h0 insta (Str P32) true;
+    update_pot_rep_basic h0 insta (Str P64) true;
+    update_pot_rep_basic h0 insta (Str P32f) true;
+    update_pot_rep_basic h0 insta (Str P64f) true;
     match (h0, h1) with
     (* Non-consecutive ldr *)
-    | PLoad (PLd_rd_a (ldi, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
-        if is_compat_load ldi then
-          let pot_rep =
-            match ldi with Pldrw | Pldrw_a -> pot_ldrw_rep | _ -> pot_ldrx_rep
-          in
+    | PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))), _ ->
+        if is_compat_load ldi then (
           (* Search a previous compatible load *)
-          match
-            search_compat_rep_inv rd1 b1 n1 insta !pot_rep (get_load_string ldi)
-          with
+          let ld_t = get_load_pht ldi in
+          let pot_rep = Hashtbl.find symb_mem ld_t in
+          (match search_compat_rep_inv rd1 b1 n1 insta !pot_rep ld_t with
           (* If we can't find a candidate, add the current load as a potential future one *)
           | None -> pot_rep := i :: !pot_rep
           (* Else, perform the peephole *)
@@ -395,53 +430,48 @@ let pair_rep_inv insta =
               pot_rep := List.filter filt !pot_rep;
               insta.(rep) <- Pnop;
               if min_is_rev n n1 then (
-                if debug then eprintf "LDP_BACK_SPACED_PEEP_IMM_INC\n";
+                if debug then
+                  eprintf "LDP_BACK_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty ld_t;
                 insta.(i) <-
                   PLoad
                     (Pldp
                        (trans_ldi ldi, r, rd1, c, chunk_load ldi, ADimm (b, n))))
               else (
-                if debug then eprintf "LDP_BACK_SPACED_PEEP_IMM_DEC\n";
+                if debug then
+                  eprintf "LDP_BACK_SPACED_PEEP_IMM_DEC_%a\n" print_ph_ty ld_t;
                 insta.(i) <-
                   PLoad
                     (Pldp
-                       (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1))))
-        )
+                       (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))));
+          Hashtbl.replace symb_mem ld_t pot_rep)
     (* Non-consecutive str *)
-    | PStore (PSt_rs_a (sti, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
-        if is_compat_store sti then
-          let pot_rep =
-            match sti with Pstrw | Pstrw_a -> pot_strw_rep | _ -> pot_strx_rep
-          in
+    | PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))), _ ->
+        if is_compat_store sti then (
           (* Search a previous compatible store *)
-          match
-            search_compat_rep_inv rd1 b1 n1 insta !pot_rep
-              (get_store_string sti)
-          with
+          let st_t = get_store_pht sti in
+          let pot_rep = Hashtbl.find symb_mem st_t in
+          (match search_compat_rep_inv rd1 b1 n1 insta !pot_rep st_t with
           (* If we can't find a candidate, clean and add the current store as a potential future one *)
           | None ->
-              pot_strw_rep := [];
-              pot_strx_rep := [];
-              pot_rep := i :: !pot_rep
+              reset_str_symb_mem ();
+              pot_rep := [ i ]
           (* Else, perform the peephole *)
           | Some (rep, c, r, b, n) ->
               (* The two lines below are used to filter the elected candidate *)
               let filt x = x != rep in
               pot_rep := List.filter filt !pot_rep;
               insta.(rep) <- Pnop;
-              if debug then eprintf "STP_BACK_SPACED_PEEP_IMM_INC\n";
+              if debug then
+                eprintf "STP_BACK_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
               insta.(i) <-
                 PStore
                   (Pstp
-                     (trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1)))
+                     (trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1))));
+          Hashtbl.replace symb_mem st_t pot_rep
           (* Any other inst *))
     | i, _ -> (
         (* Clear list of candidates if there is a non supported store *)
-        match i with
-        | PStore _ ->
-            pot_strw_rep := [];
-            pot_strx_rep := []
-        | _ -> ())
+        match i with PStore _ -> reset_str_symb_mem () | _ -> ())
   done
 
 (* Main peephole function in forward style *)
@@ -449,26 +479,29 @@ let pair_rep insta =
   (* Each list below is a symbolic mem representation
    * for one type of inst. Lists contains integers which
    * are the indices of insts in the main array "insta". *)
-  let pot_ldrw_rep = ref [] in
-  let pot_ldrx_rep = ref [] in
-  let pot_strw_rep = ref [] in
-  let pot_strx_rep = ref [] in
+  init_symb_mem ();
   for i = 0 to Array.length insta - 2 do
     let h0 = insta.(i) in
     let h1 = insta.(i + 1) in
     (* Here we need to update every symbolic memory according to the matched inst *)
-    update_pot_rep_basic h0 insta pot_ldrw_rep "ldr" false;
-    update_pot_rep_basic h0 insta pot_ldrx_rep "ldr" false;
-    update_pot_rep_basic h0 insta pot_strw_rep "str" false;
-    update_pot_rep_basic h0 insta pot_strx_rep "str" false;
+    update_pot_rep_basic h0 insta (Ldr P32) false;
+    update_pot_rep_basic h0 insta (Ldr P64) false;
+    update_pot_rep_basic h0 insta (Ldr P32f) false;
+    update_pot_rep_basic h0 insta (Ldr P64f) false;
+    update_pot_rep_basic h0 insta (Str P32) false;
+    update_pot_rep_basic h0 insta (Str P64) false;
+    update_pot_rep_basic h0 insta (Str P32f) false;
+    update_pot_rep_basic h0 insta (Str P64f) false;
     match (h0, h1) with
     (* Consecutive ldr *)
-    | ( PLoad (PLd_rd_a (ldi1, IR (RR1 rd1), ADimm (b1, n1))),
-        PLoad (PLd_rd_a (ldi2, IR (RR1 rd2), ADimm (b2, n2))) ) ->
+    | ( PLoad (PLd_rd_a (ldi1, rd1, ADimm (b1, n1))),
+        PLoad (PLd_rd_a (ldi2, rd2, ADimm (b2, n2))) ) ->
         if are_compat_load ldi1 ldi2 then
-          if is_valid_ldr rd1 rd2 b1 b2 n1 n2 (get_load_string ldi1) then (
+          let ld_t = get_load_pht ldi1 in
+          if is_valid_ldr rd1 rd2 b1 b2 n1 n2 ld_t then (
             if min_is_rev n1 n2 then (
-              if debug then eprintf "LDP_CONSEC_PEEP_IMM_INC\n";
+              if debug then
+                eprintf "LDP_CONSEC_PEEP_IMM_INC_%a\n" print_ph_ty ld_t;
               insta.(i) <-
                 PLoad
                   (Pldp
@@ -479,7 +512,8 @@ let pair_rep insta =
                        chunk_load ldi2,
                        ADimm (b1, n1) )))
             else (
-              if debug then eprintf "LDP_CONSEC_PEEP_IMM_DEC\n";
+              if debug then
+                eprintf "LDP_CONSEC_PEEP_IMM_DEC_%a\n" print_ph_ty ld_t;
               insta.(i) <-
                 PLoad
                   (Pldp
@@ -491,15 +525,12 @@ let pair_rep insta =
                        ADimm (b1, n2) )));
             insta.(i + 1) <- Pnop)
     (* Non-consecutive ldr *)
-    | PLoad (PLd_rd_a (ldi, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
-        if is_compat_load ldi then
-          let pot_rep =
-            match ldi with Pldrw | Pldrw_a -> pot_ldrw_rep | _ -> pot_ldrx_rep
-          in
+    | PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))), _ ->
+        if is_compat_load ldi then (
           (* Search a previous compatible load *)
-          match
-            search_compat_rep rd1 b1 n1 insta !pot_rep (get_load_string ldi)
-          with
+          let ld_t = get_load_pht ldi in
+          let pot_rep = Hashtbl.find symb_mem ld_t in
+          (match search_compat_rep rd1 b1 n1 insta !pot_rep ld_t with
           (* If we can't find a candidate, add the current load as a potential future one *)
           | None -> pot_rep := i :: !pot_rep
           (* Else, perform the peephole *)
@@ -509,29 +540,32 @@ let pair_rep insta =
               pot_rep := List.filter filt !pot_rep;
               insta.(rep) <- Pnop;
               if min_is_rev n n1 then (
-                if debug then eprintf "LDP_FORW_SPACED_PEEP_IMM_INC\n";
+                if debug then
+                  eprintf "LDP_FORW_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty ld_t;
                 insta.(i) <-
                   PLoad
                     (Pldp
                        (trans_ldi ldi, r, rd1, c, chunk_load ldi, ADimm (b, n))))
               else (
-                if debug then eprintf "LDP_FORW_SPACED_PEEP_IMM_DEC\n";
+                if debug then
+                  eprintf "LDP_FORW_SPACED_PEEP_IMM_DEC_%a\n" print_ph_ty ld_t;
                 insta.(i) <-
                   PLoad
                     (Pldp
-                       (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1))))
-        )
+                       (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))));
+          Hashtbl.replace symb_mem ld_t pot_rep)
     (* Consecutive str *)
-    | ( PStore (PSt_rs_a (sti1, IR (RR1 rd1), ADimm (b1, n1))),
-        PStore (PSt_rs_a (sti2, IR (RR1 rd2), ADimm (b2, n2))) ) ->
+    | ( PStore (PSt_rs_a (sti1, rd1, ADimm (b1, n1))),
+        PStore (PSt_rs_a (sti2, rd2, ADimm (b2, n2))) ) ->
         (* Regardless of whether we can perform the peephole or not,
          * we have to clean the potential candidates for stp now as we are
          * looking at two new store instructions. *)
-        pot_strw_rep := [];
-        pot_strx_rep := [];
+        reset_str_symb_mem ();
         if are_compat_store sti1 sti2 then
-          if is_valid_str b1 b2 n1 n2 (get_store_string sti1) then (
-            if debug then eprintf "STP_CONSEC_PEEP_IMM_INC\n";
+          let st_t = get_store_pht sti1 in
+          if is_valid_str b1 b2 n1 n2 st_t then (
+            if debug then
+              eprintf "STP_CONSEC_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
             insta.(i) <-
               PStore
                 (Pstp
@@ -543,39 +577,32 @@ let pair_rep insta =
                      ADimm (b1, n1) ));
             insta.(i + 1) <- Pnop)
     (* Non-consecutive str *)
-    | PStore (PSt_rs_a (sti, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
-        if is_compat_store sti then
-          let pot_rep =
-            match sti with Pstrw | Pstrw_a -> pot_strw_rep | _ -> pot_strx_rep
-          in
+    | PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))), _ ->
+        if is_compat_store sti then (
           (* Search a previous compatible store *)
-          match
-            search_compat_rep rd1 b1 n1 insta !pot_rep (get_store_string sti)
-          with
+          let st_t = get_store_pht sti in
+          let pot_rep = Hashtbl.find symb_mem st_t in
+          (match search_compat_rep rd1 b1 n1 insta !pot_rep st_t with
           (* If we can't find a candidate, clean and add the current store as a potential future one *)
           | None ->
-              pot_strw_rep := [];
-              pot_strx_rep := [];
-              pot_rep := i :: !pot_rep
+              reset_str_symb_mem ();
+              pot_rep := [ i ]
           (* Else, perform the peephole *)
           | Some (rep, c, r, b, n) ->
               (* The two lines below are used to filter the elected candidate *)
               let filt x = x != rep in
               pot_rep := List.filter filt !pot_rep;
               insta.(rep) <- Pnop;
-              if debug then eprintf "STP_FORW_SPACED_PEEP_IMM_INC\n";
+              if debug then
+                eprintf "STP_FORW_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
               insta.(i) <-
                 PStore
-                  (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))
-        )
+                  (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n))));
+          Hashtbl.replace symb_mem st_t pot_rep)
     (* Any other inst *)
     | i, _ -> (
         (* Clear list of candidates if there is a non supported store *)
-        match i with
-        | PStore _ ->
-            pot_strw_rep := [];
-            pot_strx_rep := []
-        | _ -> ())
+        match i with PStore _ -> reset_str_symb_mem () | _ -> ())
   done
 
 (* Calling peephole if flag is set *)
diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index d7fab1de..cde3e7a7 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -137,8 +137,8 @@ let load_rec ldi =
   | PLd_rd_a (ld, rd, a) ->
       load_rd_a_rec (PBasic (PLoad ldi)) (reg_of_dreg rd) a
   | Pldp (ld, rd1, rd2, _, _, a) ->
-      load_rd1_rd2_a_rec (PBasic (PLoad ldi)) (reg_of_ireg rd1)
-        (reg_of_ireg rd2) a
+      load_rd1_rd2_a_rec (PBasic (PLoad ldi)) (reg_of_dreg rd1)
+        (reg_of_dreg rd2) a
 
 let store_rs_a_rec st rs a =
   {
@@ -161,8 +161,8 @@ let store_rec sti =
   | PSt_rs_a (st, rs, a) ->
       store_rs_a_rec (PBasic (PStore sti)) (reg_of_dreg rs) a
   | Pstp (st, rs1, rs2, _, _, a) ->
-      store_rs1_rs2_a_rec (PBasic (PStore sti)) (reg_of_ireg rs1)
-        (reg_of_ireg rs2) a
+      store_rs1_rs2_a_rec (PBasic (PStore sti)) (reg_of_dreg rs1)
+        (reg_of_dreg rs2) a
 
 let loadsymbol_rec i rd id =
   { inst = i; write_locs = [ rd ]; read_locs = [ Mem ]; is_control = false }
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 40e4a182..9ec1d563 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -417,6 +417,14 @@ module Target (*: TARGET*) =
         fprintf oc "	str	%a, %a\n" sreg rd addressing a
     | Pstrd(rd, a) | Pstrd_a(rd, a) ->
         fprintf oc "	str	%a, %a\n" dreg rd addressing a
+    | Pldps(rd1, rd2, _, _, a) ->
+        fprintf oc "	ldp	%a, %a, %a\n" sreg rd1 sreg rd2 addressing a
+    | Pldpd(rd1, rd2, _, _, a) ->
+        fprintf oc "	ldp	%a, %a, %a\n" dreg rd1 dreg rd2 addressing a
+    | Pstps(rd1, rd2, _, _, a) ->
+        fprintf oc "	stp	%a, %a, %a\n" sreg rd1 sreg rd2 addressing a
+    | Pstpd(rd1, rd2, _, _, a) ->
+        fprintf oc "	stp	%a, %a, %a\n" dreg rd1 dreg rd2 addressing a
     (* Floating-point move *)
     | Pfmov(rd, r1) ->
         fprintf oc "	fmov	%a, %a\n" dreg rd dreg r1
diff --git a/arm/Op.v b/arm/Op.v
index 6f22cece..ff5fe815 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -718,7 +718,7 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
-Definition condition_depends_on_memory (c: condition) : bool :=
+Definition cond_depends_on_memory (c: condition) : bool :=
   match c with
   | Ccompu _ | Ccompushift _ _| Ccompuimm _ _ => true
   | _ => false
@@ -726,14 +726,14 @@ Definition condition_depends_on_memory (c: condition) : bool :=
 
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp c => condition_depends_on_memory c
-  | Osel c ty => condition_depends_on_memory c
+  | Ocmp c => cond_depends_on_memory c
+  | Osel c ty => cond_depends_on_memory c
   | _ => false
   end.
 
-Lemma condition_depends_on_memory_correct:
+Lemma cond_depends_on_memory_correct:
   forall c args m1 m2,
-  condition_depends_on_memory c = false ->
+  cond_depends_on_memory c = false ->
   eval_condition c args m1 = eval_condition c args m2.
 Proof.
   intros. destruct c; simpl; auto; discriminate.
@@ -745,12 +745,22 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence; intros C.
-- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- f_equal; f_equal; apply cond_depends_on_memory_correct; auto.
 - destruct args; auto. destruct args; auto.
-  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  rewrite (cond_depends_on_memory_correct c args m1 m2 C).
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
diff --git a/backend/CSE3.v b/backend/CSE3.v
index 13d07e65..746ba399 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -53,6 +53,27 @@ Definition forward_move_l_b (rb : RB.t) (xl : list reg) :=
 Definition subst_args fmap pc xl :=
   forward_move_l_b (PMap.get pc fmap) xl.
 
+Definition find_cond_in_fmap fmap pc cond args :=
+  if Compopts.optim_CSE3_conditions tt
+  then
+    match PMap.get pc fmap with
+    | Some rel =>
+      if is_condition_present (ctx:=ctx) pc rel cond args
+      then Some true
+      else
+        let ncond := negate_condition cond in
+        if is_condition_present (ctx:=ctx) pc rel ncond args
+        then Some false
+        else let args' := subst_args fmap pc args in
+             if is_condition_present (ctx:=ctx) pc rel cond args'
+             then Some true
+             else if is_condition_present (ctx:=ctx) pc rel ncond args'
+                  then Some false
+                  else None
+    | None => None
+    end
+  else None.
+
 Definition transf_instr (fmap : PMap.t RB.t)
            (pc: node) (instr: instruction) :=
   match instr with
@@ -76,7 +97,11 @@ Definition transf_instr (fmap : PMap.t RB.t)
   | Itailcall sig ros args =>
     Itailcall sig ros (subst_args fmap pc args)
   | Icond cond args s1 s2 expected =>
-    Icond cond (subst_args fmap pc args) s1 s2 expected
+    let args' := subst_args fmap pc args in
+    match find_cond_in_fmap fmap pc cond args with
+    | None => Icond cond args' s1 s2 expected
+    | Some b => Inop (if b then s1 else s2)
+    end
   | Ijumptable arg tbl =>
     Ijumptable (subst_arg fmap pc arg) tbl
   | Ireturn (Some arg) =>
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 8b7f1190..75e00f67 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -145,18 +145,17 @@ Proof.
   exact peq.
 Defined.
 
-Record equation :=
-  mkequation
-    { eq_lhs : reg;
-      eq_op : sym_op;
-      eq_args : list reg }.
+Inductive equation_or_condition :=
+| Equ : reg -> sym_op -> list reg -> equation_or_condition
+| Cond : condition -> list reg -> equation_or_condition.
 
 Definition eq_dec_equation :
-  forall eq eq' : equation, {eq = eq'} + {eq <> eq'}.
+  forall eq eq' : equation_or_condition, {eq = eq'} + {eq <> eq'}.
 Proof.
   generalize peq.
   generalize eq_dec_sym_op.
   generalize eq_dec_args.
+  generalize eq_condition.
   decide equality.
 Defined.
 
@@ -168,34 +167,42 @@ Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
 Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) :=
   List.fold_left (fun already i => add_i_j i j already) ilist m.
 
-Definition get_reg_kills (eqs : PTree.t equation) :
+Definition get_reg_kills (eqs : PTree.t equation_or_condition) :
   Regmap.t PSet.t :=
-  PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
-                add_i_j (eq_lhs eq) eqno
-                        (add_ilist_j (eq_args eq) eqno already)) eqs
+  PTree.fold (fun already (eqno : eq_id) (eq_cond : equation_or_condition) =>
+                match eq_cond with
+                | Equ lhs sop args =>
+                  add_i_j lhs eqno
+                          (add_ilist_j args eqno already)
+                | Cond cond args => add_ilist_j args eqno already
+                end) eqs
              (PMap.init PSet.empty).
 
-Definition eq_depends_on_mem eq :=
-  match eq_op eq with
-  | SLoad _ _ => true
-  | SOp op => op_depends_on_memory op
+Definition eq_cond_depends_on_mem eq_cond :=
+  match eq_cond with
+  | Equ lhs sop args =>
+    match sop with
+    | SLoad _ _ => true
+    | SOp op => op_depends_on_memory op
+    end
+  | Cond cond args => cond_depends_on_memory cond
   end.
 
-Definition eq_depends_on_store eq :=
-  match eq_op eq with
-  | SLoad _ _ => true
-  | SOp op => false
+Definition eq_cond_depends_on_store eq_cond :=
+  match eq_cond with
+  | Equ _ (SLoad _ _) _ => true
+  | _ => false
   end.
 
-Definition get_mem_kills (eqs : PTree.t equation) : PSet.t :=
-  PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
-                if eq_depends_on_mem eq
+Definition get_mem_kills (eqs : PTree.t equation_or_condition) : PSet.t :=
+  PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) =>
+                if eq_cond_depends_on_mem eq
                 then PSet.add eqno already
                 else already) eqs PSet.empty.
 
-Definition get_store_kills (eqs : PTree.t equation) : PSet.t :=
-  PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
-                if eq_depends_on_store eq
+Definition get_store_kills (eqs : PTree.t equation_or_condition) : PSet.t :=
+  PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) =>
+                if eq_cond_depends_on_store eq
                 then PSet.add eqno already
                 else already) eqs PSet.empty.
 
@@ -215,21 +222,25 @@ Proof.
   - right; congruence.
 Qed.
 
-Definition get_moves (eqs : PTree.t equation) :
+Definition get_moves (eqs : PTree.t equation_or_condition) :
   Regmap.t PSet.t :=
-  PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
-                if is_smove (eq_op eq)
-                then add_i_j (eq_lhs eq) eqno already
-                else already) eqs (PMap.init PSet.empty).
+  PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) =>
+                match eq with
+                | Equ lhs sop args =>
+                  if is_smove sop
+                  then add_i_j lhs eqno already
+                  else already
+                | _ => already
+                end) eqs (PMap.init PSet.empty).
   
 Record eq_context := mkeqcontext
-                       { eq_catalog : eq_id -> option equation;
-                         eq_find_oracle : node -> equation -> option eq_id;
-                         eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t;
-                         eq_kill_reg : reg -> PSet.t;
-                         eq_kill_mem : unit -> PSet.t;
-                         eq_kill_store : unit -> PSet.t;
-                         eq_moves : reg -> PSet.t }.
+              { eq_catalog : eq_id -> option equation_or_condition;
+                eq_find_oracle : node -> equation_or_condition -> option eq_id;
+                eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t;
+                eq_kill_reg : reg -> PSet.t;
+                eq_kill_mem : unit -> PSet.t;
+                eq_kill_store : unit -> PSet.t;
+                eq_moves : reg -> PSet.t }.
 
 Section OPERATIONS.
   Context {ctx : eq_context}.
@@ -251,10 +262,10 @@ Section OPERATIONS.
     | None => x
     | Some eqno =>
       match eq_catalog ctx eqno with
-      | Some eq =>
-        if is_smove (eq_op eq) && peq x (eq_lhs eq)
+      | Some (Equ lhs sop args) =>
+        if is_smove sop && peq x lhs
         then
-          match eq_args eq with
+          match args with
           | src::nil => src
           | _ => x
           end
@@ -269,7 +280,7 @@ Section OPERATIONS.
   Section PER_NODE.
     Variable no : node.
     
-  Definition eq_find  (eq : equation) :=
+  Definition eq_find  (eq : equation_or_condition) :=
     match eq_find_oracle ctx no eq with
     | Some id =>
       match eq_catalog ctx id with
@@ -279,25 +290,29 @@ Section OPERATIONS.
     | None => None
     end.
 
+  Definition is_condition_present
+           (rel : RELATION.t) (cond : condition) (args : list reg) :=
+    match eq_find (Cond cond args) with
+    | Some id => PSet.contains rel id
+    | None => false
+    end.
 
   Definition rhs_find (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg :=
     match pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel)) with
     | None => None
     | Some src =>
       match eq_catalog ctx src with
-      | None => None
-      | Some eq =>
-        if eq_dec_sym_op sop (eq_op eq) && eq_dec_args args (eq_args eq)
-        then Some (eq_lhs eq)
+      | Some (Equ eq_lhs eq_sop eq_args) =>
+        if eq_dec_sym_op sop eq_sop && eq_dec_args args eq_args
+        then Some eq_lhs
         else None
+      | _ => None
       end
     end.
 
   Definition oper2 (dst : reg) (op: sym_op)(args : list reg)
            (rel : RELATION.t) : RELATION.t :=
-    match eq_find {| eq_lhs := dst;
-                     eq_op  := op;
-                     eq_args:= args |} with
+    match eq_find (Equ dst op args) with
     | Some id =>
       if PSet.contains rel id
       then rel
@@ -316,9 +331,7 @@ Section OPERATIONS.
     if peq src dst
     then rel
     else
-      match eq_find {| eq_lhs := dst;
-                     eq_op  := SOp Omove;
-                     eq_args:= src::nil |} with
+      match eq_find (Equ dst (SOp Omove) (src::nil)) with
       | Some eq_id => PSet.add eq_id (kill_reg dst rel)
       | None => kill_reg dst rel
       end.
@@ -366,13 +379,13 @@ Section OPERATIONS.
       (PSet.filter
          (fun eqno =>
             match eq_catalog ctx eqno with
-            | None => false
-            | Some eq =>
-              match eq_op eq with
+            | Some (Equ eq_lhs eq_sop eq_args) =>
+              match eq_sop with
               | SOp op => true
               | SLoad chunk' addr' =>
-                may_overlap chunk addr args chunk' addr' (eq_args eq)
+                may_overlap chunk addr args chunk' addr' eq_args
               end
+            | _ => false
             end)
          (PSet.inter rel (eq_kill_store ctx tt))).
 
@@ -391,9 +404,7 @@ Section OPERATIONS.
     let rel' := store2 chunk addr args src rel in
     if loadv_storev_compatible_type chunk ty
     then
-      match eq_find {| eq_lhs := src;
-                       eq_op  := SLoad chunk addr;
-                       eq_args:= args |} with
+      match eq_find (Equ src (SLoad chunk addr) args) with
       | Some id => PSet.add id rel'
       | None => rel'
       end
@@ -450,28 +461,55 @@ Section OPERATIONS.
     | _ => rel
     end.
 
-  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t :=
+  Definition apply_cond1 cond args (rel : RELATION.t) : RB.t :=
+    match eq_find (Cond (negate_condition cond) args) with
+    | Some eq_id =>
+      if PSet.contains rel eq_id
+      then RB.bot
+      else Some rel
+    | None => Some rel
+    end.
+
+  Definition apply_cond0 cond args (rel : RELATION.t) : RELATION.t :=
+    match eq_find (Cond cond args) with
+    | Some eq_id => PSet.add eq_id rel
+    | None => rel
+    end.
+
+  Definition apply_cond cond args (rel : RELATION.t) : RB.t :=
+    if Compopts.optim_CSE3_conditions tt
+    then 
+      match apply_cond1 cond args rel with
+      | Some rel => Some (apply_cond0 cond args rel)
+      | None => RB.bot
+      end
+    else Some rel.
+      
+  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
-  | Inop _
-  | Icond _ _ _ _ _
-  | Ijumptable _ _ => Some rel
-  | Istore chunk addr args src _ =>
-    Some (store tenv chunk addr args src rel)
-  | Iop op args dst _ => Some (oper dst (SOp op) args rel)
-  | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
-  | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
-  | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel))
-  | Itailcall _ _ _ | Ireturn _ => RB.bot
+  | Inop pc' => (pc', (Some rel))::nil
+  | Icond cond args ifso ifnot _ =>
+    (ifso,  (apply_cond cond args rel))::
+    (ifnot, (apply_cond (negate_condition cond) args rel))::nil
+  | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets
+  | Istore chunk addr args src pc' =>
+    (pc', (Some (store tenv chunk addr args src rel)))::nil
+  | Iop op args dst pc' => (pc', (Some (oper dst (SOp op) args rel)))::nil
+  | Iload trap chunk addr args dst pc' => (pc', (Some (oper dst (SLoad chunk addr) args rel)))::nil
+  | Icall _ _ _ dst pc' => (pc', (Some (kill_reg dst (kill_mem rel))))::nil
+  | Ibuiltin ef _ res pc' => (pc', (Some (kill_builtin_res res (apply_external_call ef rel))))::nil
+  | Itailcall _ _ _ | Ireturn _ => nil
   end.
   End PER_NODE.
 
-Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t :=
-  match ro with
-  | None => None
-  | Some x =>
-    match code ! pc with
-    | None => RB.bot
-    | Some instr => apply_instr pc tenv instr x
+Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) :
+  list (node * RB.t)  :=
+  match code ! pc with
+  | None => nil
+  | Some instr => 
+    match ro with
+    | None => List.map (fun pc' => (pc', RB.bot)) (successors_instr instr)
+    | Some x => apply_instr pc tenv instr x
     end
   end.
 
@@ -493,24 +531,25 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva
          match PMap.get pc inv with
          | None => true
          | Some rel =>
-           let rel' := apply_instr pc tenv instr rel in
            List.forallb
-             (fun pc' => relb_leb rel' (PMap.get pc' inv))
-             (RTL.successors_instr instr)
+             (fun szz =>
+                relb_leb (snd szz) (PMap.get (fst szz) inv))
+             (apply_instr pc tenv instr rel)
          end).
+(* No longer used. Incompatible with transfer functions that yield a different result depending on the successor.
 
 Definition internal_analysis
   (tenv : typing_env)
   (f : RTL.function) : option invariants := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
   (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
-
+*)
 End OPERATIONS.
 
 Record analysis_hints :=
   mkanalysis_hints
-    { hint_eq_catalog :  PTree.t equation;
-      hint_eq_find_oracle : node -> equation -> option eq_id;
+    { hint_eq_catalog :  PTree.t equation_or_condition;
+      hint_eq_find_oracle : node -> equation_or_condition -> option eq_id;
       hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }.
 
 Definition context_from_hints (hints : analysis_hints) :=
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index e038331c..efe6b600 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -16,8 +16,15 @@ open HashedSet
 open Camlcoq
 open Coqlib
    
-let flatten_eq eq =
-  ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);;
+type flattened_equation_or_condition =
+  | Flat_equ of int * sym_op * int list
+  | Flat_cond of Op.condition * int list;;
+
+let flatten_eq = function
+  | Equ(lhs, sop, args) ->
+     Flat_equ((P.to_int lhs), sop, (List.map P.to_int args))
+  | Cond(cond, args) ->
+     Flat_cond(cond, (List.map P.to_int args));;
 
 let imp_add_i_j s i j =
   s := PMap.set i (PSet.add j (PMap.get i !s)) !s;;
@@ -45,6 +52,9 @@ let print_eq channel (lhs, sop, args) =
      Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk)
        (PrintOp.print_addressing print_reg) (addr, args);;
 
+let print_cond channel (cond, args) =
+  Printf.printf "cond %a" (PrintOp.print_condition print_reg) (cond, args);;
+
 let pp_intset oc s =
   Printf.fprintf oc "{ ";
   List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s);
@@ -58,9 +68,14 @@ let pp_rhs oc (sop, args) =
        (PrintAST.name_of_chunk chunk)
          (PrintOp.print_addressing PrintRTL.reg) (addr, args);;
 
-let pp_eq oc eq =
-  Printf.fprintf oc "x%d = %a" (P.to_int eq.eq_lhs)
-    pp_rhs (eq.eq_op, eq.eq_args);;
+let pp_eq oc eq_cond =
+  match eq_cond with
+  | Equ(lhs, sop, args) ->
+     Printf.fprintf oc "x%d = %a" (P.to_int lhs)
+       pp_rhs (sop, args)
+  | Cond(cond, args) ->
+     Printf.fprintf oc "cond %a"
+       (PrintOp.print_condition PrintRTL.reg) (cond, args);;
 
 let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x)
               
@@ -68,8 +83,9 @@ let pp_option pp oc = function
   | None -> output_string oc "none"
   | Some x -> pp oc x;;
 
-let is_trivial eq =
-  (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);;
+let is_trivial = function
+  | Equ(lhs, (SOp Op.Omove), [lhs']) -> lhs=lhs'
+  | _ -> false;;
 
 let rec pp_list separator pp_item chan = function
   | [] -> ()
@@ -86,7 +102,11 @@ let pp_equation hints chan x =
   match PTree.get x hints.hint_eq_catalog with
   | None -> output_string chan "???"
   | Some eq ->
-     print_eq chan  (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);;
+     match eq with
+     | Equ(lhs, sop, args) ->
+        print_eq chan  (P.to_int lhs, sop, List.map P.to_int args)
+     | Cond(cond, args) ->
+        print_cond chan (cond, List.map P.to_int args);;
 
 let pp_relation hints chan rel =
   pp_set "; " (pp_equation hints) chan rel;;
@@ -114,19 +134,47 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t =
   | None, _ | _, None -> None
   | (Some x'), (Some y') -> Some (RELATION.glb x' y');;
 
+let compute_invariants
+      (nodes : RTL.node list)
+      (entrypoint : RTL.node)
+      (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list) =
+  let todo = ref IntSet.empty
+  and invariants = ref (PMap.set entrypoint (Some RELATION.top) (PMap.init RB.bot)) in  
+  let add_todo (pc : RTL.node) =
+    todo := IntSet.add (P.to_int pc) !todo in 
+  let update_node (pc : RTL.node) =
+    (if !Clflags.option_debug_compcert > 9
+     then Printf.printf "UP updating node %d\n" (P.to_int pc));
+    let cur = PMap.get pc !invariants in
+    List.iter (fun (next_pc, next_contrib) ->
+        let previous = PMap.get next_pc !invariants in
+        let next = RB.lub previous next_contrib in
+        if not (RB.beq previous next)
+        then (
+          invariants := PMap.set next_pc next !invariants;
+          add_todo next_pc)) (tfr pc cur) in
+  add_todo entrypoint;
+  while not (IntSet.is_empty !todo) do
+    let nxt = IntSet.max_elt !todo in
+    todo := IntSet.remove nxt !todo;
+    update_node (P.of_int nxt)
+  done;
+  !invariants;;
+
 let refine_invariants
       (nodes : RTL.node list)
       (entrypoint : RTL.node)
       (successors : RTL.node -> RTL.node list)
       (predecessors : RTL.node -> RTL.node list)
-      (tfr : RTL.node -> RB.t -> RB.t) (invariants0 : RB.t PMap.t) =
+      (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list)
+      (invariants0 : RB.t PMap.t) =
   let todo = ref IntSet.empty
   and invariants = ref invariants0 in  
   let add_todo (pc : RTL.node) =
     todo := IntSet.add (P.to_int pc) !todo in 
   let update_node (pc : RTL.node) =
     (if !Clflags.option_debug_compcert > 9
-     then Printf.printf "updating node %d\n" (P.to_int pc));
+     then Printf.printf "DOWN updating node %d\n" (P.to_int pc));
     if not (peq pc entrypoint)
     then
       let cur = PMap.get pc !invariants in
@@ -134,7 +182,7 @@ let refine_invariants
                   (List.map
                      (fun pred_pc->
                        rb_glb cur
-                         (tfr pred_pc (PMap.get pred_pc !invariants)))
+                         (List.assoc pc (tfr pred_pc (PMap.get pred_pc !invariants))))
                      (predecessors pc)) in
       if not (RB.beq cur nxt)
       then
@@ -156,6 +204,12 @@ let get_default default x ptree =
   | None -> default
   | Some y -> y;;
 
+let initial_analysis ctx tenv (f : RTL.coq_function) =
+  let tfr = apply_instr' ctx tenv f.RTL.fn_code in
+  compute_invariants
+    (List.map fst (PTree.elements f.RTL.fn_code))
+    f.RTL.fn_entrypoint tfr;;
+
 let refine_analysis ctx tenv
       (f : RTL.coq_function) (invariants0 : RB.t PMap.t) =
   let succ_map = RTL.successors_map f in
@@ -166,6 +220,13 @@ let refine_analysis ctx tenv
   refine_invariants
     (List.map fst (PTree.elements f.RTL.fn_code))
     f.RTL.fn_entrypoint succ_f pred_f tfr invariants0;;
+
+let add_to_set_in_table table key item =
+  Hashtbl.add table key
+    (PSet.add item
+       (match Hashtbl.find_opt table key with
+        | None -> PSet.empty
+        | Some s -> s));;
   
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
@@ -179,7 +240,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let eq_find_oracle node eq =
     assert (not (is_trivial eq));
     let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
-    (if o = None then failwith "eq_find_oracle");
+    (* FIXME (if o = None then failwith "eq_find_oracle"); *)
     (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node)
             pp_eq eq (pp_option pp_P) o);
@@ -194,7 +255,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
             (P.to_int node) pp_rhs (sop, args) pp_intset o);
     o in
   let mutating_eq_find_oracle node eq : P.t option =
-    let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
+    let flat_eq = flatten_eq eq in
     let o =
     match Hashtbl.find_opt eq_table flat_eq with
     | Some x ->
@@ -207,21 +268,27 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
        begin
          Hashtbl.add eq_table flat_eq coq_id;
          (cur_catalog := PTree.set coq_id eq !cur_catalog);
-         Hashtbl.add rhs_table (flat_eq_op, flat_eq_args)
-           (PSet.add coq_id
-              (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with
-               | None -> PSet.empty
-               | Some s -> s));
-         List.iter
-           (fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
-           (eq.eq_lhs :: eq.eq_args);
-         (if eq_depends_on_mem eq
+         (match flat_eq with
+          | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) ->
+             add_to_set_in_table rhs_table
+               (flat_eq_op, flat_eq_args) coq_id
+          | Flat_cond(flat_eq_cond, flat_eq_args) -> ());
+         (match eq with
+          | Equ(lhs, sop, args) ->
+             List.iter
+               (fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
+               (lhs :: args);
+             (match sop, args with
+              | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id
+              | _, _ -> ())
+          | Cond(cond, args) ->
+             List.iter
+               (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args
+         );
+         (if eq_cond_depends_on_mem eq
           then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
-         (if eq_depends_on_store eq
+         (if eq_cond_depends_on_store eq
           then cur_kill_store := PSet.add coq_id !cur_kill_store);
-         (match eq.eq_op, eq.eq_args with
-          | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id
-          | _, _ -> ());
          Some coq_id
        end
     in
@@ -238,17 +305,15 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
               eq_kill_store  = (fun () -> !cur_kill_store);
               eq_moves       = (fun reg -> PMap.get reg !cur_moves)
             } in
-  match internal_analysis ctx tenv f
-  with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3"
-     | Some invariants ->
-        let invariants' =
-          if ! Clflags.option_fcse3_refine
-          then refine_analysis ctx tenv f invariants
-          else invariants
-        and hints = { hint_eq_catalog    = !cur_catalog;
-                      hint_eq_find_oracle= eq_find_oracle;
-                      hint_eq_rhs_oracle = rhs_find_oracle } in
-        (if !Clflags.option_debug_compcert > 1
-         then pp_results f invariants' hints stdout);
-        invariants', hints
+  let invariants = initial_analysis ctx tenv f in
+  let invariants' =
+    if ! Clflags.option_fcse3_refine
+    then refine_analysis ctx tenv f invariants
+    else invariants
+  and hints = { hint_eq_catalog    = !cur_catalog;
+                hint_eq_find_oracle= eq_find_oracle;
+                hint_eq_rhs_oracle = rhs_find_oracle } in
+  (if !Clflags.option_debug_compcert > 1
+   then pp_results f invariants' hints stdout);
+  invariants', hints
 ;;
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index b298ea65..d53cf604 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -127,22 +127,35 @@ Proof.
 Qed.
 Hint Resolve add_ilist_j_adds: cse3.
 
-Definition xlget_kills (eqs : list (eq_id * equation)) (m :  Regmap.t PSet.t) :
+Definition xlget_kills (eqs : list (eq_id * equation_or_condition))
+                       (m :  Regmap.t PSet.t) :
   Regmap.t PSet.t :=
-  List.fold_left (fun already (item : eq_id * equation) =>
-    add_i_j (eq_lhs (snd item)) (fst item)
-            (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m.
-
-Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t :=
+  List.fold_left (fun already (item : eq_id * equation_or_condition) =>
+    match snd item with
+    | Equ lhs sop args =>
+      add_i_j lhs (fst item)
+              (add_ilist_j args (fst item) already)
+    | Cond cond args => add_ilist_j args (fst item) already
+    end) eqs m.
+
+Definition xlget_mem_kills (eqs : list (positive * equation_or_condition))
+           (m : PSet.t) : PSet.t :=
 (fold_left
-       (fun (a : PSet.t) (p : positive * equation) =>
-        if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a)
+       (fun (a : PSet.t) (item : positive * equation_or_condition) =>
+          if eq_cond_depends_on_mem (snd item)
+          then PSet.add (fst item) a
+          else a
+       )
        eqs m).
 
-Definition xlget_store_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t :=
+Definition xlget_store_kills (eqs : list (positive * equation_or_condition))
+           (m : PSet.t) : PSet.t :=
 (fold_left
-       (fun (a : PSet.t) (p : positive * equation) =>
-        if eq_depends_on_store (snd p) then PSet.add (fst p) a else a)
+       (fun (a : PSet.t) (item : positive * equation_or_condition) =>
+          if eq_cond_depends_on_store (snd item)
+          then PSet.add (fst item) a
+          else a
+       )
        eqs m).
 
 Lemma xlget_kills_monotone :
@@ -152,7 +165,8 @@ Lemma xlget_kills_monotone :
 Proof.
   induction eqs; simpl; trivial.
   intros.
-  auto with cse3.
+  destruct a as [id eq_cond]; cbn.
+  destruct eq_cond as [eq_lhs eq_sop eq_args | eq_cond eq_args]; auto with cse3.
 Qed.
 
 Hint Resolve xlget_kills_monotone : cse3.
@@ -164,9 +178,10 @@ Lemma xlget_mem_kills_monotone :
 Proof.
   induction eqs; simpl; trivial.
   intros.
-  destruct eq_depends_on_mem.
+  destruct a as [id eq_cond]; cbn.
+  destruct eq_cond_depends_on_mem.
   - apply IHeqs.
-    destruct (peq (fst a) j).
+    destruct (peq id j).
     + subst j. apply PSet.gadds.
     + rewrite PSet.gaddo by congruence.
       trivial.
@@ -182,9 +197,10 @@ Lemma xlget_store_kills_monotone :
 Proof.
   induction eqs; simpl; trivial.
   intros.
-  destruct eq_depends_on_store.
+  destruct a as [id eq_cond]; cbn.
+  destruct eq_cond_depends_on_store.
   - apply IHeqs.
-    destruct (peq (fst a) j).
+    destruct (peq id j).
     + subst j. apply PSet.gadds.
     + rewrite PSet.gaddo by congruence.
       trivial.
@@ -195,9 +211,7 @@ Hint Resolve xlget_store_kills_monotone : cse3.
 
 Lemma xlget_kills_has_lhs :
   forall eqs m lhs sop args j,
-    In (j, {| eq_lhs := lhs;
-              eq_op  := sop;
-              eq_args:= args |}) eqs ->
+    In (j, (Equ lhs sop args))  eqs ->
     PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true.
 Proof.
   induction eqs; simpl.
@@ -212,9 +226,7 @@ Hint Resolve xlget_kills_has_lhs : cse3.
 
 Lemma xlget_kills_has_arg :
   forall eqs m lhs sop arg args j,
-    In (j, {| eq_lhs := lhs;
-              eq_op  := sop;
-              eq_args:= args |}) eqs ->
+    In (j, (Equ lhs sop args)) eqs ->
     In arg args ->
     PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true.
 Proof.
@@ -229,20 +241,38 @@ Qed.
 
 Hint Resolve xlget_kills_has_arg : cse3.
 
+Lemma xlget_cond_kills_has_arg :
+  forall eqs m cond arg args j,
+    In (j, (Cond cond args)) eqs ->
+    In arg args ->
+    PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true.
+Proof.
+  induction eqs; simpl.
+  contradiction.
+  intros until j.
+  intros HEAD_TAIL ARG.
+  destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl.
+  - auto with cse3.
+  - eapply IHeqs; eassumption.
+Qed.
+
+Hint Resolve xlget_cond_kills_has_arg : cse3.
+
 Lemma get_kills_has_lhs :
   forall eqs lhs sop args j,
-    PTree.get j eqs = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
+    PTree.get j eqs = Some (Equ lhs sop args) ->
     PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true.
 Proof.
   unfold get_reg_kills.
   intros.
   rewrite PTree.fold_spec.
   change (fold_left
-       (fun (a : Regmap.t PSet.t) (p : positive * equation) =>
-        add_i_j (eq_lhs (snd p)) (fst p)
-          (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills.
+       (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) =>
+        match snd p with
+        | Equ lhs0 _ args0 =>
+          add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a)
+        | Cond _ args0 => add_ilist_j args0 (fst p) a
+        end))  with xlget_kills.
   eapply xlget_kills_has_lhs.
   apply PTree.elements_correct.
   eassumption.
@@ -252,9 +282,7 @@ Hint Resolve get_kills_has_lhs : cse3.
 
 Lemma context_from_hints_get_kills_has_lhs :
   forall hints lhs sop args j,
-    PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
+    PTree.get j (hint_eq_catalog hints) = Some (Equ lhs sop args) ->
     PSet.contains  (eq_kill_reg (context_from_hints hints) lhs) j = true.
 Proof.
   intros; simpl.
@@ -266,9 +294,7 @@ Hint Resolve context_from_hints_get_kills_has_lhs : cse3.
 
 Lemma get_kills_has_arg :
   forall eqs lhs sop arg args j,
-    PTree.get j eqs = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
+    PTree.get j eqs = Some (Equ lhs sop args) ->
     In arg args ->
     PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true.
 Proof.
@@ -276,9 +302,12 @@ Proof.
   intros.
   rewrite PTree.fold_spec.
   change (fold_left
-       (fun (a : Regmap.t PSet.t) (p : positive * equation) =>
-        add_i_j (eq_lhs (snd p)) (fst p)
-          (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills.
+       (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) =>
+        match snd p with
+        | Equ lhs0 _ args0 =>
+          add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a)
+        | Cond _ args0 => add_ilist_j args0 (fst p) a
+        end)) with xlget_kills.
   eapply xlget_kills_has_arg.
   - apply PTree.elements_correct.
     eassumption.
@@ -289,9 +318,7 @@ Hint Resolve get_kills_has_arg : cse3.
 
 Lemma context_from_hints_get_kills_has_arg :
   forall hints lhs sop arg args j,
-    PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
+    PTree.get j (hint_eq_catalog hints) = Some (Equ lhs sop args) ->
     In arg args ->
     PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true.
 Proof.
@@ -302,10 +329,47 @@ Qed.
 
 Hint Resolve context_from_hints_get_kills_has_arg : cse3.
 
+Lemma get_cond_kills_has_arg :
+  forall eqs cond arg args j,
+    PTree.get j eqs = Some (Cond cond args) ->
+    In arg args ->
+    PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true.
+Proof.
+  unfold get_reg_kills.
+  intros.
+  rewrite PTree.fold_spec.
+  change (fold_left
+       (fun (a : Regmap.t PSet.t) (p : positive * equation_or_condition) =>
+        match snd p with
+        | Equ lhs0 _ args0 =>
+          add_i_j lhs0 (fst p) (add_ilist_j args0 (fst p) a)
+        | Cond _ args0 => add_ilist_j args0 (fst p) a
+        end)) with xlget_kills.
+  eapply xlget_cond_kills_has_arg.
+  - apply PTree.elements_correct.
+    eassumption.
+  - assumption.
+Qed.
+
+Hint Resolve get_cond_kills_has_arg : cse3.
+
+Lemma context_from_hints_get_cond_kills_has_arg :
+  forall hints cond arg args j,
+    PTree.get j (hint_eq_catalog hints) = Some (Cond cond args) ->
+    In arg args ->
+    PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true.
+Proof.
+  intros.
+  simpl.
+  eapply get_cond_kills_has_arg; eassumption.
+Qed.
+
+Hint Resolve context_from_hints_get_cond_kills_has_arg : cse3.
+
 Lemma xlget_kills_has_eq_depends_on_mem :
   forall eqs eq j m,
     In (j, eq) eqs ->
-    eq_depends_on_mem eq = true ->
+    eq_cond_depends_on_mem eq = true ->
     PSet.contains (xlget_mem_kills eqs m) j = true.
 Proof.
   induction eqs; simpl.
@@ -326,17 +390,16 @@ Hint Resolve xlget_kills_has_eq_depends_on_mem : cse3.
 Lemma get_kills_has_eq_depends_on_mem :
   forall eqs eq j,
     PTree.get j eqs = Some eq ->
-    eq_depends_on_mem eq = true ->
+    eq_cond_depends_on_mem eq = true ->
     PSet.contains (get_mem_kills eqs) j = true.
 Proof.
   intros.
   unfold get_mem_kills.
   rewrite PTree.fold_spec.
   change (fold_left
-       (fun (a : PSet.t) (p : positive * equation) =>
-        if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a)
-       (PTree.elements eqs) PSet.empty)
-    with (xlget_mem_kills (PTree.elements eqs) PSet.empty).
+       (fun (a : PSet.t) (p : positive * equation_or_condition) =>
+          if eq_cond_depends_on_mem (snd p) then PSet.add (fst p) a else a))
+       with xlget_mem_kills.
   eapply xlget_kills_has_eq_depends_on_mem.
   apply PTree.elements_correct.
   eassumption.
@@ -346,7 +409,7 @@ Qed.
 Lemma context_from_hints_get_kills_has_eq_depends_on_mem :
   forall hints eq j,
     PTree.get j (hint_eq_catalog hints) = Some eq ->
-    eq_depends_on_mem eq = true ->
+    eq_cond_depends_on_mem eq = true ->
     PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true.
 Proof.
   intros.
@@ -359,7 +422,7 @@ Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3.
 Lemma xlget_kills_has_eq_depends_on_store :
   forall eqs eq j m,
     In (j, eq) eqs ->
-    eq_depends_on_store eq = true ->
+    eq_cond_depends_on_store eq = true ->
     PSet.contains (xlget_store_kills eqs m) j = true.
 Proof.
   induction eqs; simpl.
@@ -380,17 +443,16 @@ Hint Resolve xlget_kills_has_eq_depends_on_store : cse3.
 Lemma get_kills_has_eq_depends_on_store :
   forall eqs eq j,
     PTree.get j eqs = Some eq ->
-    eq_depends_on_store eq = true ->
+    eq_cond_depends_on_store eq = true ->
     PSet.contains (get_store_kills eqs) j = true.
 Proof.
   intros.
   unfold get_store_kills.
   rewrite PTree.fold_spec.
   change (fold_left
-       (fun (a : PSet.t) (p : positive * equation) =>
-        if eq_depends_on_store (snd p) then PSet.add (fst p) a else a)
-       (PTree.elements eqs) PSet.empty)
-    with (xlget_store_kills (PTree.elements eqs) PSet.empty).
+       (fun (a : PSet.t) (p : positive * equation_or_condition) =>
+          if eq_cond_depends_on_store (snd p) then PSet.add (fst p) a else a))
+       with xlget_store_kills.
   eapply xlget_kills_has_eq_depends_on_store.
   apply PTree.elements_correct.
   eassumption.
@@ -400,7 +462,7 @@ Qed.
 Lemma context_from_hints_get_kills_has_eq_depends_on_store :
   forall hints eq j,
     PTree.get j (hint_eq_catalog hints) = Some eq ->
-    eq_depends_on_store eq = true ->
+    eq_cond_depends_on_store eq = true ->
     PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true.
 Proof.
   intros.
@@ -410,8 +472,12 @@ Qed.
 
 Hint Resolve context_from_hints_get_kills_has_eq_depends_on_store : cse3.
 
-Definition eq_involves (eq : equation) (i : reg) :=
-  i = (eq_lhs eq) \/ In i (eq_args eq).
+Definition eq_involves (eq : equation_or_condition) (i : reg) :=
+  match eq with
+  | Equ lhs sop args =>
+    i = lhs \/ In i args
+  | Cond cond args =>  In i args
+  end.
 
 Section SOUNDNESS.
   Context {F V : Type}.
@@ -440,8 +506,11 @@ Section SOUNDNESS.
       end
     end.
     
-  Definition sem_eq (eq : equation) (rs : regset) (m : mem) :=
-    sem_rhs (eq_op eq) (eq_args eq) rs m (rs # (eq_lhs eq)).
+  Definition sem_eq (eq : equation_or_condition) (rs : regset) (m : mem) :=
+    match eq with
+    | Equ lhs sop args => sem_rhs sop args rs m (rs # lhs)
+    | Cond cond args => eval_condition cond (rs ## args) m = Some true
+    end.
 
   Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) :=
     forall i eq,
@@ -475,16 +544,19 @@ Section SOUNDNESS.
 
   Hypothesis ctx_kill_reg_has_lhs :
     forall lhs sop args j,
-      eq_catalog ctx j = Some {| eq_lhs := lhs;
-                                 eq_op  := sop;
-                                 eq_args:= args |} ->
+      eq_catalog ctx j = Some (Equ lhs sop args) ->
       PSet.contains (eq_kill_reg ctx lhs) j = true.
 
   Hypothesis ctx_kill_reg_has_arg :
     forall lhs sop args j,
-      eq_catalog ctx j = Some {| eq_lhs := lhs;
-                                 eq_op  := sop;
-                                 eq_args:= args |} ->
+      eq_catalog ctx j = Some (Equ lhs sop args) ->
+      forall arg,
+      In arg args ->
+      PSet.contains (eq_kill_reg ctx arg) j = true.
+
+  Hypothesis ctx_cond_kill_reg_has_arg :
+    forall cond args j,
+      eq_catalog ctx j = Some (Cond cond args) ->
       forall arg,
       In arg args ->
       PSet.contains (eq_kill_reg ctx arg) j = true.
@@ -492,13 +564,13 @@ Section SOUNDNESS.
   Hypothesis ctx_kill_mem_has_depends_on_mem :
     forall eq j,
       eq_catalog ctx j = Some eq ->
-      eq_depends_on_mem eq = true ->
+      eq_cond_depends_on_mem eq = true ->
       PSet.contains (eq_kill_mem ctx tt) j = true.
 
   Hypothesis ctx_kill_store_has_depends_on_store :
     forall eq j,
       eq_catalog ctx j = Some eq ->
-      eq_depends_on_store eq = true ->
+      eq_cond_depends_on_store eq = true ->
       PSet.contains (eq_kill_store ctx tt) j = true.
 
   Theorem kill_reg_sound :
@@ -510,8 +582,8 @@ Section SOUNDNESS.
     intros until v.
     intros REL i eq.
     specialize REL with (i := i) (eq0 := eq).
-    destruct eq as [lhs sop args]; simpl.
-    specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i).
+    destruct eq as [lhs sop args | cond args]; simpl.
+  * specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i).
     specialize ctx_kill_reg_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst).
     intuition.
     rewrite PSet.gsubtract in H.
@@ -539,6 +611,24 @@ Section SOUNDNESS.
       assumption.
     - rewrite Regmap.gso by congruence.
       assumption.
+  * specialize ctx_cond_kill_reg_has_arg with (cond := cond) (args := args) (j := i) (arg := dst).
+    intuition.
+    rewrite PSet.gsubtract in H.
+    rewrite andb_true_iff in H.
+    rewrite negb_true_iff in H.
+    intuition.
+    simpl in *.
+    assert ({In dst args} + {~In dst args}) as IN_ARGS.
+    {
+      apply List.in_dec.
+      apply peq.
+    }
+    destruct IN_ARGS as [IN_ARGS | NOTIN_ARGS].
+    { intuition.
+      congruence.
+    }
+    rewrite subst_args_notin by assumption.
+    assumption.
   Qed.
 
   Hint Resolve kill_reg_sound : cse3.
@@ -552,14 +642,20 @@ Section SOUNDNESS.
     intros until dst.
     intros REL i eq.
     specialize REL with (i := i) (eq0 := eq).
-    destruct eq as [lhs sop args]; simpl.
-    specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i).
+    destruct eq as [lhs sop args | cond args]; simpl.
+  * specialize ctx_kill_reg_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i).
     specialize ctx_kill_reg_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst).
     intuition.
     rewrite PSet.gsubtract in H.
     rewrite andb_true_iff in H.
     rewrite negb_true_iff in H.
     intuition.
+  * specialize ctx_cond_kill_reg_has_arg with (cond := cond) (args := args) (j := i) (arg := dst).
+    intuition.
+    rewrite PSet.gsubtract in H.
+    rewrite andb_true_iff in H.
+    rewrite negb_true_iff in H.
+    intuition.
   Qed.
     
   Lemma pick_source_sound :
@@ -590,9 +686,11 @@ Section SOUNDNESS.
     destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG.
     2: reflexivity.
     specialize REL with (i := r) (eq0 := eq).
-    destruct (is_smove (eq_op eq)) as [MOVE | ].
+    destruct eq as [lhs sop args | cond args]; cbn in *; trivial.
+    destruct (is_smove sop) as [MOVE | ].
     2: reflexivity.
-    destruct (peq x (eq_lhs eq)).
+    rewrite MOVE in *; cbn in *.
+    destruct (peq x lhs).
     2: reflexivity.
     simpl.
     subst x.
@@ -600,9 +698,8 @@ Section SOUNDNESS.
     rewrite PSet.ginter in ELEMENT.
     rewrite andb_true_iff in ELEMENT.
     unfold sem_eq in REL.
-    rewrite MOVE in REL.
     simpl in REL.
-    destruct (eq_args eq) as [ | h t].
+    destruct args as [ | h t].
     reflexivity.
     destruct t.
     2: reflexivity.
@@ -637,22 +734,30 @@ Section SOUNDNESS.
     rewrite PSet.gsubtract in SUBTRACT.
     rewrite andb_true_iff in SUBTRACT.
     intuition.
-    destruct (eq_op eq) as [op | chunk addr] eqn:OP.
+    destruct eq as [lhs sop args | cond args] eqn:EQ.
+  * destruct sop as [op | chunk addr] eqn:OP.
     - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i).
-      unfold eq_depends_on_mem in ctx_kill_mem_has_depends_on_mem.
-      rewrite OP in ctx_kill_mem_has_depends_on_mem.
+      rewrite EQ in ctx_kill_mem_has_depends_on_mem.
+      unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem.
       rewrite (op_depends_on_memory_correct genv sp op) with (m2 := m).
       assumption.
       destruct (op_depends_on_memory op) in *; trivial.
       rewrite ctx_kill_mem_has_depends_on_mem in H0; trivial.
       discriminate H0.
     - specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i).
-      destruct eq as [lhs op args]; simpl in *.
-      rewrite OP in ctx_kill_mem_has_depends_on_mem.
+      rewrite EQ in ctx_kill_mem_has_depends_on_mem.
       rewrite negb_true_iff in H0.
-      rewrite OP in CATALOG.
       intuition.
       congruence.
+  * specialize ctx_kill_mem_has_depends_on_mem with (eq0 := eq) (j := i).
+    rewrite EQ in ctx_kill_mem_has_depends_on_mem.
+    unfold eq_cond_depends_on_mem in ctx_kill_mem_has_depends_on_mem.
+    rewrite (cond_depends_on_memory_correct cond) with (m2 := m).
+    assumption.
+    destruct (cond_depends_on_memory cond) in *; trivial.
+    rewrite negb_true_iff in H0.
+    intuition.
+    congruence.
   Qed.
 
   Hint Resolve kill_mem_sound : cse3.
@@ -691,17 +796,19 @@ Section SOUNDNESS.
     rewrite PSet.gsubtract in SUBTRACT.
     rewrite andb_true_iff in SUBTRACT.
     intuition.
-    destruct (eq_op eq) as [op | chunk addr] eqn:OP.
+    destruct eq as [lhs sop args | cond args] eqn:EQ.
+  * destruct sop as [op | chunk addr] eqn:OP.
     - rewrite op_valid_pointer_eq with (m2 := m).
       assumption.
       eapply store_preserves_validity; eauto.
     - specialize ctx_kill_store_has_depends_on_store with (eq0 := eq) (j := i).
-      destruct eq as [lhs op args]; simpl in *.
-      rewrite OP in ctx_kill_store_has_depends_on_store.
+      rewrite EQ in ctx_kill_store_has_depends_on_store.
       rewrite negb_true_iff in H0.
-      rewrite OP in CATALOG.
       intuition.
       congruence.
+  * rewrite cond_valid_pointer_eq with (m2 := m).
+    assumption.
+    eapply store_preserves_validity; eauto.
   Qed.
  
   Hint Resolve kill_store_sound : cse3.
@@ -724,6 +831,22 @@ Section SOUNDNESS.
 
   Hint Resolve eq_find_sound : cse3.
 
+  Theorem is_condition_present_sound :
+    forall node rel cond args rs m
+      (REL : sem_rel rel rs m)
+      (COND : (is_condition_present (ctx := ctx) node rel cond args) = true),
+      (eval_condition cond (rs ## args) m) = Some true.
+  Proof.
+    unfold sem_rel, is_condition_present.
+    intros.
+    destruct eq_find as [i |] eqn:FIND.
+    2: discriminate.
+    pose proof (eq_find_sound node (Cond cond args) i FIND) as CATALOG.
+    exact (REL i (Cond cond args) COND CATALOG).
+  Qed.
+
+  Hint Resolve is_condition_present_sound : cse3.
+  
   Theorem rhs_find_sound:
     forall no sop args rel src rs m,
       sem_rel rel rs m ->
@@ -742,9 +865,11 @@ Section SOUNDNESS.
     destruct (eq_catalog ctx src') as [eq | ] eqn:CATALOG.
     2: discriminate.
     specialize REL with (i := src') (eq0 := eq).
-    destruct (eq_dec_sym_op sop (eq_op eq)).
+    destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args] eqn:EQ.
+    2: discriminate.
+    destruct (eq_dec_sym_op sop eq_sop).
     2: discriminate.
-    destruct (eq_dec_args args (eq_args eq)).
+    destruct (eq_dec_args args eq_args).
     2: discriminate.
     simpl in FIND.
     intuition congruence.
@@ -794,17 +919,14 @@ Section SOUNDNESS.
     sem_rel rel rs m ->
     sem_rhs sop args rs m  v ->
     ~ In dst args ->
-    eq_find (ctx := ctx) no
-            {| eq_lhs := dst;
-               eq_op  := sop;
-               eq_args:= args |} = Some eqno ->
+    eq_find (ctx := ctx) no (Equ dst sop args) = Some eqno ->
     sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m.
   Proof.
     intros until v.
     intros REL RHS NOTIN FIND i eq CONTAINS CATALOG.
     destruct (peq i eqno).
     - subst i.
-      rewrite eq_find_sound with (no := no) (eq0 := {| eq_lhs := dst; eq_op := sop; eq_args := args |}) in CATALOG by exact FIND.
+      rewrite eq_find_sound with (no := no) (eq0 := Equ dst sop args) in CATALOG by exact FIND.
       clear FIND.
       inv CATALOG.
       unfold sem_eq.
@@ -862,7 +984,7 @@ Section SOUNDNESS.
     unfold oper2.
     intros until v.
     intros REL NOTIN RHS.    
-    pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := sop; eq_args := args |}) as EQ_FIND_SOUND.
+    pose proof (eq_find_sound no (Equ dst sop args)) as EQ_FIND_SOUND.
     destruct eq_find.
     2: auto with cse3; fail.
     specialize EQ_FIND_SOUND with (id := e).
@@ -881,14 +1003,16 @@ Section SOUNDNESS.
     }
     intros INi.
     destruct (PSet.contains rel e) eqn:CONTAINSe.
-    { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe.
+    { pose proof (REL e (Equ dst sop args) CONTAINSe H) as RELe.
       pose proof (REL i eq CONTAINS INi) as RELi.
-      unfold sem_eq in *.
-      cbn in RELe.
-      replace v with (rs # dst) by (eapply sem_rhs_det; eassumption).
-      rewrite Regmap.gsident.
-      apply sem_rhs_idem_write.
-      assumption.
+      destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; cbn in *.
+      - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption).
+        rewrite Regmap.gsident.
+        apply sem_rhs_idem_write.
+        assumption.
+      - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption).
+        rewrite arglist_idem_write.
+        assumption.
     }
     rewrite PSet.gaddo in CONTAINS by congruence.
     apply (kill_reg_sound rel rs m dst v REL i eq); auto.
@@ -919,13 +1043,17 @@ Section SOUNDNESS.
     unfold sem_rel, sem_eq, sem_rhs in *.
     intros.
     specialize REL with (i:=i) (eq0:=eq).
-    rewrite Regmap.gsident.
-    replace ((rs # r <- (rs # r)) ## (eq_args eq)) with
-        (rs ## (eq_args eq)).
+    destruct eq as [lhs sop args | cond args] eqn:EQ.
+  * rewrite Regmap.gsident.
+    replace ((rs # r <- (rs # r)) ## args) with
+        (rs ## args).
     { apply REL; auto. }
     apply list_map_exten.
     intros.
     apply Regmap.gsident.
+    (* TODO simplify? *)
+  * rewrite arglist_idem_write.
+    auto.
   Qed.
       
   Lemma move_sound :
@@ -943,7 +1071,7 @@ Section SOUNDNESS.
     { subst dst.
       apply rel_idem_replace; auto.
     }
-    pose proof (eq_find_sound no  {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND.
+    pose proof (eq_find_sound no (Equ dst (SOp Omove) (src::nil))) as EQ_FIND_SOUND.
     destruct eq_find.
     - intros i eq CONTAINS.
       destruct (peq i e).
@@ -1023,10 +1151,10 @@ Section SOUNDNESS.
     rewrite CATALOG in CONTAINS.
     unfold sem_rel in REL.
     specialize REL with (i := i) (eq0 := eq).
-    destruct eq; simpl in *.
-    unfold sem_eq in *.
+    destruct eq as [eq_lhs eq_sop eq_args | eq_cond eq_args]; simpl in *.
+  * unfold sem_eq in *.
     simpl in *.
-    destruct eq_op as [op' | chunk' addr']; simpl.
+    destruct eq_sop as [op' | chunk' addr']; simpl.
     - rewrite op_valid_pointer_eq with (m2 := m).
       + cbn in *.
         apply REL; auto.
@@ -1039,6 +1167,9 @@ Section SOUNDNESS.
       + erewrite may_overlap_sound with (chunk:=chunk) (addr:=addr) (args:=args) (chunk':=chunk') (addr':=addr') (args':=eq_args); try eassumption.
         apply REL; auto.
       + apply REL; auto.
+  * rewrite cond_valid_pointer_eq with (m2 := m).
+    auto.
+    eapply store_preserves_validity; eauto.
   Qed.
 
   Hint Resolve clever_kill_store_sound : cse3.
@@ -1076,7 +1207,7 @@ Section SOUNDNESS.
     intros i eq CONTAINS CATALOG.
     destruct (peq i eq_id).
     { subst i.
-      rewrite eq_find_sound with (no:=no) (eq0:={| eq_lhs := src; eq_op := SLoad chunk addr; eq_args := args |}) in CATALOG; trivial.
+      rewrite eq_find_sound with (no:=no) (eq0:=Equ src (SLoad chunk addr) args) in CATALOG; trivial.
       inv CATALOG.
       unfold sem_eq.
       simpl.
@@ -1157,6 +1288,79 @@ Section SOUNDNESS.
 
   Hint Resolve external_call_sound : cse3.
 
+
+  Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) :=
+    match rel with
+    | None => False
+    | Some rel => sem_rel rel rs m
+    end.
+  
+  Lemma apply_cond1_sound :
+    forall pc cond args rel rs m
+      (COND : (eval_condition cond (rs ## args) m) = Some true)
+      (REL : (sem_rel rel rs m)),
+      (sem_rel_b (apply_cond1 (ctx:=ctx) pc cond args rel) rs m).
+  Proof.
+    intros.
+    unfold apply_cond1.
+    destruct eq_find as [eq_id | ] eqn:FIND; cbn.
+    2: assumption.
+    destruct PSet.contains eqn:CONTAINS.
+    {
+      pose proof (eq_find_sound pc (Cond (negate_condition cond) args) eq_id FIND) as FIND_SOUND.
+      unfold sem_rel in REL.
+      pose proof (REL eq_id (Cond (negate_condition cond) args) CONTAINS FIND_SOUND) as REL_id.
+      cbn in REL_id.
+      rewrite eval_negate_condition in REL_id.
+      rewrite COND in REL_id.
+      discriminate.
+    }
+    exact REL.
+  Qed.
+  
+  Lemma apply_cond0_sound :
+    forall pc cond args rel rs m
+      (COND : (eval_condition cond (rs ## args) m) = Some true)
+      (REL : (sem_rel rel rs m)),
+      (sem_rel (apply_cond0 (ctx:=ctx) pc cond args rel) rs m).
+  Proof.
+    intros.
+    unfold apply_cond0.
+    destruct eq_find as [eq_id | ] eqn:FIND; cbn.
+    2: assumption.
+    pose proof (eq_find_sound pc (Cond cond args) eq_id FIND) as FIND_SOUND.
+    intros eq_id' eq' CONTAINS CATALOG.
+    destruct (peq eq_id eq_id').
+    { subst eq_id'.
+      unfold sem_eq.
+      rewrite FIND_SOUND in CATALOG.
+      inv CATALOG.
+      assumption.
+    }
+    rewrite PSet.gaddo in CONTAINS by assumption.
+    unfold sem_rel in REL.
+    eapply REL; eassumption.
+  Qed.
+
+  Lemma apply_cond_sound :
+    forall pc cond args rel rs m
+      (COND : (eval_condition cond (rs ## args) m) = Some true)
+      (REL : (sem_rel rel rs m)),
+      (sem_rel_b (apply_cond (ctx:=ctx) pc cond args rel) rs m).
+  Proof.
+    unfold apply_cond.
+    intros.
+    destruct (Compopts.optim_CSE3_conditions tt).
+    {
+      pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
+      destruct apply_cond1 eqn:COND1.
+      { apply apply_cond0_sound; auto. }
+      exact SOUND1.
+    }
+    exact REL.
+  Qed.
+  
+  (*
   Section INDUCTIVENESS.
     Variable fn : RTL.function.
     Variable tenv : typing_env.
@@ -1167,7 +1371,10 @@ Section SOUNDNESS.
         PTree.get pc (fn_code fn) = Some instr ->
         In pc' (successors_instr instr) ->
         RB.ge (PMap.get pc' inv)
-              (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (PMap.get pc inv)).
+              (match apply_instr' (ctx:=ctx) tenv (fn_code fn) pc
+                                  (PMap.get pc inv) with
+               | Abst_same rel' => rel'
+              end).
 
     Definition is_inductive_allstep :=
       forall pc pc', is_inductive_step pc pc'.
@@ -1186,11 +1393,14 @@ Section SOUNDNESS.
       pose proof (ALL INSTR) as AT_PC.
       destruct (inv # pc).
       2: apply RB.ge_bot.
-      rewrite List.forallb_forall in AT_PC.
       unfold apply_instr'.
       rewrite INSTR.
-      apply relb_leb_correct.
-      auto.
+      destruct apply_instr.
+      { (* same *)
+        rewrite List.forallb_forall in AT_PC.
+        apply relb_leb_correct.
+        auto.
+      }
     Qed.
     
     Lemma checked_is_inductive_entry:
@@ -1211,4 +1421,5 @@ Section SOUNDNESS.
   End INDUCTIVENESS.
 
   Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3.
+  *)
 End SOUNDNESS.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 2257b4de..0722f904 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -352,6 +352,23 @@ Qed.
 
 Hint Resolve rel_ge : cse3.
 
+Lemma relb_ge:
+  forall inv inv'
+         (GE : RB.ge inv' inv)
+         ctx sp rs m
+         (REL: sem_rel_b sp ctx inv rs m),
+  sem_rel_b sp ctx inv' rs m.
+Proof.
+  intros.
+  destruct inv; cbn in *.
+  2: contradiction.
+  destruct inv'; cbn in *.
+  2: assumption.
+  eapply rel_ge; eassumption.
+Qed.
+
+Hint Resolve relb_ge : cse3.
+
 Lemma sem_rhs_sop :
   forall sp op rs args m v,
   eval_operation ge sp op rs ## args m = Some v ->
@@ -422,6 +439,7 @@ Qed.
 
 Hint Resolve sem_rel_b_top : cse3.
 
+(*
 Ltac IND_STEP :=
         match goal with
         REW: (fn_code ?fn) ! ?mpc = Some ?minstr
@@ -442,19 +460,42 @@ Ltac IND_STEP :=
         eapply rel_ge; eauto with cse3 (* ; for printing
         idtac mpc mpc' fn minstr *)
       end.
-
+ *)
+  
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> 
   forall S1', match_states S1 S1' ->
               exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
 Proof.
   induction 1; intros S1' MS; inv MS.
+  all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))) in *.
+  all: try set (invs := (fst (preanalysis tenv f))) in *.
   - (* Inop *)
     exists (State ts tf sp pc' rs m). split.
     + apply exec_Inop; auto.
       TR_AT. reflexivity.
     + econstructor; eauto.
-      IND_STEP.
+      
+      (* BEGIN INVARIANT *)
+      fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      unfold sem_rel_b.
+      apply (rel_ge inv_pc inv_pc'); auto.
+      (* END INVARIANT *)
+      
   - (* Iop *)
     exists (State ts tf sp pc' (rs # res <- v) m). split.
     + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'.
@@ -516,9 +557,28 @@ Proof.
     + econstructor; eauto.
       * eapply wt_exec_Iop with (f:=f); try eassumption.
         eauto with wt.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
-
+      *
+        (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
   - (* Iload *)
     exists (State ts tf sp pc' (rs # dst <- v) m). split.
     + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
@@ -575,8 +635,27 @@ Proof.
     + econstructor; eauto.
       * eapply wt_exec_Iload with (f:=f); try eassumption.
         eauto with wt.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
+      *         (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
         
   - (* Iload notrap1 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
@@ -632,8 +711,27 @@ Proof.
            assumption.
     + econstructor; eauto.
       * apply wt_undef; assumption.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
+      *          (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
         
   - (* Iload notrap2 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
@@ -690,8 +788,27 @@ Proof.
            assumption.
     + econstructor; eauto.
       * apply wt_undef; assumption.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
+      *  (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
 
   - (* Istore *)
     exists (State ts tf sp pc' rs m'). split.
@@ -704,8 +821,27 @@ Proof.
       * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
         assumption.
     + econstructor; eauto.
-      IND_STEP.
-      apply store_sound with (a0:=a) (m0:=m); eauto with cse3.
+  (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply store_sound with (a0:=a) (m0:=m); unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
       
   - (* Icall *)
     destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]].
@@ -720,9 +856,29 @@ Proof.
       * econstructor; eauto.
         ** rewrite sig_preserved with (f:=fd); assumption.
         ** intros.
-           IND_STEP.
-           apply kill_reg_sound; eauto with cse3.
-           eapply kill_mem_sound; eauto with cse3.
+
+            (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      (* END INVARIANT *)
+      { apply kill_reg_sound; unfold ctx; eauto with cse3.
+           eapply kill_mem_sound; unfold ctx; eauto with cse3. }
       * rewrite sig_preserved with (f:=fd) by trivial.
         rewrite <- H7.
         apply wt_regset_list; auto.
@@ -760,19 +916,159 @@ Proof.
       * eapply external_call_symbols_preserved; eauto. apply senv_preserved.
     + econstructor; eauto.
       * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt.
-      * IND_STEP.
-        apply kill_builtin_res_sound; eauto with cse3.
-        eapply external_call_sound; eauto with cse3.
+      *   (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      (* END INVARIANT *)
+
+        apply kill_builtin_res_sound; unfold ctx; eauto with cse3.
+        eapply external_call_sound; unfold ctx; eauto with cse3.
         
   - (* Icond *)
-    econstructor. split.
-    + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
-      * TR_AT. reflexivity.
-      * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
-        eassumption.
-      * reflexivity.
-    + econstructor; eauto.
-      destruct b; IND_STEP.
+    destruct (find_cond_in_fmap (ctx := ctx) invs pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
+    + econstructor; split.
+      * eapply exec_Inop; try eassumption.
+        TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
+      * replace bfound with b.
+        { econstructor; eauto.
+          (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me as [IND_so [IND_not ZOT]].
+      clear ZOT.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
+      destruct b.
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
+      (* END INVARIANT *)
+        }
+        unfold sem_rel_b in REL.
+        destruct (invs # pc) as [rel | ] eqn:FIND_REL.
+        2: contradiction.
+        pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE.
+        pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE.
+        rewrite eval_negate_condition in COND_PRESENT_FALSE.
+        unfold find_cond_in_fmap in FIND_COND.
+        change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND.
+        rewrite FIND_REL in FIND_COND.
+        destruct (Compopts.optim_CSE3_conditions tt).
+        2: discriminate.
+        destruct (is_condition_present pc rel cond args).
+        { rewrite COND_PRESENT_TRUE in H0 by trivial.
+          congruence.
+        }
+        destruct (is_condition_present pc rel (negate_condition cond) args).
+        { destruct (eval_condition cond rs ## args m) as [b0 | ].
+          2: discriminate.
+          inv H0.
+          cbn in COND_PRESENT_FALSE.
+          intuition.
+          inv H0.
+          inv FIND_COND.
+          destruct b; trivial; cbn in H2; discriminate.
+        }
+        clear COND_PRESENT_TRUE COND_PRESENT_FALSE.
+        pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE.
+        pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE.
+        rewrite eval_negate_condition in COND_PRESENT_FALSE.
+        
+        destruct is_condition_present.
+        { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE.
+          { rewrite COND_PRESENT_TRUE in H0 by trivial.
+            congruence.
+          }
+          unfold fmap_sem.
+          unfold sem_rel_b.
+          fold invs.
+          rewrite FIND_REL.
+          exact REL.
+        }
+        destruct is_condition_present.
+        { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE.
+          { destruct (eval_condition cond rs ## args m) as [b0 | ].
+            2: discriminate.
+            inv H0.
+            cbn in COND_PRESENT_FALSE.
+            intuition.
+            inv H0.
+            inv FIND_COND.
+            destruct b; trivial; cbn in H2; discriminate.
+          }
+          unfold fmap_sem.
+          unfold sem_rel_b.
+          fold invs.
+          rewrite FIND_REL.
+          exact REL.          
+        }
+        discriminate.
+   + econstructor; split.        
+      * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
+        ** TR_AT. unfold transf_instr. fold invs. fold ctx.
+           rewrite FIND_COND.
+           reflexivity.
+        ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
+           eassumption.
+        ** reflexivity.
+     * econstructor; eauto.
+
+          (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me as [IND_so [IND_not ZOT]].
+      clear ZOT.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
+      destruct b.
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
+      (* END INVARIANT *)
       
   - (* Ijumptable *)
     econstructor. split.
@@ -781,8 +1077,33 @@ Proof.
       * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
         assumption.
     + econstructor; eauto.
-      assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption).
-      IND_STEP.
+      
+      (* BEGIN INVARIANT *)
+      fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite forallb_forall in IND_step_me.
+      assert (RB.ge (invs # pc') (Some inv_pc)) as GE.
+      {
+        apply relb_leb_correct.
+        specialize IND_step_me with (pc', Some inv_pc).
+        apply IND_step_me.
+        apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))).
+        eapply list_nth_z_in.
+        eassumption.
+      }
+      destruct (invs # pc'); cbn in *.
+      2: contradiction.
+      eapply rel_ge; eauto.
+      (* END INVARIANT *)
 
   - (* Ireturn *)
     destruct or as [arg | ].
@@ -824,9 +1145,18 @@ Proof.
         apply wt_init_regs.
         rewrite <- wt_params in WTARGS.
         assumption.
-      * rewrite @checked_is_inductive_entry with (tenv:=tenv) (ctx:=(context_from_hints (snd (preanalysis tenv f)))).
-        ** apply sem_rel_b_top.
-        ** apply transf_function_invariants_inductive with (tf:=tf); auto.
+      * assert ((check_inductiveness f tenv (fst (preanalysis tenv f)))=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+        unfold check_inductiveness in IND.
+        rewrite andb_true_iff in IND.
+        destruct IND as [IND_entry IND_step].
+        clear IND_step.
+        apply RB.beq_correct in IND_entry.
+        unfold RB.eq in *.
+        destruct ((fst (preanalysis tenv f)) # (fn_entrypoint f)).
+        2: contradiction.
+        cbn.
+        rewrite <- IND_entry.
+        apply sem_rel_top.
            
   - (* external *)
     simpl in FUN.
diff --git a/config_rv32.sh b/config_rv32.sh
index a5a5cf1c..654cacfa 100755
--- a/config_rv32.sh
+++ b/config_rv32.sh
@@ -1 +1 @@
-exec ./config_simple.sh rv32-linux --toolprefix riscv64-linux-gnu- "$@"
+exec ./config_simple.sh rv32-linux --toolprefix riscv64-unknown-elf- "$@"
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 60d532db..9b7b5c4d 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -34,7 +34,9 @@ let option_fcse3_across_calls = ref false
 let option_fcse3_across_merges = ref true
 let option_fcse3_glb = ref true
 let option_fcse3_trivial_ops = ref false
-let option_fcse3_refine = ref true                             
+let option_fcse3_refine = ref true
+let option_fcse3_conditions = ref true
+                        
 let option_fredundancy = ref true
 
 (** Options relative to superblock scheduling *)
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 0c90ee52..65264124 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -57,6 +57,9 @@ Parameter optim_CSE3_glb: unit -> bool.
 (** Flag -fcse3-trivial-ops. For DMonniaux's common subexpression elimination, simplify trivial operations as well. *)
 Parameter optim_CSE3_trivial_ops: unit -> bool.
 
+(** Flag -fcse3-conditions. For DMonniaux's common subexpression elimination: remove redundant conditional branches. *)
+Parameter optim_CSE3_conditions: unit -> bool.
+
 (** Flag -fmove-loop-invariants. *)
 Parameter optim_move_loop_invariants: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 30c31c27..c9eacadc 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -204,6 +204,7 @@ Processing options:
   -fcse3-glb            Refine CSE3 information using greatest lower bounds [on]
   -fcse3-trivial-ops    Replace trivial operations as well using CSE3 [off]
   -fcse3-refine         Refine CSE3 invariants by descending iteration [on]
+  -fcse3-conditions     Remove redundant conditions using CSE3 [on]
   -fmove-loop-invariants Perform loop-invariant code motion [off]
   -fredundancy   Perform redundancy elimination [on]
   -mtune=         Type of CPU (for scheduling on some architectures)
@@ -418,6 +419,7 @@ let cmdline_actions =
   @ f_opt "cse3-glb" option_fcse3_glb
   @ f_opt "cse3-trivial-ops" option_fcse3_trivial_ops
   @ f_opt "cse3-refine" option_fcse3_refine
+  @ f_opt "cse3-conditions" option_fcse3_conditions
   @ f_opt "move-loop-invariants" option_fmove_loop_invariants
   @ f_opt "redundancy" option_fredundancy
   @ [ Exact "-mtune", String (fun s -> option_mtune := s) ]
diff --git a/extraction/extraction.vexpand b/extraction/extraction.vexpand
index 568b1b46..55ca3b5c 100644
--- a/extraction/extraction.vexpand
+++ b/extraction/extraction.vexpand
@@ -130,6 +130,8 @@ Extract Constant Compopts.optim_CSE3_glb =>
   "fun _ -> !Clflags.option_fcse3_glb".
 Extract Constant Compopts.optim_CSE3_trivial_ops =>
   "fun _ -> !Clflags.option_fcse3_trivial_ops".
+Extract Constant Compopts.optim_CSE3_conditions =>
+  "fun _ -> !Clflags.option_fcse3_conditions".
 Extract Constant Compopts.optim_move_loop_invariants =>
   "fun _ -> !Clflags.option_fmove_loop_invariants".
 
@@ -223,7 +225,7 @@ Cd "extraction".
 
 Separate Extraction 
    Z.ldiff Z.lnot Nat.leb
-   CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem
+   CSE3analysis.eq_cond_depends_on_mem CSE3analysis.apply_instr'
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
diff --git a/kvx/Op.v b/kvx/Op.v
index 794bc87b..4458adb3 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -1205,12 +1205,25 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
+Definition cond_depends_on_memory (c: condition) : bool :=
+  match c with
+  | Ccompu _ | Ccompuimm _ _ => negb Archi.ptr64
+  | Ccomplu _ | Ccompluimm _ _  => Archi.ptr64
+  | _ => false
+  end.
+
+Lemma cond_depends_on_memory_correct:
+  forall c args m1 m2,
+  cond_depends_on_memory c = false ->
+  eval_condition c args m1 = eval_condition c args m2.
+Proof.
+  intros; destruct c; cbn; discriminate || reflexivity.
+Qed.
+
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _) => negb Archi.ptr64
-  | Ocmp (Ccompuimm _ _) => negb Archi.ptr64
-  | Ocmp (Ccomplu _) => Archi.ptr64
-  | Ocmp (Ccompluimm _ _) => Archi.ptr64
+  | Ocmp (Ccompu _ | Ccompuimm _ _) => negb Archi.ptr64
+  | Ocmp (Ccomplu _ | Ccompluimm _ _) => Archi.ptr64
   
   | Osel (Ccompu0 _) _   | Oselimm (Ccompu0 _) _   | Osellimm (Ccompu0 _) _ => negb Archi.ptr64
   | Osel (Ccomplu0 _) _ | Oselimm (Ccomplu0 _) _ | Osellimm (Ccomplu0 _) _ => Archi.ptr64
@@ -1238,23 +1251,33 @@ Proof.
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence.
-  - intros MEM; destruct cond; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  intros until m2. destruct op; cbn; try congruence.
+  - intros MEM; destruct cond; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intros MEM; destruct c0; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  - intros MEM; destruct c0; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intros MEM; destruct c0; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  - intros MEM; destruct c0; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intros MEM; destruct c0; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  - intros MEM; destruct c0; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.
 
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 684b90bf..505b7545 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -748,7 +748,7 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
-Definition condition_depends_on_memory (c: condition) : bool :=
+Definition cond_depends_on_memory (c: condition) : bool :=
   match c with
   | Ccompu _ => true
   | Ccompuimm _ _ => true
@@ -759,14 +759,14 @@ Definition condition_depends_on_memory (c: condition) : bool :=
 
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp c => condition_depends_on_memory c
-  | Osel c ty => condition_depends_on_memory c
+  | Ocmp c => cond_depends_on_memory c
+  | Osel c ty => cond_depends_on_memory c
   | _ => false
   end.
 
-Lemma condition_depends_on_memory_correct:
+Lemma cond_depends_on_memory_correct:
   forall c args m1 m2,
-  condition_depends_on_memory c = false ->
+  cond_depends_on_memory c = false ->
   eval_condition c args m1 = eval_condition c args m2.
 Proof.
   intros. destruct c; simpl; auto; discriminate.
@@ -778,12 +778,22 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence; intros C.
-- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- f_equal; f_equal; apply cond_depends_on_memory_correct; auto.
 - destruct args; auto. destruct args; auto.
-  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  rewrite (cond_depends_on_memory_correct c args m1 m2 C).
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
diff --git a/riscV/Op.v b/riscV/Op.v
index 62999a2f..2271ecd2 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -858,25 +858,53 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
+Definition cond_depends_on_memory (cond : condition) : bool :=
+  match cond with
+  | Ccompu _ => negb Archi.ptr64
+  | Ccompuimm _ _ => negb Archi.ptr64
+  | Ccomplu _ => Archi.ptr64
+  | Ccompluimm _ _ => Archi.ptr64
+  | _ => false
+  end.
+
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _) => negb Archi.ptr64
-  | Ocmp (Ccompuimm _ _) => negb Archi.ptr64
-  | Ocmp (Ccomplu _) => Archi.ptr64
-  | Ocmp (Ccompluimm _ _) => Archi.ptr64
+  | Ocmp cmp => cond_depends_on_memory cmp
   | _ => false
   end.
 
+Lemma cond_depends_on_memory_correct:
+  forall cond args m1 m2,
+  cond_depends_on_memory cond = false ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2.
+  destruct cond; cbn; try congruence.
+  all: unfold Val.cmpu_bool, Val.cmplu_bool.
+  all: destruct Archi.ptr64; cbn; intro SF; try discriminate.
+  all: reflexivity.
+Qed.
+
 Lemma op_depends_on_memory_correct:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   op_depends_on_memory op = false ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence.
-  destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
-  unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  intro DEPEND.
+  f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+ 
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
diff --git a/test/monniaux/if/if2.c b/test/monniaux/if/if2.c
new file mode 100644
index 00000000..2a6d5507
--- /dev/null
+++ b/test/monniaux/if/if2.c
@@ -0,0 +1,11 @@
+int toto(int x) {
+  if (2*x+1 >= 3) {
+    if (2*x+1 >= 3) {
+      return 3;
+    } else {
+      return 2;
+    }
+  } else {
+    return 1;
+  }
+}
diff --git a/x86/Op.v b/x86/Op.v
index 776f9495..caa63235 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -999,7 +999,7 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
-Definition condition_depends_on_memory (c: condition) : bool :=
+Definition cond_depends_on_memory (c: condition) : bool :=
   match c with
   | Ccompu _ => negb Archi.ptr64
   | Ccompuimm _ _ => negb Archi.ptr64
@@ -1010,14 +1010,14 @@ Definition condition_depends_on_memory (c: condition) : bool :=
 
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp c => condition_depends_on_memory c
-  | Osel c ty => condition_depends_on_memory c
+  | Ocmp c => cond_depends_on_memory c
+  | Osel c ty => cond_depends_on_memory c
   | _ => false
   end.
 
-Lemma condition_depends_on_memory_correct:
+Lemma cond_depends_on_memory_correct:
   forall c args m1 m2,
-  condition_depends_on_memory c = false ->
+  cond_depends_on_memory c = false ->
   eval_condition c args m1 = eval_condition c args m2.
 Proof.
   intros until m2. 
@@ -1031,12 +1031,22 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence; intros C.
-- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- f_equal; f_equal; apply cond_depends_on_memory_correct; auto.
 - destruct args; auto. destruct args; auto.
-  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  rewrite (cond_depends_on_memory_correct c args m1 m2 C).
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->