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.
11	import Base
12	import ../../finding.bend as F
13	import ../digest.bend as Digest
14	import ../imports.bend as Imports
15	
16	# a law file and what it reaches
17	type 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
21	def 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
35	def 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
44	def 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
53	def 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	
60	def 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
68	def 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)))