Reworked CSE for operations.

Reworked CSE to also work if the result after the transformation is more
defined than the original value. This allows simplifying comparisons
operations as well as selection operations.
Bug 34849

aarch64/CombineOp.v

@@ -144,14 +144,23 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       | _ => None
       end
   | Ocmp cond, _ =>
-      match combine_cond cond args with
-      | Some(cond', args') => Some(Ocmp cond', args')
-      | None => None
+      match combine_cond' cond args with
+      | Some b => Some ((if b then Ointconst Int.one else Ointconst Int.zero), nil)
+      | None =>
+          match combine_cond cond args with
+          | Some(cond', args') => Some(Ocmp cond', args')
+          | None => None
+          end
       end
   | Osel cond ty, x :: y :: args =>
-      match combine_cond cond args with
-      | Some (cond', args') => Some (Osel cond' ty, x :: y :: args')
-      | None => None
+      match combine_cond' cond args with
+      | Some b => Some (Omove, (if b then x else y) :: nil)
+      | None =>
+          if eq_valnum x y then Some (Omove, x :: nil) else
+          match combine_cond cond args with
+          | Some (cond', args') => Some (Osel cond' ty, x :: y :: args')
+          | None => None
+          end
       end
   | _, _ => None
   end.

aarch64/CombineOpproof.v

@@ -204,41 +204,60 @@ Proof.
 Qed.
 
 Theorem combine_op_sound:
-  forall op args op' args',
+  forall op args op' args' r,
   combine_op get op args = Some(op', args') ->
-  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+  eval_operation ge sp op (map valu args) m = Some r ->
+  exists r', eval_operation ge sp op' (map valu args') m = Some r' /\ Val.lessdef r r'.
 Proof.
   intros. functional inversion H; subst.
   (* addimm - addimm *)
-  - UseGetSound. FuncInv. simpl.
-    rewrite <- H0. rewrite Val.add_assoc. auto.
+  - UseGetSound. exists r; split; auto.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.add_assoc. auto.
   (* andimm - andimm *)
   - UseGetSound; simpl.
-    generalize (Int.eq_spec p m0); rewrite H7; intros.
-    rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
-  - UseGetSound; simpl.
-    rewrite <- H0. rewrite Val.and_assoc. auto.
+    generalize (Int.eq_spec p m0); rewrite H8; intros. exists r; split; auto.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.and_assoc.
+    simpl. fold p. rewrite H2. auto.
+  - UseGetSound; simpl. exists r; split; auto.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.and_assoc. auto.
   (* orimm - orimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1. rewrite Val.or_assoc. auto.
   (* xorimm - xorimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1. rewrite Val.xor_assoc. auto.
   (* addlimm - addlimm *)
-  - UseGetSound. FuncInv. simpl.
-    rewrite <- H0. rewrite Val.addl_assoc. auto.
+  - UseGetSound. exists r; split; auto.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.addl_assoc. auto.
   (* andlimm - andlimm *)
-  - UseGetSound; simpl.
-    generalize (Int64.eq_spec p m0); rewrite H7; intros.
-    rewrite <- H0. rewrite Val.andl_assoc. simpl. fold p. rewrite H1. auto.
-  - UseGetSound; simpl.
-    rewrite <- H0. rewrite Val.andl_assoc. auto.
+  - UseGetSound. exists r; split; auto.
+    generalize (Int64.eq_spec p m0); rewrite H8; intros.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.andl_assoc. simpl. fold p. rewrite H2. auto.
+  - UseGetSound. exists r; split; auto.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.andl_assoc. auto.
   (* orlimm - orlimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.orl_assoc. auto.
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1. rewrite Val.orl_assoc. auto.
   (* xorlimm - xorlimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto.
-  (* cmp *)
-  - simpl. decEq; decEq. eapply combine_cond_sound; eauto.
-  (* sel *)
-  - simpl. erewrite combine_cond_sound; eauto.
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1. rewrite Val.xorl_assoc. auto.
+  (* cmp true *)
+  - exists Vtrue; split; auto. inv H0. destruct (eval_condition cond (map valu args) m) eqn:?; auto.
+    rewrite (combine_cond'_sound cond args b true); eauto.
+  (* cmp false *)
+  - exists Vfalse; split; auto. inv H0. destruct (eval_condition cond (map valu args) m) eqn:?; auto.
+    rewrite (combine_cond'_sound cond args b false); eauto.
+  (* cmp reduce *)
+  - exists r; split; auto. decEq; decEq. simpl. erewrite combine_cond_sound; eauto.
+  (* sel cond true *)
+  - exists (valu x). simpl in H0.
+   destruct (eval_condition cond (map valu args1) m) eqn:?; simpl; split; auto; inv H0; auto.
+   rewrite (combine_cond'_sound cond args1 b true); eauto.  destruct (valu x), ty; auto.
+  (* sel cond false *)
+  - exists (valu y). simpl in H0.
+   destruct (eval_condition cond (map valu args1) m) eqn:?; simpl; split; auto; inv H0; auto.
+   rewrite (combine_cond'_sound cond args1 b false); eauto.  destruct (valu y), ty; auto.
+  (* sel cond same *)
+  - exists (valu y); split; auto. inv H0. destruct (eval_condition cond (map valu args1) m); auto.
+   simpl. destruct b, (valu y), ty; auto.
+  - exists r; split; auto. rewrite <- H0.
+   simpl. erewrite combine_cond_sound; eauto.
 Qed.
 
 End COMBINE.

arm/CombineOp.v

@@ -131,14 +131,23 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       | _ => None
       end
   | Ocmp cond, _ =>
-      match combine_cond cond args with
-      | Some(cond', args') => Some(Ocmp cond', args')
-      | None => None
+      match combine_cond' cond args with
+      | Some b => Some ((if b then Ointconst Int.one else Ointconst Int.zero), nil)
+      | None =>
+          match combine_cond cond args with
+          | Some(cond', args') => Some(Ocmp cond', args')
+          | None => None
+          end
       end
   | Osel cond ty, x :: y :: args =>
-      match combine_cond cond args with
-      | Some (cond', args') => Some (Osel cond' ty, x :: y :: args')
-      | None => None
+      match combine_cond' cond args with
+      | Some b => Some (Omove, (if b then x else y) :: nil)
+      | None =>
+          if eq_valnum x y then Some (Omove, x :: nil) else
+          match combine_cond cond args with
+          | Some (cond', args') => Some (Osel cond' ty, x :: y :: args')
+          | None => None
+          end
       end
   | _, _ => None
   end.

arm/CombineOpproof.v

@@ -187,38 +187,58 @@ Proof.
 Qed.
 
 Theorem combine_op_sound:
-  forall op args op' args',
+  forall op args op' args' r,
   combine_op get op args = Some(op', args') ->
-  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+  eval_operation ge sp op (map valu args) m = Some r ->
+  exists r', eval_operation ge sp op' (map valu args') m = Some r' /\ Val.lessdef r r'.
 Proof.
   intros. functional inversion H; subst.
-(* addimm - addimm *)
-  UseGetSound. FuncInv. simpl.
-  rewrite <- H0. rewrite Val.add_assoc. auto.
-(* addimm - subimm *)
-Opaque Val.sub.
-  UseGetSound. FuncInv. simpl.
+  (* addimm - addimm *)
+  - UseGetSound. exists r; split; auto.
+    rewrite <- H0. simpl. rewrite <- H1. rewrite Val.add_assoc. auto.
+  (* addimm - subimm *)
+  - Opaque Val.sub.
+  UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1.
   change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)).
-  rewrite <- H0. rewrite Val.sub_add_l. auto.
-(* subimm - addimm *)
-  UseGetSound. FuncInv. simpl. rewrite <- H0.
+  rewrite Val.sub_add_l. auto.
+  (* subimm - addimm *)
+  -  UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1.
 Transparent Val.sub.
   destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc.
   rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut.
-(* andimm - andimm *)
-  UseGetSound; simpl.
-  generalize (Int.eq_spec p m0); rewrite H7; intros.
-  rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
-  UseGetSound; simpl.
-  rewrite <- H0. rewrite Val.and_assoc. auto.
-(* orimm - orimm *)
-  UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
-(* xorimm - xorimm *)
-  UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
-(* cmp *)
-  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
-(* sel *)
-  simpl. erewrite combine_cond_sound; eauto.
+  (* andimm - andimm *)
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1.
+  generalize (Int.eq_spec p m0); rewrite H8; intros.
+  rewrite Val.and_assoc. simpl. fold p. rewrite H2. auto.
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1.
+    rewrite Val.and_assoc. auto.
+  (* orimm - orimm *)
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1.
+    rewrite Val.or_assoc. auto.
+  (* xorimm - xorimm *)
+  - UseGetSound. exists r; split; auto. rewrite <- H0. simpl. rewrite <- H1.
+    rewrite Val.xor_assoc. auto.
+  (* cmp true *)
+  - exists Vtrue; split; auto. inv H0. destruct (eval_condition cond (map valu args) m) eqn:?; auto.
+    rewrite (combine_cond'_sound cond args b true); eauto.
+  (* cmp false *)
+  - exists Vfalse; split; auto. inv H0. destruct (eval_condition cond (map valu args) m) eqn:?; auto.
+    rewrite (combine_cond'_sound cond args b false); eauto.
+  (* cmp reduce *)
+  - exists r; split; auto. decEq; decEq. simpl. erewrite combine_cond_sound; eauto.
+  (* sel cond true *)
+  - exists (valu x). simpl in H0.
+   destruct (eval_condition cond (map valu args1) m) eqn:?; simpl; split; auto; inv H0; auto.
+   rewrite (combine_cond'_sound cond args1 b true); eauto.  destruct (valu x), ty; auto.
+  (* sel cond false *)
+  - exists (valu y). simpl in H0.
+   destruct (eval_condition cond (map valu args1) m) eqn:?; simpl; split; auto; inv H0; auto.
+   rewrite (combine_cond'_sound cond args1 b false); eauto.  destruct (valu y), ty; auto.
+  (* sel cond same *)
+  - exists (valu y); split; auto. inv H0. destruct (eval_condition cond (map valu args1) m); auto.
+   simpl. destruct b, (valu y), ty; auto.
+  - exists r; split; auto. rewrite <- H0.
+   simpl. erewrite combine_cond_sound; eauto.
 Qed.
 
 End COMBINE.

backend/CSEproof.v

@@ -776,6 +776,73 @@ Qed.
 
 End REDUCE.
 
+
+Section REDUCELD.
+
+Variable A: Type.
+Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
+Variable ge: genv.
+Variable sp: val.
+Variable rs: regset.
+Variable m: mem.
+Variable sem: A -> list val -> option val.
+Hypothesis f_sound:
+  forall eqs valu op args op' args' r,
+  (forall v rhs, eqs v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v)) ->
+  f eqs op args = Some(op', args') ->
+  sem op (map valu args) = Some r ->
+  exists r',
+  sem op' (map valu args') = Some r' /\ Val.lessdef r r'.
+Variable n: numbering.
+Variable valu: valnum -> val.
+Hypothesis n_holds: numbering_holds valu ge sp rs m n.
+
+Lemma reduce_rec_sound':
+  forall niter op args op' rl' r,
+  reduce_rec A f n niter op args = Some(op', rl') ->
+  sem op (map valu args) = Some r ->
+  exists r',
+  sem op' (rs##rl') = Some r' /\ Val.lessdef r r'.
+Proof.
+  induction niter; simpl; intros.
+  discriminate.
+  destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
+           as [[op1 args1] | ] eqn:?; try discriminate.
+  assert (exists r': val, sem op1 (map valu args1) = Some r' /\ Val.lessdef r r').
+  { exploit f_sound.
+    simpl; intros.
+    exploit num_holds_eq; eauto.
+    eapply find_valnum_num_charact; eauto with cse.
+    eapply H1.
+    intros EH; inv EH; auto. eexact H3. eexact Heqo. eexact H0.
+    intros. eauto.
+  }
+  destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?.
+  destruct H1. destruct H1.
+  exploit IHniter. eexact Heqo0. eexact H1. inv H.
+  intros. destruct H. destruct H. exists x0. split; eauto.
+  eapply Val.lessdef_trans. eexact H2. eexact H3.
+  destruct (regs_valnums n args1) as [rl|] eqn:?; try discriminate.
+  inv H. erewrite regs_valnums_sound; eauto.
+Qed.
+
+
+Lemma reduce_sound':
+  forall op rl vl op' rl' r,
+  reduce A f n op rl vl = (op', rl') ->
+  map valu vl = rs##rl ->
+  sem op rs##rl = Some r ->
+  exists r', sem op' rs##rl' = Some r' /\ Val.lessdef r r'.
+Proof.
+  unfold reduce; intros.
+  destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?.
+  eapply reduce_rec_sound'; eauto. inv H. eexact Heqo. congruence.
+  exists r. inv H. auto.
+Qed.
+
+End REDUCELD.
+
+
 (** The numberings associated to each instruction by the static analysis
   are inductively satisfiable, in the following sense: the numbering
   at the function entry point is satisfiable, and for any RTL execution
@@ -1016,20 +1083,24 @@ Proof.
   eapply Val.lessdef_trans; eauto.
 * (* possibly simplified *)
   destruct (reduce operation combine_op n1 op args vl) as [op' args'] eqn:?.
-  assert (RES: eval_operation ge sp op' rs##args' m = Some v).
-    eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto.
-    intros; eapply combine_op_sound; eauto.
-  exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto.
-  intros [v' [A B]].
+  assert (RES: exists v', eval_operation ge sp op' rs##args' m = Some v' /\ Val.lessdef v v').
+  { exploit (reduce_sound' operation combine_op ge sp rs m (fun op vl => eval_operation ge sp op vl m)); eauto.
+    intros. exploit combine_op_sound. intros; eauto. eexact H2. eexact H3. intros (v' & EV & LD).
+    exists v'; auto.
+  }
+  destruct RES as (v' & EV' & LD').
+  assert  (exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v'').
+  { eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto. }
+  destruct H1 as [v'' [EV'' LD'']].
   econstructor; split.
-  eapply exec_Iop with (v := v'); eauto.
-  rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
+  eapply exec_Iop. eexact C. erewrite eval_operation_preserved. eexact EV''.
+  exact symbols_preserved.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   eapply add_op_holds; eauto.
   apply set_reg_lessdef; auto.
-
+  eapply (Val.lessdef_trans v v' v''); auto.
 - (* Iload *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].

powerpc/CombineOp.v

@@ -141,18 +141,25 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       | _ => None
       end
   | Ocmp cond, _ =>
-      match combine_cond cond args with
-      | Some(cond', args') => Some(Ocmp cond', args')
-      | None => None
+      match combine_cond' cond args with
+      | Some b => Some ((if b then Ointconst Int.one else Ointconst Int.zero), nil)
+      | None =>
+          match combine_cond cond args with
+          | Some(cond', args') => Some(Ocmp cond', args')
+          | None => None
+          end
       end
   | Osel cond ty, x :: y :: args =>
-      match combine_cond cond args with
-      | Some (cond', args') => Some (Osel cond' ty, x :: y :: args')
-      | None => None
+      match combine_cond' cond args with
+      | Some b => Some (Omove, (if b then x else y) :: nil)
+      | None =>
+          if eq_valnum x y then Some (Omove, x :: nil) else
+          match combine_cond cond args with
+          | Some (cond', args') => Some (Osel cond' ty, x :: y :: args')
+          | None => None
+          end
       end
   | _, _ => None
   end.
 
 End COMBINE.
-
-