src/rules/suspicious/empty.bend

bolt@1.27.0.0 · 372 lines · 36 definitions

1# rule empty: a length compared to zero when the value is kept. Among the
2# significant tokens (spaces, newlines and comments dropped): a `(`, `[`,
3# `{` or `,`, then a dotted `Nat.is_eq`, `(`, and either a dotted
4# `List.length`, `(`, any tokens up to its matching `)` whose last two are a
5# `,` and a plain name x, or a dotted `String.length`, `(`, a plain name x
6# and `)`; then `,`, `0n` and `)`; and x again, as a plain name, among the
7# tokens after that `)` and before the bracket that closes the group the
8# test sits in (brackets opened on the way are skipped over, not ended on).
9# One finding, on the `Nat.is_eq` token, for each such test.
10# Base's List.length and String.length count every cell (and are not tail
11# calls); List.is_empty and String.is_empty, which take the same arguments,
12# look at one and give the same Bool. The second read is what makes the fix
13# pay on both lanes: x is kept past the test, so the test's own reference is
14# dropped by a count, never by freeing x. Where the test is x's last use,
15# the native lane frees the cells the walk would have, and freeing a list
16# the program never walked costs more than walking it (bend 2.0.38: a
17# 0-1000 char String tested then dropped ran 0.27x as fast as a length,
18# kept 1.57x; JS 1.65x and 1.31x), so a test with no read after it in its
19# group, a test outside any group, and a read before the test are left
20# alone. A LAWS.bend or a PROOF.bend, which never runs, is exempt, and so
21# is a `law` and a def that is a proof (no type, `def f(x):`, or one that
22# returns `-> {..}`) in any file, from its keyword to the next `def`, `type`
23# or `import`. A comment is never read, and a string literal is one token
24# that is no name.
25import Base
26import bolt@1.27.0.0/src/src.bend as Src
27import bolt@1.27.0.0/src/paths.bend as Paths
28import bolt@1.27.0.0/src/role.bend as Role
29import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy
30import bolt@1.27.0.0/src/finding.bend as F
31import bolt@1.27.0.0/src/syntax/lex.bend as Lex
32import bolt@1.27.0.0/src/rules/tokens.bend as T
33
34# which length a test takes: a list's, a String's, or neither
35type Form is Data:
36  FList{}
37  FStr{}
38  FNone{}
39
40# what the last tokens of a List.length's arguments were: a comma, a plain
41# name right after a comma, or anything else
42type Last is Data:
43  LComma{}
44  LName{name: String}
45  LOther{}
46
47# the name a test takes the length of, and the tokens after its `)`
48type Taken is Data:
49  Taken{name: String, rest: List<&2, Lex.Tok>}
50
51# where a finding goes and what it says
52type Hit is Data:
53  Hit{line: U32, col: U32, msg: String}
54
55# a bracket that opens a group, or a comma inside one: what may stand right
56# before a test
57def opener(kk: Lex.TokKind) -> Bool:
58  match kk:
59    case Lex.TOpen{}:
60      True{}
61    case Lex.TComma{}:
62      True{}
63    case other:
64      False{}
65
66# a token's text where it is code: a string literal or a comment says
67# nothing the rule reads
68def code(kk: Lex.TokKind, tt: String) -> String:
69  match kk:
70    case Lex.TStr{}:
71      ""
72    case Lex.TComment{}:
73      ""
74    case other:
75      tt
76
77# a dotted name
78def dotted(kk: Lex.TokKind) -> Bool:
79  match kk:
80    case Lex.TDotted{}:
81      True{}
82    case other:
83      False{}
84
85# a plain name
86def plain(kk: Lex.TokKind) -> Bool:
87  match kk:
88    case Lex.TName{}:
89      True{}
90    case other:
91      False{}
92
93# the length a dotted name takes
94def form(+tt: String) -> Form:
95  Bool.pick(Form, String.eq(tt, "List.length"), FList{}, Bool.pick(Form, String.eq(tt, "String.length"), FStr{}, FNone{}))
96
97# an opener, `Nat.is_eq`, `(`, a dotted name and `(`?
98def head(
99  k0: Lex.TokKind,
100  +k1: Lex.TokKind,
101  +t1: String,
102  k2: Lex.TokKind,
103  +t2: String,
104  +k3: Lex.TokKind,
105  k4: Lex.TokKind,
106  +t4: String
107) -> Bool:
108  Bool.and(opener(k0), Bool.and(dotted(k1), Bool.and(dotted(k3), Bool.and(String.eq(code(k1, t1), "Nat.is_eq"),
109    Bool.and(String.eq(code(k2, t2), "("), String.eq(code(k4, t4), "("))))))
110
111# what a token leaves of the last tokens: a comma, a name after a comma, or
112# anything else
113def last.step(+kk: Lex.TokKind, +tt: String, ll: Last) -> Last:
114  match kk:
115    case Lex.TComma{}:
116      LComma{}
117    case Lex.TName{}:
118      match ll:
119        case LComma{}:
120          LName{code(kk, tt)}
121        case other:
122          LOther{}
123    case other:
124      LOther{}
125
126# the name a List.length's arguments end in, when the last two were a comma
127# and a plain name
128def last.name(ll: Last, rest: List<&2, Lex.Tok>) -> Maybe<&2, Taken>:
129  match ll:
130    case LName{nn}:
131      Some{Taken{nn, rest}}
132    case other:
133      None{}
134
135# a bracket at the depth: the length's own `)` at depth zero; else the depth
136# it leaves
137def close.depth(kk: Lex.TokKind, dd: Nat) -> Nat:
138  match kk:
139    case Lex.TOpen{}:
140      1n+dd
141    case Lex.TClose{}:
142      match dd:
143        case 0n:
144          0n
145        case 1n+p:
146          p
147    case other:
148      dd
149
150# is the token the bracket that closes the arguments, at depth zero?
151def close.here(kk: Lex.TokKind, dd: Nat) -> Bool:
152  match kk:
153    case Lex.TClose{}:
154      match dd:
155        case 0n:
156          True{}
157        case 1n+p:
158          False{}
159    case other:
160      False{}
161
162# a List.length's arguments, scanned to the `)` that closes them: the name
163# they end in and the tokens after that `)`; none when they end otherwise
164# or run out. done carries whether the last token read was that `)`.
165def close.list(toks: List<&2, Lex.Tok>, +dd: Nat, +ll: Last, done: Bool, got: Maybe<&2, Taken>) -> Maybe<&2, Taken>:
166  match toks:
167    case Nil{}:
168      got
169    case Con{Lex.Tok{+k, +t, l, c}, +rest}:
170      match done:
171        case True{}:
172          got
173        case False{}:
174          +here = close.here(k, dd)
175          close.list(rest, close.depth(k, dd), last.step(k, t, ll), here, Bool.pick(Maybe<&2, Taken>, here,
176            last.name(ll, rest), None{}))
177
178# a String.length's argument: a plain name and `)`, then the tokens after
179def close.str(toks: List<&2, Lex.Tok>) -> Maybe<&2, Taken>:
180  match toks:
181    case Con{Lex.Tok{+k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, rest}}:
182      Bool.pick(Maybe<&2, Taken>, Bool.and(plain(k1), String.eq(code(k2, t2), ")")), Some{Taken{code(k1, t1), rest}},
183        None{})
184    case other:
185      None{}
186
187# the length's argument, by its form
188def taken(fm: Form, +toks: List<&2, Lex.Tok>) -> Maybe<&2, Taken>:
189  match fm:
190    case FList{}:
191      close.list(toks, 0n, LOther{}, False{}, None{})
192    case FStr{}:
193      close.str(toks)
194    case FNone{}:
195      None{}
196
197# a plain name with x's text?
198def same(+kk: Lex.TokKind, +tt: String, +xx: String) -> Bool:
199  Bool.and(plain(kk), String.eq(code(kk, tt), xx))
200
201# is x read among the tokens before the bracket that closes the group they
202# sit in? found carries whether the last token read was x, live whether that
203# bracket is still ahead
204def kept(toks: List<&2, Lex.Tok>, +xx: String, +dd: Nat, found: Bool, live: Bool) -> Bool:
205  match toks:
206    case Nil{}:
207      found
208    case Con{Lex.Tok{+k, +t, l, c}, rest}:
209      match found:
210        case True{}:
211          True{}
212        case False{}:
213          match live:
214            case False{}:
215              False{}
216            case True{}:
217              kept(rest, xx, close.depth(k, dd), same(k, t, xx), Bool.not(close.here(k, dd)))
218
219# what a finding says: the test, its fix and why
220def say(fm: Form, +xx: String) -> String:
221  match fm:
222    case FList{}:
223      "Nat.is_eq(List.length(.., " ++ xx ++ "), 0n) counts every cell of " ++ xx ++ ", which is read again; List.is_empty(.., "
224        ++ xx ++ ") looks at one and gives the same answer."
225    case other:
226      "Nat.is_eq(String.length(" ++ xx ++ "), 0n) counts every char of " ++ xx ++ ", which is read again; String.is_empty("
227        ++ xx ++ ") looks at one and gives the same answer."
228
229# a finding, if the test is whole and x kept
230def tail.go(ok: Bool, fm: Form, xx: String, ll: U32, cc: U32) -> Maybe<&2, Hit>:
231  match ok:
232    case True{}:
233      Some{Hit{ll, cc, say(fm, xx)}}
234    case False{}:
235      None{}
236
237# the test's end, `,`, `0n` and `)`, then x kept: the finding, if any
238def tail(mm: Maybe<&2, Taken>, +fm: Form, +ll: U32, +cc: U32) -> Maybe<&2, Hit>:
239  match mm:
240    case None{}:
241      None{}
242    case Some{Taken{+xx, r}}:
243      match r:
244        case Con{Lex.Tok{k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{k3, +t3, l3, c3}, rest}}}:
245          tail.go(Bool.and(String.eq(code(k1, t1), ","), Bool.and(String.eq(code(k2, t2), "0n"),
246            Bool.and(String.eq(code(k3, t3), ")"),
247            kept(rest, xx, 0n, False{}, True{})))), fm, xx, ll, cc)
248        case other:
249          None{}
250
251# the test, its head read: the finding, if any
252def at.go(ok: Bool, +fm: Form, +ll: U32, +cc: U32, r4: List<&2, Lex.Tok>) -> Maybe<&2, Hit>:
253  match ok:
254    case True{}:
255      tail(taken(fm, r4), fm, ll, cc)
256    case False{}:
257      None{}
258
259# a token of kind k0, then these: a kept test?
260def at(k0: Lex.TokKind, toks: List<&2, Lex.Tok>) -> Maybe<&2, Hit>:
261  match toks:
262    case Con{Lex.Tok{k1, +t1, +l1, +c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{+k3, +t3, l3, c3},
263      Con{Lex.Tok{k4, +t4, l4, c4}, r4}}}}:
264      at.go(head(k0, k1, t1, k2, t2, k3, k4, t4), form(code(k3, t3)), l1, c1, r4)
265    case other:
266      None{}
267
268# the finding a test makes, if any, before the rest
269def hit(mm: Maybe<&2, Hit>, +path: String, more: List<&2, F.Finding>) -> List<&2, F.Finding>:
270  match mm:
271    case None{}:
272      more
273    case Some{Hit{ll, cc, msg}}:
274      F.Finding{path, ll, cc, 9, "empty", msg} <> more
275
276# what the two tokens after a def's parameters say: a `:` (no type: the
277# def fills a law) or `->` then `{` (it returns a proof)
278def proofy.head(k1: Lex.TokKind, +k2: Lex.TokKind, +t2: String) -> Bool:
279  match k1:
280    case Lex.TColon{}:
281      True{}
282    case Lex.TArrow{}:
283      String.eq(code(k2, t2), "{")
284    case other:
285      False{}
286
287# what a def's header says once its parameters close
288def proofy.end(toks: List<&2, Lex.Tok>) -> Bool:
289  match toks:
290    case Con{Lex.Tok{k1, t1, l1, c1}, Con{Lex.Tok{k2, t2, l2, c2}, rest}}:
291      proofy.head(k1, k2, t2)
292    case Con{Lex.Tok{k1, t1, l1, c1}, Nil{}}:
293      proofy.head(k1, Lex.TSpace{}, "")
294    case other:
295      False{}
296
297# does the token close the parameters: a bracket closing at depth one?
298def proofy.fin(kk: Lex.TokKind, dd: Nat) -> Bool:
299  match kk:
300    case Lex.TClose{}:
301      match dd:
302        case 1n:
303          True{}
304        case other:
305          False{}
306    case other:
307      False{}
308
309# is the def these tokens head (after `def`) a proof? Its tokens are read to
310# the bracket that closes its parameters, at depth zero; fin carries whether
311# the last token read was that bracket
312def proofy(toks: List<&2, Lex.Tok>, +dd: Nat, fin: Bool) -> Bool:
313  match toks:
314    case Nil{}:
315      False{}
316    case Con{Lex.Tok{+k, t, l, c}, +rest}:
317      match fin:
318        case True{}:
319          proofy.end(Lex.Tok{k, t, l, c} <> rest)
320        case False{}:
321          proofy(rest, close.depth(k, dd), proofy.fin(k, dd))
322
323# what is skipped after a token that is no def: inside a law, from `law` on;
324# code again from `type` or `import`; else as before
325def item.other(+word: String, skip: Bool) -> Bool:
326  Bool.pick(Bool, String.eq(word, "law"), True{}, Bool.pick(Bool, Bool.or(String.eq(word, "type"),
327    String.eq(word, "import")), False{}, skip))
328
329# what is skipped after a keyword: a def is skipped when it is a proof
330def item.word(isdef: Bool, +word: String, rest: List<&2, Lex.Tok>, skip: Bool) -> Bool:
331  match isdef:
332    case True{}:
333      proofy(rest, 0n, False{})
334    case False{}:
335      item.other(word, skip)
336
337# what is skipped after a token: a law, and a def that is a proof, never run
338def item(+kk: Lex.TokKind, +tt: String, rest: List<&2, Lex.Tok>, skip: Bool) -> Bool:
339  match kk:
340    case Lex.TKey{}:
341      item.word(String.eq(code(kk, tt), "def"), code(kk, tt), rest, skip)
342    case other:
343      skip
344
345# the kept test a token opens, if any, outside what is skipped
346def found(skip: Bool, kk: Lex.TokKind, rest: List<&2, Lex.Tok>) -> Maybe<&2, Hit>:
347  match skip:
348    case True{}:
349      None{}
350    case False{}:
351      at(kk, rest)
352
353# every kept test among the tokens, in order; skip says whether the tokens
354# so far sit in a law or a def that is a proof
355def walk(toks: List<&2, Lex.Tok>, +path: String, skip: Bool) -> List<&2, F.Finding>:
356  match toks:
357    case Nil{}:
358      Nil{}
359    case Con{Lex.Tok{+k, +t, l, c}, +rest}:
360      +sk = item(k, t, rest, skip)
361      hit(found(sk, k, rest), path, walk(rest, path, sk))
362
363# the rule
364def check(ss: Src.Src) -> List<&2, F.Finding>:
365  Src.Src{+path, text, toks, tree, bound, items} = ss
366  Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => walk(T.sig(toks), path, False{}))
367
368# the rule, told the file's role (src/role.bend): a law or proof file is
369# skipped
370def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
371  Src.Src{path, text, toks, tree, bound, items} = ss
372  Lazy.stop(List<&2, F.Finding>, Role.is_law_file(rr), [], _u => walk(T.sig(toks), path, False{}))