From 1031c65ac836d53b01a1ec150481f2f70b1af5a7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 18 Aug 2024 18:01:44 +0200 Subject: [PATCH] CombineOp: optimize `(x ^ n) != 0` into `x != n` Likewise for `(x ^ n) == 0` that becomes `x == n`. --- aarch64/CombineOp.v | 2 ++ aarch64/CombineOpproof.v | 6 ++++++ arm/CombineOp.v | 2 ++ arm/CombineOpproof.v | 6 ++++++ powerpc/CombineOp.v | 2 ++ powerpc/CombineOpproof.v | 6 ++++++ riscV/CombineOp.v | 2 ++ riscV/CombineOpproof.v | 6 ++++++ test | 2 +- x86/CombineOp.v | 2 ++ x86/CombineOpproof.v | 6 ++++++ 11 files changed, 41 insertions(+), 1 deletion(-) diff --git a/aarch64/CombineOp.v b/aarch64/CombineOp.v index 333f656d27..88dacbfae9 100644 --- a/aarch64/CombineOp.v +++ b/aarch64/CombineOp.v @@ -25,12 +25,14 @@ 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) => 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 (Oxorimm n) ys) => Some (Ccompimm Ceq n, ys) | _ => 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..80be30d33c 100644 --- a/arm/CombineOp.v +++ b/arm/CombineOp.v @@ -26,12 +26,14 @@ 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) => 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 (Oxorimm n) ys) => Some (Ccompimm Ceq n, ys) | _ => 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..7dc23aa57c 100644 --- a/powerpc/CombineOp.v +++ b/powerpc/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/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/riscV/CombineOp.v b/riscV/CombineOp.v index 589b86753b..07406aa111 100644 --- a/riscV/CombineOp.v +++ b/riscV/CombineOp.v @@ -26,12 +26,14 @@ 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) => 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 (Oxorimm n) ys) => Some (Ccompimm Ceq n, ys) | _ => None end. diff --git a/riscV/CombineOpproof.v b/riscV/CombineOpproof.v index 81226a8201..bd39f595bb 100644 --- a/riscV/CombineOpproof.v +++ b/riscV/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/test b/test index 34ba42654d..0dedd895f6 160000 --- a/test +++ b/test @@ -1 +1 @@ -Subproject commit 34ba42654dd841f043698b1ee0e9e1700beb33e9 +Subproject commit 0dedd895f6379b5ed12a65c9db492f93e8a60636 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: