src/rules/correctness/pick.bend
bolt@1.22.0.0 · 108 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# law file, a proof file and a def that is a proof never run, so they are
14# exempt: a def that returns a proof, or one written with no type at all
15# (`def f(x, y):`), which fills the law named f.
16import Base
17import bolt@1.22.0.0/src/src.bend as Src
18import bolt@1.22.0.0/src/finding.bend as F
19import bolt@1.22.0.0/src/syntax/lex.bend as Lex
20import bolt@1.22.0.0/src/syntax/tree.bend as Tree
21import bolt@1.22.0.0/src/rules/calls.bend as Calls
22import bolt@1.22.0.0/src/lazy/lazy.bend as Lazy
23
24# do both branches (the third and fourth arguments) call the def?
25def both(+as: List<&2, Tree.Node>, +name: String) -> Bool:
26 Bool.and(Calls.calls(Calls.arg(as, 2n), name), Calls.calls(Calls.arg(as, 3n), name))
27
28# does either branch call the def?
29def once(+as: List<&2, Tree.Node>, +name: String) -> Bool:
30 Bool.or(Calls.calls(Calls.arg(as, 2n), name), Calls.calls(Calls.arg(as, 3n), name))
31
32# is argument nth of a group quiet: the group's own quiet, or, in a branch
33# (the third or fourth argument) of a reported pick, hushed
34def mute(+quiet: Bool, +hush: Bool, nth: Nat) -> Bool:
35 match nth:
36 case 0n:
37 quiet
38 case 1n:
39 quiet
40 case 2n:
41 Bool.or(quiet, hush)
42 case 3n:
43 Bool.or(quiet, hush)
44 case 4n+p:
45 quiet
46
47# the argument a token leaves the walk in: one further past a top-level comma
48def next(kk: Lex.TokKind, nth: Nat) -> Nat:
49 match kk:
50 case Lex.TComma{}:
51 1n+nth
52 case other:
53 nth
54
55# every `Bool.pick(..)` in a chain, at any depth, that recurses in both
56# branches or in one. The chain is argument nth of a group with quiet
57# (inside a branch of a reported pick) and hush (the group is a reported
58# pick, so its branches are quiet); a pick in the condition still counts.
59def walk(nn: Tree.Node, +name: String, +path: String, +quiet: Bool, +hush: Bool, +nth: Nat) -> List<&2, F.Finding>:
60 match nn:
61 case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{open, +kids, close}, rest}}:
62 +at = next(k, nth)
63 +q = mute(quiet, hush, at)
64 +as = Calls.args(kids)
65 +ispick = String.eq(t, "Bool.pick")
66 +two = Bool.and(Bool.and(ispick, Bool.not(q)), both(as, name))
67 +one = Bool.and(Bool.and(ispick, Bool.not(two)), Bool.and(Bool.not(q), once(as, name)))
68 +more = List.concat(&2, F.Finding, [walk(kids, name, path, q, Bool.or(two, one), 0n),
69 walk(rest, name, path, quiet, hush, at)])
70 Bool.pick(List<&2, F.Finding>, two,
71 F.Finding{path, l, c, 9, "pick",
72 name ++ " calls itself in both branches of Bool.pick, which evaluates both, so both calls run; bind the call once above the pick."}
73 <> more,
74 Bool.pick(List<&2, F.Finding>, one,
75 F.Finding{path, l, c, 9, "pick",
76 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."}
77 <> more,
78 more))
79 case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}:
80 walk(rest, name, path, quiet, hush, next(k, nth))
81 case Tree.NCons{Tree.Group{open, kids, close}, rest}:
82 List.concat(&2, F.Finding, [walk(kids, name, path, mute(quiet, hush, nth), False{}, 0n),
83 walk(rest, name, path, quiet, hush, nth)])
84 case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
85 List.concat(&2, F.Finding, [walk(kids, name, path, mute(quiet, hush, nth), False{}, 0n),
86 walk(body, name, path, mute(quiet, hush, nth), False{}, 0n), walk(rest, name, path, quiet, hush, nth)])
87 case Tree.NCons{h, rest}:
88 walk(rest, name, path, quiet, hush, nth)
89 case other:
90 Nil{}
91
92# every reported pick in a chain walked at quiet, outside any pick's arguments
93def picks(nn: Tree.Node, +name: String, +path: String, +quiet: Bool) -> List<&2, F.Finding>:
94 walk(nn, name, path, quiet, False{}, 0n)
95
96def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>:
97 match ds:
98 case Nil{}:
99 List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
100 case Con{Calls.Def{+name, +sig, body}, rest}:
101 check.go(rest, path,
102 Lazy.stop(List<&2, F.Finding>, Calls.exempt(path, sig), [],
103 _u => picks(body, name, path, False{})) <> acc)
104
105# the rule
106def check(ss: Src.Src) -> List<&2, F.Finding>:
107 Src.Src{path, text, toks, tree, bound, items} = ss
108 check.go(Calls.defs(tree), path, [])