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.
10	import Base
11	import bend-lint-api@0.2.0.0/linter/lint.bend as Lint
12	import bend-lint-api@0.2.0.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.
20	type Owner is Data:
21	  Owner{loops: List<&2, String>, target: String, name: String, fixed: List<&2, U32>}
22	
23	# Functions
24	# =========
25	def 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	
31	def 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`.
35	def 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.
68	def 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	
79	def 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`.
87	def 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.
98	def 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.
118	def 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.
143	def 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`.
165	def 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`).
186	def 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	
195	def 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	
202	# Whether the branch a node below `path` is in calls `target` again, if `found`.
203	def repeats.if(found: Bool, path: List<&2, Lint.Above>, target: String) -> Bool:
204	  match found:
205	    case True{}:
206	      repeats(branch(path, None{}), target)
207	    case False{}:
208	      False{}
209	
210	def visit(+owner: Owner, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, Lint.Finding>:
211	  match owner node:
212	    case Owner{
213	      loops,
214	      +target,
215	      name,
216	      fixed
217	    } Lint.Node{
218	      Lint.Application{},
219	      n,
220	      span,
221	      Con{Lint.Node{Lint.Reference{+t}, callee, rs, rk, rf}, args},
222	      facts
223	    }:
224	      Lint.finding(
225	        Lint.Information{},
226	        repeats.if(
227	          invariant(
228	            64n,
229	            args,
230	            fixed,
231	            Bool.not(String.eq(t, target)) && List.contains(~String, ~String.eq, loops, t)
232	          )
233	            && Lint.is_live(path),
234	          path,
235	          target
236	        ),
237	        span,
238	        message(callee, name)
239	      )
240	    case _ _:
241	      []
242	
243	# Whether a definition's nodes say it is a proof: it has no return type written (it fills a law), or it returns an
244	# equality.
245	def is_proof(nodes: List<&2, Lint.Node>) -> Bool:
246	  match nodes:
247	    case Nil{}:
248	      True{}
249	    case Con{
250	      Lint.Node{Lint.Returns{}, n, s, Con{Lint.Node{Lint.Equality{}, en, es, ek, ef}, k}, f},
251	      rest
252	    }:
253	      True{}
254	    case Con{Lint.Node{Lint.Returns{}, n, s, k, f}, rest}:
255	      False{}
256	    case Con{node, rest}:
257	      is_proof(rest)
258	
259	# The findings in the definition `owner`, unless it is `skipped`.
260	def defs.if(skipped: Bool, loops: List<&2, String>, +owner: Lint.Node) -> List<&2, Lint.Finding>:
261	  match skipped:
262	    case True{}:
263	      []
264	    case False{}:
265	      Lint.visit(~Owner, ~Lint.Finding, ~visit, Owner.of(loops, owner), [owner])
266	
267	def defs(
268	  nodes: List<&2, Lint.Node>,
269	  +loops: List<&2, String>,
270	  out: List<&2, Lint.Finding>
271	) -> List<&2, Lint.Finding>:
272	  match nodes:
273	    case Nil{}:
274	      List.reverse(&2, Lint.Finding, out)
275	    case Con{Lint.Node{Lint.Definition{+t, u}, n, s, +k, f}, rest}:
276	      owner = {Lint.Node{Lint.Definition{t, u}, n, s, k, f}: Lint.Node}
277	      defs(
278	        rest,
279	        loops,
280	        Lists.onto(
281	          &2,
282	          Lint.Finding,
283	          defs.if(
284	            Bool.not(List.contains(~String, ~String.eq, loops, t)) || is_proof(k),
285	            loops,
286	            owner
287	          ),
288	          out
289	        )
290	      )
291	    case Con{node, rest}:
292	      defs(rest, loops, out)
293	
294	def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
295	  +nodes = Lint.Here.nodes(here)
296	  Lint.done(defs(nodes, loops(nodes, []), []))
297	
298	def rule() -> Lint.Rule:
299	  Lint.Rule{Lint.Needs{False{}, False{}}, [], Lint.OnFile{run}}