Skip to content

Commit

Permalink
CombineOp: optimize (x ^ n) != 0 into x != n
Browse files Browse the repository at this point in the history 
Likewise for `(x ^ n) == 0` that becomes `x == n`.
  • Loading branch information
@xavierleroy
xavierleroy committed Aug 19, 2024
1 parent 406ae8b commit 1031c65
Show file tree
Hide file tree
Showing 11 changed files with 41 additions and 1 deletion.
2 changes: 2 additions & 0 deletions aarch64/CombineOp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 6 additions & 0 deletions aarch64/CombineOpproof.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand Down
2 changes: 2 additions & 0 deletions arm/CombineOp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 6 additions & 0 deletions arm/CombineOpproof.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand Down
2 changes: 2 additions & 0 deletions powerpc/CombineOp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 6 additions & 0 deletions powerpc/CombineOpproof.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand Down
2 changes: 2 additions & 0 deletions riscV/CombineOp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 6 additions & 0 deletions riscV/CombineOpproof.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion test
Submodule test updated 6 files
+3 −0 Makefile
+2 −1 abi/Makefile
+5 −0 compression/Makefile
+1 −1 export/Makefile
+5 −0 raytracer/Makefile
+5 −0 spass/Makefile
2 changes: 2 additions & 0 deletions x86/CombineOp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 6 additions & 0 deletions x86/CombineOpproof.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand Down

0 comments on commit 1031c65

Please sign in to comment.