src/rules/laws/unsafe.bend
bolt@1.11.0.0 · 70 lines · 0 definitions
1# rule unsafe (project-wide): an `@unsafe def` that a LAWS.bend or PROOF.bend
2# reaches by relative imports, over the files bolt read. The checker skips its
3# termination check, prints "All terms check, but N defs rely on unsafe or
4# foreign code:" (2.0.16: "with N unsafe annotation(s).") and exits 0, so a
5# gate that only reads the exit status goes green on a proof that is not
6# sound (a def that never returns proves anything). Recurse
7# on a shrinking argument, or on a fuel, and drop the `@unsafe`; or keep the
8# def out of what the laws import. An `@unsafe` def no law file reaches is
9# not this rule's business. The rule reads each file's digest
10# (src/rules/digest.bend), and takes every closure over one import graph.
11import Base
12import bolt@1.11.0.0/src/finding.bend as F
13import bolt@1.11.0.0/src/rules/digest.bend as Digest
14import bolt@1.11.0.0/src/rules/imports.bend as Imports
15
16# a law file and what it reaches
17type Reach is Data:
18 Reach{origin: String, files: List<&2, String>}
19
20# every LAWS.bend and PROOF.bend with its closure over the graph
21def reaches(
22 ds: List<&2, Digest.Digest>,
23 +es: List<&2, Imports.Edge>,
24 +read: List<&2, String>,
25 +fuel: Nat
26) -> List<&2, Reach>:
27 match ds:
28 case Nil{}:
29 Nil{}
30 case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
31 +more = reaches(rest, es, read, fuel)
32 Bool.pick(List<&2, Reach>, is_law_file, Reach{path, Imports.closure.go(es, read, fuel, norm)} <> more, more)
33
34# the first law file that reaches the path
35def reacher(rs: List<&2, Reach>, +pp: String) -> Maybe<&2, String>:
36 match rs:
37 case Nil{}:
38 None{}
39 case Con{Reach{origin, ps}, rest}:
40 +more = reacher(rest, pp)
41 Bool.pick(Maybe<&2, String>, Imports.has(ps, pp), Some{origin}, more)
42
43# each unsafe def as a finding, reached from the law file
44def report(us: List<&2, Digest.Unsafe>, +origin: String, +path: String) -> List<&2, F.Finding>:
45 match us:
46 case Nil{}:
47 Nil{}
48 case Con{Digest.Unsafe{n, l, c}, rest}:
49 F.Finding{path, l, c, 7, "unsafe", "@unsafe def " ++ n ++ " is reachable from " ++ origin
50 ++ ", where the checker skips its termination check and still exits 0; recurse on a shrinking argument or on fuel, and drop @unsafe."} <> report(rest, origin, path)
51
52# the unsafe defs of a file, when a law file reaches it
53def found(mm: Maybe<&2, String>, us: List<&2, Digest.Unsafe>, path: String) -> List<&2, F.Finding>:
54 match mm:
55 case None{}:
56 Nil{}
57 case Some{origin}:
58 report(us, origin, path)
59
60def check.go(ds: List<&2, Digest.Digest>, +rs: List<&2, Reach>) -> List<&2, F.Finding>:
61 match ds:
62 case Nil{}:
63 Nil{}
64 case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
65 List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path), check.go(rest, rs))
66
67# the rule, over every file the linter read
68def check(+ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
69 +es = Digest.edges(ds)
70 check.go(ds, reaches(ds, es, Imports.paths(es), List.length(&2, Digest.Digest, ds)))