CombineOp: optimize (x ^ n) != 0 into x != n

Likewise for `(x ^ n) == 0` that becomes `x == n`.

Do this only when we're sure it results in smaller code:

- On RISC-V, the optimization is useless, as there is no conditional
  branch instruction for != n and == n conditions, just for != 0 and == 0.

- On ARM, AArch64, PowerPC: we limit the optimization to values of n
  that are small enough to not need extra instructions to load the
  immediate n in a register.

aarch64/CombineOp.v

@@ -25,12 +25,16 @@ Variable get: valnum -> option rhs.
 Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | Some(Op (Oxorimm n) ys) =>
+      if Int.eq n (Int.zero_ext 12 n) then Some (Ccompimm Cne n, ys) else None
   | _ => None
   end.
 
 Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | Some(Op (Oxorimm n) ys) =>
+      if Int.eq n (Int.zero_ext 12 n) then Some (Ccompimm Ceq n, ys) else None
   | _ => None
   end.
 

aarch64/CombineOpproof.v

@@ -48,6 +48,9 @@ Proof.
   (* of cmp *)
   UseGetSound. rewrite <- H.
   destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -61,6 +64,9 @@ Proof.
   UseGetSound. rewrite <- H.
   rewrite eval_negate_condition.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_1_sound:

arm/CombineOp.v

@@ -26,12 +26,16 @@ Variable get: valnum -> option rhs.
 Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | Some(Op (Oxorimm n) ys) =>
+      if Int.eq n (Int.zero_ext 8 n) then Some (Ccompimm Cne n, ys) else None
   | _ => None
   end.
 
 Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | Some(Op (Oxorimm n) ys) =>
+      if Int.eq n (Int.zero_ext 8 n) then Some (Ccompimm Ceq n, ys) else None
   | _ => None
   end.
 

arm/CombineOpproof.v

@@ -56,6 +56,9 @@ Proof.
   (* of cmp *)
   UseGetSound. rewrite <- H.
   destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -69,6 +72,9 @@ Proof.
   UseGetSound. rewrite <- H.
   rewrite eval_negate_condition.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_1_sound:

powerpc/CombineOp.v

@@ -27,13 +27,17 @@ Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (c, ys)
   | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys)
+  | Some(Op (Oxorimm n) ys) =>
+      if Int.eq n (Int.sign_ext 16 n) then Some (Ccompimm Cne n, ys) else None
   | _ => None
   end.
 
 Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
   | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys)
+  | Some(Op (Oxorimm n) ys) =>
+      if Int.eq n (Int.sign_ext 16 n) then Some (Ccompimm Ceq n, ys) else None
   | _ => None
   end.
 

powerpc/CombineOpproof.v

@@ -59,6 +59,9 @@ Proof.
   (* of and *)
   UseGetSound. rewrite <- H.
   destruct v; simpl; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -74,6 +77,9 @@ Proof.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
   (* of and *)
   UseGetSound. rewrite <- H. destruct v; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_1_sound:

x86/CombineOp.v

@@ -27,13 +27,15 @@ Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (c, ys)
   | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys)
+  | Some(Op (Oxorimm n) ys) => Some (Ccompimm Cne n, ys)
   | _ => None
   end.
 
 Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
   match get x with
   | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
   | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys)
+  | Some(Op (Oxorimm n) ys) => Some (Ccompimm Ceq n, ys)
   | _ => None
   end.
 

x86/CombineOpproof.v

@@ -53,6 +53,9 @@ Proof.
   (* of and *)
   UseGetSound. rewrite <- H.
   destruct v; simpl; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -68,6 +71,9 @@ Proof.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
   (* of and *)
   UseGetSound. rewrite <- H. destruct v; auto.
+  (* of xorimm *)
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto. rewrite Int.xor_is_zero; auto.
 Qed.
 
 Lemma combine_compimm_eq_1_sound: