src/rules/suspicious/prefix.bend

bolt@1.27.0.0 · 293 lines · 33 definitions

1# rule prefix: a String.take compared to a literal of its length:
2# `String.eq(String.take(s, k), "..")` or `String.eq("..", String.take(s,
3# k))`. Among the significant tokens (spaces, newlines and comments dropped):
4# a dotted name `String.eq`, `(`, `String.take` and `(`, then the take's
5# first argument s, any tokens up to the first comma outside the brackets
6# they open (a call such as `String.drop(m, 4n)` is one argument), then a
7# Nat literal k, `)`, `,`, a string literal and `)`; or the dotted name
8# `String.eq`, `(`, the string literal, `,`, `String.take`, `(`, s, the
9# comma, k, `)` and `)`. Only when k's text is the literal's length (an
10# escape, `\n` or `\u{1B}`, one char) written in decimal with an `n`, as
11# `4n` for `"ERR "`. A bracket that closes the take before any such comma
12# ends the scan with no finding. One finding, on the `String.eq` token, for
13# each such run, and nothing else: a take of another length is another bug.
14# String.take copies k chars into a new String only to compare them;
15# `String.starts_with(s, "ERR ")` (Base) walks s in place and gives the same
16# answer for every s, False when s is shorter, s any expression. A LAWS.bend
17# or a PROOF.bend, which never runs, is exempt. A comment is never read, and
18# a string literal is one token, so the shape written inside either is not
19# the shape.
20import Base
21import bolt@1.27.0.0/src/src.bend as Src
22import bolt@1.27.0.0/src/paths.bend as Paths
23import bolt@1.27.0.0/src/role.bend as Role
24import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy
25import bolt@1.27.0.0/src/finding.bend as F
26import bolt@1.27.0.0/src/syntax/lex.bend as Lex
27import bolt@1.27.0.0/src/rules/tokens.bend as T
28
29# where the length of a string literal's text is: before its opening
30# quote, in plain text, just after a backslash, inside a `\u{..}`, or past
31# its closing quote
32type Mode is Data:
33  MOpen{}
34  MPlain{}
35  MEsc{}
36  MUni{}
37  MDone{}
38
39# is the char the code point?
40def is_cp(+cc: Char, +xx: U32) -> Bool:
41  U32.is_eq(Char.to_u32(cc), xx)
42
43# what the char adds to the length: one in plain text, but not the closing
44# quote; nothing anywhere else
45def len.add(mm: Mode, +cc: Char) -> Nat:
46  match mm:
47    case MPlain{}:
48      Bool.pick(Nat, is_cp(cc, 34), 0n, 1n)
49    case other:
50      0n
51
52# where the char leaves the length: a backslash starts an escape, a quote
53# closes the literal, `u` after a backslash opens a `\u{..}` and `}` closes
54# it
55def len.next(mm: Mode, +cc: Char) -> Mode:
56  match mm:
57    case MOpen{}:
58      MPlain{}
59    case MPlain{}:
60      Bool.pick(Mode, is_cp(cc, 92), MEsc{}, Bool.pick(Mode, is_cp(cc, 34), MDone{}, MPlain{}))
61    case MEsc{}:
62      Bool.pick(Mode, is_cp(cc, 117), MUni{}, MPlain{})
63    case MUni{}:
64      Bool.pick(Mode, is_cp(cc, 125), MPlain{}, MUni{})
65    case MDone{}:
66      MDone{}
67
68# the length of the rest of a literal's text, from where it is
69def len.go(tt: String, +mm: Mode) -> Nat:
70  match tt:
71    case SNil{}:
72      0n
73    case SCon{+cc, rest}:
74      Nat.add(len.add(mm, cc), len.go(rest, len.next(mm, cc)))
75
76# the length of a string literal, its text as the lexer keeps it (quotes
77# and escapes as written): each escape one char
78def len(tt: String) -> Nat:
79  len.go(tt, MOpen{})
80
81# is the Nat literal's text the literal's length?
82def fits(+kk: String, lit: String) -> Bool:
83  String.eq(kk, Nat.show(len(lit)) ++ "n")
84
85# what the finding says: the take, and the starts_with that replaces it
86def say(+ss: String, +kk: String, +lit: String) -> String:
87  "String.eq(String.take(" ++ ss ++ ", " ++ kk ++ "), " ++ lit ++ ") copies " ++ kk
88    ++ " chars only to compare them; String.starts_with(" ++ ss ++ ", " ++ lit ++ ") gives the same answer in place."
89
90# where the scan of a take's first argument stands: inside it at a depth of
91# brackets it opened, just past the comma that ends it, or at the bracket
92# that closes the take before any such comma
93type Skip is Data:
94  SGo{depth: Nat}
95  SComma{}
96  SClose{}
97
98# the argument as the finding writes it, and the tokens after its comma
99type Arg is Data:
100  Arg{text: String, rest: List<&2, Lex.Tok>}
101
102# a comma at the depth: the argument's end at depth zero, else inside it
103def skip.comma(dd: Nat) -> Skip:
104  match dd:
105    case 0n:
106      SComma{}
107    case 1n+p:
108      SGo{1n+p}
109
110# a closing bracket at the depth: the take's own at depth zero, else one
111# bracket the argument opened
112def skip.close(dd: Nat) -> Skip:
113  match dd:
114    case 0n:
115      SClose{}
116    case 1n+p:
117      SGo{p}
118
119# where a token of the kind leaves the scan at the depth
120def skip.step(kk: Lex.TokKind, dd: Nat) -> Skip:
121  match kk:
122    case Lex.TComma{}:
123      skip.comma(dd)
124    case Lex.TOpen{}:
125      SGo{1n+dd}
126    case Lex.TClose{}:
127      skip.close(dd)
128    case other:
129      SGo{dd}
130
131# a token as the finding writes it: a comma with a space after it, an
132# operator with one on each side
133def piece(kk: Lex.TokKind, +tt: String) -> String:
134  match kk:
135    case Lex.TComma{}:
136      ", "
137    case Lex.TOp{}:
138      " " ++ tt ++ " "
139    case other:
140      tt
141
142# what a token adds to the argument's text, given where it leaves the scan:
143# nothing for the comma that ends the argument
144def skip.piece(sk: Skip, kk: Lex.TokKind, +tt: String) -> String:
145  match sk:
146    case SComma{}:
147      ""
148    case other:
149      piece(kk, tt)
150
151# the take's first argument, scanned from where the scan stands: what it
152# says (acc: its pieces so far, last first) and the tokens after the comma
153# that ends it; none when the take
154# closes first or the tokens run out
155def skip(toks: List<&2, Lex.Tok>, sk: Skip, +acc: List<&2, String>) -> Maybe<&2, Arg>:
156  match toks:
157    case Nil{}:
158      None{}
159    case Con{Lex.Tok{+k, +t, l, c}, rest}:
160      match sk:
161        case SComma{}:
162          Some{Arg{String.join(List.reverse(&2, String, acc), ""), Lex.Tok{k, t, l, c} <> rest}}
163        case SClose{}:
164          None{}
165        case SGo{dd}:
166          +nx = skip.step(k, dd)
167          skip(rest, nx, skip.piece(nx, k, t) <> acc)
168
169# a dotted name: what `String.eq` is
170def dotted(kk: Lex.TokKind) -> Bool:
171  match kk:
172    case Lex.TDotted{}:
173      True{}
174    case other:
175      False{}
176
177# after the argument's comma, k, `)`, `,`, a string literal and `)`: is k
178# the literal's length?
179def tail_a.ok(+kk: String, +t7: String, +t8: String, k9: Lex.TokKind, +t9: String, +t10: String) -> Bool:
180  Bool.and(String.eq(t7, ")"), Bool.and(String.eq(t8, ","), Bool.and(Lex.is_str(k9),
181    Bool.and(String.eq(t10, ")"), fits(kk, t9)))))
182
183# the take-first shape's end, after the argument: what the finding says
184def tail_a(ma: Maybe<&2, Arg>) -> Maybe<&2, String>:
185  match ma:
186    case None{}:
187      None{}
188    case Some{Arg{+ss, r}}:
189      match r:
190        case Con{Lex.Tok{k6, +t6, l6, c6}, Con{Lex.Tok{k7, +t7, l7, c7}, Con{Lex.Tok{k8, +t8, l8, c8},
191          Con{Lex.Tok{k9, +t9, l9, c9}, Con{Lex.Tok{k10, +t10, l10, c10}, rest}}}}}:
192          Bool.pick(Maybe<&2, String>, tail_a.ok(t6, t7, t8, k9, t9, t10), Some{say(ss, t6, t9)}, None{})
193        case other:
194          None{}
195
196# after the argument's comma, k, `)` and `)`: is k the literal's length?
197def tail_b.ok(+kk: String, +t9: String, +t10: String, +lit: String) -> Bool:
198  Bool.and(String.eq(t9, ")"), Bool.and(String.eq(t10, ")"), fits(kk, lit)))
199
200# the literal-first shape's end, after the argument: what the finding says
201def tail_b(ma: Maybe<&2, Arg>, +lit: String) -> Maybe<&2, String>:
202  match ma:
203    case None{}:
204      None{}
205    case Some{Arg{+ss, r}}:
206      match r:
207        case Con{Lex.Tok{k8, +t8, l8, c8}, Con{Lex.Tok{k9, +t9, l9, c9}, Con{Lex.Tok{k10, +t10, l10, c10}, rest}}}:
208          Bool.pick(Maybe<&2, String>, tail_b.ok(t8, t9, t10, lit), Some{say(ss, t8, lit)}, None{})
209        case other:
210          None{}
211
212# a dotted `String.eq`, `(`, `String.take` and `(`?
213def head_a(k0: Lex.TokKind, +t0: String, +t1: String, +t2: String, +t3: String) -> Bool:
214  Bool.and(dotted(k0), Bool.and(String.eq(t0, "String.eq"), Bool.and(String.eq(t1, "("),
215    Bool.and(String.eq(t3, "("), String.eq(t2, "String.take")))))
216
217# the take-first shape, its head read: the end, after the argument
218def at_a.go(ok: Bool, r3: List<&2, Lex.Tok>) -> Maybe<&2, String>:
219  match ok:
220    case True{}:
221      tail_a(skip(r3, SGo{0n}, []))
222    case False{}:
223      None{}
224
225# a token of kind k0 and text t0, then these: the take-first shape?
226def at_a(k0: Lex.TokKind, +t0: String, toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
227  match toks:
228    case Con{Lex.Tok{k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{k3, +t3, l3, c3}, r3}}}:
229      at_a.go(head_a(k0, t0, t1, t2, t3), r3)
230    case other:
231      None{}
232
233# a dotted `String.eq`, `(`, a string literal, `,`, `String.take` and `(`?
234def head_b(k0: Lex.TokKind, +t0: String, +t1: String, k2: Lex.TokKind, +t3: String, +t4: String, +t5: String) -> Bool:
235  Bool.and(dotted(k0), Bool.and(String.eq(t0, "String.eq"), Bool.and(String.eq(t1, "("), Bool.and(Lex.is_str(k2),
236    Bool.and(String.eq(t3, ","), Bool.and(String.eq(t4, "String.take"), String.eq(t5, "(")))))))
237
238# the literal-first shape, its head read: the end, after the argument
239def at_b.go(ok: Bool, r5: List<&2, Lex.Tok>, +lit: String) -> Maybe<&2, String>:
240  match ok:
241    case True{}:
242      tail_b(skip(r5, SGo{0n}, []), lit)
243    case False{}:
244      None{}
245
246# a token of kind k0 and text t0, then these: the literal-first shape?
247def at_b(k0: Lex.TokKind, +t0: String, toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
248  match toks:
249    case Con{Lex.Tok{k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{k3, +t3, l3, c3},
250      Con{Lex.Tok{k4, +t4, l4, c4}, Con{Lex.Tok{k5, +t5, l5, c5}, r5}}}}}:
251      at_b.go(head_b(k0, t0, t1, k2, t3, t4, t5), r5, t2)
252    case other:
253      None{}
254
255# the first message, else the second
256def either(ma: Maybe<&2, String>, mb: Maybe<&2, String>) -> Maybe<&2, String>:
257  match ma:
258    case None{}:
259      mb
260    case Some{x}:
261      Some{x}
262
263# a token of kind k0 and text t0, then these: either shape? what the finding
264# says when they make one
265def at(+k0: Lex.TokKind, +t0: String, +toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
266  either(at_a(k0, t0, toks), at_b(k0, t0, toks))
267
268# the finding a run makes, if any, before the rest
269def hit(mm: Maybe<&2, String>, +path: String, +ll: U32, +cc: U32, more: List<&2, F.Finding>) -> List<&2, F.Finding>:
270  match mm:
271    case None{}:
272      more
273    case Some{msg}:
274      F.Finding{path, ll, cc, 9, "prefix", msg} <> more
275
276# every run of either shape among the tokens, in order
277def walk(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
278  match toks:
279    case Nil{}:
280      Nil{}
281    case Con{Lex.Tok{+k, +t, +l, +c}, +rest}:
282      hit(at(k, t, rest), path, l, c, walk(rest, path))
283
284# the rule
285def check(ss: Src.Src) -> List<&2, F.Finding>:
286  Src.Src{+path, text, toks, tree, bound, items} = ss
287  Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => walk(T.sig(toks), path))
288
289# the rule, told the file's role (src/role.bend): a law or proof file is
290# skipped
291def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
292  Src.Src{path, text, toks, tree, bound, items} = ss
293  Lazy.stop(List<&2, F.Finding>, Role.is_law_file(rr), [], _u => walk(T.sig(toks), path))