1	# rule table: `List.get` or `List.set` at a computed index inside a def that
2	# calls itself, when the list is a fixed table: a literal, an array, or
3	# `List.replicate` / `Array.new` / `List.range` with a constant count, written
4	# inline, defined beside the loop, or held by the let of that name in scope.
5	# The index walks that table on every step. Keep it in an Array. A let reaches
6	# the statements after it and the blocks under them, not a sibling case arm,
7	# and a later let of the name to anything else ends it. A literal index (a
8	# fixed slot, including 0 and 1), a growing or data-dependent list, a one-shot
9	# outside the recursion, and `List.head` / `List.tail` do not run. `index`
10	# leaves a table this rule owns, so one call is one finding. Laws and proofs
11	# do not run (a def with no type at all fills a law: it is a proof).
12	import Base
13	import ../../src.bend as Src
14	import ../../finding.bend as F
15	import ../../syntax/lex.bend as Lex
16	import ../../syntax/tree.bend as Tree
17	import ../calls.bend as Calls
18	import ../../lazy/lazy.bend as Lazy
19	
20	# is the chain exactly one number?
21	def literal(nn: Tree.Node) -> Bool:
22	  match nn:
23	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, t, l, c}}, Tree.NNil{}}:
24	      True{}
25	    case other:
26	      False{}
27	
28	# a top-level token of this text, not one nested in a group
29	def top_has(nn: Tree.Node, +want: String) -> Bool:
30	  match nn:
31	    case Tree.NCons{Tree.Group{open, kids, close}, rest}:
32	      top_has(rest, want)
33	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, rest}:
34	      +more = top_has(rest, want)
35	      Bool.or(String.eq(t, want), more)
36	    case Tree.NCons{h, rest}:
37	      top_has(rest, want)
38	    case other:
39	      False{}
40	
41	# `[v : T*n]` or `[v : T^d]`, and the size is a number
42	def array_sized(nn: Tree.Node) -> Bool:
43	  match nn:
44	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TOp{}, +op, l, c}},
45	        Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, t, l2, c2}}, rest}}:
46	      +here = Bool.or(String.eq(op, "*"), String.eq(op, "^"))
47	      +more = array_sized(rest)
48	      Bool.or(here, more)
49	    case Tree.NCons{Tree.Group{open, kids, close}, rest}:
50	      array_sized(rest)
51	    case Tree.NCons{h, rest}:
52	      array_sized(rest)
53	    case other:
54	      False{}
55	
56	# the chain is exactly one number
57	def lone_num(nn: Tree.Node) -> Bool:
58	  match nn:
59	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, t, l, c}}, Tree.NNil{}}:
60	      True{}
61	    case other:
62	      False{}
63	
64	# `List.replicate` / `Array.new` count at argument 2; `List.range` at the end
65	def range_count(as: List<&2, Tree.Node>) -> Bool:
66	  match as:
67	    case Nil{}:
68	      False{}
69	    case Con{h, Nil{}}:
70	      lone_num(h)
71	    case Con{h, rest}:
72	      range_count(rest)
73	
74	# a constant-size constructor, not a length taken from the data
75	def built_call(+tt: String, kids: Tree.Node) -> Bool:
76	  +as = Calls.args(kids)
77	  +rep = Bool.or(String.eq(tt, "List.replicate"), String.eq(tt, "Array.new"))
78	  Bool.or(Bool.and(rep, lone_num(Calls.arg(as, 2n))), Bool.and(String.eq(tt, "List.range"), range_count(as)))
79	
80	# a list literal, a sized array, or a constant-size constructor
81	def built(nn: Tree.Node) -> Bool:
82	  match nn:
83	    case Tree.NCons{Tree.Group{Lex.Tok{k, +o, l, c}, +kids, close}, Tree.NNil{}}:
84	      Bool.and(String.eq(o, "["), Bool.or(top_has(kids, ","), Bool.and(top_has(kids, ":"), array_sized(kids))))
85	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}},
86	        Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, Tree.NNil{}}}:
87	      Bool.and(String.eq(o, "("), built_call(t, kids))
88	    case other:
89	      False{}
90	
91	# the chain is exactly this call's name, with no arguments that matter: `name()`
92	def call_name(nn: Tree.Node) -> String:
93	  match nn:
94	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, l, c}},
95	        Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, kids, _}, Tree.NNil{}}}:
96	      Bool.pick(String, String.eq(o, "("), t, "")
97	    case other:
98	      ""
99	
100	# the chain is exactly one lowercase name
101	def lone_name(nn: Tree.Node) -> String:
102	  match nn:
103	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, l, c}}, Tree.NNil{}}:
104	      t
105	    case other:
106	      ""
107	
108	# one use of a name, told apart from its other uses by where it stands
109	def key(+tt: String, +line: U32, +col: U32) -> String:
110	  tt ++ "@" ++ U32.show(line) ++ ":" ++ U32.show(col)
111	
112	# the chain is exactly one lowercase name: that use's key
113	def lone_key(nn: Tree.Node) -> String:
114	  match nn:
115	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, +l, +c}}, Tree.NNil{}}:
116	      key(t, l, c)
117	    case other:
118	      ""
119	
120	# the list argument is a fixed table: inline, a use of a let that holds one,
121	# or `name()` / `name` for a table def of the file
122	def owns(+nn: Tree.Node, +fixed: List<&2, String>) -> Bool:
123	  +called = call_name(nn)
124	  +named = lone_name(nn)
125	  +used = lone_key(nn)
126	  Bool.or(built(nn), Bool.or(
127	    Bool.and(Bool.not(String.is_empty(named)),
128	      Bool.or(List.contains(~String, ~String.eq, fixed, named), List.contains(~String, ~String.eq, fixed, used))),
129	    Bool.and(Bool.not(String.is_empty(called)), List.contains(~String, ~String.eq, fixed, called))))
130	
131	# one plain name before `=`, when the pattern is not a destructure
132	def bind_bad(+bad: Bool, +nm: String) -> String:
133	  match bad:
134	    case True{}:
135	      ""
136	    case False{}:
137	      nm
138	
139	# one plain name before `=`, when there is one
140	def bind_at(+seen: Bool, +bad: Bool, +nm: String) -> String:
141	  match seen:
142	    case False{}:
143	      ""
144	    case True{}:
145	      bind_bad(bad, nm)
146	
147	# the one plain name a statement binds, or empty
148	def bind_name(nn: Tree.Node, +seen: Bool, +bad: Bool, +nm: String) -> String:
149	  match nn:
150	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TEq{}, t, l, c}}, rest}:
151	      bind_at(seen, bad, nm)
152	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, l, c}}, rest}:
153	      bind_name(rest, True{}, Bool.or(bad, seen), t)
154	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, t, l, c}}, rest}:
155	      bind_name(rest, seen, True{}, nm)
156	    case Tree.NCons{Tree.Group{open, kids, close}, rest}:
157	      bind_name(rest, seen, bad, nm)
158	    case Tree.NCons{h, rest}:
159	      bind_name(rest, seen, bad, nm)
160	    case other:
161	      ""
162	
163	# the right-hand side: the chain after a statement's top-level `=`
164	def bind_rhs(nn: Tree.Node) -> Tree.Node:
165	  match nn:
166	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TEq{}, t, l, c}}, rest}:
167	      rest
168	    case Tree.NCons{h, rest}:
169	      bind_rhs(rest)
170	    case other:
171	      Tree.NNil{}
172	
173	# the names in scope without this one
174	def drop(live: List<&2, String>, +nm: String) -> List<&2, String>:
175	  match live:
176	    case Nil{}:
177	      []
178	    case Con{+h, rest}:
179	      +more = drop(rest, nm)
180	      Bool.pick(List<&2, String>, String.eq(h, nm), more, h <> more)
181	
182	# after a let of `nm`: it holds a table only when this binding is one
183	def rebind(+nm: String, +tab: Bool, +live: List<&2, String>) -> List<&2, String>:
184	  +out = drop(live, nm)
185	  Bool.pick(List<&2, String>, String.is_empty(nm), live,
186	    Bool.pick(List<&2, String>, tab, nm <> out, out))
187	
188	# a name use joins the keys when the let in scope for it holds a table
189	def use_at(+tt: String, +line: U32, +col: U32, +live: List<&2, String>, +acc: List<&2, String>) -> List<&2, String>:
190	  Bool.pick(List<&2, String>, List.contains(~String, ~String.eq, live, tt), key(tt, line, col) <> acc, acc)
191	
192	# the keys of every name use under the node whose binding in scope is a
193	# table: a let reaches the statements after it and their bodies, not an
194	# enclosing block or a sibling arm, and a later let of the name replaces it
195	def lets(nn: Tree.Node, +live: List<&2, String>, acc: List<&2, String>) -> List<&2, String>:
196	  match nn:
197	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
198	      +next = rebind(bind_name(kids, False{}, False{}, ""), built(bind_rhs(kids)), live)
199	      lets(rest, next, lets(body, live, lets(kids, live, acc)))
200	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
201	      lets(rest, live, lets(kids, live, acc))
202	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, +l, +c}}, rest}:
203	      lets(rest, live, use_at(t, l, c, live, acc))
204	    case Tree.NCons{h, rest}:
205	      lets(rest, live, acc)
206	    case other:
207	      acc
208	
209	# a def whose body is one fixed table
210	def mod_one(body: Tree.Node, +name: String, +acc: List<&2, String>) -> List<&2, String>:
211	  match body:
212	    case Tree.NCons{Tree.Stmt{kind, +kids, inn}, Tree.NNil{}}:
213	      Bool.pick(List<&2, String>, built(kids), name <> acc, acc)
214	    case other:
215	      acc
216	
217	# defs of this file whose body is one fixed table
218	def modules(ds: List<&2, Calls.Def>, acc: List<&2, String>) -> List<&2, String>:
219	  match ds:
220	    case Nil{}:
221	      acc
222	    case Con{Calls.Def{+name, sig, +body}, rest}:
223	      modules(rest, mod_one(body, name, acc))
224	
225	# fixed tables visible in this def: the file's table defs by name, and each
226	# use of a let whose binding in scope is a table, by its key
227	def scope(body: Tree.Node, +mods: List<&2, String>) -> List<&2, String>:
228	  lets(body, [], mods)
229	
230	# the finding for a get or a set
231	def cite(+get: Bool, +path: String, +line: U32, +col: U32, +len: U32) -> F.Finding:
232	  match get:
233	    case True{}:
234	      F.Finding{path, line, col, len, "table",
235	        "List.get in a recursive def walks the table from its head on every step; keep the table in an Array and use Array.get."}
236	    case False{}:
237	      F.Finding{path, line, col, len, "table",
238	        "List.set in a recursive def copies the list to change one element; keep the table in an Array and use Array.set."}
239	
240	# a get or a set of a fixed table at a computed index
241	def hit(
242	  +open: Bool,
243	  +tt: String,
244	  kids: Tree.Node,
245	  +fixed: List<&2, String>,
246	  +path: String,
247	  +line: U32,
248	  +col: U32
249	) -> List<&2, F.Finding>:
250	  +get = String.eq(tt, "List.get")
251	  +set = String.eq(tt, "List.set")
252	  +op = Bool.and(open, Bool.or(get, set))
253	  +as = Calls.args(kids)
254	  +fire = Bool.and(op, Bool.and(Bool.not(literal(Calls.arg(as, 3n))), owns(Calls.arg(as, 2n), fixed)))
255	  Bool.pick(List<&2, F.Finding>, fire,
256	    [cite(get, path, line, col, U32.from_nat(String.length(tt)))], [])
257	
258	# every fixed-table get or set
259	def walk(nn: Tree.Node, +path: String, +fixed: List<&2, String>) -> List<&2, F.Finding>:
260	  match nn:
261	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
262	      +own = hit(String.eq(o, "("), t, kids, fixed, path, l, c)
263	      List.concat(&2, F.Finding, [own, walk(kids, path, fixed), walk(rest, path, fixed)])
264	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
265	      List.concat(&2, F.Finding, [walk(kids, path, fixed), walk(rest, path, fixed)])
266	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
267	      List.concat(&2, F.Finding, [walk(kids, path, fixed), walk(body, path, fixed), walk(rest, path, fixed)])
268	    case Tree.NCons{h, rest}:
269	      walk(rest, path, fixed)
270	    case other:
271	      Nil{}
272	
273	def check.go(
274	  ds: List<&2, Calls.Def>,
275	  +mods: List<&2, String>,
276	  +path: String,
277	  acc: List<&2, List<&2, F.Finding>>
278	) -> List<&2, F.Finding>:
279	  match ds:
280	    case Nil{}:
281	      List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
282	    case Con{Calls.Def{+name, +sig, +body}, rest}:
283	      check.go(rest, mods, path,
284	        Lazy.stop(List<&2, F.Finding>,
285	          Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), [],
286	          _u => walk(body, path, scope(body, mods))) <> acc)
287	
288	# the rule
289	def check(ss: Src.Src) -> List<&2, F.Finding>:
290	  Src.Src{path, text, toks, tree, bound, items} = ss
291	  +ds = Calls.defs(tree)
292	  check.go(ds, modules(ds, []), path, [])