Conditions now propagated by CSE3

Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work

17 files changed, 1091 insertions, 312 deletions

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