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)
}
/// The low bits of a zero extension's operand.
#[example("trunc<8>(zext<16>(p) & zext<16>(q))" => "p & q")]
rule trunc_and_zext<W, U>(a: W, b: W) where W < U {
trunc<W>(zext<U>(a) & zext<U>(b)) => a & b
}
}
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)
}
}
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) }
}
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) }
}
// 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
}
#[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)
}
}
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
}
#[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
}
}
group core.guarded_recovery_mba_normalized {
#[example("((p << 1) | 2) - (p + 1)" => "p ^ 1")]
rule xor_from_distributed_double_or<W>(x: W, c: const W, k: const W) {
((x << 1) | k) - (x + c) => x ^ c if k == c << 1
}
#[example("((p << 1) | 2) - (p ^ 1)" => "p + 1")]
rule sum_from_distributed_double_or<W>(x: W, c: const W, k: const W) {
((x << 1) | k) - (x ^ c) => x + c if k == 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)
}
}
// 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.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 writes `x · 2` as `x + x`, which is not smaller.
#[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) }
}