1;; rewrites for integer and floating-point arithmetic
2;; eg: `iadd`, `isub`, `ineg`, `imul`, `fadd`, `fsub`, `fmul`
3
4;; For commutative instructions, we depend on cprop.isle pushing immediates to
5;; the right, and thus only simplify patterns like `x+0`, not `0+x`.
6
7;; x+0 == x.
8(rule (simplify (iadd ty
9                      x
10                      (iconst ty (u64_from_imm64 0))))
11      (subsume x))
12;; x-0 == x.
13(rule (simplify (isub ty
14                      x
15                      (iconst ty (u64_from_imm64 0))))
16      (subsume x))
17;; 0-x == (ineg x).
18(rule (simplify (isub ty
19                      (iconst ty (u64_from_imm64 0))
20                      x))
21      (ineg ty x))
22
23;; x + -y == -y + x == -(y - x) == x - y
24(rule (simplify (iadd ty x (ineg ty y)))
25      (isub ty x y))
26(rule (simplify (iadd ty (ineg ty y) x))
27      (isub ty x y))
28(rule (simplify (ineg ty (isub ty y x)))
29      (isub ty x y))
30;; x - -y == x + y
31(rule (simplify (isub ty x (ineg ty y)))
32      (iadd ty x y))
33
34;; ineg(ineg(x)) == x.
35(rule (simplify (ineg ty (ineg ty x))) (subsume x))
36
37;; ineg(x) * ineg(y) == x*y.
38(rule (simplify (imul ty (ineg ty x) (ineg ty y)))
39      (subsume (imul ty x y)))
40
41;; iabs(ineg(x)) == iabs(x).
42(rule (simplify (iabs ty (ineg ty x)))
43      (iabs ty x))
44
45;; iabs(iabs(x)) == iabs(x).
46(rule (simplify (iabs ty inner @ (iabs ty x)))
47      (subsume inner))
48
49;; x-x == 0.
50(rule (simplify (isub (fits_in_64 (ty_int ty)) x x)) (subsume (iconst ty (imm64 0))))
51
52;; x*1 == x.
53(rule (simplify (imul ty
54                      x
55                      (iconst ty (u64_from_imm64 1))))
56      (subsume x))
57
58;; x*0 == 0.
59(rule (simplify (imul ty
60                      _
61                      zero @ (iconst ty (u64_from_imm64 0))))
62      (subsume zero))
63
64;; x*-1 == ineg(x).
65(rule (simplify (imul ty x (iconst ty c)))
66      (if-let -1 (i64_sextend_imm64 ty c))
67      (ineg ty x))
68
69;; (!x) + 1 == ineg(x)
70(rule (simplify (iadd ty (bnot ty x) (iconst ty (u64_from_imm64 1))))
71      (ineg ty x))
72
73;; !(x - 1) == !(x + (-1)) == ineg(x)
74(rule (simplify (bnot ty (isub ty x (iconst ty (u64_from_imm64 1)))))
75      (ineg ty x))
76(rule (simplify (bnot ty (iadd ty x (iconst ty c))))
77      (if-let -1 (i64_sextend_imm64 ty c))
78      (ineg ty x))
79
80;; x/1 == x.
81(rule (simplify (sdiv ty
82                      x
83                      (iconst ty (u64_from_imm64 1))))
84      (subsume x))
85(rule (simplify (udiv ty
86                      x
87                      (iconst ty (u64_from_imm64 1))))
88      (subsume x))
89
90;; TODO: strength reduction: div to shifts
91;; TODO: div/rem by constants -> magic multiplications
92
93;; x*2 == x+x.
94(rule (simplify (imul ty x (iconst _ (simm32 2))))
95      (iadd ty x x))
96
97;; x*c == x<<log2(c) when c is a power of two.
98;; Note that the type of `iconst` must be the same as the type of `imul`,
99;; so these rules can only fire in situations where it's safe to construct an
100;; `iconst` of that type.
101(rule (simplify (imul ty x (iconst _ (imm64_power_of_two c))))
102      (ishl ty x (iconst ty (imm64 c))))
103(rule (simplify (imul ty (iconst _ (imm64_power_of_two c)) x))
104      (ishl ty x (iconst ty (imm64 c))))
105
106;; fneg(fneg(x)) == x.
107(rule (simplify (fneg ty (fneg ty x))) (subsume x))
108
109;; If both of the multiplied arguments to an `fma` are negated then remove
110;; both of them since they cancel out.
111(rule (simplify (fma ty (fneg ty x) (fneg ty y) z))
112      (fma ty x y z))
113
114;; If both of the multiplied arguments to an `fmul` are negated then remove
115;; both of them since they cancel out.
116(rule (simplify (fmul ty (fneg ty x) (fneg ty y)))
117      (fmul ty x y))
118
119;; (a op (b op (c op d))) ==> ((a op b) op (c op d))
120;;
121;; and
122;;
123;; (((a op b) op c) op d) ==> ((a op b) op (c op d))
124;;
125;; where `op` is an associative operation: `iadd`, `imul`, `band`, or `bxor`.
126;;
127;; This increases instruction-level parallelism and shrinks live ranges. It also
128;; canonicalizes into the shallow-and-wide form for reassociating constants
129;; together for cprop.
130;;
131;; NB: We subsume to avoid exponential e-node blow up due to reassociating very
132;; large chains of operations.
133;;
134;; TODO: We should add `bor` rules for this as well. Unfortunately, they
135;; conflict with our `bswap` recognizing rules when we `subsume`.
136
137(rule (simplify (iadd ty a (iadd ty b (iadd ty c d))))
138      (subsume (iadd ty (iadd ty a b) (iadd ty c d))))
139(rule (simplify (iadd ty (iadd ty (iadd ty a b) c) d))
140      (subsume (iadd ty (iadd ty a b) (iadd ty c d))))
141
142(rule (simplify (imul ty a (imul ty b (imul ty c d))))
143      (subsume (imul ty (imul ty a b) (imul ty c d))))
144(rule (simplify (imul ty (imul ty (imul ty a b) c) d))
145      (subsume (imul ty (imul ty a b) (imul ty c d))))
146
147(rule (simplify (band ty a (band ty b (band ty c d))))
148      (subsume (band ty (band ty a b) (band ty c d))))
149(rule (simplify (band ty (band ty (band ty a b) c) d))
150      (subsume (band ty (band ty a b) (band ty c d))))
151
152(rule (simplify (bxor ty a (bxor ty b (bxor ty c d))))
153      (subsume (bxor ty (bxor ty a b) (bxor ty c d))))
154(rule (simplify (bxor ty (bxor ty (bxor ty a b) c) d))
155      (subsume (bxor ty (bxor ty a b) (bxor ty c d))))
156