src/rules/suspicious/prefix.bend
bolt@1.25.0.0 · 293 lines · 0 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.25.0.0/src/src.bend as Src
22import bolt@1.25.0.0/src/paths.bend as Paths
23import bolt@1.25.0.0/src/role.bend as Role
24import bolt@1.25.0.0/src/lazy/lazy.bend as Lazy
25import bolt@1.25.0.0/src/finding.bend as F
26import bolt@1.25.0.0/src/syntax/lex.bend as Lex
27import bolt@1.25.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))