src/rules/suspicious/fuel.bend
bolt@1.19.0.0 · 183 lines · 0 definitions
1# rule fuel: a call to a def of the same file, its name then `(`, passes a
2# fixed number where that def takes its fuel: a Nat literal (`1000n`: digits,
3# then `n`), or `U32.to_nat` of a U32 literal (`U32.to_nat(100000)`: digits
4# alone), the form a big fuel is written in. A fuel parameter is known by its
5# name alone (its first lowercase name before the colon): `fuel`, `gas`,
6# `steps` or `budget`, or any name starting with `fuel`. The fuel-0 arm
7# returns what it has, so input past the number comes out cut short, with no
8# error (a JSON printer that stopped at 1000 tasks). A law is no safer: a law
9# proved over every fuel and then used at a big fixed one, against a goal
10# written another way, overflows the checker ("the machine stack overflowed",
11# bend 2.0.33 and 2.0.34; ez's lock walk at `U32.to_nat(100000)` did). Before
12# 2.0.29 the checker unrolled the fixed fuel and hung; 2.0.29 made a checked
13# recursion on a Nat literal linear. Derive the fuel from the input's size
14# (`Nat.mul(size, 4n)`) or take it as a parameter. A number of any size
15# counts, an exact repeat count such as `3n` included. Only an argument that
16# is the literal alone, or `U32.to_nat(` the U32 literal alone `)`, counts: a
17# let-bound literal and a parenthesized `(7n)` are not seen. A def's own calls
18# are exempt: its step passes `fuel - 1`, not a literal. So is a call to a
19# def that returns an effect: its header holds a top-level `->` token with
20# the capitalized name token `IO` right after it (`-> IO(Unit):`, parameters
21# wrapped over lines or not), or, when the `->` is the header's last token,
22# first on the line under it (`->` then `IO(Unit):`). An effect loop's fuel
23# bounds its reads, frames or retries, a budget the outside world sets, not
24# the size of an input it was handed (a netcode drain of 256 datagrams a
25# tick, a read of 100000 chunks).
26import Base
27import bolt@1.19.0.0/src/src.bend as Src
28import bolt@1.19.0.0/src/lazy/lazy.bend as Lazy
29import bolt@1.19.0.0/src/finding.bend as F
30import bolt@1.19.0.0/src/syntax/lex.bend as Lex
31import bolt@1.19.0.0/src/syntax/tree.bend as Tree
32import bolt@1.19.0.0/src/syntax/bind.bend as Bind
33import bolt@1.19.0.0/src/rules/calls.bend as Calls
34import bolt@1.19.0.0/src/rules/tokens.bend as T
35
36# a def of the file and the position of a fuel parameter
37type Fuel is Data:
38 Fuel{name: String, at: Nat}
39
40# is it a fuel parameter's name?
41def is_fuel(+nn: String) -> Bool:
42 Bool.or(String.starts_with(nn, "fuel"),
43 List.contains(~String, ~String.eq, ["gas", "steps", "budget"], nn))
44
45# the fuel parameters among a def's parameters, from position i on
46def fuels.params(ps: List<&2, Tree.Node>, +name: String, +ii: Nat) -> List<&2, Fuel>:
47 match ps:
48 case Nil{}:
49 Nil{}
50 case Con{p, rest}:
51 +more = fuels.params(rest, name, 1n+ii)
52 Bool.pick(List<&2, Fuel>, is_fuel(Calls.param_name(p)), Fuel{name, ii} <> more, more)
53
54# is the chain's first node the capitalized name `IO`?
55def effect.io(nn: Tree.Node) -> Bool:
56 match nn:
57 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, +t, l, c}}, rest}:
58 String.eq(t, "IO")
59 case other:
60 False{}
61
62# the kids of the first statement under a def: the line a header wrapped
63# after its `->` continues on (`->` then `IO(Unit):` on the next line)
64def under(body: Tree.Node) -> Tree.Node:
65 match body:
66 case Tree.NCons{Tree.Stmt{kind, kids, inner}, rest}:
67 kids
68 case other:
69 Tree.NNil{}
70
71# what follows an arrow: the rest of the header, or the line under it (below)
72# when the arrow ends the header; is it `IO`?
73def effect.next(rest: Tree.Node, +below: Tree.Node) -> Bool:
74 match rest:
75 case Tree.NCons{h, tail}:
76 effect.io(Tree.NCons{h, tail})
77 case other:
78 effect.io(below)
79
80# does a def's header return an effect: a top-level `->` with the
81# capitalized name `IO` right after it, on the next line (below) when the
82# arrow ends the header?
83def effect(sig: Tree.Node, +below: Tree.Node) -> Bool:
84 match sig:
85 case Tree.NCons{h, +rest}:
86 +more = effect(rest, below)
87 Bool.or(Bool.and(Calls.kind.leaf(~Calls.kind.arrow, h), effect.next(rest, below)), more)
88 case other:
89 False{}
90
91# the parameters a def's fuel may sit in: none when it returns an effect
92def slots(+sig: Tree.Node, body: Tree.Node) -> List<&2, Tree.Node>:
93 Bool.pick(List<&2, Tree.Node>, effect(sig, under(body)), [], Calls.params(sig))
94
95# every fuel parameter of every def of the file that returns no effect
96def fuels(ds: List<&2, Calls.Def>) -> List<&2, Fuel>:
97 match ds:
98 case Nil{}:
99 Nil{}
100 case Con{Calls.Def{name, sig, body}, rest}:
101 List.append(&2, Fuel, fuels.params(slots(sig, body), name, 0n), fuels(rest))
102
103# the group of a call at line ll, column cc, as a finding when it holds one
104# U32 literal alone (digits) and ok says the call is `U32.to_nat(`
105def converted(kids: Tree.Node, ok: Bool, +ll: U32, +cc: U32, +path: String) -> List<&2, F.Finding>:
106 match kids:
107 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}:
108 Bool.pick(List<&2, F.Finding>, Bool.and(ok, T.digits_ok(String.to_list(t))),
109 [F.Finding{path, ll, cc, U32.from_nat(Nat.add(String.length(t), 12n)), "fuel",
110 "The fuel is fixed at U32.to_nat(" ++ t
111 ++ "), so longer input is silently cut short; derive the fuel from the input size."}],
112 [])
113 case other:
114 Nil{}
115
116# an argument that is a Nat literal alone (digits, then `n`), or
117# `U32.to_nat` of a U32 literal alone, as a finding
118def literal(aa: Tree.Node, +path: String) -> List<&2, F.Finding>:
119 match aa:
120 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}:
121 Bool.pick(List<&2, F.Finding>, T.nat_ok(String.to_list(t)),
122 [F.Finding{path, l, c, U32.from_nat(String.length(t)), "fuel",
123 "The fuel is fixed at " ++ t ++ ", so longer input is silently cut short; derive the fuel from the input size."}],
124 [])
125 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TDotted{}, +t, l, c}},
126 Tree.NCons{Tree.Group{Lex.Tok{ok, +o, ol, oc}, kids, cl}, Tree.NNil{}}}:
127 converted(kids, Bool.and(String.eq(t, "U32.to_nat"), String.eq(o, "(")), l, c, path)
128 case other:
129 Nil{}
130
131# a call to name with these arguments, against every fuel parameter
132def call(fs: List<&2, Fuel>, +name: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
133 match fs:
134 case Nil{}:
135 Nil{}
136 case Con{Fuel{+fn, at}, rest}:
137 +more = call(rest, name, as, path)
138 Lazy.stop(List<&2, F.Finding>, Bool.not(String.eq(fn, name)), more,
139 _u => List.append(&2, F.Finding, literal(Calls.arg(as, at), path), more))
140
141# every call at any depth of a chain, but the def's own (self)
142def calls(nn: Tree.Node, +fs: List<&2, Fuel>, +self: String, +path: String) -> List<&2, F.Finding>:
143 match nn:
144 case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
145 +more = List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(rest, fs, self, path)])
146 +hit = Bool.and(Bool.and(Lex.is_name(k), String.eq(o, "(")), Bool.not(String.eq(t, self)))
147 Lazy.stop(List<&2, F.Finding>, Bool.not(hit), more,
148 _u => List.append(&2, F.Finding, call(fs, t, Calls.args(kids), path), more))
149 case Tree.NCons{Tree.Group{open, kids, close}, rest}:
150 List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(rest, fs, self, path)])
151 case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
152 List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(body, fs, self, path),
153 calls(rest, fs, self, path)])
154 case Tree.NCons{h, rest}:
155 calls(rest, fs, self, path)
156 case other:
157 Nil{}
158
159# a def's (or a law's) name, "" when it has none
160def own(mm: Maybe<&2, String>) -> String:
161 match mm:
162 case None{}:
163 ""
164 case Some{n}:
165 n
166
167# each top-level statement, walked as its own def
168def check.go(root: Tree.Node, +fs: List<&2, Fuel>, +path: String) -> List<&2, F.Finding>:
169 match root:
170 case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
171 +self = own(Bind.declared(kids))
172 +head = calls(kids, fs, self, path)
173 +inner = calls(body, fs, self, path)
174 List.concat(&2, F.Finding, [head, inner, check.go(rest, fs, path)])
175 case Tree.NCons{h, rest}:
176 check.go(rest, fs, path)
177 case other:
178 Nil{}
179
180# the rule
181def check(ss: Src.Src) -> List<&2, F.Finding>:
182 Src.Src{path, text, toks, +tree, bound, items} = ss
183 check.go(tree, fuels(Calls.defs(tree)), path)