bitwright 1;
// The built-in local rules. Every rule is checked by `bitwright::check` (exhaustively at small
// widths, sampled up to 512 bits) and recorded in `core.bwr.proof`. Algebra that a normal form
// decides (linear forms, truth tables, comparison lattices) belongs in a pass, not here.
group core.bitwise {
/// Absorption.
#[example("(q | p) & p" => "p")]
rule and_absorb_or<W>(x: W, y: W) { x & (x | y) => x }
/// Absorption.
#[example("(q & p) | p" => "p")]
rule or_absorb_and<W>(x: W, y: W) { x | (x & y) => x }
/// Complement.
#[example("p & ~p" => "0:8")]
rule and_not_self<W>(x: W) { x & ~x => 0 }
/// Complement.
#[example("p | ~p" => "255:8")]
rule or_not_self<W>(x: W) { x | ~x => ones }
/// Complement.
#[example("p ^ ~p" => "255:8")]
rule xor_not_self<W>(x: W) { x ^ ~x => ones }
/// The and and the or of two values differ exactly in their xor.
#[example("(p & q) ^ (p | q)" => "p ^ q")]
rule xor_and_or<W>(x: W, y: W) { (x & y) ^ (x | y) => x ^ y }
/// A mask that keeps every bit the value may have set.
#[example("(q & 15) & 0x3f" => "q & 15")]
rule and_mask_redundant<W>(x: W, c: const W) { x & c => x if zero_bits(x, ~c) }
/// A mask that keeps none of the bits the value may have set.
#[example("(q & 0xf0) & 15" => "0:8")]
rule and_mask_disjoint<W>(x: W, c: const W) { x & c => 0 if zero_bits(x, c) }
/// Clearing bits the value does not have.
#[example("~(p & 15) & (q << 4)" => "q << 4")]
rule and_not_disjoint<W>(x: W, y: W) { ~x & y => y if disjoint(x, y) }
/// Setting bits that are already set.
#[example("(q | 0x81) | 1" => "q | 0x81")]
rule or_known_ones<W>(x: W, c: const W) { x | c => x if one_bits(x, c) }
}
group core.arith {
/// And plus or is plus.
#[example("(p & q) + (p | q)" => "p + q")]
identity add_and_or<W>(x: W, y: W) { (x & y) + (x | y) <=> x + y }
/// Xor plus twice the and is plus. (Twice is written as the shift `mul_pow2` makes of it:
/// patterns are written in normal form, or bottom-up rewriting never reaches them.)
#[example("(p ^ q) + ((p & q) << 1)" => "p + q")]
identity add_xor_and<W>(x: W, y: W) { (x ^ y) + ((x & y) << 1) <=> x + y }
/// Xor plus and is or (the two parts share no bits).
#[example("(p ^ q) + (p & q)" => "p | q")]
rule or_from_xor_and<W>(x: W, y: W) { (x ^ y) + (x & y) => x | y }
/// Removing the common bits.
#[example("p - (p & q)" => "p & ~q")]
rule sub_and<W>(x: W, y: W) { x - (x & y) => x & ~y }
/// `-~x = x + 1`.
#[example("-(~p)" => "p + 1")]
rule neg_not<W>(x: W) { -(~x) => x + 1 }
/// `~-x = x - 1`.
#[example("~(-p)" => "p - 1")]
rule not_neg<W>(x: W) { ~(-x) => x - 1 }
/// `-(x + 1) = ~x`, with the increment spelled as an or.
#[example("-((p << 1) | 1)" => "~(p << 1)")]
rule neg_or_one<W>(x: W) { -(x | 1) => ~x if zero_bits(x, 1) }
/// An add without carries is an or.
#[example("(p & 0xf0) + (q & 15)" => "(p & 0xf0) | (q & 15)")]
rule add_disjoint<W>(x: W, y: W) { x + y => x | y if disjoint(x, y) }
/// Multiplying by a power of two is a shift.
#[example("p * 8" => "p << 3")]
rule mul_pow2<W>(x: W, c: const W) { x * c => x << k if is_pow2(c) let k: W = ctz(c) }
/// Unsigned division by a power of two is a shift.
#[example("udiv(p, 16)" => "p >>u 4")]
rule udiv_pow2<W>(x: W, c: const W) { udiv(x, c) => x >>u k if is_pow2(c) let k: W = ctz(c) }
/// Unsigned remainder by a power of two is a mask.
#[example("urem(p, 16)" => "p & 15")]
rule urem_pow2<W>(x: W, c: const W) { urem(x, c) => x & m if is_pow2(c) let m: W = c - 1 }
}
group core.compare {
/// A zero difference is equality.
#[example("p - q == 0" => "p == q")]
rule eq_sub_zero<W>(a: W, b: W) { (a - b) == 0 => a == b }
/// A zero xor is equality.
#[example("(p ^ q) == 0" => "p == q")]
rule eq_xor_zero<W>(a: W, b: W) { (a ^ b) == 0 => a == b }
/// A nonzero xor is inequality.
#[example("(p ^ q) != 0" => "p != q")]
rule ne_xor_zero<W>(a: W, b: W) { (a ^ b) != 0 => a != b }
/// Complementing reverses the order (signed less-than).
#[example("~p <s ~q" => "q <s p")]
rule slt_not_not<W>(x: W, y: W) { ~x <s ~y => y <s x }
/// Complementing reverses the order against a constant (signed less-than).
#[example("5 <s ~p" => "p <s 250")]
rule slt_const_not<W>(x: W, c: const W) { c <s ~x => x <s k let k: W = ~c }
/// Complementing reverses the order against a constant (signed less-than).
#[example("~p <s 5" => "250 <s p")]
rule slt_not_const<W>(x: W, c: const W) { ~x <s c => k <s x if c != 0 let k: W = ~c }
/// The complement is negative when the value is not (spelled as the compares pass does).
#[example("~p <s 0" => "0 <=s p")]
rule slt_not_zero<W>(x: W) { ~x <s 0 => 0 <=s x }
/// Complementing reverses the order (signed less-or-equal).
#[example("~p <=s ~q" => "q <=s p")]
rule sle_not_not<W>(x: W, y: W) { ~x <=s ~y => y <=s x }
/// Complementing reverses the order against a constant (signed less-or-equal).
#[example("5 <=s ~p" => "p <=s 250")]
rule sle_const_not<W>(x: W, c: const W) { c <=s ~x => x <=s k let k: W = ~c }
/// Complementing reverses the order against a constant (signed less-or-equal).
#[example("~p <=s 5" => "250 <=s p")]
rule sle_not_const<W>(x: W, c: const W) { ~x <=s c => k <=s x let k: W = ~c }
/// Complementing reverses the order (unsigned less-than).
#[example("~p <u ~q" => "q <u p")]
rule ult_not_not<W>(x: W, y: W) { ~x <u ~y => y <u x }
/// Complementing reverses the order against a constant (unsigned less-than).
#[example("5 <u ~p" => "p <u 250")]
rule ult_const_not<W>(x: W, c: const W) { c <u ~x => x <u k let k: W = ~c }
/// Complementing reverses the order against a constant (unsigned less-than).
#[example("~p <u 5" => "250 <u p")]
rule ult_not_const<W>(x: W, c: const W) { ~x <u c => k <u x let k: W = ~c }
/// Complementing reverses the order (unsigned less-or-equal).
#[example("~p <=u ~q" => "q <=u p")]
rule ule_not_not<W>(x: W, y: W) { ~x <=u ~y => y <=u x }
/// Complementing reverses the order against a constant (unsigned less-or-equal).
#[example("5 <=u ~p" => "p <=u 250")]
rule ule_const_not<W>(x: W, c: const W) { c <=u ~x => x <=u k let k: W = ~c }
/// Complementing reverses the order against a constant (unsigned less-or-equal).
#[example("~p <=u 5" => "250 <=u p")]
rule ule_not_const<W>(x: W, c: const W) { ~x <=u c => k <=u x let k: W = ~c }
/// Bits set in both operands, outside their masks, do not decide the order (signed less-than).
#[example("((p & 0xfc) | 1) <s ((q & 0xfc) | 1)" => "(p & 0xfc) <s (q & 0xfc)")]
rule slt_or_common<W>(x: W, y: W, m: const W, c: const W) {
((x & m) | c) <s ((y & m) | c) => (x & m) <s (y & m) if (m & c) == 0
}
/// Bits set in both operands, outside their masks, do not decide the order (signed less-or-equal).
#[example("((p & 0xfc) | 1) <=s ((q & 0xfc) | 1)" => "(p & 0xfc) <=s (q & 0xfc)")]
rule sle_or_common<W>(x: W, y: W, m: const W, c: const W) {
((x & m) | c) <=s ((y & m) | c) => (x & m) <=s (y & m) if (m & c) == 0
}
/// Bits set in both operands, outside their masks, do not decide the order (unsigned less-than).
#[example("((p & 0xfc) | 1) <u ((q & 0xfc) | 1)" => "(p & 0xfc) <u (q & 0xfc)")]
rule ult_or_common<W>(x: W, y: W, m: const W, c: const W) {
((x & m) | c) <u ((y & m) | c) => (x & m) <u (y & m) if (m & c) == 0
}
/// Bits set in both operands, outside their masks, do not decide the order (unsigned less-or-equal).
#[example("((p & 0xfc) | 1) <=u ((q & 0xfc) | 1)" => "(p & 0xfc) <=u (q & 0xfc)")]
rule ule_or_common<W>(x: W, y: W, m: const W, c: const W) {
((x & m) | c) <=u ((y & m) | c) => (x & m) <=u (y & m) if (m & c) == 0
}
/// Low bits set outside the mask do not change the sign.
#[example("((p & 0xfc) | 1) <s 0" => "(p & 0xfc) <s 0")]
rule slt_zero_or_low<W>(x: W, m: const W, c: const W) {
((x & m) | c) <s 0 => (x & m) <s 0 if (m & c) == 0 && (c & smin_lit) == 0
}
/// Low bits set outside the mask do not change the sign, and make the value nonzero.
#[example("((p & 0xfc) | 1) <=s 0" => "(p & 0xfc) <s 0")]
rule sle_zero_or_low<W>(x: W, m: const W, c: const W) {
((x & m) | c) <=s 0 => (x & m) <s 0 if (m & c) == 0 && (c & smin_lit) == 0 && c != 0
}
/// Low bits set outside the mask do not change the sign, and make the value nonzero.
#[example("0 <s ((p & 0xfc) | 1)" => "0 <=s (p & 0xfc)")]
rule zero_slt_or_low<W>(x: W, m: const W, c: const W) {
0 <s ((x & m) | c) => 0 <=s (x & m) if (m & c) == 0 && (c & smin_lit) == 0 && c != 0
}
/// Low bits set outside the mask do not change the sign.
#[example("0 <=s ((p & 0xfc) | 1)" => "0 <=s (p & 0xfc)")]
rule zero_sle_or_low<W>(x: W, m: const W, c: const W) {
0 <=s ((x & m) | c) => 0 <=s (x & m) if (m & c) == 0 && (c & smin_lit) == 0
}
/// Below one is zero.
#[example("p <u 1" => "p == 0")]
rule ult_one<W>(x: W) { x <u 1 => x == 0 }
/// A value cannot equal two provably different values.
#[example("(p == 1) & (p == 2)" => "0:1")]
rule eq_eq_distinct<W>(a: W, b: W, c: W) { (a == b) & (a == c) => false if proves(b != c) }
/// Unsigned comparison of zero-extended values is the narrow comparison.
#[example("zext<16>(p) <u zext<16>(q)" => "p <u q")]
rule ult_zext<W, U>(a: W, b: W) where W < U { zext<U>(a) <u zext<U>(b) => a <u b }
/// Signed comparison of sign-extended values is the narrow comparison.
#[example("sext<16>(p) <s sext<16>(q)" => "p <s q")]
rule slt_sext<W, U>(a: W, b: W) where W < U { sext<U>(a) <s sext<U>(b) => a <s b }
/// Equality of extended values is equality.
#[example("zext<16>(p) == zext<16>(q)" => "p == q")]
rule eq_zext<W, U>(a: W, b: W) where W < U { zext<U>(a) == zext<U>(b) => a == b }
}
group core.sign {
// Sign bits, spelled as a lifter spells them, and the conditions of a signed comparison
// computed from a subtraction's flags: SF is the sign of `a - b`, OF the sign of
// `(a - b ^ a) & (a ^ b)`, and `a <s b` is SF != OF.
/// Two signs differ when their xor is negative.
#[example("(p <s 0) != (q <s 0)" => "(p ^ q) <s 0")]
rule ne_signs<W>(x: W, y: W) { (x <s 0) != (y <s 0) => (x ^ y) <s 0 }
/// Two signs differ when their xor is negative.
#[example("(p <s 0) ^ (q <s 0)" => "(p ^ q) <s 0")]
rule xor_signs<W>(x: W, y: W) { (x <s 0) ^ (y <s 0) => (x ^ y) <s 0 }
/// Two signs agree when their xor is not negative.
#[example("(p <s 0) == (q <s 0)" => "0 <=s (p ^ q)")]
rule eq_signs<W>(x: W, y: W) { (x <s 0) == (y <s 0) => 0 <=s (x ^ y) }
/// Both are negative when their and is.
#[example("(p <s 0) & (q <s 0)" => "(p & q) <s 0")]
rule and_signs<W>(x: W, y: W) { (x <s 0) & (y <s 0) => (x & y) <s 0 }
/// Either is negative when their or is.
#[example("(p <s 0) | (q <s 0)" => "(p | q) <s 0")]
rule or_signs<W>(x: W, y: W) { (x <s 0) | (y <s 0) => (x | y) <s 0 }
/// The sign bit shifted down is one when the value is negative.
#[example("p >>u 7 == 1" => "p <s 0")]
rule lshr_sign_eq_one<W>(x: W) where 1 < W { x >>u (W - 1) == 1 => x <s 0 }
/// The sign bit shifted down is nonzero when the value is negative.
#[example("p >>u 7 != 0" => "p <s 0")]
rule lshr_sign_ne_zero<W>(x: W) { x >>u (W - 1) != 0 => x <s 0 }
/// The xor of two sign bits shifted down is the sign bit of the xor.
#[example("(p >>u 7) ^ (q >>u 7)" => "(p ^ q) >>u 7")]
rule xor_lshr_signs<W>(x: W, y: W) {
(x >>u (W - 1)) ^ (y >>u (W - 1)) => (x ^ y) >>u (W - 1)
}
/// Two sign bits differ when the xor's sign bit is set.
#[example("extract<7, 1>(p) != extract<7, 1>(q)" => "extract<7, 1>(p ^ q)")]
rule ne_sign_bits<W>(x: W, y: W) {
extract<W - 1, 1>(x) != extract<W - 1, 1>(y) => extract<W - 1, 1>(x ^ y)
}
/// The xor of two sign bits is the sign bit of the xor.
#[example("extract<7, 1>(p) ^ extract<7, 1>(q)" => "extract<7, 1>(p ^ q)")]
rule xor_sign_bits<W>(x: W, y: W) {
extract<W - 1, 1>(x) ^ extract<W - 1, 1>(y) => extract<W - 1, 1>(x ^ y)
}
/// SF != OF after `a - b` (x86 `setl`, AArch64 `lt`) is signed less-than.
#[example("(p - q ^ ((p - q ^ p) & (p ^ q))) <s 0" => "p <s q")]
rule slt_from_flags<W>(a: W, b: W) {
((a - b) ^ (((a - b) ^ a) & (a ^ b))) <s 0 => a <s b
}
/// SF == OF after `a - b` (x86 `setge`, AArch64 `ge`) is signed greater-or-equal.
#[example("0 <=s (p - q ^ ((p - q ^ p) & (p ^ q)))" => "q <=s p")]
rule sge_from_flags<W>(a: W, b: W) {
0 <=s ((a - b) ^ (((a - b) ^ a) & (a ^ b))) => b <=s a
}
/// SF != OF after `a - k` for a constant `k` (whose subtraction is built as `a + -k`).
#[example("(p + 0xfb ^ ((p + 0xfb ^ p) & (p ^ 5))) <s 0" => "p <s 5")]
rule slt_from_flags_const<W>(a: W, c: const W, k: const W) {
((a + c) ^ (((a + c) ^ a) & (a ^ k))) <s 0 => a <s k
if c + k == 0
}
/// SF == OF after `a - k` for a constant `k`.
#[example("0 <=s (p + 0xfb ^ ((p + 0xfb ^ p) & (p ^ 5)))" => "5 <=s p")]
rule sge_from_flags_const<W>(a: W, c: const W, k: const W) {
0 <=s ((a + c) ^ (((a + c) ^ a) & (a ^ k))) => k <=s a
if c + k == 0
}
/// SF != OF as a 0 or 1 word.
#[example("(p - q ^ ((p - q ^ p) & (p ^ q))) >>u 7" => "zext<8>(p <s q)")]
rule slt_from_flags_word<W>(a: W, b: W) where 1 < W {
((a - b) ^ (((a - b) ^ a) & (a ^ b))) >>u (W - 1) => zext<W>(a <s b)
}
/// SF != OF as a bit.
#[example("extract<7, 1>(p - q ^ ((p - q ^ p) & (p ^ q)))" => "p <s q")]
rule slt_from_flag_bits<W>(a: W, b: W) {
extract<W - 1, 1>((a - b) ^ (((a - b) ^ a) & (a ^ b))) => a <s b
}
/// SF == OF as bits.
#[example("extract<7, 1>(p - q) == extract<7, 1>((p - q ^ p) & (p ^ q))" => "q <=s p")]
rule sge_from_flag_bits<W>(a: W, b: W) {
extract<W - 1, 1>(a - b) == extract<W - 1, 1>(((a - b) ^ a) & (a ^ b)) => b <=s a
}
}
group core.casts {
/// Truncate, then zero-extend back: a mask.
#[example("zext<8>(trunc<4>(p))" => "p & 15")]
rule zext_trunc<W, N>(x: W) where N < W { zext<W>(trunc<N>(x)) => x & lowmask(N) }
/// Sign extension spelled as "value | (sign word << W)". Needs `U <= 2W` to be exact.
#[example("zext<16>(p) | (zext<16>(p >>s 7) << 8)" => "sext<16>(p)")]
rule sext_from_sign_word<W, U>(a: W) where W < U, U <= 2 * W {
zext<U>(a) | (zext<U>(a >>s (W - 1)) << W) => sext<U>(a)
}
}
group core.select {
/// A condition selecting one or zero is its zero extension.
#[example("select(p <u q, 1:16, 0:16)" => "zext<16>(p <u q)")]
rule select_one_zero<W>(c: 1) where 1 < W { select(c, 1, 0) => zext<W>(c) }
/// A condition selecting all ones or zero is its sign extension.
#[example("select(p <u q, 0xffff:16, 0:16)" => "sext<16>(p <u q)")]
rule select_ones_zero<W>(c: 1) where 1 < W { select(c, ones, 0) => sext<W>(c) }
}
group core.shift {
/// Two left shifts by constants that do not overflow the width.
#[example("(p << 2) << 3" => "p << 5")]
rule shl_shl<W>(x: W, a: const W, b: const W) {
(x << a) << b => x << k
if (a <u W) && (b <u W) && (a + b <u W)
let k: W = a + b
}
/// Two logical right shifts by constants that do not overflow the width.
#[example("(p >>u 2) >>u 3" => "p >>u 5")]
rule lshr_lshr<W>(x: W, a: const W, b: const W) {
(x >>u a) >>u b => x >>u k
if (a <u W) && (b <u W) && (a + b <u W)
let k: W = a + b
}
/// Shifting right then left by the same amount clears the low bits.
#[example("(p >>u 3) << 3" => "p & 0xf8")]
rule lshr_shl<W>(x: W, c: const W) {
(x >>u c) << c => x & m
if c <u W
let m: W = ones << c
}
/// Two rotations by constants.
#[example("rotl(rotl(p, 3), 7)" => "rotl(p, 2)")]
rule rotl_rotl<W>(x: W, a: const W, b: const W) {
rotl(rotl(x, a), b) => rotl(x, k)
let k: W = urem(urem(a, W) + urem(b, W), W)
}
/// Rotating back by the same count, whatever it is.
#[example("rotl(rotr(p, q), q)" => "p")]
rule rotl_rotr<W>(x: W, y: W) { rotl(rotr(x, y), y) => x }
/// Rotating back by the same count, whatever it is.
#[example("rotr(rotl(p, q), q)" => "p")]
rule rotr_rotl<W>(x: W, y: W) { rotr(rotl(x, y), y) => x }
}
// Valeria corpus gaps measured against 0.4.1's standard strategy. These are
// mathematical bit-vector identities; ISA-masked shifts remain a host concern.
group core.recovery_arith {
// universal r0037/r0054-r0057/r0287-r0290.
#[example("(p | q) - (p & q)" => "p ^ q")]
rule xor_from_or_minus_and<W>(x: W, y: W) { (x | y) - (x & y) => x ^ y }
#[example("(p + q) - ((p & q) << 1)" => "p ^ q")]
rule xor_from_sum_double_and<W>(x: W, y: W) { (x + y) - ((x & y) << 1) => x ^ y }
#[example("(p + q) - (p & q)" => "p | q")]
rule or_from_sum_minus_and<W>(x: W, y: W) { (x + y) - (x & y) => x | y }
#[example("(p + q) - (p | q)" => "p & q")]
rule and_from_sum_minus_or<W>(x: W, y: W) { (x + y) - (x | y) => x & y }
#[example("(p | q) - (p ^ q)" => "p & q")]
rule and_from_or_minus_xor<W>(x: W, y: W) { (x | y) - (x ^ y) => x & y }
#[example("((p | q) << 1) - (p + q)" => "p ^ q")]
rule xor_from_double_or_sum<W>(x: W, y: W) { ((x | y) << 1) - (x + y) => x ^ y }
#[example("((p | q) << 1) - (p ^ q)" => "p + q")]
rule sum_from_double_or_xor<W>(x: W, y: W) { ((x | y) << 1) - (x ^ y) => x + y }
// join r0108-r0109/r0111; universal r0041/r0045-r0046.
#[example("-p - p" => "p * 254")]
rule negative_double<W>(x: W) { -x - x => x * k let k: W = ones - 1 }
}
group core.recovery_compare {
// universal r0137-r0144; boolean-simplifiers r0000-r0005/r0016-r0017.
#[example("p == ~p" => "0:1")]
rule eq_complement<W>(x: W) { x == ~x => false }
#[example("p != ~p" => "1:1")]
rule ne_complement<W>(x: W) { x != ~x => true }
#[example("(p + q) <=u q" => "-p <=u q")]
rule ule_add_carry<W>(x: W, y: W) { (x + y) <=u y => -x <=u y }
#[example("q <u (p + q)" => "q <u -p")]
rule ugt_add_no_carry<W>(x: W, y: W) { y <u (x + y) => y <u -x }
#[example("q <=u (p + q)" => "q <=u ~p")]
rule uge_add_no_carry<W>(x: W, y: W) { y <=u (x + y) => y <=u ~x }
#[example("(p - q) <=u ~q" => "q <=u p")]
rule ule_sub_no_borrow<W>(x: W, y: W) { (x - y) <=u ~y => y <=u x }
#[example("~q <u (p - q)" => "p <u q")]
rule ugt_sub_borrow<W>(x: W, y: W) { ~y <u (x - y) => x <u y }
// universal r0185.
#[example("(p - q) != 0" => "p != q")]
rule ne_sub_zero<W>(x: W, y: W) { (x - y) != 0 => x != y }
}
group core.recovery_shift {
// join r0058-r0061; total shifts also cover c >= W.
#[example("(p << 1) >>u 1" => "p & 127")]
rule shl_lshr<W>(x: W, c: const W) { (x << c) >>u c => x & m let m: W = ones >>u c }
// universal r0086-r0091. Saturate before adding to avoid count overflow.
#[example("(p >>s 7) >>s 7" => "p >>s 7")]
rule ashr_ashr<W>(x: W, a: const W, b: const W) {
(x >>s a) >>s b => x >>s k
let k: W = umin(umin(a, W - 1) + umin(b, W - 1), W - 1)
}
// join r0043/r0057: discard constant bits shifted entirely out of the result.
#[example("(p ^ 128) << 7" => "p << 7")]
rule shl_xor_dead_constant<W>(x: W, c: const W, k: const W) {
(x ^ c) << k => x << k if (c << k) == 0
}
#[example("(p ^ 1) >>u 1" => "p >>u 1")]
rule lshr_xor_dead_constant<W>(x: W, c: const W, k: const W) {
(x ^ c) >>u k => x >>u k if (c >>u k) == 0
}
// universal r0181 and r0258-r0273 (width-preserving Boolean result).
#[example("-(p >>u 7)" => "p >>s 7")]
rule negate_sign_bit<W>(x: W) { -(x >>u (W - 1)) => x >>s (W - 1) }
#[example("(p | -p) >>u 7" => "zext<8>(p != 0)")]
rule nonzero_from_sign_union<W>(x: W) where 1 < W {
(x | -x) >>u (W - 1) => zext<W>(x != 0)
}
}
group core.recovery_bmi2 {
// universal r0172-r0174/r0274-r0281.
#[example("pdep(pext(p, q), q)" => "p & q")]
rule pdep_pext<W>(x: W, m: W) { pdep(pext(x, m), m) => x & m }
#[example("pext(pdep(p, 0x55), 0x55)" => "p & 15")]
rule pext_pdep<W>(x: W, m: const W) {
pext(pdep(x, m), m) => x & k let k: W = ones >>u (W - popcnt(m))
}
#[example("pdep(255, p)" => "p")]
rule pdep_ones<W>(m: W) { pdep(ones, m) => m }
#[example("pext(~p, p)" => "0:8")]
rule pext_complement_mask<W>(m: W) { pext(~m, m) => 0 }
#[example("pdep(p, q) & ~q" => "0:8")]
rule pdep_outside_mask<W>(x: W, m: W) { pdep(x, m) & ~m => 0 }
#[example("pdep(p, q) & q" => "pdep(p, q)")]
rule pdep_inside_mask<W>(x: W, m: W) { pdep(x, m) & m => pdep(x, m) }
#[example("pdep(pext(p, r) & pext(q, r), r)" => "(p & q) & r")]
rule pdep_pext_and<W>(x: W, y: W, m: W) { pdep(pext(x, m) & pext(y, m), m) => (x & y) & m }
#[example("pdep(pext(p, r) | pext(q, r), r)" => "(p | q) & r")]
rule pdep_pext_or<W>(x: W, y: W, m: W) { pdep(pext(x, m) | pext(y, m), m) => (x | y) & m }
#[example("pdep(pext(p, r) ^ pext(q, r), r)" => "(p ^ q) & r")]
rule pdep_pext_xor<W>(x: W, y: W, m: W) { pdep(pext(x, m) ^ pext(y, m), m) => (x ^ y) & m }
}
group core.recovery_cast {
// universal r0195-r0203. Only low bits are observed; high carries are irrelevant.
#[example("trunc<4>(p) + trunc<4>(q)" => "trunc<4>(p + q)")]
rule add_trunc_pair<W, N>(x: W, y: W) where N < W {
trunc<N>(x) + trunc<N>(y) => trunc<N>(x + y)
}
#[example("trunc<4>(p) - trunc<4>(q)" => "trunc<4>(p - q)")]
rule sub_trunc_pair<W, N>(x: W, y: W) where N < W {
trunc<N>(x) - trunc<N>(y) => trunc<N>(x - y)
}
#[example("trunc<4>(p) * trunc<4>(q)" => "trunc<4>(p * q)")]
rule mul_trunc_pair<W, N>(x: W, y: W) where N < W {
trunc<N>(x) * trunc<N>(y) => trunc<N>(x * y)
}
}
group core.recovery_select {
// universal r0191 and display/pack r0003-r0010.
#[example("select(0 <u p, p, 0)" => "p")]
rule select_nonzero_self<W>(x: W) { select(0 <u x, x, 0) => x }
#[example("select(p == 0, q, 0) | select(p == 0, 0, r)" => "select(p == 0, q, r)")]
rule merge_complementary_select_or<W>(c: 1, x: W, y: W) {
select(c, x, 0) | select(c, 0, y) => select(c, x, y)
}
#[example("select(p == 0, q, 0) + select(p == 0, 0, r)" => "select(p == 0, q, r)")]
rule merge_complementary_select_add<W>(c: 1, x: W, y: W) {
select(c, x, 0) + select(c, 0, y) => select(c, x, y)
}
// With `x` one or all ones, `select(c, x, 0)` is already `zext(c)` or `sext(c)`.
#[example("zext<8>(p == 0) | select(p == 0, 0, r)" => "select(p == 0, 1:8, r)")]
rule merge_complementary_zext_or<W>(c: 1, y: W) where 1 < W {
zext<W>(c) | select(c, 0, y) => select(c, 1, y)
}
#[example("zext<8>(p == 0) + select(p == 0, 0, r)" => "select(p == 0, 1:8, r)")]
rule merge_complementary_zext_add<W>(c: 1, y: W) where 1 < W {
zext<W>(c) + select(c, 0, y) => select(c, 1, y)
}
#[example("sext<8>(p == 0) | select(p == 0, 0, r)" => "select(p == 0, 255:8, r)")]
rule merge_complementary_sext_or<W>(c: 1, y: W) where 1 < W {
sext<W>(c) | select(c, 0, y) => select(c, ones, y)
}
#[example("sext<8>(p == 0) + select(p == 0, 0, r)" => "select(p == 0, 255:8, r)")]
rule merge_complementary_sext_add<W>(c: 1, y: W) where 1 < W {
sext<W>(c) + select(c, 0, y) => select(c, ones, y)
}
}
group core.recovery_canonical {
// Forms exposed by constructor/normal-form rewrites of the measured ports.
#[example("(p ^ 128) + 128" => "p")]
rule xor_sign_bit_add<W>(x: W) { (x ^ bit(W - 1)) + bit(W - 1) => x }
#[example("p + 255 <=u 254" => "1 <=u p")]
rule ule_constant_borrow<W>(x: W, c: const W, m: const W) {
(x + c) <=u m => k <=u x if m == c - 1 let k: W = -c
}
#[example("254 <u p + 255" => "p <u 1")]
rule ugt_constant_borrow<W>(x: W, c: const W, m: const W) {
m <u (x + c) => x <u k if m == c - 1 let k: W = -c
}
#[example("pdep(pext(p, 1) ^ 1, 1)" => "(p ^ 1) & 1")]
rule pdep_pext_xor_constant<W>(x: W, c: const W, m: const W) {
pdep(pext(x, m) ^ c, m) => (x ^ k) & m let k: W = pdep(c, m)
}
}
group core.recovery_minmax {
#[example("select(p <=s q, p, 0) | select(q <s p, q, 0)" => "smin(p, q)")]
rule smin_select_or<W>(x: W, y: W) { select(x <=s y, x, 0) | select(y <s x, y, 0) => smin(x, y) }
#[example("select(p <=s q, p, 0) + select(q <s p, q, 0)" => "smin(p, q)")]
rule smin_select_add<W>(x: W, y: W) { select(x <=s y, x, 0) + select(y <s x, y, 0) => smin(x, y) }
#[example("select(q <=s p, p, 0) | select(p <s q, q, 0)" => "smax(p, q)")]
rule smax_select_or<W>(x: W, y: W) { select(y <=s x, x, 0) | select(x <s y, y, 0) => smax(x, y) }
#[example("select(q <=s p, p, 0) + select(p <s q, q, 0)" => "smax(p, q)")]
rule smax_select_add<W>(x: W, y: W) { select(y <=s x, x, 0) + select(x <s y, y, 0) => smax(x, y) }
#[example("select(p <=u q, p, 0) | select(q <u p, q, 0)" => "umin(p, q)")]
rule umin_select_or<W>(x: W, y: W) { select(x <=u y, x, 0) | select(y <u x, y, 0) => umin(x, y) }
#[example("select(p <=u q, p, 0) + select(q <u p, q, 0)" => "umin(p, q)")]
rule umin_select_add<W>(x: W, y: W) { select(x <=u y, x, 0) + select(y <u x, y, 0) => umin(x, y) }
#[example("select(q <=u p, p, 0) | select(p <u q, q, 0)" => "umax(p, q)")]
rule umax_select_or<W>(x: W, y: W) { select(y <=u x, x, 0) | select(x <u y, y, 0) => umax(x, y) }
#[example("select(q <=u p, p, 0) + select(p <u q, q, 0)" => "umax(p, q)")]
rule umax_select_add<W>(x: W, y: W) { select(y <=u x, x, 0) + select(x <u y, y, 0) => umax(x, y) }
// select(c, ones, 0) canonicalizes to sext(c) before its parent is visited.
#[example("sext<8>(p <u 255) | select(255 <=u p, p, 0)" => "255:8")]
rule umax_ones_sext_or<W>(x: W) where 1 < W {
sext<W>(x <u ones) | select(ones <=u x, x, 0) => ones
}
#[example("sext<8>(p <u 255) + select(255 <=u p, p, 0)" => "255:8")]
rule umax_ones_sext_add<W>(x: W) where 1 < W {
sext<W>(x <u ones) + select(ones <=u x, x, 0) => ones
}
}
group core.recovery_select_one {
#[example("zext<8>(1 <s p) | select(p <=s 1, p, 0)" => "smin(p, 1)")]
rule smin_one_or<W>(x: W) where 1 < W { zext<W>(1 <s x) | select(x <=s 1, x, 0) => smin(x, 1) }
#[example("zext<8>(1 <s p) + select(p <=s 1, p, 0)" => "smin(p, 1)")]
rule smin_one_add<W>(x: W) where 1 < W { zext<W>(1 <s x) + select(x <=s 1, x, 0) => smin(x, 1) }
#[example("zext<8>(p <s 1) | select(1 <=s p, p, 0)" => "smax(p, 1)")]
rule smax_one_or<W>(x: W) where 1 < W { zext<W>(x <s 1) | select(1 <=s x, x, 0) => smax(x, 1) }
#[example("zext<8>(p <s 1) + select(1 <=s p, p, 0)" => "smax(p, 1)")]
rule smax_one_add<W>(x: W) where 1 < W { zext<W>(x <s 1) + select(1 <=s x, x, 0) => smax(x, 1) }
#[example("zext<8>(1 <u p) | select(p <=u 1, p, 0)" => "umin(p, 1)")]
rule umin_one_or<W>(x: W) where 1 < W { zext<W>(1 <u x) | select(x <=u 1, x, 0) => umin(x, 1) }
#[example("zext<8>(1 <u p) + select(p <=u 1, p, 0)" => "umin(p, 1)")]
rule umin_one_add<W>(x: W) where 1 < W { zext<W>(1 <u x) + select(x <=u 1, x, 0) => umin(x, 1) }
#[example("zext<8>(p == 0) | select(1 <=u p, p, 0)" => "umax(p, 1)")]
rule umax_one_or<W>(x: W) where 1 < W { zext<W>(x == 0) | select(1 <=u x, x, 0) => umax(x, 1) }
#[example("zext<8>(p == 0) + select(1 <=u p, p, 0)" => "umax(p, 1)")]
rule umax_one_add<W>(x: W) where 1 < W { zext<W>(x == 0) + select(1 <=u x, x, 0) => umax(x, 1) }
// The same with the one first: ties select it rather than `x` (the same value).
#[example("zext<8>(1 <=s p) | select(p <s 1, p, 0)" => "smin(p, 1)")]
rule smin_one_first_or<W>(x: W) where 1 < W { zext<W>(1 <=s x) | select(x <s 1, x, 0) => smin(x, 1) }
#[example("zext<8>(1 <=s p) + select(p <s 1, p, 0)" => "smin(p, 1)")]
rule smin_one_first_add<W>(x: W) where 1 < W { zext<W>(1 <=s x) + select(x <s 1, x, 0) => smin(x, 1) }
#[example("zext<8>(p <=s 1) | select(1 <s p, p, 0)" => "smax(p, 1)")]
rule smax_one_first_or<W>(x: W) where 1 < W { zext<W>(x <=s 1) | select(1 <s x, x, 0) => smax(x, 1) }
#[example("zext<8>(p <=s 1) + select(1 <s p, p, 0)" => "smax(p, 1)")]
rule smax_one_first_add<W>(x: W) where 1 < W { zext<W>(x <=s 1) + select(1 <s x, x, 0) => smax(x, 1) }
#[example("zext<8>(p <=u 1) | select(1 <u p, p, 0)" => "select(1 <u p, p, 1)")]
rule umax_one_first_or<W>(x: W) where 1 < W { zext<W>(x <=u 1) | select(1 <u x, x, 0) => select(1 <u x, x, 1) }
#[example("zext<8>(p <=u 1) + select(1 <u p, p, 0)" => "select(1 <u p, p, 1)")]
rule umax_one_first_add<W>(x: W) where 1 < W { zext<W>(x <=u 1) + select(1 <u x, x, 0) => select(1 <u x, x, 1) }
}
group core.recovery_shuffle {
#[example("concat(trunc<1>(p), 0:7)" => "p << 7")]
rule concat_low_zero<N, U>(x: N + U, z: const U) where N + U <= 512 {
concat(trunc<N>(x), z) => x << U if z == 0
}
}
group core.recovery_select_ones {
#[example("sext<8>(255 <s p) | select(p <=s 255, p, 0)" => "smin(p, 255)")]
rule smin_ones_or<W>(x: W) where 1 < W { sext<W>(ones <s x) | select(x <=s ones, x, 0) => smin(x, ones) }
#[example("sext<8>(255 <s p) + select(p <=s 255, p, 0)" => "smin(p, 255)")]
rule smin_ones_add<W>(x: W) where 1 < W { sext<W>(ones <s x) + select(x <=s ones, x, 0) => smin(x, ones) }
#[example("sext<8>(p <s 255) | select(255 <=s p, p, 0)" => "smax(p, 255)")]
rule smax_ones_or<W>(x: W) where 1 < W { sext<W>(x <s ones) | select(ones <=s x, x, 0) => smax(x, ones) }
#[example("sext<8>(p <s 255) + select(255 <=s p, p, 0)" => "smax(p, 255)")]
rule smax_ones_add<W>(x: W) where 1 < W { sext<W>(x <s ones) + select(ones <=s x, x, 0) => smax(x, ones) }
// The same with all ones first: ties select it rather than `x` (the same value).
#[example("sext<8>(255 <=s p) | select(p <s 255, p, 0)" => "smin(p, 255)")]
rule smin_ones_first_or<W>(x: W) where 1 < W { sext<W>(ones <=s x) | select(x <s ones, x, 0) => smin(x, ones) }
#[example("sext<8>(255 <=s p) + select(p <s 255, p, 0)" => "smin(p, 255)")]
rule smin_ones_first_add<W>(x: W) where 1 < W { sext<W>(ones <=s x) + select(x <s ones, x, 0) => smin(x, ones) }
#[example("sext<8>(p <=s 255) | select(255 <s p, p, 0)" => "smax(p, 255)")]
rule smax_ones_first_or<W>(x: W) where 1 < W { sext<W>(x <=s ones) | select(ones <s x, x, 0) => smax(x, ones) }
#[example("sext<8>(p <=s 255) + select(255 <s p, p, 0)" => "smax(p, 255)")]
rule smax_ones_first_add<W>(x: W) where 1 < W { sext<W>(x <=s ones) + select(ones <s x, x, 0) => smax(x, ones) }
// `umin(x, ones)` is `x`, whichever of the two a tie selects.
#[example("select(p <u 255, p, 0) + sext<8>(255 <=u p)" => "p")]
rule umin_ones_first_add<W>(x: W) where 1 < W { select(x <u ones, x, 0) + sext<W>(ones <=u x) => x }
#[example("select(p <u 255, p, 0) | sext<8>(255 <=u p)" => "p")]
rule umin_ones_first_or<W>(x: W) where 1 < W { select(x <u ones, x, 0) | sext<W>(ones <=u x) => x }
}
// Remaining Valeria rules: guards are retained as facts, never erased.
group core.guarded_recovery {
#[example("-((p & 252) | 2) <s -((q & 252) | 2)" => "((q & 252) | 2) <s ((p & 252) | 2)")]
rule slt_neg_pair<W>(x: W, y: W) {
-x <s -y => y <s x if proves(x != bit(W - 1)) && proves(y != bit(W - 1))
}
#[example("-((p & 252) | 2) <=s -((q & 252) | 2)" => "((q & 252) | 2) <=s ((p & 252) | 2)")]
rule sle_neg_pair<W>(x: W, y: W) {
-x <=s -y => y <=s x if proves(x != bit(W - 1)) && proves(y != bit(W - 1))
}
#[example("select(p != 0, p, 0)" => "p")]
rule select_nonzero_value<W>(x: W) { select(x != 0, x, 0) => x }
#[example("-p:1" => "p:1")]
rule negate_boolean(x: 1) { -x => x }
#[example("p:1 + 1:1" => "~p:1")]
rule increment_boolean(x: 1) { x + 1 => ~x }
#[example("(p >>u 3) | (p << 5)" => "rotr(p, 3)")]
rule complementary_shift_rotate<W>(x: W, a: const W, b: const W) {
(x >>u a) | (x << b) => rotr(x, a)
if (a <u W) && (b <u W) && (a + b == W)
}
#[example("zext<16>(p) ^ 255:16" => "zext<16>(~p)")]
rule xor_zext_lowmask<W, U>(x: W) where W < U {
zext<U>(x) ^ lowmask(W) => zext<U>(~x)
}
#[example("(p & 254) ^ 1" => "p | 1")]
rule xor_complement_mask<W>(x: W, m: const W, n: const W) {
(x & n) ^ m => x | m if n == ~m
}
#[example("((p | 3) & 15) + 255" => "(p & 12) | 2")]
rule mask_or_add_constant<W>(x: W, c: const W, m: const W, d: const W) {
((x | c) & m) + d => (x & kept) | k
if (((c & m) + d) & (m & ~c)) == 0
let kept: W = m & ~c
let k: W = (c & m) + d
}
// The same when the constant carries into the kept bits: `(x | c) & m` is
// `(x & (m & ~c)) + (c & m)`, whose parts share no bits.
#[example("((p | 127) & 0xf0) + 16" => "(p & 128) + 128")]
rule mask_or_add_constant_carry<W>(x: W, c: const W, m: const W, d: const W) {
((x | c) & m) + d => (x & kept) + k
let kept: W = m & ~c
let k: W = (c & m) + d
}
#[example("-(p & 1) & q" => "select(trunc<1>(p), q, 0)")]
rule boolean_lowbit_mask_keep<W>(x: W, y: W) where 1 < W {
-(x & 1) & y => select(trunc<1>(x), y, 0)
}
#[example("-zext<8>(p:1) & q" => "select(p:1, q, 0)")]
rule boolean_zext_mask_keep<W>(x: 1, y: W) where 1 < W {
-zext<W>(x) & y => select(x, y, 0)
}
#[example("(p & 240) + ((p & 15) + q)" => "p + q")]
rule split_mask_add<W>(x: W, c: W, m: const W, n: const W) {
(x & m) + ((x & n) + c) => (x & k) + c if (m & n) == 0 let k: W = m | n
}
// A constant sharing no bit with `x & n` makes the inner add an or first (`add_disjoint`),
// and the outer one too when it is disjoint.
#[example("(p & 240) | ((p & 2) | 1)" => "(p & 242) | 1")]
rule split_mask_or_or<W>(x: W, c: W, m: const W, n: const W) {
(x & m) | ((x & n) | c) => (x & k) | c let k: W = m | n
}
#[example("(p & 240) + ((p & 15) - q)" => "p - q")]
rule split_mask_sub<W>(x: W, c: W, m: const W, n: const W) {
(x & m) + ((x & n) - c) => x - c if (m | n) == ones && (m & n) == 0
}
// The linear pass writes `a + b + 1` as `a - ~b`.
#[example("(p & 240) - ~(p & 15)" => "p + 1")]
rule split_mask_increment<W>(x: W, m: const W, n: const W) {
(x & m) - ~(x & n) => x + 1 if (m | n) == ones && (m & n) == 0
}
#[example("(p & 15) | (((p >>u 4) + q) << 4)" => "p + (q << 4)")]
rule recombine_shifted_field_or<W>(x: W, a: W, m: const W, k: const W) {
(x & m) | (((x >>u k) + a) << k) => (x & keep) + (a << k)
if (k <=u W) && (m & (ones << k)) == 0
let keep: W = (ones << k) | m
}
}
group core.guarded_recovery_canonical {
#[example("-((p & 252) | 2) <s 0" => "0 <s ((p & 252) | 2)")]
rule slt_neg_zero<W>(x: W) { -x <s 0 => 0 <s x if proves(x != bit(W - 1)) }
#[example("0 <s -((p & 252) | 2)" => "((p & 252) | 2) <s 0")]
rule slt_zero_neg<W>(x: W) { 0 <s -x => x <s 0 if proves(x != bit(W - 1)) }
#[example("-((p & 252) | 2) <=s 0" => "0 <=s ((p & 252) | 2)")]
rule sle_neg_zero<W>(x: W) { -x <=s 0 => 0 <=s x if proves(x != bit(W - 1)) }
#[example("0 <=s -((p & 252) | 2)" => "((p & 252) | 2) <=s 0")]
rule sle_zero_neg<W>(x: W) { 0 <=s -x => x <=s 0 if proves(x != bit(W - 1)) }
#[example("(p & 240) + ((p & 15) | 128)" => "p + 128")]
rule split_mask_or_add<W>(x: W, c: W, m: const W, n: const W) {
(x & m) + ((x & n) | c) => x + c
if (m | n) == ones && (m & n) == 0 && zero_bits(c, n)
}
}
group core.guarded_recovery_shuffle {
#[example("concat(trunc<4>(zext<8>(extract<4,3>(p)) + q), trunc<4>(p))" => "(p & 127) + (q << 4)")]
rule recombine_extracted_field<N, K, M>(x: N + K, a: N + K) where M <= N, N + K <= 512 {
concat(trunc<N>(zext<N + K>(extract<K, M>(x)) + a), trunc<K>(x))
=> (x & lowmask(K + M)) + (a << K)
}
// As an or (what `add_disjoint` makes of a disjoint add), at every value.
#[example("concat(trunc<4>(zext<8>(extract<4,3>(p)) | q), trunc<4>(p))" => "(p & 127) | (q << 4)")]
rule recombine_extracted_field_or<N, K, M>(x: N + K, a: N + K) where M <= N, N + K <= 512 {
concat(trunc<N>(zext<N + K>(extract<K, M>(x)) | a), trunc<K>(x))
=> (x & lowmask(K + M)) | (a << K)
}
}
group core.guarded_recovery_layout {
#[example("(((p >>u 4) & 8) + q) << 4" => "(p & 128) + (q << 4)")]
rule shifted_masked_add<W>(x: W, a: W, s: const W, k: const W) {
(((x >>u k) & s) + a) << k => (x & keep) + (a << k)
let keep: W = s << k
}
// With `s` keeping every bit of `x >>u k`, the mask is gone first (`and_mask_redundant`).
#[example("((p >>u 4) + 3) << 4" => "(p & 240) + 48")]
rule shifted_add_constant<W>(x: W, c: const W, k: const W) {
((x >>u k) + c) << k => (x & keep) + d
let keep: W = ones << k
let d: W = c << k
}
#[example("((p >>u 4) | 3) << 4" => "(p & 240) | 48")]
rule shifted_or_constant<W>(x: W, c: const W, k: const W) {
((x >>u k) | c) << k => (x & keep) | d
let keep: W = ones << k
let d: W = c << k
}
#[example("(((p >>u 4) + q) << 4) | 15" => "(p | 15) + (q << 4)")]
rule recombine_low_constant<W>(x: W, a: W, c: const W, k: const W) {
(((x >>u k) + a) << k) | c => (x | c) + (a << k)
if (k <=u W) && c == ones >>u (W - k)
}
#[example("(p & 14) | ((p & 240) + (q << 4))" => "(p & 254) + (q << 4)")]
rule split_or_masked_sum<W>(x: W, c: W, m: const W, n: const W) {
(x & m) | ((x & n) + c) => (x & keep) + c
if (n & prefix) == 0 && zero_bits(c, prefix)
let prefix: W = ones >>u clz(m)
let keep: W = m | n
}
#[example("concat(extract<7,1>(p), 112:7) + 16" => "(p & 128) + 128")]
rule add_constant_to_concat<H, L>(x: H + L, c: const L, d: const H + L) where H + L <= 512 {
concat(extract<L,H>(x), c) + d => (x & ~lowmask(L)) + k
let k: H + L = zext<H + L>(c) + d
}
#[example("concat(extract<7,1>(p), 112:7) | 3" => "(p & 128) | 115")]
rule or_constant_to_concat<H, L>(x: H + L, c: const L, d: const H + L) where H + L <= 512 {
concat(extract<L,H>(x), c) | d => (x & ~lowmask(L)) | k
let k: H + L = zext<H + L>(c) | d
}
}
group core.guarded_recovery_mba_normalized {
// `((x << 1) | (c << 1))`, as `or_shl_const` writes it: `c`'s top bit may differ from `a`'s.
#[example("((p | 1) << 1) - (p + 129)" => "p ^ 129")]
rule xor_from_distributed_double_or<W>(x: W, a: const W, c: const W) {
((x | a) << 1) - (x + c) => x ^ c if (a << 1) == (c << 1)
}
#[example("((p | 1) << 1) - (p ^ 129)" => "p + 129")]
rule sum_from_distributed_double_or<W>(x: W, a: const W, c: const W) {
((x | a) << 1) - (x ^ c) => x + c if (a << 1) == (c << 1)
}
#[example("(p << 1) - (p ^ 128)" => "p + 128")]
rule sum_from_vanishing_double_mask<W>(x: W, c: const W) {
(x << 1) - (x ^ c) => x + c if (c << 1) == 0
}
}
group core.guarded_recovery_concat {
#[example("(q << 4) + concat(extract<4,4>(p), 15:4)" => "concat(trunc<4>(q) + extract<4,4>(p), 15:4)")]
rule add_aligned_to_concat<H, L>(a: H + L, x: H + L, c: const L) where H + L <= 512 {
(a << L) + concat(extract<L,H>(x), c)
=> concat(trunc<H>(a) + extract<L,H>(x), c)
}
}
// A constant mask (or an or or xor) above a left shift moves below it: `(x << k) & m` and
// `(x & (m >>u k)) << k` are one value, and the second is `2^k` times a bitwise term, which the
// linear and MBA passes read (the linear pass writes `2·t` as `t + t`, so that spelling moves
// too). Only when the shift has no other user: else it stays, and the move would add a node.
// Patterns with a constant and a shift are written in this form; `check::preempted` finds the
// ones that are not.
group core.shift_canonical {
/// A mask that keeps every bit the shift keeps.
#[example("(p & 63) << 2" => "p << 2")]
rule shl_mask_dead<W>(x: W, c: const W, k: const W) {
(x & c) << k => x << k if (c | ~(ones >>u k)) == ones
}
#[example("(p << 2) & 60" => "(p & 15) << 2")]
rule and_shl_const<W>(x: W, k: const W, m: const W) {
(x << k) & m => (x & c) << k if one_use(x << k) let c: W = m >>u k
}
#[example("(p + p) & 30" => "(p & 15) << 1")]
rule and_double_const<W>(x: W, m: const W) {
(x + x) & m => (x & c) << 1 if one_use(x + x) let c: W = m >>u 1
}
/// An or or xor moves too when it sets no bit the shift clears.
#[example("(p << 2) | 12" => "(p | 3) << 2")]
rule or_shl_const<W>(x: W, k: const W, m: const W) {
(x << k) | m => (x | c) << k if (m & ~(ones << k)) == 0 && one_use(x << k) let c: W = m >>u k
}
#[example("(p << 2) ^ 12" => "(p ^ 3) << 2")]
rule xor_shl_const<W>(x: W, k: const W, m: const W) {
(x << k) ^ m => (x ^ c) << k if (m & ~(ones << k)) == 0 && one_use(x << k) let c: W = m >>u k
}
#[example("(p + p) | 6" => "(p | 3) << 1")]
rule or_double_const<W>(x: W, m: const W) {
(x + x) | m => (x | c) << 1 if (m & 1) == 0 && one_use(x + x) let c: W = m >>u 1
}
#[example("(p + p) ^ 6" => "(p ^ 3) << 1")]
rule xor_double_const<W>(x: W, m: const W) {
(x + x) ^ m => (x ^ c) << 1 if (m & 1) == 0 && one_use(x + x) let c: W = m >>u 1
}
}
// Floating point. Construction already applies what holds bit for bit on every encoding; these
// need a constant of a kind or the facts (an operand that is no NaN: a NaN operand gives the
// canonical NaN, and an identity on values would keep its payload).
group core.factor {
/// A left shift distributes over `&`, so the shift of the conjunction is one shift.
#[example("(p << 3) & (q << 3)" => "(p & q) << 3")]
rule shl_and<W>(x: W, y: W, s: W) { (x << s) & (y << s) => (x & y) << s }
/// Likewise over `|`.
#[example("(p << 3) | (q << 3)" => "(p | q) << 3")]
rule shl_or<W>(x: W, y: W, s: W) { (x << s) | (y << s) => (x | y) << s }
/// Likewise over `^`.
#[example("(p << 3) ^ (q << 3)" => "(p ^ q) << 3")]
rule shl_xor<W>(x: W, y: W, s: W) { (x << s) ^ (y << s) => (x ^ y) << s }
/// A left shift multiplies by a power of two (or by 0), which distributes over `+`.
#[example("(p << 3) + (q << 3)" => "(p + q) << 3")]
rule shl_add<W>(x: W, y: W, s: W) { (x << s) + (y << s) => (x + y) << s }
/// And over `-`.
#[example("(p << 3) - (q << 3)" => "(p - q) << 3")]
rule shl_sub<W>(x: W, y: W, s: W) { (x << s) - (y << s) => (x - y) << s }
/// A logical right shift moves every bit alike, so it distributes over `&`.
#[example("(p >>u 3) & (q >>u 3)" => "(p & q) >>u 3")]
rule lshr_and<W>(x: W, y: W, s: W) { (x >>u s) & (y >>u s) => (x & y) >>u s }
/// Likewise over `|`.
#[example("(p >>u 3) | (q >>u 3)" => "(p | q) >>u 3")]
rule lshr_or<W>(x: W, y: W, s: W) { (x >>u s) | (y >>u s) => (x | y) >>u s }
/// Likewise over `^`.
#[example("(p >>u 3) ^ (q >>u 3)" => "(p ^ q) >>u 3")]
rule lshr_xor<W>(x: W, y: W, s: W) { (x >>u s) ^ (y >>u s) => (x ^ y) >>u s }
/// An arithmetic right shift copies the sign bit, a bit like the others, so it distributes
/// over `&`.
#[example("(p >>s 3) & (q >>s 3)" => "(p & q) >>s 3")]
rule ashr_and<W>(x: W, y: W, s: W) { (x >>s s) & (y >>s s) => (x & y) >>s s }
/// Likewise over `|`.
#[example("(p >>s 3) | (q >>s 3)" => "(p | q) >>s 3")]
rule ashr_or<W>(x: W, y: W, s: W) { (x >>s s) | (y >>s s) => (x | y) >>s s }
/// Likewise over `^`.
#[example("(p >>s 3) ^ (q >>s 3)" => "(p ^ q) >>s 3")]
rule ashr_xor<W>(x: W, y: W, s: W) { (x >>s s) ^ (y >>s s) => (x ^ y) >>s s }
/// An arithmetic right shift commutes with complement.
#[example("~(~p >>s 3)" => "p >>s 3")]
rule not_ashr_not<W>(x: W, s: W) { ~(~x >>s s) => x >>s s }
/// A rotation moves every bit alike, so it distributes over `&`.
#[example("rotl(p, 3) & rotl(q, 3)" => "rotl(p & q, 3)")]
rule rotl_and<W>(x: W, y: W, s: W) { rotl(x, s) & rotl(y, s) => rotl(x & y, s) }
/// Likewise over `|`.
#[example("rotl(p, 3) | rotl(q, 3)" => "rotl(p | q, 3)")]
rule rotl_or<W>(x: W, y: W, s: W) { rotl(x, s) | rotl(y, s) => rotl(x | y, s) }
/// Likewise over `^`.
#[example("rotl(p, 3) ^ rotl(q, 3)" => "rotl(p ^ q, 3)")]
rule rotl_xor<W>(x: W, y: W, s: W) { rotl(x, s) ^ rotl(y, s) => rotl(x ^ y, s) }
/// A rotation commutes with complement.
#[example("~rotl(~p, 3)" => "rotl(p, 3)")]
rule not_rotl_not<W>(x: W, s: W) { ~rotl(~x, s) => rotl(x, s) }
/// Zero extension distributes over `&`.
#[example("zext<16>(p) & zext<16>(q)" => "zext<16>(p & q)")]
rule zext_and<W, U>(x: W, y: W) where W < U { zext<U>(x) & zext<U>(y) => zext<U>(x & y) }
/// Likewise over `|`.
#[example("zext<16>(p) | zext<16>(q)" => "zext<16>(p | q)")]
rule zext_or<W, U>(x: W, y: W) where W < U { zext<U>(x) | zext<U>(y) => zext<U>(x | y) }
/// Likewise over `^`.
#[example("zext<16>(p) ^ zext<16>(q)" => "zext<16>(p ^ q)")]
rule zext_xor<W, U>(x: W, y: W) where W < U { zext<U>(x) ^ zext<U>(y) => zext<U>(x ^ y) }
/// Sign extension copies the top bit, a bit like the others: it distributes over `&`.
#[example("sext<16>(p) & sext<16>(q)" => "sext<16>(p & q)")]
rule sext_and<W, U>(x: W, y: W) where W < U { sext<U>(x) & sext<U>(y) => sext<U>(x & y) }
/// Likewise over `|`.
#[example("sext<16>(p) | sext<16>(q)" => "sext<16>(p | q)")]
rule sext_or<W, U>(x: W, y: W) where W < U { sext<U>(x) | sext<U>(y) => sext<U>(x | y) }
/// Likewise over `^`.
#[example("sext<16>(p) ^ sext<16>(q)" => "sext<16>(p ^ q)")]
rule sext_xor<W, U>(x: W, y: W) where W < U { sext<U>(x) ^ sext<U>(y) => sext<U>(x ^ y) }
/// A slice of each operand of `&` is the slice of the conjunction.
#[example("extract<4, 4>(p) & extract<4, 4>(q)" => "extract<4, 4>(p & q)")]
rule extract_and<W, N, L>(x: W, y: W) where N + L <= W, N < W {
extract<L, N>(x) & extract<L, N>(y) => extract<L, N>(x & y)
}
/// Likewise for `|`.
#[example("extract<4, 4>(p) | extract<4, 4>(q)" => "extract<4, 4>(p | q)")]
rule extract_or<W, N, L>(x: W, y: W) where N + L <= W, N < W {
extract<L, N>(x) | extract<L, N>(y) => extract<L, N>(x | y)
}
/// Likewise for `^`.
#[example("extract<4, 4>(p) ^ extract<4, 4>(q)" => "extract<4, 4>(p ^ q)")]
rule extract_xor<W, N, L>(x: W, y: W) where N + L <= W, N < W {
extract<L, N>(x) ^ extract<L, N>(y) => extract<L, N>(x ^ y)
}
/// The low bits of each operand of `&` are the low bits of the conjunction.
#[example("trunc<4>(p) & trunc<4>(q)" => "trunc<4>(p & q)")]
rule trunc_and<W, N>(x: W, y: W) where N < W { trunc<N>(x) & trunc<N>(y) => trunc<N>(x & y) }
/// Likewise for `|`.
#[example("trunc<4>(p) | trunc<4>(q)" => "trunc<4>(p | q)")]
rule trunc_or<W, N>(x: W, y: W) where N < W { trunc<N>(x) | trunc<N>(y) => trunc<N>(x | y) }
/// Likewise for `^`.
#[example("trunc<4>(p) ^ trunc<4>(q)" => "trunc<4>(p ^ q)")]
rule trunc_xor<W, N>(x: W, y: W) where N < W { trunc<N>(x) ^ trunc<N>(y) => trunc<N>(x ^ y) }
}
group core.select_idioms {
/// Both arms add the same term.
#[example("select(p <u q, p + r, q + r)" => "select(p <u q, p, q) + r")]
rule select_add<W>(c: 1, x: W, y: W, z: W) { select(c, x + z, y + z) => select(c, x, y) + z }
/// Both arms xor the same term.
#[example("select(p <u q, p ^ r, q ^ r)" => "select(p <u q, p, q) ^ r")]
rule select_xor<W>(c: 1, x: W, y: W, z: W) { select(c, x ^ z, y ^ z) => select(c, x, y) ^ z }
/// Swapped arms under one condition, combined commutatively: the minimum plus the
/// maximum is the sum.
#[example("select(p <u q, p, q) + select(p <u q, q, p)" => "p + q")]
rule select_swapped_add<W>(c: 1, x: W, y: W) { select(c, x, y) + select(c, y, x) => x + y }
/// Likewise for `*`.
#[example("select(p <u q, p, q) * select(p <u q, q, p)" => "p * q")]
rule select_swapped_mul<W>(c: 1, x: W, y: W) { select(c, x, y) * select(c, y, x) => x * y }
/// Likewise for `&`.
#[example("select(p <u q, p, q) & select(p <u q, q, p)" => "p & q")]
rule select_swapped_and<W>(c: 1, x: W, y: W) { select(c, x, y) & select(c, y, x) => x & y }
/// Likewise for `|`.
#[example("select(p <u q, p, q) | select(p <u q, q, p)" => "p | q")]
rule select_swapped_or<W>(c: 1, x: W, y: W) { select(c, x, y) | select(c, y, x) => x | y }
/// Likewise for `^`.
#[example("select(p <u q, p, q) ^ select(p <u q, q, p)" => "p ^ q")]
rule select_swapped_xor<W>(c: 1, x: W, y: W) { select(c, x, y) ^ select(c, y, x) => x ^ y }
/// Both arms complement.
#[example("select(p <u q, ~p, ~q)" => "~select(p <u q, p, q)")]
rule select_not<W>(c: 1, x: W, y: W) { select(c, ~x, ~y) => ~select(c, x, y) }
/// The same condition again in the chosen arm.
#[example("select(p <u q, select(p <u q, p, q), r)" => "select(p <u q, p, r)")]
rule select_then_same<W>(c: 1, x: W, y: W, z: W) { select(c, select(c, x, y), z) => select(c, x, z) }
/// The same condition again in the other arm.
#[example("select(p <u q, r, select(p <u q, p, q))" => "select(p <u q, r, q)")]
rule select_else_same<W>(c: 1, x: W, y: W, z: W) { select(c, x, select(c, y, z)) => select(c, x, z) }
/// Choosing `x` when it equals `y`, else `y`: always `y` (`==` is commutative, so this is
/// also `select(y == x, x, y)`).
#[example("select(p == q, p, q)" => "q")]
#[example("select(p == q, q, p)" => "p")]
rule select_eq_then<W>(x: W, y: W) { select(x == y, x, y) => y }
/// When `x == y`, `x - y` is 0.
#[example("select(p == q, p - q, 0)" => "0")]
rule select_eq_difference<W>(x: W, y: W) { select(x == y, x - y, 0) => 0 }
/// When `x == c`, `x + d` is `c + d`.
#[example("select(p == 5, p + 1, 6)" => "6")]
rule select_eq_offset<W>(x: W, c: const W, d: const W, e: const W) {
select(x == c, x + d, e) => e if e == c + d
}
/// When `x == 0`, `x + y` is `y`.
#[example("select(p == 0, p + q, q)" => "q")]
rule select_zero_sum<W>(x: W, y: W) { select(x == 0, x + y, y) => y }
/// Choosing by a mask: `m` all ones takes `x`, all zeros `y`.
#[example("(p & sext<8>(r:1)) | (q & ~sext<8>(r:1))" => "select(r:1, p, q)")]
rule select_by_mask<W>(c: 1, x: W, y: W) where 1 < W {
(x & sext<W>(c)) | (y & ~sext<W>(c)) => select(c, x, y)
}
/// Choosing by a mask with xor: `y ^ ((x ^ y) & m)`.
#[example("q ^ ((p ^ q) & sext<8>(r:1))" => "select(r:1, p, q)")]
rule select_by_xor_mask<W>(c: 1, x: W, y: W) where 1 < W {
((x ^ y) & sext<W>(c)) ^ y => select(c, x, y)
}
/// The xor-mask choice once the mask became a select.
#[example("select(r:1, p ^ q, 0) ^ q" => "select(r:1, p, q)")]
rule select_xor_zero<W>(c: 1, x: W, y: W) { select(c, x ^ y, 0) ^ y => select(c, x, y) }
/// `zext(c) - 1` is all ones when `c` is false and zero when it is true: a mask. (With the
/// rules that make `x & -zext(c)` a select and merge complementary selects, the branchless
/// choice `(x & -zext(c)) | (y & (zext(c) - 1))` becomes `select(c, x, y)`.)
#[example("(zext<8>(r:1) - 1) & q" => "select(r:1, 0, q)")]
rule mask_by_decremented_bit<W>(c: 1, y: W) where 1 < W {
(zext<W>(c) + ones) & y => select(c, 0, y)
}
}
group core.division {
/// `x` divided by itself leaves no remainder (and `x mod 0` is `x`, which is 0 then too).
#[example("urem(p, p)" => "0")]
rule urem_self<W>(x: W) { urem(x, x) => 0 }
/// Likewise signed.
#[example("srem(p, p)" => "0")]
rule srem_self<W>(x: W) { srem(x, x) => 0 }
/// A remainder is already reduced.
#[example("urem(urem(p, q), q)" => "urem(p, q)")]
rule urem_urem<W>(x: W, y: W) { urem(urem(x, y), y) => urem(x, y) }
/// Division identity: quotient times divisor plus remainder (a zero divisor included: its
/// quotient is all ones, times 0, and its remainder is `x`).
#[example("udiv(p, q) * q + urem(p, q)" => "p")]
rule udiv_identity<W>(x: W, y: W) { udiv(x, y) * y + urem(x, y) => x }
/// Likewise signed (for 0: a quotient of ±1 times 0, and the remainder `x`).
#[example("sdiv(p, q) * q + srem(p, q)" => "p")]
rule sdiv_identity<W>(x: W, y: W) { sdiv(x, y) * y + srem(x, y) => x }
/// The same by a power of two, whose product `mul_pow2` makes a shift.
#[example("(sdiv(p, 8) << 3) + srem(p, 8)" => "p")]
rule sdiv_pow2_identity<W>(x: W, c: const W, k: const W) {
(sdiv(x, c) << k) + srem(x, c) => x if is_pow2(c) && k == ctz(c)
}
/// Signed division of a value the facts show nonnegative by a positive power of two is a
/// logical right shift.
#[example("sdiv(p >>u 1, 8)" => "p >>u 1 >>u 3")]
rule sdiv_nonnegative_pow2<W>(x: W, c: const W) {
sdiv(x, c) => x >>u k if is_pow2(c) && 0 <s c && proves(0 <=s x) let k: W = ctz(c)
}
}
group core.sign_tests {
/// The sign bit of `x` as a word: `x >>u (W - 1)`.
#[example("zext<8>(p <s 0)" => "p >>u 7")]
rule zext_negative<W>(x: W) where 1 < W { zext<W>(x <s 0) => x >>u (W - 1) }
/// The sign mask of `x`: `x >>s (W - 1)`.
#[example("sext<8>(p <s 0)" => "p >>s 7")]
rule sext_negative<W>(x: W) where 1 < W { sext<W>(x <s 0) => x >>s (W - 1) }
/// The sign bit is clear: `x` is nonnegative.
#[example("(p >>u 7) == 0" => "0 <=s p")]
rule sign_bit_clear<W>(x: W) where 1 < W { (x >>u (W - 1)) == 0 => 0 <=s x }
/// The sign mask is 0: `x` is nonnegative.
#[example("(p >>s 7) == 0" => "0 <=s p")]
rule sign_mask_zero<W>(x: W) where 1 < W { (x >>s (W - 1)) == 0 => 0 <=s x }
/// The sign mask is all ones: `x` is negative.
#[example("(p >>s 7) == 0xff" => "p <s 0")]
rule sign_mask_ones<W>(x: W) where 1 < W { (x >>s (W - 1)) == ones => x <s 0 }
/// The sign bit tested through a mask.
#[example("(p & 0x80) != 0" => "p <s 0")]
rule sign_by_mask<W>(x: W) { (x & smin_lit) != 0 => x <s 0 }
/// The sign bit clear, tested through a mask.
#[example("(p & 0x80) == 0" => "0 <=s p")]
rule sign_clear_by_mask<W>(x: W) { (x & smin_lit) == 0 => 0 <=s x }
/// The sign mask's low bit is the sign bit.
#[example("(p >>s 7) & (p >>u 7)" => "p >>u 7")]
rule sign_mask_and_bit<W>(x: W) where 1 < W { (x >>s (W - 1)) & (x >>u (W - 1)) => x >>u (W - 1) }
/// The negated sign mask is the sign bit.
#[example("-(p >>s 7)" => "p >>u 7")]
rule neg_sign_mask<W>(x: W) where 1 < W { -(x >>s (W - 1)) => x >>u (W - 1) }
/// Flipping both sign bits turns an unsigned comparison into a signed one.
#[example("(p ^ 0x80) <u (q ^ 0x80)" => "p <s q")]
rule ult_sign_flipped<W>(x: W, y: W) { (x ^ smin_lit) <u (y ^ smin_lit) => x <s y }
/// And a signed one into an unsigned one.
#[example("(p ^ 0x80) <s (q ^ 0x80)" => "p <u q")]
rule slt_sign_flipped<W>(x: W, y: W) { (x ^ smin_lit) <s (y ^ smin_lit) => x <u y }
/// Adding the sign bit flips it (the builder's form of `x + smin`).
#[example("(p + 0x80) <u (q + 0x80)" => "p <s q")]
rule ult_offset_by_smin<W>(x: W, y: W) { (x + smin_lit) <u (y + smin_lit) => x <s y }
/// Likewise signed.
#[example("(p + 0x80) <s (q + 0x80)" => "p <u q")]
rule slt_offset_by_smin<W>(x: W, y: W) { (x + smin_lit) <s (y + smin_lit) => x <u y }
/// Zero-extended values are nonnegative, so their signed order is the unsigned one.
#[example("zext<16>(p) <s zext<16>(q)" => "p <u q")]
rule slt_zext<W, U>(x: W, y: W) where W < U { zext<U>(x) <s zext<U>(y) => x <u y }
}
group core.bounds {
/// A conjunction is at most each operand (so is `x & -x`, its lowest set bit).
#[example("(p & q) <=u p" => "true")]
#[example("(p & -p) <=u p" => "true")]
rule and_at_most<W>(x: W, y: W) { (x & y) <=u x => true }
/// No operand is below its conjunction with anything.
#[example("p <u (p & q)" => "false")]
rule and_not_above<W>(x: W, y: W) { x <u (x & y) => false }
/// A disjunction is at least each operand.
#[example("p <=u (p | q)" => "true")]
rule or_at_least<W>(x: W, y: W) { x <=u (x | y) => true }
/// No disjunction is below one of its operands.
#[example("(p | q) <u p" => "false")]
rule or_not_below<W>(x: W, y: W) { (x | y) <u x => false }
/// A conjunction is at most the disjunction.
#[example("(p & q) <=u (p | q)" => "true")]
rule and_at_most_or<W>(x: W, y: W) { (x & y) <=u (x | y) => true }
/// A logical right shift does not grow a value.
#[example("(p >>u 1) <=u p" => "true")]
rule lshr_at_most<W>(x: W, s: W) { (x >>u s) <=u x => true }
/// Nor does unsigned division (by 0 it is all ones... except that `x / 0` is all ones,
/// so only by a divisor the facts show nonzero).
#[example("udiv(p, q | 1) <=u p" => "true")]
rule udiv_at_most<W>(x: W, y: W) { udiv(x, y) <=u x => true if proves(y != 0) }
/// A remainder is at most the dividend (by 0 it is the dividend).
#[example("urem(p, q) <=u p" => "true")]
rule urem_at_most<W>(x: W, y: W) { urem(x, y) <=u x => true }
/// A remainder is below its divisor, or (for 0) at most `y - 1`, all ones.
#[example("urem(p, q) <=u q - 1" => "true")]
rule urem_below_divisor<W>(x: W, y: W) { urem(x, y) <=u (y + ones) => true }
/// `x - 1 < x` except at 0, where it wraps.
#[example("p - 1 <u p" => "p != 0")]
rule decrement_below<W>(x: W) { (x + ones) <u x => x != 0 }
/// `x + 1 < x` only at all ones, where it wraps.
#[example("p + 1 <u p" => "p == 0xff")]
rule increment_wraps<W>(x: W) { (x + 1) <u x => x == ones }
/// `x + 1 <s x` only at the signed maximum.
#[example("p + 1 <s p" => "p == 0x7f")]
rule signed_increment_wraps<W>(x: W) { (x + 1) <s x => x == smax_lit }
/// `x <s x + 1` except at the signed maximum.
#[example("p <s p + 1" => "p != 0x7f")]
rule signed_increment_grows<W>(x: W) { x <s (x + 1) => x != smax_lit }
/// The larger of two shifts right by constants leaves the smaller value.
#[allow(BW0402)] // the lint's probes use equal constants, which the builder folds
#[example("(p >>u 3) <=u (p >>u 1)" => "true")]
rule longer_shift_smaller<W>(x: W, a: const W, b: const W) {
(x >>u a) <=u (x >>u b) => true if b <=u a
}
/// Halves of two values never overflow their sum.
#[example("((p >>u 1) + (q >>u 1)) <u (p >>u 1)" => "false")]
rule halves_sum_no_overflow<W>(x: W, y: W) where 1 < W {
((x >>u 1) + (y >>u 1)) <u (x >>u 1) => false
}
}
group core.concat {
/// `&` of concatenations with one low part: the low part stays.
#[example("concat(p, r:4) & concat(q, r:4)" => "concat(p & q, r:4)")]
rule concat_and_low<W, V>(x: W, y: V, z: W) { concat(x, y) & concat(z, y) => concat(x & z, y) }
/// Likewise with one high part.
#[example("concat(r:4, p) & concat(r:4, q)" => "concat(r:4, p & q)")]
rule concat_and_high<W, V>(x: W, y: V, z: V) { concat(x, y) & concat(x, z) => concat(x, y & z) }
/// `|` of concatenations with one low part.
#[example("concat(p, r:4) | concat(q, r:4)" => "concat(p | q, r:4)")]
rule concat_or_low<W, V>(x: W, y: V, z: W) { concat(x, y) | concat(z, y) => concat(x | z, y) }
/// Likewise with one high part.
#[example("concat(r:4, p) | concat(r:4, q)" => "concat(r:4, p | q)")]
rule concat_or_high<W, V>(x: W, y: V, z: V) { concat(x, y) | concat(x, z) => concat(x, y | z) }
/// `^` of concatenations with one low part: that part cancels.
#[example("concat(p, r:4) ^ concat(q, r:4)" => "concat(p ^ q, 0:4)")]
rule concat_xor_low<W, V>(x: W, y: V, z: W) { concat(x, y) ^ concat(z, y) => concat(x ^ z, zero) }
/// Concatenation associates; right nesting is the canonical one.
#[example("concat(concat(p, q), r)" => "concat(p, concat(q, r))")]
rule concat_assoc<A, B, C>(x: A, y: B, z: C) { concat(concat(x, y), z) => concat(x, concat(y, z)) }
/// An arithmetic shift right by the low part's width sign-extends the high part.
#[example("concat(p, q:4) >>s 4" => "sext<12>(p)")]
rule concat_ashr<W, V>(x: W, y: V) { concat(x, y) >>s V => sext<W + V>(x) }
/// A logical shift right by the low part's width zero-extends the high part.
#[example("concat(p, q:4) >>u 4" => "zext<12>(p)")]
rule concat_lshr<W, V>(x: W, y: V) { concat(x, y) >>u V => zext<W + V>(x) }
/// A value above a sign-extended copy of its top bit is its sign extension.
#[example("concat(sext<8>(extract<7, 1>(p)), p)" => "sext<16>(p)")]
rule concat_sign_word<W>(x: W) where 1 < W {
concat(sext<W>(extract<W - 1, 1>(x)), x) => sext<W + W>(x)
}
/// A zero low part with a zero-extended value in it is their concatenation (a sum of the
/// two has no carries, so it is this `|` too).
#[example("concat(p, 0:4) | zext<12>(q:4)" => "concat(p, q:4)")]
rule concat_or_zext<W, V>(x: W, y: V) { concat(x, 0) | zext<W + V>(y) => concat(x, y) }
}
group core.single_bit {
/// A power of two shares no bit with the value one below it (and `1 << s` past the width
/// is 0).
#[example("(1 << (q & 7)) & ((1 << (q & 7)) - 1)" => "0")]
rule pow2_and_below<W>(s: W) { (one << s) & ((one << s) + ones) => 0 }
}
group core.float {
/// Dividing by a power of two is multiplying by its reciprocal when that is a normal
/// number: the two are the same real number, rounded once in the same mode, so every result
/// (a NaN, an infinity, the sign of a zero, an underflow) is the same. Not by ½: the
/// builder already writes `x / ½` (and `x · 2`) as `x + x`.
#[example("fp.div.rne.f32(p:32, 0x40800000)" => "fp.mul.rne.f32(p:32, 0x3e800000)")]
rule div_pow2<E, S>(x: E + S, c: const E + S, r: rm) {
fp.div.r<E, S>(x, c) => fp.mul.r<E, S>(x, k)
if (c & lowmask(S - 1)) == 0 && (c & smax_lit) != 0 && (c & smax_lit) <u fp.inf<E, S>
&& m >=u fp.min_normal<E, S> && m != fp.two<E, S>
let m: E + S = fp.one<E, S> + fp.one<E, S> - (c & smax_lit)
let k: E + S = (c & smin_lit) | m
}
/// `x · 1` is `x` for every number.
#[example("fp.mul.rne.f64(fp.from_sbv.rne.f64(i:32), 0x3ff0000000000000)" => "fp.from_sbv.rne.f64(i:32)")]
rule mul_one<E, S>(x: E + S, r: rm) {
fp.mul.r<E, S>(x, fp.one<E, S>) => x if fp.not_nan<E, S>(x)
}
/// `x · −1` is `−x` for every number.
#[example("fp.mul.rtz.f64(fp.from_sbv.rne.f64(i:32), 0xbff0000000000000)" => "fp.from_sbv.rne.f64(i:32) ^ 0x8000000000000000")]
rule mul_neg_one<E, S>(x: E + S, r: rm) {
fp.mul.r<E, S>(x, fp.none<E, S>) => fp.neg<E, S>(x) if fp.not_nan<E, S>(x)
}
/// Adding +0 to a nonzero number changes nothing, in every mode.
#[example("fp.add.rtp.f32(fp.from_ubv.rne.f32(i:8 | 1), 0)" => "fp.from_ubv.rne.f32(i:8 | 1)")]
rule add_zero<E, S>(x: E + S, r: rm) {
fp.add.r<E, S>(x, fp.zero<E, S>) => x if fp.not_nan<E, S>(x) && fp.nonzero<E, S>(x)
}
/// Adding −0 to a nonzero number changes nothing, in every mode.
#[example("fp.add.rtn.f32(fp.from_ubv.rne.f32(i:8 | 1), 0x80000000)" => "fp.from_ubv.rne.f32(i:8 | 1)")]
rule add_neg_zero<E, S>(x: E + S, r: rm) {
fp.add.r<E, S>(x, fp.nzero<E, S>) => x if fp.not_nan<E, S>(x) && fp.nonzero<E, S>(x)
}
/// To nearest even, adding −0 changes no number, a zero included (−0 + −0 is −0,
/// +0 + −0 is +0): `x − 0` is `x`.
#[example("fp.sub.rne.f64(fp.from_sbv.rne.f64(i:32), 0)" => "fp.from_sbv.rne.f64(i:32)")]
rule add_neg_zero_rne<E, S>(x: E + S) {
fp.add.rne<E, S>(x, fp.nzero<E, S>) => x if fp.not_nan<E, S>(x)
}
/// A number equals itself (a NaN does not).
#[example("fp.eq.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "true")]
rule eq_self<E, S>(x: E + S) { fp.eq<E, S>(x, x) => true if fp.not_nan<E, S>(x) }
/// A number is at most itself.
#[example("fp.le.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "true")]
rule le_self<E, S>(x: E + S) { fp.le<E, S>(x, x) => true if fp.not_nan<E, S>(x) }
/// A number is its own minimum and maximum.
#[example("fp.min.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "fp.from_sbv.rne.f64(i:32)")]
rule min_self<E, S>(x: E + S) { fp.min<E, S>(x, x) => x if fp.not_nan<E, S>(x) }
#[example("fp.max.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "fp.from_sbv.rne.f64(i:32)")]
rule max_self<E, S>(x: E + S) { fp.max<E, S>(x, x) => x if fp.not_nan<E, S>(x) }
/// A finite nonzero number divided by itself is exactly 1, in every mode.
#[example("fp.div.rne.f64(fp.from_ubv.rne.f64(zext<32>(u:8) + 1), fp.from_ubv.rne.f64(zext<32>(u:8) + 1))" => "0x3ff0000000000000:64")]
rule div_self<E, S>(x: E + S, r: rm) {
fp.div.r<E, S>(x, x) => fp.one<E, S> if fp.finite<E, S>(x) && fp.nonzero<E, S>(x)
}
/// A finite number minus itself is +0 (the sum of opposites rounds to +0 except toward −∞).
#[example("fp.sub.rne.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "0:64")]
rule sub_self_rne<E, S>(x: E + S) { fp.add.rne<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }
/// Likewise to nearest, ties away.
#[example("fp.sub.rna.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "0:64")]
rule sub_self_rna<E, S>(x: E + S) { fp.add.rna<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }
/// Likewise toward +∞.
#[example("fp.sub.rtp.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "0:64")]
rule sub_self_rtp<E, S>(x: E + S) { fp.add.rtp<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }
/// Likewise toward 0.
#[example("fp.sub.rtz.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "0:64")]
rule sub_self_rtz<E, S>(x: E + S) { fp.add.rtz<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }
/// Toward −∞, a finite number minus itself is −0.
#[example("fp.sub.rtn.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32))" => "0x8000000000000000:64")]
rule sub_self_rtn<E, S>(x: E + S) { fp.add.rtn<E, S>(x, fp.neg<E, S>(x)) => fp.nzero<E, S> if fp.finite<E, S>(x) }
/// The square root of a square is the magnitude when the square is a normal number (no
/// overflow, no underflow), to nearest: `|x|` between `2^⌈emin/2⌉` and `2^⌊emax/2⌋`.
#[example("fp.sqrt.rne.f64(fp.mul.rne.f64(fp.from_ubv.rne.f64(zext<32>(u:8) + 1), fp.from_ubv.rne.f64(zext<32>(u:8) + 1)))" => "fp.from_ubv.rne.f64(zext<32>(u:8) + 1) & 0x7fffffffffffffff")]
rule sqrt_square<E, S>(x: E + S) {
fp.sqrt.rne<E, S>(fp.mul.rne<E, S>(x, x)) => fp.abs<E, S>(x)
if (proves(lo <=u x) && proves(x <u hi)) || (proves(nlo <=u x) && proves(x <u nhi))
let b: E + S = (one << (E - 1)) - one
let lo: E + S = (b - ((b - one) >>u 1)) << (S - 1)
let hi: E + S = (b + (b >>u 1)) << (S - 1)
let nlo: E + S = lo | smin_lit
let nhi: E + S = hi | smin_lit
}
/// Widening and narrowing back is exact for numbers (every number of the narrower format
/// is one of the wider).
#[example("fp.convert.rne.f64.f32(fp.convert.rne.f32.f64(fp.from_sbv.rne.f32(i:16)))" => "fp.from_sbv.rne.f32(i:16)")]
rule widen_narrow<E, S, F, T>(x: E + S, r: rm, q: rm) where E <= F, S <= T {
fp.convert.r<F, T, E, S>(fp.convert.q<E, S, F, T>(x)) => x if fp.not_nan<E, S>(x)
}
}
group core.float_values {
/// `x · 1` is `x` as a float (a NaN's product is the canonical NaN). With `div_pow2`,
/// `x / 1` is `x` too.
#[float_values]
#[example("fp.mul.rne.f32(p:32, 0x3f800000)" => "p:32")]
rule mul_one<E, S>(x: E + S, r: rm) { fp.mul.r<E, S>(x, fp.one<E, S>) => x }
/// `x · −1` is `−x` as a float.
#[float_values]
#[example("fp.mul.rne.f32(p:32, 0xbf800000)" => "p:32 ^ 0x80000000")]
rule mul_neg_one<E, S>(x: E + S, r: rm) { fp.mul.r<E, S>(x, fp.none<E, S>) => fp.neg<E, S>(x) }
/// `x + (−0)` is `x` as a float, to nearest (toward −∞, `+0 + −0` is `−0`).
#[float_values]
#[example("fp.add.rne.f32(p:32, 0x80000000)" => "p:32")]
rule add_neg_zero_rne<E, S>(x: E + S) { fp.add.rne<E, S>(x, fp.nzero<E, S>) => x }
/// Likewise to nearest, ties away.
#[float_values]
#[example("fp.add.rna.f32(p:32, 0x80000000)" => "p:32")]
rule add_neg_zero_rna<E, S>(x: E + S) { fp.add.rna<E, S>(x, fp.nzero<E, S>) => x }
/// Likewise toward +∞.
#[float_values]
#[example("fp.add.rtp.f32(p:32, 0x80000000)" => "p:32")]
rule add_neg_zero_rtp<E, S>(x: E + S) { fp.add.rtp<E, S>(x, fp.nzero<E, S>) => x }
/// Likewise toward 0.
#[float_values]
#[example("fp.add.rtz.f32(p:32, 0x80000000)" => "p:32")]
rule add_neg_zero_rtz<E, S>(x: E + S) { fp.add.rtz<E, S>(x, fp.nzero<E, S>) => x }
/// A value is its own minimum.
#[float_values]
#[example("fp.min.f32(p:32, p:32)" => "p:32")]
rule min_self<E, S>(x: E + S) { fp.min<E, S>(x, x) => x }
/// And its own maximum.
#[float_values]
#[example("fp.max.f32(p:32, p:32)" => "p:32")]
rule max_self<E, S>(x: E + S) { fp.max<E, S>(x, x) => x }
/// Widening and narrowing back is `x` as a float.
#[float_values]
#[example("fp.convert.rne.f64.f32(fp.convert.rne.f32.f64(p:32))" => "p:32")]
rule widen_narrow<E, S, F, T>(x: E + S, r: rm, q: rm) where E <= F, S <= T {
fp.convert.r<F, T, E, S>(fp.convert.q<E, S, F, T>(x)) => x
}
}