;; rewrites for integer and floating-point arithmetic
;; eg: `iadd`, `isub`, `ineg`, `imul`, `fadd`, `fsub`, `fmul`
;; For commutative instructions, we depend on cprop.isle pushing immediates to
;; the right, and thus only simplify patterns like `x+0`, not `0+x`.
;; x+0 == x.
(rule (simplify (iadd ty
x
(iconst_u ty 0)))
(subsume x))
;; x-0 == x.
(rule (simplify (isub ty
x
(iconst_u ty 0)))
(subsume x))
;; 0-x == (ineg x).
(rule (simplify (isub ty
(iconst_u ty 0)
x))
(ineg ty x))
;; x + -y == -y + x == -(y - x) == x - y
(rule (simplify (iadd ty x (ineg ty y)))
(isub ty x y))
(rule (simplify (iadd ty (ineg ty y) x))
(isub ty x y))
(rule (simplify (ineg ty (isub ty y x)))
(isub ty x y))
;; x - -y == x + y
(rule (simplify (isub ty x (ineg ty y)))
(iadd ty x y))
;; ineg(ineg(x)) == x.
(rule (simplify (ineg ty (ineg ty x))) (subsume x))
;; ineg(x) * ineg(y) == x*y.
(rule (simplify (imul ty (ineg ty x) (ineg ty y)))
(subsume (imul ty x y)))
;; iabs(ineg(x)) == iabs(x).
(rule (simplify (iabs ty (ineg ty x)))
(iabs ty x))
;; iabs(iabs(x)) == iabs(x).
(rule (simplify (iabs ty inner @ (iabs ty x)))
(subsume inner))
;; x-x == 0.
(rule (simplify (isub ty x x)) (subsume (iconst_u ty 0)))
;; x*1 == x.
(rule (simplify (imul ty
x
(iconst_u ty 1)))
(subsume x))
;; x*0 == 0.
(rule (simplify (imul ty
_
zero @ (iconst_u ty 0)))
(subsume zero))
;; x*-1 == ineg(x).
(rule (simplify (imul ty x (iconst_s ty -1)))
(ineg ty x))
;; (!x) + 1 == ineg(x)
(rule (simplify (iadd ty (bnot ty x) (iconst_u ty 1)))
(ineg ty x))
;; !(x - 1) == !(x + (-1)) == ineg(x)
(rule (simplify (bnot ty (isub ty x (iconst_s ty 1))))
(ineg ty x))
(rule (simplify (bnot ty (iadd ty x (iconst_s ty -1))))
(ineg ty x))
;; x / 1 == x.
(rule (simplify_skeleton (sdiv x (iconst_s ty 1))) x)
(rule (simplify_skeleton (udiv x (iconst_u ty 1))) x)
;; Unsigned `x / d == x >> ilog2(d)` when d is a power of two.
(rule (simplify_skeleton (udiv x (iconst_u ty (u64_extract_power_of_two d))))
(ushr ty x (iconst_u ty (u64_ilog2 d))))
;; Signed `x / d` when d is a power of two is a bit more involved...
(rule (simplify_skeleton (sdiv x (iconst_u ty (u64_extract_power_of_two d))))
(if-let true (u64_gt d 1))
;; This rule musn't fire for the most negative number - which looks like
;; a power of two (sign bit set and otherwise all zeros)
(if-let true (u32_lt (u64_trailing_zeros d)
(u32_sub (ty_bits ty) 1)))
(let ((k u32 (u64_trailing_zeros d))
(t1 Value (sshr ty x (iconst_u ty (u32_sub k 1))))
(t2 Value (ushr ty t1 (iconst_u ty (u32_sub (ty_bits ty) k))))
(t3 Value (iadd ty x t2))
(t4 Value (sshr ty t3 (iconst_s ty k))))
t4))
;; And signed `x / d` when d is a negative power of two is the same, but with a
;; negation.
(rule (simplify_skeleton (sdiv x (iconst_s ty d)))
(if-let true (i64_is_negative_power_of_two d))
(if-let true (i64_ne d -1))
(let ((k u32 (i64_trailing_zeros d))
(t1 Value (sshr ty x (iconst_u ty (u32_sub k 1))))
(t2 Value (ushr ty t1 (iconst_u ty (u32_sub (ty_bits ty) k))))
(t3 Value (iadd ty x t2))
(t4 Value (sshr ty t3 (iconst_s ty k)))
(t5 Value (ineg ty t4)))
t5))
;; General cases for `udiv` with constant divisors.
(rule (simplify_skeleton (udiv x (iconst_u $I32 (u64_extract_non_zero (u32_from_u64 d)))))
(if-let false (u32_is_power_of_two d))
(apply_div_const_magic_u32 (Opcode.Udiv) x d))
(rule (simplify_skeleton (udiv x (iconst_u $I64 (u64_extract_non_zero d))))
(if-let false (u64_is_power_of_two d))
(apply_div_const_magic_u64 (Opcode.Udiv) x d))
;; General cases for `sdiv` with constant divisors.
(rule (simplify_skeleton (sdiv x (iconst_s $I32 (i64_extract_non_zero (i32_from_i64 d)))))
(if-let false (i64_is_any_sign_power_of_two d))
(apply_div_const_magic_s32 (Opcode.Sdiv) x d))
(rule (simplify_skeleton (sdiv x (iconst_s $I64 (i64_extract_non_zero d))))
(if-let false (i64_is_any_sign_power_of_two d))
(apply_div_const_magic_s64 (Opcode.Sdiv) x d))
;; x % 1 == 0
(rule (simplify_skeleton (urem x (iconst_u ty 1))) (iconst_u ty 0))
(rule (simplify_skeleton (srem x (iconst_u ty 1))) (iconst_u ty 0))
(rule (simplify_skeleton (srem x (iconst_s ty -1))) (iconst_u ty 0))
;; Unsigned `x % d == x & ((1 << ilog2(d)) - 1)` when `d` is a power of two.
(rule (simplify_skeleton (urem x (iconst_u ty (u64_extract_power_of_two d))))
(if-let true (u64_gt d 1))
(let ((mask Value (iconst_u ty (u64_sub (u64_shl 1 (u64_ilog2 d)) 1))))
(band ty x mask)))
;; Signed `x % d` when `d` is a (possibly negative) power of two is a little
;; more complicated.
(rule (simplify_skeleton (srem x d_val @ (iconst_s ty d)))
;; Interestingly, this same sequence works for both positive and negative
;; powers of two.
(if-let true (i64_is_any_sign_power_of_two d))
(if-let true (i64_ne d 1))
(if-let true (i64_ne d -1))
(let ((k u32 (i64_trailing_zeros d))
(t1 Value (sshr ty x (iconst_u ty (u32_sub k 1))))
(t2 Value (ushr ty t1 (iconst_u ty (u32_sub (ty_bits ty) k))))
(t3 Value (iadd ty x t2))
(t4 Value (band ty t3 (iconst_s ty (i64_wrapping_neg (i64_shl 1 k)))))
(t5 Value (isub ty x t4)))
t5))
;; General cases for `urem` with constant divisors.
(rule (simplify_skeleton (urem x (iconst_u $I32 (u64_extract_non_zero (u32_from_u64 d)))))
(if-let false (u32_is_power_of_two d))
(apply_div_const_magic_u32 (Opcode.Urem) x d))
(rule (simplify_skeleton (urem x (iconst_u $I64 (u64_extract_non_zero d))))
(if-let false (u64_is_power_of_two d))
(apply_div_const_magic_u64 (Opcode.Urem) x d))
;; General cases for `srem` with constant divisors.
(rule (simplify_skeleton (srem x (iconst_s $I32 (i64_extract_non_zero (i32_from_i64 d)))))
(if-let false (i64_is_any_sign_power_of_two d))
(apply_div_const_magic_s32 (Opcode.Srem) x d))
(rule (simplify_skeleton (srem x (iconst_s $I64 (i64_extract_non_zero d))))
(if-let false (i64_is_any_sign_power_of_two d))
(apply_div_const_magic_s64 (Opcode.Srem) x d))
;; x*2 == x+x.
(rule (simplify (imul ty x (iconst_u _ 2)))
(iadd ty x x))
;; x*c == x<<log2(c) when c is a power of two.
;;
;; Note that the type of `iconst` must be the same as the type of `imul`,
;; so these rules can only fire in situations where it's safe to construct an
;; `iconst` of that type.
(rule (simplify (imul ty x (iconst _ (imm64_power_of_two c))))
(ishl ty x (iconst ty (imm64 c))))
(rule (simplify (imul ty (iconst _ (imm64_power_of_two c)) x))
(ishl ty x (iconst ty (imm64 c))))
;; fneg(fneg(x)) == x.
(rule (simplify (fneg ty (fneg ty x))) (subsume x))
;; If both of the multiplied arguments to an `fma` are negated then remove
;; both of them since they cancel out.
(rule (simplify (fma ty (fneg ty x) (fneg ty y) z))
(fma ty x y z))
;; If both of the multiplied arguments to an `fmul` are negated then remove
;; both of them since they cancel out.
(rule (simplify (fmul ty (fneg ty x) (fneg ty y)))
(fmul ty x y))
;; Detect people open-coding `mulhi`: (x as big * y as big) >> bits
;; LLVM doesn't have an intrinsic for it, so you'll see it in code like
;; <https://github.com/rust-lang/rust/blob/767453eb7ca188e991ac5568c17b984dd4893e77/library/core/src/num/mod.rs#L174-L180>
(rule (simplify (sshr ty (imul ty (sextend _ x@(value_type half_ty))
(sextend _ y@(value_type half_ty)))
(iconst_u _ k)))
(if-let true (ty_equal half_ty (ty_half_width ty)))
(if-let true (u64_eq k (ty_bits_u64 half_ty)))
(sextend ty (smulhi half_ty x y)))
(rule (simplify (ushr ty (imul ty (uextend _ x@(value_type half_ty))
(uextend _ y@(value_type half_ty)))
(iconst_u _ k)))
(if-let true (ty_equal half_ty (ty_half_width ty)))
(if-let true (u64_eq k (ty_bits_u64 half_ty)))
(uextend ty (umulhi half_ty x y)))
;; Cranelift's `fcvt_from_{u,s}int` instructions are polymorphic over the input
;; type so remove any unnecessary `uextend` or `sextend` to give backends
;; the chance to convert from the smallest integral type to the float. This
;; can help lowerings on x64 for example which has a less efficient u64-to-float
;; conversion than other bit widths.
(rule (simplify (fcvt_from_uint ty (uextend _ val)))
(fcvt_from_uint ty val))
(rule (simplify (fcvt_from_sint ty (sextend _ val)))
(fcvt_from_sint ty val))
;; or(x, C) + (-C) --> and(x, ~C)
(rule
(simplify (iadd ty
(bor ty x (iconst ty n))
(iconst ty m)))
(if-let m (imm64_neg ty n))
(band ty x (iconst ty (imm64_not ty n))))
;; (x + y) - (x | y) --> x & y
(rule (simplify (isub ty (iadd ty x y) (bor ty x y))) (band ty x y))
;; x * (1 << y) == x << y
(rule (simplify (imul ty x (ishl ty (iconst_s ty 1) y))) (ishl ty x y))
;; (x - y) + x --> x
(rule (simplify (iadd ty (isub ty x y) y)) x)
(rule (simplify (iadd ty y (isub ty x y))) x)
;; (x + y) - y --> x
(rule (simplify (isub ty (iadd ty x y) x)) y)
(rule (simplify (isub ty (iadd ty x y) y)) x)
;; (x - y) - x => -y
(rule (simplify (isub ty (isub ty x y) x))(ineg ty y))
;; (x * C) (==/!=) D --> x (==/!=) (D / C) when C is odd and divides D
(rule
(simplify (ne ty (iconst_u ty1 x) (imul ty1 y (iconst_u ty1 z))))
(if-let 0 (u64_checked_rem x z))
(if-let 1 (u64_rem z 2))
(ne ty y (iconst ty1 (imm64 (u64_div x z)))))
(rule
(simplify (ne ty (iconst_u ty1 x) (imul ty1 (iconst_u ty1 y) z)))
(if-let 0 (u64_checked_rem x y))
(if-let 1 (u64_rem y 2))
(ne ty z (iconst ty1 (imm64 (u64_div x y)))))
(rule
(simplify (ne ty (imul ty1 x (iconst_u ty1 y)) (iconst_u ty1 z)))
(if-let 0 (u64_checked_rem z y))
(if-let 1 (u64_rem y 2))
(ne ty x (iconst ty1 (imm64 (u64_div z y)))))
(rule
(simplify (ne ty (imul ty1 (iconst_u ty1 x) y) (iconst_u ty1 z)))
(if-let 0 (u64_checked_rem z x))
(if-let 1 (u64_rem x 2))
(ne ty y (iconst ty1 (imm64 (u64_div z x)))))
(rule
(simplify (eq ty (iconst_u ty1 x) (imul ty1 y (iconst_u ty1 z))))
(if-let 0 (u64_checked_rem x z))
(if-let 1 (u64_rem z 2))
(eq ty y (iconst ty1 (imm64 (u64_div x z)))))
(rule
(simplify (eq ty (iconst_u ty1 x) (imul ty1 (iconst_u ty1 y) z)))
(if-let 0 (u64_checked_rem x y))
(if-let 1 (u64_rem y 2))
(eq ty z (iconst ty1 (imm64 (u64_div x y)))))
(rule
(simplify (eq ty (imul ty1 x (iconst_u ty1 y)) (iconst_u ty1 z)))
(if-let 0 (u64_checked_rem z y))
(if-let 1 (u64_rem y 2))
(eq ty x (iconst ty1 (imm64 (u64_div z y)))))
(rule
(simplify (eq ty (imul ty1 (iconst_u ty1 x) y) (iconst_u ty1 z)))
(if-let 0 (u64_checked_rem z x))
(if-let 1 (u64_rem x 2))
(eq ty y (iconst ty1 (imm64 (u64_div z x)))))
;; (x + y) + (-y) ==> x
;; and equivalent operand-order variants.
(rule (simplify (iadd ty (iadd ty x y) (ineg ty y))) x)
(rule (simplify (iadd ty (ineg ty y) (iadd ty x y))) x)
(rule (simplify (iadd ty (iadd ty y x) (ineg ty y))) x)
(rule (simplify (iadd ty (ineg ty y) (iadd ty y x))) x)
;; (x | y) - (x & y) ==> (x ^ y)
(rule (simplify (isub ty (bor ty x y) (band ty x y))) (bxor ty x y))
(rule (simplify (isub ty (bor ty x y) (band ty y x))) (bxor ty x y))
(rule (simplify (isub ty (bor ty y x) (band ty x y))) (bxor ty x y))
(rule (simplify (isub ty (bor ty y x) (band ty y x))) (bxor ty x y))
;; (x + y) - (x & y) ==> (x | y)
(rule (simplify (isub ty (iadd ty x y) (band ty x y))) (bor ty x y))
(rule (simplify (isub ty (iadd ty x y) (band ty y x))) (bor ty x y))
(rule (simplify (isub ty (iadd ty y x) (band ty x y))) (bor ty x y))
(rule (simplify (isub ty (iadd ty y x) (band ty y x))) (bor ty x y))
;; (x | y) - (x ^ y) ==> (x & y)
(rule (simplify (isub ty (bor ty x y) (bxor ty x y))) (band ty x y))
(rule (simplify (isub ty (bor ty x y) (bxor ty y x))) (band ty x y))
(rule (simplify (isub ty (bor ty y x) (bxor ty x y))) (band ty x y))
(rule (simplify (isub ty (bor ty y x) (bxor ty y x))) (band ty x y))
;; (~x) + x == -1
(rule (simplify (iadd ty (bnot ty x) x)) (iconst_s ty -1))
(rule (simplify (iadd ty x (bnot ty x))) (iconst_s ty -1))
;; (x - y) == x --> y == 0
(rule (simplify (eq cty (isub ty x y) x)) (eq cty y (iconst_u ty 0)))
(rule (simplify (eq cty x (isub ty x y))) (eq cty y (iconst_u ty 0)))
;; (x + y) == y --> x == 0
(rule (simplify (eq cty (iadd ty x y) y)) (eq cty x (iconst_u ty 0)))
(rule (simplify (eq cty (iadd ty y x) y)) (eq cty x (iconst_u ty 0)))
(rule (simplify (eq cty y (iadd ty x y))) (eq cty x (iconst_u ty 0)))
(rule (simplify (eq cty y (iadd ty y x))) (eq cty x (iconst_u ty 0)))
;; -x == -y --> x == y
(rule (simplify (eq ty (ineg ty x) (ineg ty y))) (eq ty x y))
;; -((-y) * x) --> x * y
(rule (simplify (ineg ty (imul ty (ineg ty y) x))) (imul ty x y))
(rule (simplify (ineg ty (imul ty x (ineg ty y)))) (imul ty x y))
;; Helper to create a "true" value for a comparison. For scalar integers this is
;; a value of 1 but for vectors this is -1 since each lane is filled with all
;; 1s. We use `(iconst_u ty 0)` for falses for both integers and vector. This is
;; because of the Cranelift semantics:
;; When comparing scalars, the result is 1 if the condition holds, or 0 otherwise.
;; When comparing vectors, the result is -1 (all-ones) if the condition holds, or 0 otherwise.
(decl cmp_true (Type) Value)
(rule 0 (cmp_true (ty_int ty)) (iconst_u ty 1))
(rule 1 (cmp_true (ty_vec128 ty)) (iconst_s ty -1))
;; max(x, y) >= x
(rule (simplify (sge ty (smax ty x y) x)) (cmp_true ty))
(rule (simplify (sge ty (smax ty y x) x)) (cmp_true ty))
(rule (simplify (sle ty x (smax ty x y))) (cmp_true ty))
(rule (simplify (sle ty x (smax ty y x))) (cmp_true ty))
(rule (simplify (uge ty (umax ty x y) x)) (cmp_true ty))
(rule (simplify (uge ty (umax ty y x) x)) (cmp_true ty))
(rule (simplify (ule ty x (umax ty x y))) (cmp_true ty))
(rule (simplify (ule ty x (umax ty y x))) (cmp_true ty))
;; x >= min(x, y)
(rule (simplify (sge ty x (smin ty x y))) (cmp_true ty))
(rule (simplify (sge ty x (smin ty y x))) (cmp_true ty))
(rule (simplify (sle ty (smin ty x y) x)) (cmp_true ty))
(rule (simplify (sle ty (smin ty y x) x)) (cmp_true ty))
(rule (simplify (uge ty x (umin ty x y))) (cmp_true ty))
(rule (simplify (uge ty x (umin ty y x))) (cmp_true ty))
(rule (simplify (ule ty (umin ty x y) x)) (cmp_true ty))
(rule (simplify (ule ty (umin ty y x) x)) (cmp_true ty))
;; min/max(x,x) --> x
(rule (simplify (umin ty x x)) x)
(rule (simplify (smin ty x x)) x)
(rule (simplify (umax ty x x)) x)
(rule (simplify (smax ty x x)) x)
;; max(max(x, y), x) --> max(x, y)
(rule (simplify (smax ty (smax ty x y) x)) (smax ty x y))
(rule (simplify (smax ty (smax ty y x) x)) (smax ty x y))
(rule (simplify (smax ty x (smax ty x y))) (smax ty x y))
(rule (simplify (smax ty x (smax ty y x))) (smax ty x y))
(rule (simplify (umax ty (umax ty x y) x)) (umax ty x y))
(rule (simplify (umax ty (umax ty y x) x)) (umax ty x y))
(rule (simplify (umax ty x (umax ty x y))) (umax ty x y))
(rule (simplify (umax ty x (umax ty y x))) (umax ty x y))
;; min(min(x, y), x) --> min(x, y)
(rule (simplify (smin ty (smin ty x y) x)) (smin ty x y))
(rule (simplify (smin ty (smin ty y x) x)) (smin ty x y))
(rule (simplify (smin ty x (smin ty x y))) (smin ty x y))
(rule (simplify (smin ty x (smin ty y x))) (smin ty x y))
(rule (simplify (umin ty (umin ty x y) x)) (umin ty x y))
(rule (simplify (umin ty (umin ty y x) x)) (umin ty x y))
(rule (simplify (umin ty x (umin ty x y))) (umin ty x y))
(rule (simplify (umin ty x (umin ty y x))) (umin ty x y))
;; min(max(x, y), y) --> y ; max(min(x, y), y) --> y
(rule (simplify (smin ty (smax ty x y) y)) y)
(rule (simplify (smin ty (smax ty y x) y)) y)
(rule (simplify (smin ty y (smax ty x y))) y)
(rule (simplify (smin ty y (smax ty y x))) y)
(rule (simplify (umin ty (umax ty x y) y)) y)
(rule (simplify (umin ty (umax ty y x) y)) y)
(rule (simplify (umin ty y (umax ty x y))) y)
(rule (simplify (umin ty y (umax ty y x))) y)
(rule (simplify (smax ty (smin ty x y) y)) y)
(rule (simplify (smax ty (smin ty y x) y)) y)
(rule (simplify (smax ty y (smin ty x y))) y)
(rule (simplify (smax ty y (smin ty y x))) y)
(rule (simplify (umax ty (umin ty x y) y)) y)
(rule (simplify (umax ty (umin ty y x) y)) y)
(rule (simplify (umax ty y (umin ty x y))) y)
(rule (simplify (umax ty y (umin ty y x))) y)
;; min(min(x, y), max(x, y)) --> min(x,y)
(rule (simplify (smin ty (smax ty x y) (smin ty x y))) (smin ty x y))
(rule (simplify (smin ty (smax ty x y) (smin ty y x))) (smin ty x y))
(rule (simplify (smin ty (smax ty x y) (umin ty x y))) (umin ty x y))
(rule (simplify (smin ty (smax ty x y) (umin ty y x))) (umin ty x y))
(rule (simplify (smin ty (smin ty x y) (smax ty x y))) (smin ty x y))
(rule (simplify (smin ty (smin ty x y) (smax ty y x))) (smin ty x y))
(rule (simplify (smin ty (smin ty x y) (umax ty x y))) (smin ty x y))
(rule (simplify (smin ty (smin ty x y) (umax ty y x))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (smin ty x y))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (smin ty y x))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (umin ty x y))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (umin ty y x))) (smin ty x y))
(rule (simplify (smin ty (umin ty x y) (smax ty x y))) (umin ty x y))
(rule (simplify (smin ty (umin ty x y) (smax ty y x))) (umin ty x y))
(rule (simplify (smin ty (umin ty x y) (umax ty x y))) (smin ty x y))
(rule (simplify (smin ty (umin ty x y) (umax ty y x))) (smin ty x y))
(rule (simplify (umin ty (smax ty x y) (smin ty x y))) (umin ty x y))
(rule (simplify (umin ty (smax ty x y) (smin ty y x))) (umin ty x y))
(rule (simplify (umin ty (smax ty x y) (umin ty x y))) (umin ty x y))
(rule (simplify (umin ty (smax ty x y) (umin ty y x))) (umin ty x y))
(rule (simplify (umin ty (smin ty x y) (smax ty x y))) (umin ty x y))
(rule (simplify (umin ty (smin ty x y) (smax ty y x))) (umin ty x y))
(rule (simplify (umin ty (smin ty x y) (umax ty x y))) (smin ty x y))
(rule (simplify (umin ty (smin ty x y) (umax ty y x))) (smin ty x y))
(rule (simplify (umin ty (umax ty x y) (smin ty x y))) (smin ty x y))
(rule (simplify (umin ty (umax ty x y) (smin ty y x))) (smin ty x y))
(rule (simplify (umin ty (umax ty x y) (umin ty x y))) (umin ty x y))
(rule (simplify (umin ty (umax ty x y) (umin ty y x))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (smax ty x y))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (smax ty y x))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (umax ty x y))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (umax ty y x))) (umin ty x y))
;; max(min(x, y), max(x, y)) --> max(x, y)
(rule (simplify (smax ty (smax ty x y) (smin ty x y))) (smax ty x y))
(rule (simplify (smax ty (smax ty x y) (smin ty y x))) (smax ty x y))
(rule (simplify (smax ty (smax ty x y) (umin ty x y))) (smax ty x y))
(rule (simplify (smax ty (smax ty x y) (umin ty y x))) (smax ty x y))
(rule (simplify (smax ty (smin ty x y) (smax ty x y))) (smax ty x y))
(rule (simplify (smax ty (smin ty x y) (smax ty y x))) (smax ty x y))
(rule (simplify (smax ty (smin ty x y) (umax ty x y))) (umax ty x y))
(rule (simplify (smax ty (smin ty x y) (umax ty y x))) (umax ty x y))
(rule (simplify (smax ty (umax ty x y) (smin ty x y))) (umax ty x y))
(rule (simplify (smax ty (umax ty x y) (smin ty y x))) (umax ty x y))
(rule (simplify (smax ty (umax ty x y) (umin ty x y))) (smax ty x y))
(rule (simplify (smax ty (umax ty x y) (umin ty y x))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (smax ty x y))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (smax ty y x))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (umax ty x y))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (umax ty y x))) (smax ty x y))
(rule (simplify (umax ty (smax ty x y) (smin ty x y))) (umax ty x y))
(rule (simplify (umax ty (smax ty x y) (smin ty y x))) (umax ty x y))
(rule (simplify (umax ty (smax ty x y) (umin ty x y))) (smax ty x y))
(rule (simplify (umax ty (smax ty x y) (umin ty y x))) (smax ty x y))
(rule (simplify (umax ty (smin ty x y) (smax ty x y))) (umax ty x y))
(rule (simplify (umax ty (smin ty x y) (smax ty y x))) (umax ty x y))
(rule (simplify (umax ty (smin ty x y) (umax ty x y))) (umax ty x y))
(rule (simplify (umax ty (smin ty x y) (umax ty y x))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (smin ty x y))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (smin ty y x))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (umin ty x y))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (umin ty y x))) (umax ty x y))
(rule (simplify (umax ty (umin ty x y) (smax ty x y))) (smax ty x y))
(rule (simplify (umax ty (umin ty x y) (smax ty y x))) (smax ty x y))
(rule (simplify (umax ty (umin ty x y) (umax ty x y))) (umax ty x y))
(rule (simplify (umax ty (umin ty x y) (umax ty y x))) (umax ty x y))
;; x > max(x, y) --> 0
(rule (simplify (sgt ty x (smax ty x y))) (iconst_u ty 0))
(rule (simplify (sgt ty x (smax ty y x))) (iconst_u ty 0))
(rule (simplify (slt ty (smax ty x y) x)) (iconst_u ty 0))
(rule (simplify (slt ty (smax ty y x) x)) (iconst_u ty 0))
(rule (simplify (ugt ty x (umax ty x y))) (iconst_u ty 0))
(rule (simplify (ugt ty x (umax ty y x))) (iconst_u ty 0))
(rule (simplify (ult ty (umax ty x y) x)) (iconst_u ty 0))
(rule (simplify (ult ty (umax ty y x) x)) (iconst_u ty 0))
;; (-X) * C = X * (-C)
(rule (simplify (imul (fits_in_64 ty) (ineg ty x) (iconst ty y))) (imul ty x (iconst ty (imm64_neg ty y))))