From bd3813f3f648994c689b416871e9aa0fe6d1be08 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 26 Aug 2024 16:18:29 +0200 Subject: [PATCH] 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 | 4 ++++ aarch64/CombineOpproof.v | 6 ++++++ arm/CombineOp.v | 4 ++++ arm/CombineOpproof.v | 6 ++++++ powerpc/CombineOp.v | 4 ++++ powerpc/CombineOpproof.v | 6 ++++++ x86/CombineOp.v | 2 ++ x86/CombineOpproof.v | 6 ++++++ 8 files changed, 38 insertions(+) diff --git a/aarch64/CombineOp.v b/aarch64/CombineOp.v index 333f656d27..53a0166624 100644 --- a/aarch64/CombineOp.v +++ b/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. diff --git a/aarch64/CombineOpproof.v b/aarch64/CombineOpproof.v index 4c4d27ede8..57778a67ef 100644 --- a/aarch64/CombineOpproof.v +++ b/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: diff --git a/arm/CombineOp.v b/arm/CombineOp.v index 49c5bc1174..76c09583a2 100644 --- a/arm/CombineOp.v +++ b/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. diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v index 3aee745a83..c8b332081e 100644 --- a/arm/CombineOpproof.v +++ b/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: diff --git a/powerpc/CombineOp.v b/powerpc/CombineOp.v index 268ce7d5a3..4ee1757c26 100644 --- a/powerpc/CombineOp.v +++ b/powerpc/CombineOp.v @@ -27,6 +27,8 @@ 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. @@ -34,6 +36,8 @@ 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. diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v index 29f74e5175..68eb42e711 100644 --- a/powerpc/CombineOpproof.v +++ b/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: diff --git a/x86/CombineOp.v b/x86/CombineOp.v index 907a49e178..2faf278c7b 100644 --- a/x86/CombineOp.v +++ b/x86/CombineOp.v @@ -27,6 +27,7 @@ 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. @@ -34,6 +35,7 @@ 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. diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v index e1d2e65046..1712538eb1 100644 --- a/x86/CombineOpproof.v +++ b/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: