src/rules/correctness/pick.bend
bolt@1.24.0.0 · 374 lines · 0 definitions
1# rule pick: a def calls itself in a branch of a `Bool.pick`. Bool.pick is a
2# function, so both branches are evaluated whatever the condition. In both
3# branches, two recursive calls a step is 2^n work where one was meant (a
4# per-token scan that took 20 s this way took 20 ms as one pass): bind the
5# call once above the pick (`+more = go(rest)`) and pick between `x <> more`
6# and `more`. In one branch, the recursion runs even when the other branch
7# was the answer: a search never stops early and walks the whole input
8# (portal-bend's `get`, bendoom's sorted insert). Match on the Bool instead,
9# in a helper that takes it as a parameter. A self-call is the def's name
10# followed by `(..)`: a parameter or a value named like the def is not one. A
11# pick nested in a branch of one already reported is not reported again; one
12# nested in its condition is. A
13# search can hide the same bug by binding its recursion above the pick
14# (`+more = go(rest)`, then `Bool.pick(T, hit, x, more)`): the walk still runs
15# when the head is the answer (ez's `text.at`, native 8.81 s -> 4.15 s once it
16# stopped). `search` reports that let, when the first statement after it in
17# the same chain that reads the name is a pick alone that reads it only in
18# its else branch: a filter, which reads it in both, is not a search. A
19# do-bind, a let and a pick in different case arms, and a self-call that
20# holds a pick on the same condition (which makes the call cheap on purpose)
21# are left alone. The fix is to carry the test as a Bool into the next call
22# and `match hit` first when the else branch is the bound name alone (a tail
23# call), else a helper that matches on the condition; not a `Lazy` thunk,
24# which stops early but leaves the loop on every step. rules.bend runs
25# `check` and `search` both, as one rule. A
26# law file, a proof file and a def that is a proof never run, so they are
27# exempt: a def that returns a proof, or one written with no type at all
28# (`def f(x, y):`), which fills the law named f.
29import Base
30import bolt@1.24.0.0/src/src.bend as Src
31import bolt@1.24.0.0/src/finding.bend as F
32import bolt@1.24.0.0/src/syntax/lex.bend as Lex
33import bolt@1.24.0.0/src/syntax/tree.bend as Tree
34import bolt@1.24.0.0/src/rules/calls.bend as Calls
35import bolt@1.24.0.0/src/lazy/lazy.bend as Lazy
36
37# do both branches (the third and fourth arguments) call the def?
38def both(+as: List<&2, Tree.Node>, +name: String) -> Bool:
39 Bool.and(Calls.calls(Calls.arg(as, 2n), name), Calls.calls(Calls.arg(as, 3n), name))
40
41# does either branch call the def?
42def once(+as: List<&2, Tree.Node>, +name: String) -> Bool:
43 Bool.or(Calls.calls(Calls.arg(as, 2n), name), Calls.calls(Calls.arg(as, 3n), name))
44
45# is argument nth of a group quiet: the group's own quiet, or, in a branch
46# (the third or fourth argument) of a reported pick, hushed
47def mute(+quiet: Bool, +hush: Bool, nth: Nat) -> Bool:
48 match nth:
49 case 0n:
50 quiet
51 case 1n:
52 quiet
53 case 2n:
54 Bool.or(quiet, hush)
55 case 3n:
56 Bool.or(quiet, hush)
57 case 4n+p:
58 quiet
59
60# the argument a token leaves the walk in: one further past a top-level comma
61def next(kk: Lex.TokKind, nth: Nat) -> Nat:
62 match kk:
63 case Lex.TComma{}:
64 1n+nth
65 case other:
66 nth
67
68# every `Bool.pick(..)` in a chain, at any depth, that recurses in both
69# branches or in one. The chain is argument nth of a group with quiet
70# (inside a branch of a reported pick) and hush (the group is a reported
71# pick, so its branches are quiet); a pick in the condition still counts.
72def walk(nn: Tree.Node, +name: String, +path: String, +quiet: Bool, +hush: Bool, +nth: Nat) -> List<&2, F.Finding>:
73 match nn:
74 case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{open, +kids, close}, rest}}:
75 +at = next(k, nth)
76 +q = mute(quiet, hush, at)
77 +as = Calls.args(kids)
78 +ispick = String.eq(t, "Bool.pick")
79 +two = Bool.and(Bool.and(ispick, Bool.not(q)), both(as, name))
80 +one = Bool.and(Bool.and(ispick, Bool.not(two)), Bool.and(Bool.not(q), once(as, name)))
81 +more = List.concat(&2, F.Finding, [walk(kids, name, path, q, Bool.or(two, one), 0n),
82 walk(rest, name, path, quiet, hush, at)])
83 Bool.pick(List<&2, F.Finding>, two,
84 F.Finding{path, l, c, 9, "pick",
85 name ++ " calls itself in both branches of Bool.pick, which evaluates both, so both calls run; bind the call once above the pick."}
86 <> more,
87 Bool.pick(List<&2, F.Finding>, one,
88 F.Finding{path, l, c, 9, "pick",
89 name ++ " calls itself in one branch of Bool.pick, which evaluates both, so the call always runs and never exits early; branch with `match` on the condition instead."}
90 <> more,
91 more))
92 case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}:
93 walk(rest, name, path, quiet, hush, next(k, nth))
94 case Tree.NCons{Tree.Group{open, kids, close}, rest}:
95 List.concat(&2, F.Finding, [walk(kids, name, path, mute(quiet, hush, nth), False{}, 0n),
96 walk(rest, name, path, quiet, hush, nth)])
97 case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
98 List.concat(&2, F.Finding, [walk(kids, name, path, mute(quiet, hush, nth), False{}, 0n),
99 walk(body, name, path, mute(quiet, hush, nth), False{}, 0n), walk(rest, name, path, quiet, hush, nth)])
100 case Tree.NCons{h, rest}:
101 walk(rest, name, path, quiet, hush, nth)
102 case other:
103 Nil{}
104
105# every reported pick in a chain walked at quiet, outside any pick's arguments
106def picks(nn: Tree.Node, +name: String, +path: String, +quiet: Bool) -> List<&2, F.Finding>:
107 walk(nn, name, path, quiet, False{}, 0n)
108
109def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>:
110 match ds:
111 case Nil{}:
112 List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
113 case Con{Calls.Def{+name, +sig, body}, rest}:
114 check.go(rest, path,
115 Lazy.stop(List<&2, F.Finding>, Calls.exempt(path, sig), [],
116 _u => picks(body, name, path, False{})) <> acc)
117
118# the rule
119def check(ss: Src.Src) -> List<&2, F.Finding>:
120 Src.Src{path, text, toks, tree, bound, items} = ss
121 check.go(Calls.defs(tree), path, [])
122
123# A search bound above its pick (laws/PickReportsBoundSearches.bend). In one
124# chain of statements (a def's body, or one case arm's), a let `x = name(..)`
125# or `+x = name(..)` of nothing but a self-call, and the first statement
126# after it that reads x a `Bool.pick(..)` alone, whose condition and then
127# branch do not read x and whose else branch does: a first-match search
128# whose walk runs even when the head is the answer. A do-bind (`x <- ..`), a
129# let and a pick in different arms, and a self-call that holds a
130# `Bool.pick` on the pick's own condition (it makes the call cheap on
131# purpose) are left alone.
132
133# does a name leaf under the node spell xx?
134def search.reads(nn: Tree.Node, +xx: String) -> Bool:
135 match nn:
136 case Tree.Leaf{Lex.Tok{k, +t, _l, _c}}:
137 Bool.and(Lex.is_name(k), String.eq(t, xx))
138 case Tree.Group{_o, kids, _cl}:
139 search.reads(kids, xx)
140 case Tree.Stmt{_k, kids, body}:
141 +a = search.reads(kids, xx)
142 +b = search.reads(body, xx)
143 Bool.or(a, b)
144 case Tree.NCons{h, t}:
145 +a = search.reads(h, xx)
146 +b = search.reads(t, xx)
147 Bool.or(a, b)
148 case Tree.NNil{}:
149 False{}
150
151# the node's tokens, each then a space (a group's open, not its close)
152def search.text(nn: Tree.Node) -> String:
153 match nn:
154 case Tree.Leaf{Lex.Tok{_k, t, _l, _c}}:
155 t ++ " "
156 case Tree.Group{Lex.Tok{_k, o, _l, _c}, kids, _cl}:
157 o ++ " " ++ search.text(kids)
158 case Tree.Stmt{_k, kids, body}:
159 +a = search.text(kids)
160 +b = search.text(body)
161 a ++ b
162 case Tree.NCons{h, t}:
163 +a = search.text(h)
164 +b = search.text(t)
165 a ++ b
166 case Tree.NNil{}:
167 ""
168
169# does a `Bool.pick(..)` under the node, at any depth, have the condition
170# whose text is cond?
171def search.cheap(nn: Tree.Node, +cond: String) -> Bool:
172 match nn:
173 case Tree.NCons{Tree.Leaf{Lex.Tok{_k, +t, _l, _c}}, Tree.NCons{Tree.Group{Lex.Tok{_ko, +o, _lo, _co}, +kids, _cl},
174 rest}}:
175 +here = Bool.and(Bool.and(String.eq(t, "Bool.pick"), String.eq(o, "(")),
176 String.eq(search.text(Calls.arg(Calls.args(kids), 1n)), cond))
177 +a = search.cheap(kids, cond)
178 +b = search.cheap(rest, cond)
179 Bool.or(here, Bool.or(a, b))
180 case Tree.Group{_o, kids, _cl}:
181 search.cheap(kids, cond)
182 case Tree.Stmt{_k, kids, body}:
183 +a = search.cheap(kids, cond)
184 +b = search.cheap(body, cond)
185 Bool.or(a, b)
186 case Tree.NCons{h, t}:
187 +a = search.cheap(h, cond)
188 +b = search.cheap(t, cond)
189 Bool.or(a, b)
190 case _other:
191 False{}
192
193# is the chain empty?
194def search.empty(nn: Tree.Node) -> Bool:
195 match nn:
196 case Tree.NNil{}:
197 True{}
198 case _other:
199 False{}
200
201# is the chain the one name xx alone?
202def search.lone(nn: Tree.Node, +xx: String) -> Bool:
203 match nn:
204 case Tree.NCons{Tree.Leaf{Lex.Tok{_k, +t, _l, _c}}, rest}:
205 Bool.and(String.eq(t, xx), search.empty(rest))
206 case _other:
207 False{}
208
209# the finding at the bound self-call; tail: the else branch is the bound
210# name alone, so the call can carry the test instead
211def search.cite(+ll: U32, +cc: U32, +name: String, +path: String, tail: Bool) -> F.Finding:
212 match tail:
213 case True{}:
214 F.Finding{path, ll, cc, U32.from_nat(String.length(name)), "pick",
215 name ++ " binds its own call above a Bool.pick that reads it only in the else branch, so the walk runs even when the condition holds and the search never stops early; carry the test as a Bool into the next call (`go(rest, k, test(h))`) and `match hit` first, so the search stops and stays a loop."}
216 case False{}:
217 F.Finding{path, ll, cc, U32.from_nat(String.length(name)), "pick",
218 name ++ " binds its own call above a Bool.pick that reads it only in the else branch, so the walk runs even when the condition holds and the search never stops early; branch with `match` on the condition in a helper that takes it as a parameter, so the call runs only in the branch that needs it."}
219
220# the statement that reads the bound name first: a finding when it is a
221# `Bool.pick(..)` alone that reads the name only in its else branch, and the
222# self-call (its arguments args) holds no pick on the same condition
223def search.judge(
224 ss: Tree.Node,
225 +xx: String,
226 +args: Tree.Node,
227 +ll: U32,
228 +cc: U32,
229 +name: String,
230 +path: String
231) -> List<&2, F.Finding>:
232 match ss:
233 case Tree.Stmt{_k, Tree.NCons{Tree.Leaf{Lex.Tok{_kt, +t, _lt, _ct}}, Tree.NCons{Tree.Group{Lex.Tok{_ko, +o, _lo,
234 _co}, +kids, _cl}, after}}, _body}:
235 +as = Calls.args(kids)
236 +cond = Calls.arg(as, 1n)
237 +yes = Calls.arg(as, 2n)
238 +no = Calls.arg(as, 3n)
239 +shape = Bool.and(Bool.and(String.eq(t, "Bool.pick"), String.eq(o, "(")), search.empty(after))
240 +only = Bool.and(Bool.not(Bool.or(search.reads(cond, xx), search.reads(yes, xx))), search.reads(no, xx))
241 Bool.pick(List<&2, F.Finding>,
242 Bool.and(Bool.and(shape, only), Bool.not(search.cheap(args, search.text(cond)))),
243 [search.cite(ll, cc, name, path, search.lone(no, xx))], [])
244 case _other:
245 []
246
247# the first statement of the chain that reads xx, the chain's end (NNil)
248# when none does; hit: prev, the one before the chain, did
249def search.first(nn: Tree.Node, +xx: String, prev: Tree.Node, hit: Bool) -> Tree.Node:
250 match nn:
251 case Tree.NCons{+h, t}:
252 match hit:
253 case True{}:
254 prev
255 case False{}:
256 search.first(t, xx, h, search.reads(h, xx))
257 case _other:
258 match hit:
259 case True{}:
260 prev
261 case False{}:
262 Tree.NNil{}
263
264# past the bound name, `=` and the callee: a `(` group and nothing after it,
265# and then the finding the first reader of the name gives
266def search.call(
267 kx: Lex.TokKind,
268 +xx: String,
269 +ee: String,
270 +nn: String,
271 +ll: U32,
272 +cc: U32,
273 r3: Tree.Node,
274 rest: Tree.Node,
275 +name: String,
276 +path: String
277) -> List<&2, F.Finding>:
278 match r3:
279 case Tree.NCons{Tree.Group{Lex.Tok{_ko, +o, _lo, _co}, +args, _cl}, after}:
280 +ok = Bool.and(Bool.and(Lex.is_name(kx), String.eq(ee, "=")),
281 Bool.and(Bool.and(String.eq(nn, name), String.eq(o, "(")), search.empty(after)))
282 Lazy.stop(List<&2, F.Finding>, Bool.not(ok), [],
283 _u => search.judge(search.first(rest, xx, Tree.NNil{}, False{}), xx, args, ll, cc, name, path))
284 case _other:
285 []
286
287# past the bound name and `=`: the leaf that names the call
288def search.callee(
289 kx: Lex.TokKind,
290 +xx: String,
291 +ee: String,
292 r2: Tree.Node,
293 rest: Tree.Node,
294 +name: String,
295 +path: String
296) -> List<&2, F.Finding>:
297 match r2:
298 case Tree.NCons{Tree.Leaf{Lex.Tok{_kn, +n, +l, +c}}, r3}:
299 search.call(kx, xx, ee, n, l, c, r3, rest, name, path)
300 case _other:
301 []
302
303# past the bound name: the leaf that should be `=`
304def search.eq(
305 kx: Lex.TokKind,
306 +xx: String,
307 r1: Tree.Node,
308 rest: Tree.Node,
309 +name: String,
310 +path: String
311) -> List<&2, F.Finding>:
312 match r1:
313 case Tree.NCons{Tree.Leaf{Lex.Tok{_ke, +e, _le, _ce}}, r2}:
314 search.callee(kx, xx, e, r2, rest, name, path)
315 case _other:
316 []
317
318# a let's own tokens past any `+`: the leaf of the bound name
319def search.bound(nn: Tree.Node, rest: Tree.Node, +name: String, +path: String) -> List<&2, F.Finding>:
320 match nn:
321 case Tree.NCons{Tree.Leaf{Lex.Tok{kx, +x, _lx, _cx}}, r1}:
322 search.eq(kx, x, r1, rest, name, path)
323 case _other:
324 []
325
326# a let's own tokens, a leading `+` skipped
327def search.lead(kids: Tree.Node, rest: Tree.Node, +name: String, +path: String) -> List<&2, F.Finding>:
328 match kids:
329 case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, +more}:
330 search.bound(Bool.pick(Tree.Node, String.eq(t, "+"), more, Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, more}),
331 rest, name, path)
332 case _other:
333 []
334
335# a statement of the kind and own tokens, the chain after it rest: a let is
336# read, anything else gives nothing
337def search.stmt(
338 kind: Tree.StmtKind,
339 kids: Tree.Node,
340 rest: Tree.Node,
341 +name: String,
342 +path: String
343) -> List<&2, F.Finding>:
344 match kind:
345 case Tree.SLet{}:
346 search.lead(kids, rest, name, path)
347 case _other:
348 []
349
350# every search bound above its pick in a chain of statements and in the
351# chains under them
352def search.walk(nn: Tree.Node, +name: String, +path: String) -> List<&2, F.Finding>:
353 match nn:
354 case Tree.NCons{Tree.Stmt{kind, kids, body}, +rest}:
355 List.concat(&2, F.Finding, [search.stmt(kind, kids, rest, name, path), search.walk(body, name, path),
356 search.walk(rest, name, path)])
357 case Tree.NCons{_h, rest}:
358 search.walk(rest, name, path)
359 case _other:
360 Nil{}
361
362def search.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>:
363 match ds:
364 case Nil{}:
365 List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
366 case Con{Calls.Def{+name, +sig, body}, rest}:
367 search.go(rest, path,
368 Lazy.stop(List<&2, F.Finding>, Calls.exempt(path, sig), [], _u => search.walk(body, name, path)) <> acc)
369
370# the rule's other half, run beside check: every search bound above its
371# pick, def by def
372def search(ss: Src.Src) -> List<&2, F.Finding>:
373 Src.Src{path, text, toks, tree, bound, items} = ss
374 search.go(Calls.defs(tree), path, [])