performance/loop_invariant_call.bend
bend-lint-rules@0.1.1.0 · 281 lines · 0 definitions
1# performance/loop_invariant_call: a call that gets the same arguments on every step of a loop, so it
2# computes the same value each time: in a definition that calls itself, a call of a definition of the
3# file that loops too, in the branch that repeats (the one with the loop's call of itself), whose
4# arguments are literals, or parameters that the loop passes unchanged to each call of itself.
5# Heuristics: clang hoists plain arithmetic out of a loop (and folds constants), but not a call of a
6# definition that loops: Bend runs it through its own calls. Compute it once, before the loop, and pass
7# it as a parameter. A definition that does not call itself is cheap, and not reported. A proof (a
8# definition that fills a law, or returns an equality) does not run, and is skipped. A loop that repeats
9# work on purpose, such as a benchmark's, is the case to expect.
10import Base
11import bend-lint-api@0.1.1.0/linter/lint.bend as Lint
12import bend-lint-api@0.1.1.0/shared/lists.bend as Lists
13
14# Types
15# =====
16
17# What judging the calls of one definition reads: the definitions of the file that call themselves (as the check
18# names them), the definition (as the check names it, and as written), and its parameters that it passes unchanged
19# to each call of itself, by binder.
20type Owner is Data:
21 Owner{loops: List<&2, String>, target: String, name: String, fixed: List<&2, U32>}
22
23# Functions
24# =========
25def message(callee: String, loop: String) -> String:
26 callee
27 ++ " gets the same arguments on every step of "
28 ++ loop
29 ++ ", so it computes the same value each time: clang hoists plain arithmetic out of a loop, but not a call of a definition that loops. All lanes. Confidence: medium, as the gain is what the call costs. Compute it once before the loop, and pass it as a parameter. If the call is cheap, or the loop repeats it on purpose (a benchmark), expect this finding."
30
31def loop.visit(+u: Unit, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, Unit>:
32 Bool.pick(List<&2, Unit>, Lint.is_recursive(path, node), [Unit{}], [])
33
34# The definitions among `nodes` that call themselves, as the check names them, onto `out`.
35def loops(nodes: List<&2, Lint.Node>, out: List<&2, String>) -> List<&2, String>:
36 match nodes:
37 case Nil{}:
38 out
39 case Con{Lint.Node{Lint.Definition{+t, u}, n, s, k, f}, rest}:
40 loops(
41 rest,
42 Lists.push(
43 String,
44 Lists.when(
45 String,
46 Bool.not(
47 List.is_empty(
48 &2,
49 Unit,
50 Lint.visit(
51 ~Unit,
52 ~Unit,
53 ~loop.visit,
54 Unit{},
55 [Lint.Node{Lint.Definition{t, u}, n, s, k, f}]
56 )
57 )
58 ),
59 t
60 ),
61 out
62 )
63 )
64 case Con{node, rest}:
65 loops(rest, out)
66
67# The arguments of each call of the definition below `path` to itself.
68def self.visit(
69 +u: Unit,
70 +path: List<&2, Lint.Above>,
71 +node: Lint.Node
72) -> List<&2, List<&2, Lint.Node>>:
73 match node:
74 case Lint.Node{Lint.Application{}, n, s, Con{f, args}, fs}:
75 Bool.pick(List<&2, List<&2, Lint.Node>>, Lint.is_recursive(path, node), [args], [])
76 case _:
77 []
78
79def passed.at(arg: Maybe<&2, Lint.Node>, b: U32) -> Bool:
80 match arg:
81 case Some{Lint.Node{Lint.Variable{v}, n, s, k, f}}:
82 U32.is_eq(v, b)
83 case _:
84 False{}
85
86# Whether the argument at `at` of each of `calls` is the variable of `b`.
87def passed(calls: List<&2, List<&2, Lint.Node>>, +at: Nat, +b: U32, ok: Bool) -> Bool:
88 match calls ok:
89 case _ False{}:
90 False{}
91 case Nil{} True{}:
92 True{}
93 case Con{args, rest} True{}:
94 passed(rest, at, b, passed.at(List.get(&2, Lint.Node, args, at), b))
95
96# The runtime parameters among a definition's nodes that it passes unchanged to each of `calls` (its calls of itself),
97# by binder; `at` counts the runtime parameters, as the calls' arguments do.
98def fixed(
99 nodes: List<&2, Lint.Node>,
100 +calls: List<&2, List<&2, Lint.Node>>,
101 +at: Nat,
102 out: List<&2, U32>
103) -> List<&2, U32>:
104 match nodes:
105 case Nil{}:
106 out
107 case Con{Lint.Node{Lint.Parameter{+b, q}, n, s, k, f}, rest}:
108 fixed(
109 rest,
110 calls,
111 1n+at,
112 Lists.push(U32, Lists.when(U32, passed(calls, at, b, True{}), b), out)
113 )
114 case Con{node, rest}:
115 fixed(rest, calls, at, out)
116
117# What judging the calls of the definition `node` reads, with `loops`, the definitions of the file that call themselves.
118def Owner.of(loops: List<&2, String>, +node: Lint.Node) -> Owner:
119 match node:
120 case Lint.Node{Lint.Definition{+t, u}, +n, s, +k, f}:
121 Owner{
122 loops,
123 t,
124 n,
125 fixed(
126 k,
127 Lint.visit(
128 ~Unit,
129 ~List<&2, Lint.Node>,
130 ~self.visit,
131 Unit{},
132 [Lint.Node{Lint.Definition{t, u}, n, s, k, f}]
133 ),
134 0n,
135 []
136 )
137 }
138 case _:
139 Owner{loops, "", "", []}
140
141# Whether `nodes`, the arguments of a call, are the same on every step: literals, the variables of `fixed`, and calls,
142# annotations or constructions of those alone; `fuel` bounds the depth.
143def invariant(+fuel: Nat, nodes: List<&2, Lint.Node>, +fixed: List<&2, U32>, ok: Bool) -> Bool:
144 match fuel nodes ok:
145 case _ _ False{}:
146 False{}
147 case _ Nil{} True{}:
148 True{}
149 case 0n _ True{}:
150 False{}
151 case 1n+f Con{Lint.Node{Lint.Literal{t}, n, s, k, fs}, rest} True{}:
152 invariant(f, rest, fixed, True{})
153 case 1n+f Con{Lint.Node{Lint.Variable{v}, n, s, k, fs}, rest} True{}:
154 invariant(f, rest, fixed, List.contains(~U32, ~U32.is_eq, fixed, v))
155 case 1n+f Con{Lint.Node{Lint.Application{}, n, s, Con{h, args}, fs}, rest} True{}:
156 invariant(f, rest, fixed, invariant(f, args, fixed, True{}))
157 case 1n+f Con{Lint.Node{Lint.Annotation{}, n, s, Con{x, ts}, fs}, rest} True{}:
158 invariant(f, rest, fixed, invariant(f, [x], fixed, True{}))
159 case 1n+f Con{Lint.Node{Lint.Construction{t}, n, s, k, fs}, rest} True{}:
160 invariant(f, rest, fixed, invariant(f, k, fixed, True{}))
161 case 1n+f Con{x, rest} True{}:
162 False{}
163
164# Whether a call of `target` is among `nodes` or under them, or `found`.
165def has_call(nodes: List<&2, Lint.Node>, +target: String, found: Bool) -> Bool:
166 match nodes found:
167 case _ True{}:
168 True{}
169 case Nil{} False{}:
170 False{}
171 case Con{
172 Lint.Node{
173 Lint.Application{},
174 n,
175 s,
176 Con{Lint.Node{Lint.Reference{t}, rn, rs, rk, rf}, args},
177 f
178 },
179 rest
180 } False{}:
181 has_call(rest, target, has_call(args, target, String.eq(t, target)))
182 case Con{Lint.Node{syntax, n, s, kids, f}, rest} False{}:
183 has_call(rest, target, has_call(kids, target, False{}))
184
185# The branch a node below `path` is in: the innermost case above it, or the definition's body (the last of `path`).
186def branch(path: List<&2, Lint.Above>, last: Maybe<&2, Lint.Node>) -> Maybe<&2, Lint.Node>:
187 match path:
188 case Nil{}:
189 last
190 case Con{Lint.Above{Lint.Node{Lint.Case{}, n, s, k, f}, at}, rest}:
191 Some{Lint.Node{Lint.Case{}, n, s, k, f}}
192 case Con{Lint.Above{p, at}, rest}:
193 branch(rest, Some{p})
194
195def repeats(b: Maybe<&2, Lint.Node>, target: String) -> Bool:
196 match b:
197 case Some{node}:
198 has_call([node], target, False{})
199 case None{}:
200 False{}
201
202def visit(+owner: Owner, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, Lint.Finding>:
203 match owner node:
204 case Owner{
205 loops,
206 +target,
207 name,
208 fixed
209 } Lint.Node{
210 Lint.Application{},
211 n,
212 span,
213 Con{Lint.Node{Lint.Reference{+t}, callee, rs, rk, rf}, args},
214 facts
215 }:
216 Lint.finding(
217 Lint.Information{},
218 invariant(
219 64n,
220 args,
221 fixed,
222 Bool.not(String.eq(t, target)) && List.contains(~String, ~String.eq, loops, t)
223 )
224 && Lint.is_live(path)
225 && repeats(branch(path, None{}), target),
226 span,
227 message(callee, name)
228 )
229 case _ _:
230 []
231
232# Whether a definition's nodes say it is a proof: it has no return type written (it fills a law), or it returns an
233# equality.
234def is_proof(nodes: List<&2, Lint.Node>) -> Bool:
235 match nodes:
236 case Nil{}:
237 True{}
238 case Con{
239 Lint.Node{Lint.Returns{}, n, s, Con{Lint.Node{Lint.Equality{}, en, es, ek, ef}, k}, f},
240 rest
241 }:
242 True{}
243 case Con{Lint.Node{Lint.Returns{}, n, s, k, f}, rest}:
244 False{}
245 case Con{node, rest}:
246 is_proof(rest)
247
248def defs(
249 nodes: List<&2, Lint.Node>,
250 +loops: List<&2, String>,
251 out: List<&2, Lint.Finding>
252) -> List<&2, Lint.Finding>:
253 match nodes:
254 case Nil{}:
255 List.reverse(&2, Lint.Finding, out)
256 case Con{Lint.Node{Lint.Definition{+t, u}, n, s, +k, f}, rest}:
257 +owner = {Lint.Node{Lint.Definition{t, u}, n, s, k, f}: Lint.Node}
258 defs(
259 rest,
260 loops,
261 Lists.onto(
262 &2,
263 Lint.Finding,
264 Bool.pick(
265 List<&2, Lint.Finding>,
266 Bool.not(List.contains(~String, ~String.eq, loops, t)) || is_proof(k),
267 [],
268 Lint.visit(~Owner, ~Lint.Finding, ~visit, Owner.of(loops, owner), [owner])
269 ),
270 out
271 )
272 )
273 case Con{node, rest}:
274 defs(rest, loops, out)
275
276def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
277 +nodes = Lint.Here.nodes(here)
278 Lint.done(defs(nodes, loops(nodes, []), []))
279
280def rule() -> Lint.Rule:
281 Lint.Rule{Lint.Needs{False{}, False{}}, [], Lint.OnFile{run}}