1	# bend-osdev-apparmor: signal rules (apparmor.d(5), "SIGNAL RULE", "Signal
2	# rules"): `signal [ACCESS] [set=(SIGNALS)] [peer=AARE]`, the conditions in
3	# any order. Permission bits: send 0, receive 1; with no access list both
4	# are implied. r and read are receive, w and write send, rw both (the page
5	# gives these synonyms for dbus; the package reads signal's the same way).
6	import Base
7	import ./text.bend as X
8	import ./glob.bend as G
9	import ./perm.bend as P
10	import ./token.bend as T
11	import ./error.bend as E
12	import ./rule.bend as R
13	
14	# signals: None for every signal; peer: None for every peer
15	type AaSignalRule is Data:
16	  AaSignalRule{qual: P.AaQual, perms: P.AaPerms, signals: Maybe<&2, List<&2, List<&2, U32>>>, peer: Maybe<&2, G.AaGlob>}
17	
18	# a signal sent or received (req: send and/or receive), by name (hup, int,
19	# ..., rtmin+N) and the peer's profile name
20	type AaSignalQuery is Data:
21	  AaSignalQuery{req: P.AaPerms, signal: List<&2, U32>, peer: List<&2, U32>}
22	
23	def AaSignal.send() -> Nat:
24	  0n
25	
26	def AaSignal.receive() -> Nat:
27	  1n
28	
29	def AaSignal.names() -> List<&2, String>:
30	  ["hup", "int", "quit", "ill", "trap", "abrt", "bus", "fpe", "kill", "usr1", "segv", "usr2", "pipe", "alrm", "term", "stkflt", "chld", "cont", "stop", "stp", "ttin", "ttou", "urg", "xcpu", "xfsz", "vtalrm", "prof", "winch", "io", "pwr", "sys", "emt", "exists"]
31	
32	# the digits of xs as a number, if every character is a digit (at most 3)
33	def AaSignal.num.go(xs: List<&2, U32>, +acc: U32, +n: Nat) -> Maybe<&2, U32>:
34	  match xs:
35	    case Nil{}:
36	      Bool.pick(Maybe<&2, U32>, Nat.is_eq(n, 0n), None{}, Some{acc})
37	    case Con{+h, t}:
38	      Bool.pick(Maybe<&2, U32>, Bool.and(Bool.and(U32.is_ge(h, 48), U32.is_le(h, 57)), Nat.is_lt(n, 3n)), AaSignal.num.go(t, U32.add(U32.mul(acc, 10), U32.sub(h, 48)), 1n+n), None{})
39	
40	def AaSignal.rt.go(m: Maybe<&2, U32>) -> Bool:
41	  match m:
42	    case None{}:
43	      False{}
44	    case Some{v}:
45	      U32.is_le(v, 32)
46	
47	# rtmin+0 ... rtmin+32
48	def AaSignal.is_rt(+w: List<&2, U32>) -> Bool:
49	  Bool.and(X.AaText.starts(w, "rtmin+"), AaSignal.rt.go(AaSignal.num.go(X.AaText.drop(6n, w), 0, 0n)))
50	
51	def AaSignal.valid(+w: List<&2, U32>) -> Bool:
52	  Bool.or(X.AaText.one_of(AaSignal.names(), w), AaSignal.is_rt(w))
53	
54	def AaSignal.check(xs: List<&2, List<&2, U32>>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>:
55	  match xs:
56	    case Nil{}:
57	      Done{Nil{}}
58	    case Con{+x, rest}:
59	      R.AaRule.check_names.go(AaSignal.valid(x), x, AaSignal.check(rest, src), src)
60	
61	# the bits of an access word
62	def AaSignal.access(+w: List<&2, U32>) -> Maybe<&2, P.AaPerms>:
63	  Bool.pick(Maybe<&2, P.AaPerms>, Bool.or(X.AaText.is(w, "send"), Bool.or(X.AaText.is(w, "w"), X.AaText.is(w, "write"))), Some{P.AaPerms.bit(0n)}, Bool.pick(Maybe<&2, P.AaPerms>, Bool.or(X.AaText.is(w, "receive"), Bool.or(X.AaText.is(w, "r"), X.AaText.is(w, "read"))), Some{P.AaPerms.bit(1n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "rw"), Some{P.AaPerms.of_bits([True{}, True{}])}, None{})))
64	
65	# Reading the conditions: the permissions so far (None: none given yet)
66	
67	type AaSigB is Data:
68	  AaSigB{perms: Maybe<&2, P.AaPerms>, signals: Maybe<&2, List<&2, List<&2, U32>>>, peer: Maybe<&2, G.AaGlob>}
69	
70	def AaSigB.perms(m: Maybe<&2, P.AaPerms>, b: AaSigB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
71	  match m:
72	    case None{}:
73	      Fail{E.AaSrc.syntax(src)}
74	    case Some{p}:
75	      match b:
76	        case AaSigB{bp, s, pe}:
77	          match bp:
78	            case None{}:
79	              Done{AaSigB{Some{p}, s, pe}}
80	            case Some{q}:
81	              Done{AaSigB{Some{P.AaPerms.union(q, p)}, s, pe}}
82	
83	def AaSigB.access_list(xs: List<&2, T.AaTerm>, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
84	  match xs:
85	    case Nil{}:
86	      Done{b}
87	    case Con{x, rest}:
88	      match x:
89	        case T.AaTmWord{w}:
90	          do Result<&2, &2, E.AaError, AaSigB>:
91	            b2 : AaSigB <- AaSigB.perms(AaSignal.access(w), b, src)
92	            AaSigB.access_list(rest, b2, src)
93	        case _:
94	          Fail{E.AaSrc.syntax(src)}
95	
96	def AaSigB.add_signals(b: AaSigB, xs: List<&2, List<&2, U32>>) -> AaSigB:
97	  match b:
98	    case AaSigB{p, s, pe}:
99	      match s:
100	        case None{}:
101	          AaSigB{p, Some{xs}, pe}
102	        case Some{ys}:
103	          AaSigB{p, Some{X.AaText.lappend(ys, xs)}, pe}
104	
105	def AaSigB.set_peer(b: AaSigB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
106	  match b:
107	    case AaSigB{p, s, pe}:
108	      match pe:
109	        case None{}:
110	          Done{AaSigB{p, s, Some{g}}}
111	        case Some{h}:
112	          Fail{E.AaSrc.syntax(src)}
113	
114	def AaSigB.cond.set(v: T.AaTerm, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
115	  do Result<&2, &2, E.AaError, AaSigB>:
116	    xs : List<&2, List<&2, U32>> <- R.AaRule.texts(T.AaTerm.texts(v), src)
117	    ys : List<&2, List<&2, U32>> <- AaSignal.check(xs, src)
118	    return AaSigB.add_signals(b, ys)
119	
120	def AaSigB.cond.peer(v: T.AaTerm, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
121	  do Result<&2, &2, E.AaError, AaSigB>:
122	    g : G.AaGlob <- R.AaRule.value_glob(v, src)
123	    AaSigB.set_peer(b, g, src)
124	
125	def AaSigB.cond(+k: List<&2, U32>, +v: T.AaTerm, +b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
126	  Bool.pick(Result<&2, &2, E.AaError, AaSigB>, X.AaText.is(k, "set"), AaSigB.cond.set(v, b, src), Bool.pick(Result<&2, &2, E.AaError, AaSigB>, X.AaText.is(k, "peer"), AaSigB.cond.peer(v, b, src), Fail{E.AaSrc.syntax(src)}))
127	
128	def AaSigB.step(t: T.AaTerm, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
129	  match t:
130	    case T.AaTmWord{w}:
131	      AaSigB.perms(AaSignal.access(w), b, src)
132	    case T.AaTmList{xs}:
133	      AaSigB.access_list(xs, b, src)
134	    case T.AaTmCond{k, v}:
135	      AaSigB.cond(k, v, b, src)
136	    case _:
137	      Fail{E.AaSrc.syntax(src)}
138	
139	def AaSigB.run(ts: List<&2, T.AaTerm>, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
140	  match ts:
141	    case Nil{}:
142	      Done{b}
143	    case Con{t, rest}:
144	      do Result<&2, &2, E.AaError, AaSigB>:
145	        b2 : AaSigB <- AaSigB.step(t, b, src)
146	        AaSigB.run(rest, b2, src)
147	
148	def AaSigB.finish(q: P.AaQual, b: AaSigB) -> AaSignalRule:
149	  match b:
150	    case AaSigB{p, s, pe}:
151	      AaSignalRule{q, Maybe.default(&2, P.AaPerms, p, P.AaPerms.of_bits([True{}, True{}])), s, pe}
152	
153	def AaSignal.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSignalRule>:
154	  match r:
155	    case Fail{e}:
156	      Fail{e}
157	    case Done{q}:
158	      do Result<&2, &2, E.AaError, AaSignalRule>:
159	        b : AaSigB <- AaSigB.run(ts, AaSigB{None{}, None{}, None{}}, src)
160	        return AaSigB.finish(q, b)
161	
162	# the terms after `signal`
163	def AaSignal.parse(ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSignalRule>:
164	  AaSignal.parse.q(R.AaRule.no_owner(q, src), ts, src)
165	
166	# Matching
167	
168	def AaSignal.opt_member(m: Maybe<&2, List<&2, List<&2, U32>>>, +x: List<&2, U32>) -> Bool:
169	  match m:
170	    case None{}:
171	      True{}
172	    case Some{xs}:
173	      X.AaText.member(xs, x)
174	
175	def AaSignalRule.matches(r: AaSignalRule, q: AaSignalQuery) -> Bool:
176	  match r:
177	    case AaSignalRule{qu, p, s, pe}:
178	      match q:
179	        case AaSignalQuery{req, sig, peer}:
180	          Bool.and(AaSignal.opt_member(s, sig), R.AaRule.opt_match(pe, peer))
181	
182	def AaSignalRule.matching.go(hit: Bool, r: AaSignalRule, rest: List<&2, AaSignalRule>) -> List<&2, AaSignalRule>:
183	  match hit:
184	    case True{}:
185	      Con{r, rest}
186	    case False{}:
187	      rest
188	
189	def AaSignalRule.matching(rs: List<&2, AaSignalRule>, +q: AaSignalQuery) -> List<&2, AaSignalRule>:
190	  match rs:
191	    case Nil{}:
192	      Nil{}
193	    case Con{+r, t}:
194	      AaSignalRule.matching.go(AaSignalRule.matches(r, q), r, AaSignalRule.matching(t, q))
195	
196	def AaSignalRule.grants.of(rs: List<&2, AaSignalRule>) -> List<&2, P.AaGrant>:
197	  match rs:
198	    case Nil{}:
199	      Nil{}
200	    case Con{r, t}:
201	      match r:
202	        case AaSignalRule{qu, p, s, pe}:
203	          Con{P.AaGrant.of(qu, p), AaSignalRule.grants.of(t)}
204	
205	def AaSignalRule.grants(rs: List<&2, AaSignalRule>, +q: AaSignalQuery) -> List<&2, P.AaGrant>:
206	  AaSignalRule.grants.of(AaSignalRule.matching(rs, q))
207	
208	def AaSignalRule.append(xs: List<&2, AaSignalRule>, ys: List<&2, AaSignalRule>) -> List<&2, AaSignalRule>:
209	  match xs:
210	    case Nil{}:
211	      ys
212	    case Con{h, t}:
213	      Con{h, AaSignalRule.append(t, ys)}
214	
215	def AaSignalQuery.req(q: AaSignalQuery) -> P.AaPerms:
216	  match q:
217	    case AaSignalQuery{r, s, p}:
218	      r