src/rules/suspicious/fuel.bend
bolt@1.11.0.0 · 110 lines · 0 definitions
1# rule fuel: a call to a def of the same file, its name then `(`, passes a Nat
2# literal (`1000n`: digits, then `n`) where that def takes its fuel. A fuel
3# parameter is known by its name alone (its first lowercase name before the
4# colon): `fuel`, `gas`, `steps` or `budget`, or any name starting with
5# `fuel`. The fuel-0 arm returns what it has, so input past the literal comes
6# out cut short, with no error (a JSON printer that stopped at 1000 tasks).
7# Inside a law, the checker unrolls the fixed fuel and hangs. Derive the fuel
8# from the input's size (`Nat.mul(size, 4n)`) or take it as a parameter. A
9# literal of any size counts, an exact repeat count such as `3n` included.
10# Only an argument that is one literal token alone counts: `U32.to_nat(1000)`,
11# a let-bound literal and a parenthesized `(7n)` are not seen. A def's own
12# calls are exempt: its step passes `fuel - 1`, not a literal.
13import Base
14import bolt@1.11.0.0/src/src.bend as Src
15import bolt@1.11.0.0/src/lazy/lazy.bend as Lazy
16import bolt@1.11.0.0/src/finding.bend as F
17import bolt@1.11.0.0/src/syntax/lex.bend as Lex
18import bolt@1.11.0.0/src/syntax/tree.bend as Tree
19import bolt@1.11.0.0/src/syntax/bind.bend as Bind
20import bolt@1.11.0.0/src/rules/calls.bend as Calls
21import bolt@1.11.0.0/src/rules/tokens.bend as T
22
23# a def of the file and the position of a fuel parameter
24type Fuel is Data:
25 Fuel{name: String, at: Nat}
26
27# is it a fuel parameter's name?
28def is_fuel(+nn: String) -> Bool:
29 Bool.or(String.starts_with(nn, "fuel"),
30 List.contains(~String, ~String.eq, ["gas", "steps", "budget"], nn))
31
32# the fuel parameters among a def's parameters, from position i on
33def fuels.params(ps: List<&2, Tree.Node>, +name: String, +ii: Nat) -> List<&2, Fuel>:
34 match ps:
35 case Nil{}:
36 Nil{}
37 case Con{p, rest}:
38 +more = fuels.params(rest, name, 1n+ii)
39 Bool.pick(List<&2, Fuel>, is_fuel(Calls.param_name(p)), Fuel{name, ii} <> more, more)
40
41# every fuel parameter of every def of the file
42def fuels(ds: List<&2, Calls.Def>) -> List<&2, Fuel>:
43 match ds:
44 case Nil{}:
45 Nil{}
46 case Con{Calls.Def{name, sig, body}, rest}:
47 List.append(&2, Fuel, fuels.params(Calls.params(sig), name, 0n), fuels(rest))
48
49# an argument that is a Nat literal alone (digits, then `n`), as a finding
50def literal(aa: Tree.Node, +path: String) -> List<&2, F.Finding>:
51 match aa:
52 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}:
53 Bool.pick(List<&2, F.Finding>, T.nat_ok(String.to_list(t)),
54 [F.Finding{path, l, c, U32.from_nat(String.length(t)), "fuel",
55 "The fuel is fixed at " ++ t ++ ", so longer input is silently cut short; derive the fuel from the input size."}],
56 [])
57 case other:
58 Nil{}
59
60# a call to name with these arguments, against every fuel parameter
61def call(fs: List<&2, Fuel>, +name: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
62 match fs:
63 case Nil{}:
64 Nil{}
65 case Con{Fuel{+fn, at}, rest}:
66 +more = call(rest, name, as, path)
67 Lazy.stop(List<&2, F.Finding>, Bool.not(String.eq(fn, name)), more,
68 _u => List.append(&2, F.Finding, literal(Calls.arg(as, at), path), more))
69
70# every call at any depth of a chain, but the def's own (self)
71def calls(nn: Tree.Node, +fs: List<&2, Fuel>, +self: String, +path: String) -> List<&2, F.Finding>:
72 match nn:
73 case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
74 +more = List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(rest, fs, self, path)])
75 +hit = Bool.and(Bool.and(Lex.is_name(k), String.eq(o, "(")), Bool.not(String.eq(t, self)))
76 Lazy.stop(List<&2, F.Finding>, Bool.not(hit), more,
77 _u => List.append(&2, F.Finding, call(fs, t, Calls.args(kids), path), more))
78 case Tree.NCons{Tree.Group{open, kids, close}, rest}:
79 List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(rest, fs, self, path)])
80 case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
81 List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(body, fs, self, path),
82 calls(rest, fs, self, path)])
83 case Tree.NCons{h, rest}:
84 calls(rest, fs, self, path)
85 case other:
86 Nil{}
87
88# a def's (or a law's) name, "" when it has none
89def own(mm: Maybe<&2, String>) -> String:
90 match mm:
91 case None{}:
92 ""
93 case Some{n}:
94 n
95
96# each top-level statement, walked as its own def
97def check.go(root: Tree.Node, +fs: List<&2, Fuel>, +path: String) -> List<&2, F.Finding>:
98 match root:
99 case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
100 +self = own(Bind.declared(kids))
101 List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(body, fs, self, path), check.go(rest, fs, path)])
102 case Tree.NCons{h, rest}:
103 check.go(rest, fs, path)
104 case other:
105 Nil{}
106
107# the rule
108def check(ss: Src.Src) -> List<&2, F.Finding>:
109 Src.Src{path, text, toks, +tree, bound, items} = ss
110 check.go(tree, fuels(Calls.defs(tree)), path)