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.
19	import Base
20	import ../../src.bend as Src
21	import ../../lazy/lazy.bend as Lazy
22	import ../../finding.bend as F
23	import ../../syntax/lex.bend as Lex
24	import ../../syntax/tree.bend as Tree
25	import ../../syntax/bind.bend as Bind
26	import ../calls.bend as Calls
27	import ../tokens.bend as T
28	
29	# a def of the file and the position of a fuel parameter
30	type Fuel is Data:
31	  Fuel{name: String, at: Nat}
32	
33	# is it a fuel parameter's name?
34	def is_fuel(+nn: String) -> Bool:
35	  Bool.or(String.starts_with(nn, "fuel"),
36	    List.contains(~String, ~String.eq, ["gas", "steps", "budget"], nn))
37	
38	# the fuel parameters among a def's parameters, from position i on
39	def fuels.params(ps: List<&2, Tree.Node>, +name: String, +ii: Nat) -> List<&2, Fuel>:
40	  match ps:
41	    case Nil{}:
42	      Nil{}
43	    case Con{p, rest}:
44	      +more = fuels.params(rest, name, 1n+ii)
45	      Bool.pick(List<&2, Fuel>, is_fuel(Calls.param_name(p)), Fuel{name, ii} <> more, more)
46	
47	# every fuel parameter of every def of the file
48	def fuels(ds: List<&2, Calls.Def>) -> List<&2, Fuel>:
49	  match ds:
50	    case Nil{}:
51	      Nil{}
52	    case Con{Calls.Def{name, sig, body}, rest}:
53	      List.append(&2, Fuel, fuels.params(Calls.params(sig), name, 0n), fuels(rest))
54	
55	# the group of a call at line ll, column cc, as a finding when it holds one
56	# U32 literal alone (digits) and ok says the call is `U32.to_nat(`
57	def converted(kids: Tree.Node, ok: Bool, +ll: U32, +cc: U32, +path: String) -> List<&2, F.Finding>:
58	  match kids:
59	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}:
60	      Bool.pick(List<&2, F.Finding>, Bool.and(ok, T.digits_ok(String.to_list(t))),
61	        [F.Finding{path, ll, cc, U32.from_nat(Nat.add(String.length(t), 12n)), "fuel",
62	          "The fuel is fixed at U32.to_nat(" ++ t
63	            ++ "), so longer input is silently cut short; derive the fuel from the input size."}],
64	        [])
65	    case other:
66	      Nil{}
67	
68	# an argument that is a Nat literal alone (digits, then `n`), or
69	# `U32.to_nat` of a U32 literal alone, as a finding
70	def literal(aa: Tree.Node, +path: String) -> List<&2, F.Finding>:
71	  match aa:
72	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}:
73	      Bool.pick(List<&2, F.Finding>, T.nat_ok(String.to_list(t)),
74	        [F.Finding{path, l, c, U32.from_nat(String.length(t)), "fuel",
75	          "The fuel is fixed at " ++ t ++ ", so longer input is silently cut short; derive the fuel from the input size."}],
76	        [])
77	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TDotted{}, +t, l, c}},
78	      Tree.NCons{Tree.Group{Lex.Tok{ok, +o, ol, oc}, kids, cl}, Tree.NNil{}}}:
79	      converted(kids, Bool.and(String.eq(t, "U32.to_nat"), String.eq(o, "(")), l, c, path)
80	    case other:
81	      Nil{}
82	
83	# a call to name with these arguments, against every fuel parameter
84	def call(fs: List<&2, Fuel>, +name: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
85	  match fs:
86	    case Nil{}:
87	      Nil{}
88	    case Con{Fuel{+fn, at}, rest}:
89	      +more = call(rest, name, as, path)
90	      Lazy.stop(List<&2, F.Finding>, Bool.not(String.eq(fn, name)), more,
91	        _u => List.append(&2, F.Finding, literal(Calls.arg(as, at), path), more))
92	
93	# every call at any depth of a chain, but the def's own (self)
94	def calls(nn: Tree.Node, +fs: List<&2, Fuel>, +self: String, +path: String) -> List<&2, F.Finding>:
95	  match nn:
96	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
97	      +more = List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(rest, fs, self, path)])
98	      +hit = Bool.and(Bool.and(Lex.is_name(k), String.eq(o, "(")), Bool.not(String.eq(t, self)))
99	      Lazy.stop(List<&2, F.Finding>, Bool.not(hit), more,
100	        _u => List.append(&2, F.Finding, call(fs, t, Calls.args(kids), path), more))
101	    case Tree.NCons{Tree.Group{open, kids, close}, rest}:
102	      List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(rest, fs, self, path)])
103	    case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
104	      List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(body, fs, self, path),
105	        calls(rest, fs, self, path)])
106	    case Tree.NCons{h, rest}:
107	      calls(rest, fs, self, path)
108	    case other:
109	      Nil{}
110	
111	# a def's (or a law's) name, "" when it has none
112	def own(mm: Maybe<&2, String>) -> String:
113	  match mm:
114	    case None{}:
115	      ""
116	    case Some{n}:
117	      n
118	
119	# each top-level statement, walked as its own def
120	def check.go(root: Tree.Node, +fs: List<&2, Fuel>, +path: String) -> List<&2, F.Finding>:
121	  match root:
122	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
123	      +self = own(Bind.declared(kids))
124	      List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(body, fs, self, path), check.go(rest, fs, path)])
125	    case Tree.NCons{h, rest}:
126	      check.go(rest, fs, path)
127	    case other:
128	      Nil{}
129	
130	# the rule
131	def check(ss: Src.Src) -> List<&2, F.Finding>:
132	  Src.Src{path, text, toks, +tree, bound, items} = ss
133	  check.go(tree, fuels(Calls.defs(tree)), path)