1;; Rewrites for `band`, `bnot`, `bor`, `bxor` 2 3;; x | 0 == x | x == x. 4(rule (simplify (bor ty 5 x 6 (iconst_u ty 0))) 7 (subsume x)) 8(rule (simplify (bor ty x x)) 9 (subsume x)) 10 11;; x ^ 0 == x. 12(rule (simplify (bxor ty 13 x 14 (iconst_u ty 0))) 15 (subsume x)) 16 17;; x ^ x == 0. 18(rule (simplify (bxor (ty_int ty) x x)) 19 (subsume (iconst_u ty 0))) 20 21;; x ^ not(x) == not(x) ^ x == x | not(x) == not(x) | x == -1. 22;; This identity also holds for non-integer types, vectors, and wider types. 23(rule (simplify (bxor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1))) 24(rule (simplify (bxor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1))) 25(rule (simplify (bor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1))) 26(rule (simplify (bor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1))) 27 28;; x & x == x & -1 == x. 29(rule (simplify (band ty x x)) (subsume x)) 30(rule (simplify (band ty x (iconst_s ty -1))) 31 (subsume x)) 32 33;; x & 0 == x & not(x) == not(x) & x == 0. 34(rule (simplify (band ty _ zero @ (iconst_u ty 0))) (subsume zero)) 35(rule (simplify (band (ty_int ty) x (bnot ty x))) (subsume (iconst_u ty 0))) 36(rule (simplify (band (ty_int ty) (bnot ty x) x)) (subsume (iconst_u ty 0))) 37 38;; (x & y) ^ (x ^ y) == x | y 39(rule (simplify (bxor ty (band ty X Y) (bxor ty X Y))) (bor ty X Y)) 40 41;; not(not(x)) == x. 42(rule (simplify (bnot ty (bnot ty x))) (subsume x)) 43 44;; DeMorgan's rule (two versions): 45;; bnot(bor(x, y)) == band(bnot(x), bnot(y)) 46(rule (simplify (bnot ty (bor ty x y))) 47 (band ty (bnot ty x) (bnot ty y))) 48;; bnot(band(x, y)) == bor(bnot(x), bnot(y)) 49(rule (simplify (bnot ty (band t x y))) 50 (bor ty (bnot ty x) (bnot ty y))) 51 52;; `or(and(x, y), not(y)) == or(x, not(y))` 53(rule (simplify (bor ty 54 (band ty x y) 55 z @ (bnot ty y))) 56 (bor ty x z)) 57;; Duplicate the rule but swap the `bor` operands because `bor` is 58;; commutative. We could, of course, add a `simplify` rule to do the commutative 59;; swap for all `bor`s but this will bloat the e-graph with many e-nodes. It is 60;; cheaper to have additional rules, rather than additional e-nodes, because we 61;; amortize their cost via ISLE's smart codegen. 62(rule (simplify (bor ty 63 z @ (bnot ty y) 64 (band ty x y))) 65 (bor ty x z)) 66 67;; `or(and(x, y), not(y)) == or(x, not(y))` specialized for constants, since 68;; otherwise we may not know that `z == not(y)` since we don't generally expand 69;; constants in the e-graph. 70;; 71;; (No need to duplicate for commutative `bor` for this constant version because 72;; we move constants to the right.) 73(rule (simplify (bor ty 74 (band ty x (iconst_u ty y)) 75 z @ (iconst_u ty zk))) 76 (if-let true (u64_eq (u64_and (ty_mask ty) zk) 77 (u64_and (ty_mask ty) (u64_not y)))) 78 (bor ty x z)) 79 80;; (x ^ -1) can be replaced with the `bnot` instruction 81(rule (simplify (bxor ty x (iconst_s ty -1))) 82 (bnot ty x)) 83 84;; sshr((x | -x), N) == bmask(x) where N = ty_bits(ty) - 1. 85;; 86;; (x | -x) sets the sign bit to 1 if x is nonzero, and 0 if x is zero. sshr propagates 87;; the sign bit to the rest of the value. 88(rule (simplify (sshr ty (bor ty x (ineg ty x)) (iconst_u ty shift_amt))) 89 (if-let true (u64_eq shift_amt (ty_shift_mask ty))) 90 (bmask ty x)) 91 92(rule (simplify (sshr ty (bor ty (ineg ty x) x) (iconst_u ty shift_amt))) 93 (if-let true (u64_eq shift_amt (ty_shift_mask ty))) 94 (bmask ty x)) 95 96;; Since icmp is always 0 or 1, bmask is just a negation. 97;; TODO: Explore whether this makes sense for things needing extension too. 98(rule (simplify (bmask $I8 cmp@(icmp $I8 _ _ _))) 99 (ineg $I8 cmp)) 100 101;; Matches any expressions that preserve "truthiness". 102;; i.e. If the input is zero it remains zero, and if it is nonzero it can have 103;; a different value as long as it is still nonzero. 104(decl pure multi truthy (Value) Value) 105(rule (truthy (sextend _ x)) x) 106(rule (truthy (uextend _ x)) x) 107(rule (truthy (bmask _ x)) x) 108(rule (truthy (ineg _ x)) x) 109(rule (truthy (bswap _ x)) x) 110(rule (truthy (bitrev _ x)) x) 111(rule (truthy (popcnt _ x)) x) 112(rule (truthy (rotl _ x _)) x) 113(rule (truthy (rotr _ x _)) x) 114(rule (truthy (select _ x (iconst_u _ (u64_when_non_zero)) (iconst_u _ 0))) x) 115;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule 116(rule (truthy (ne _ x (iconst_u _ 0))) x) 117 118;; All of these expressions don't care about their input as long as it is truthy. 119;; so we can remove expressions that preserve that property from the input. 120(rule (simplify (bmask ty v)) (if-let x (truthy v)) (bmask ty x)) 121(rule (simplify (select ty v t f)) (if-let c (truthy v)) (select ty c t f)) 122;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule 123(rule (simplify (ne cty v (iconst_u _ 0))) 124 (if-let c (truthy v)) 125 (if-let (value_type (ty_int_ref_scalar_64 ty)) c) 126 (ne cty c (iconst_u ty 0))) 127 128 129 130;; (sextend (bmask x)) can be replaced with (bmask x) since bmask 131;; supports any size of output type, regardless of input. 132;; Same with `ireduce` 133(rule (simplify (sextend ty (bmask _ x))) (bmask ty x)) 134(rule (simplify (ireduce ty (bmask _ x))) (bmask ty x)) 135 136;; (bswap (bswap x)) == x 137(rule (simplify (bswap ty (bswap ty x))) (subsume x)) 138 139;; (bitrev (bitrev x)) == x 140(rule (simplify (bitrev ty (bitrev ty x))) (subsume x)) 141 142;; WebAssembly doesn't have a native byte-swapping instruction at this time so 143;; languages which have a byte-swapping operation will compile it down to bit 144;; shifting and twiddling. This attempts to pattern match what LLVM currently 145;; generates today for the Rust code `a.swap_bytes()`. This might be a bit 146;; brittle over time and/or with other possible LLVM backend optimizations, but 147;; it's at least one way to generate a byte swap. 148;; 149;; Technically this could be permuted quite a few ways and currently there's no 150;; easy way to match all of them, so only one is matched here. 151(rule (simplify (bor ty @ $I32 152 (bor ty 153 (ishl ty x (iconst_u ty 24)) 154 (ishl ty 155 (band ty x (iconst_u ty 0xff00)) 156 (iconst_u ty 8))) 157 (bor ty 158 (band ty 159 (ushr ty x (iconst_u ty 8)) 160 (iconst_u ty 0xff00)) 161 (ushr ty x (iconst_u ty 24))))) 162 (bswap ty x)) 163 164(rule (simplify (bor ty @ $I64 165 (bor ty 166 (bor ty 167 (ishl ty x (iconst_u ty 56)) 168 (ishl ty 169 (band ty x (iconst_u ty 0xff00)) 170 (iconst_u ty 40))) 171 (bor ty 172 (ishl ty 173 (band ty x (iconst_u ty 0xff_0000)) 174 (iconst_u ty 24)) 175 (ishl ty 176 (band ty x (iconst_u ty 0xff00_0000)) 177 (iconst_u ty 8)))) 178 (bor ty 179 (bor ty 180 (band ty 181 (ushr ty x (iconst_u ty 8)) 182 (iconst_u ty 0xff00_0000)) 183 (band ty 184 (ushr ty x (iconst_u ty 24)) 185 (iconst_u ty 0xff_0000))) 186 (bor ty 187 (band ty 188 (ushr ty x (iconst_u ty 40)) 189 (iconst_u ty 0xff00)) 190 (ushr ty x (iconst_u ty 56)))))) 191 (bswap ty x)) 192 193(rule (simplify (bxor ty (bor ty x y) (band ty x y))) (bxor ty x y)) 194 195 196(rule (simplify (bor ty (bor ty x y) x)) (bor ty x y)) 197(rule (simplify (bor ty (bor ty x y) y)) (bor ty x y)) 198(rule (simplify (bor ty x (bor ty x y))) (bor ty x y)) 199(rule (simplify (bor ty y (bor ty x y))) (bor ty x y)) 200 201(rule (simplify (band ty (band ty x y) x)) (band ty x y)) 202(rule (simplify (band ty (band ty x y) y)) (band ty x y)) 203(rule (simplify (band ty x (band ty x y))) (band ty x y)) 204(rule (simplify (band ty y (band ty x y))) (band ty x y)) 205 206;; (x ^ ~y) & x --> x & y 207(rule (simplify (band ty (bxor ty x (bnot ty y)) x)) (band ty x y)) 208(rule (simplify (band ty (bxor ty (bnot ty y) x) x)) (band ty x y)) 209(rule (simplify (band ty x (bxor ty x (bnot ty y)))) (band ty x y)) 210(rule (simplify (band ty x (bxor ty (bnot ty y) x))) (band ty x y)) 211 212; (x & y) + (x ^ y) --> x | y 213(rule (simplify (iadd ty (band ty x y) (bxor ty x y))) (bor ty x y)) 214(rule (simplify (iadd ty (bxor ty x y) (band ty x y))) (bor ty x y)) 215 216; (x | y) + (x & y) --> x + y 217(rule (simplify (iadd ty (bor ty x y) (band ty x y))) (iadd ty x y)) 218(rule (simplify (iadd ty (band ty x y) (bor ty x y))) (iadd ty x y)) 219 220; (x & y) | x --> x 221(rule (simplify (bor ty (band ty x y) x)) x) 222(rule (simplify (bor ty x (band ty x y))) x) 223 224; (x ^ y) ^ y --> x 225(rule (simplify (bxor ty (bxor ty x y) y)) x) 226(rule (simplify (bxor ty y (bxor ty x y))) x) 227 228; (x & y) | ~x -> y | ~x 229(rule (simplify (bor ty (band ty x y) (bnot ty x))) (bor ty y (bnot ty x))) 230(rule (simplify (bor ty (bnot ty x) (band ty x y))) (bor ty y (bnot ty x))) 231 232