1	# bend-osdev-acpi, aml_resource.bend: resource data types (ACPI 6.5,
2	# section 6.4), what _CRS, _PRS and _SRS buffers hold. A resource template
3	# is a run of descriptors ending with an End Tag:
4	#
5	#   small (bit 7 clear): a byte holding the type (bits 6-3) and the length
6	#     (bits 2-0), then that many bytes. Read here: IRQ (type 4, 6.4.2.1),
7	#     DMA (5, 6.4.2.2), I/O port (8, 6.4.2.5), fixed I/O (9, 6.4.2.6),
8	#     End Tag (15)
9	#   large (bit 7 set): the type in bits 6-0, a 2-byte length, then that
10	#     many bytes. Read here: 32-bit memory range (5, 6.4.3.3), 32-bit fixed
11	#     memory range (6, 6.4.3.4), DWord, Word and QWord address space (7, 8,
12	#     10: 6.4.3.5.1-3), extended interrupt (9, 6.4.3.6)
13	#
14	# Every other descriptor is kept as AmlROther with its tag and bytes.
15	import Base
16	import bend-osdev-word64@0.1.0.0/word64.bend as W
17	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18	import ./error.bend as E
19	import ./fields.bend as F
20	
21	type AmlResource is Data:
22	  # IRQ: the mask of IRQs 0-15, and the flags byte (0x01 if absent: edge,
23	  # active high)
24	  AmlRIrq{mask: U32, flags: U32}
25	  AmlRDma{mask: U32, flags: U32}
26	  # I/O port: decode (1: 16-bit), minimum and maximum base, alignment,
27	  # length
28	  AmlRIo{decode: U32, min: U32, max: U32, align: U32, len: U32}
29	  AmlRFixedIo{base: U32, len: U32}
30	  # 32-bit memory: write status (1: writable), minimum and maximum base,
31	  # alignment, length
32	  AmlRMem32{writable: U32, min: U32, max: U32, align: U32, len: U32}
33	  AmlRMem32Fixed{writable: U32, base: U32, len: U32}
34	  # an address space descriptor (DWord, Word or QWord: width 32, 16, 64):
35	  # resource type (0 memory, 1 I/O, 2 bus number), general flags, type
36	  # specific flags, then granularity, minimum, maximum, translation offset
37	  # and length, in an address-range record
38	  AmlRAddr{width: U32, kind: U32, flags: U32, tflags: U32, range: AmlRange}
39	  # extended interrupt: flags (bit 0 consumer, 1 edge, 2 active low,
40	  # 3 shared, 4 wake capable) and the interrupt numbers
41	  AmlRExtIrq{flags: U32, irqs: List<&2, U32>}
42	  AmlROther{tag: U32, data: B.Octets}
43	
44	type AmlRange is Data:
45	  AmlRange{gran: W.W64, min: W.W64, max: W.W64, tra: W.W64, len: W.W64}
46	
47	# Reading one descriptor; d: its bytes after the tag (and, for a large
48	# one, after its length)
49	
50	def res.u.go(+w: Nat, +d: B.Octets, +i: Nat) -> W.W64:
51	  match w:
52	    case 2n:
53	      W.W64.from_u32(F.AcpiF.u16(d, i))
54	    case 4n:
55	      W.W64.from_u32(F.AcpiF.u32(d, i))
56	    case _:
57	      F.AcpiF.u64(d, i)
58	
59	def res.u(+d: B.Octets, +i: Nat, +w: Nat) -> W.W64:
60	  res.u.go(w, d, i)
61	
62	# an address space descriptor whose fields are w bytes wide
63	def res.addr(+bits: U32, +w: Nat, +d: B.Octets) -> AmlResource:
64	  AmlRAddr{bits, F.AcpiF.u8(d, 0n), F.AcpiF.u8(d, 1n), F.AcpiF.u8(d, 2n), AmlRange{res.u(d, 3n, w), res.u(d, Nat.add(3n, w), w), res.u(d, Nat.add(3n, Nat.mul(2n, w)), w), res.u(d, Nat.add(3n, Nat.mul(3n, w)), w), res.u(d, Nat.add(3n, Nat.mul(4n, w)), w)}}
65	
66	def res.irqs(n: Nat, +d: B.Octets, +i: Nat) -> List<&2, U32>:
67	  match n:
68	    case 0n:
69	      Nil{}
70	    case 1n+p:
71	      Con{F.AcpiF.u32(d, i), res.irqs(p, d, Nat.add(i, 4n))}
72	
73	def res.irq.flags.pick(has: Bool, +d: B.Octets) -> U32:
74	  match has:
75	    case True{}:
76	      F.AcpiF.u8(d, 2n)
77	    case False{}:
78	      1
79	
80	def res.irq.flags(+d: B.Octets) -> U32:
81	  res.irq.flags.pick(Nat.is_le(3n, B.Octets.len(d)), d)
82	
83	def res.small(+t: Nat, +d: B.Octets) -> AmlResource:
84	  match t:
85	    case 4n:
86	      AmlRIrq{F.AcpiF.u16(d, 0n), res.irq.flags(d)}
87	    case 5n:
88	      AmlRDma{F.AcpiF.u8(d, 0n), F.AcpiF.u8(d, 1n)}
89	    case 8n:
90	      AmlRIo{F.AcpiF.u8(d, 0n), F.AcpiF.u16(d, 1n), F.AcpiF.u16(d, 3n), F.AcpiF.u8(d, 5n), F.AcpiF.u8(d, 6n)}
91	    case 9n:
92	      AmlRFixedIo{F.AcpiF.u16(d, 0n), F.AcpiF.u8(d, 2n)}
93	    case _:
94	      AmlROther{U32.shln(U32.from_nat(t), 3n), d}
95	
96	# the minimum lengths of the descriptors read
97	def res.min.small(+t: Nat) -> Nat:
98	  match t:
99	    case 4n:
100	      2n
101	    case 5n:
102	      2n
103	    case 8n:
104	      7n
105	    case 9n:
106	      3n
107	    case _:
108	      0n
109	
110	def res.min.large(+t: Nat) -> Nat:
111	  match t:
112	    case 5n:
113	      17n
114	    case 6n:
115	      9n
116	    case 7n:
117	      23n
118	    case 8n:
119	      13n
120	    case 10n:
121	      43n
122	    case 9n:
123	      2n
124	    case _:
125	      0n
126	
127	# The walk: one descriptor per step
128	
129	type AmlResNext is Data:
130	  AmlResMore{res: AmlResource, rest: B.Octets}
131	  AmlResEnd{}
132	
133	def res.small.end(end: Bool, +t: Nat, +n: Nat, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
134	  match end:
135	    case True{}:
136	      Done{AmlResEnd{}}
137	    case False{}:
138	      Done{AmlResMore{res.small(t, B.Octets.take(n, o)), B.Octets.drop(n, o)}}
139	
140	def res.small.fit(ok: Bool, +t: Nat, +n: Nat, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
141	  match ok:
142	    case False{}:
143	      Fail{E.AcpiBadEntry{0n, U32.from_nat(t)}}
144	    case True{}:
145	      res.small.end(Nat.is_eq(t, 15n), t, n, o)
146	
147	def res.small.go(+t: Nat, +n: Nat, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
148	  res.small.fit(Bool.and(Nat.is_le(n, B.Octets.len(o)), Nat.is_le(res.min.small(t), n)), t, n, o)
149	
150	# Text
151	
152	def res.show.irqs(xs: List<&2, U32>) -> List<&2, String>:
153	  match xs:
154	    case Nil{}:
155	      Nil{}
156	    case Con{x, t}:
157	      Con{U32.show(x), res.show.irqs(t)}
158	
159	def AmlResource.show(r: AmlResource) -> String:
160	  match r:
161	    case AmlRIrq{m, f}:
162	      "irq mask " ++ U32.show(m) ++ " flags " ++ U32.show(f)
163	    case AmlRDma{m, f}:
164	      "dma mask " ++ U32.show(m) ++ " flags " ++ U32.show(f)
165	    case AmlRIo{dc, mn, mx, al, l}:
166	      "io " ++ U32.show(mn) ++ "-" ++ U32.show(mx) ++ " align " ++ U32.show(al) ++ " len " ++ U32.show(l)
167	    case AmlRFixedIo{b, l}:
168	      "fixed io " ++ U32.show(b) ++ " len " ++ U32.show(l)
169	    case AmlRMem32{wr, mn, mx, al, l}:
170	      "mem32 " ++ U32.show(mn) ++ "-" ++ U32.show(mx) ++ " len " ++ U32.show(l)
171	    case AmlRMem32Fixed{wr, b, l}:
172	      "mem32 fixed " ++ U32.show(b) ++ " len " ++ U32.show(l)
173	    case AmlRAddr{bits, k, f, tf, AmlRange{g, mn, mx, t, l}}:
174	      "addr" ++ U32.show(bits) ++ " type " ++ U32.show(k) ++ " " ++ W.W64.show_hex(mn) ++ "-" ++ W.W64.show_hex(mx) ++ " len " ++ W.W64.show_hex(l)
175	    case AmlRExtIrq{f, irqs}:
176	      "extirq flags " ++ U32.show(f) ++ " " ++ String.join(res.show.irqs(irqs), ",")
177	    case AmlROther{t, d}:
178	      "other " ++ U32.show(t) ++ " " ++ B.Octets.hex(d)
179	
180	# Writing: each descriptor as bytes, and a template (descriptors, then an
181	# End Tag whose checksum byte is 0, which section 6.4.2 accepts)
182	
183	def res.b(xs: List<&2, U32>) -> B.Octets:
184	  B.Octets.of_list(xs)
185	
186	def res.w.go(+n: Nat, +v: W.W64) -> B.Octets:
187	  match n:
188	    case 16n:
189	      B.Octets.le16(W.W64.lo(v))
190	    case 32n:
191	      B.Octets.le32(W.W64.lo(v))
192	    case _:
193	      B.Octets.le64(v)
194	
195	def res.w(+width: U32, +v: W.W64) -> B.Octets:
196	  res.w.go(U32.to_nat(width), v)
197	
198	def res.lenc(+t: U32, +d: B.Octets) -> B.Octets:
199	  B.Octets.append(B.Octets.append(res.b([t]), B.Octets.le16(U32.from_nat(B.Octets.len(d)))), d)
200	
201	def res.large(+t: Nat, +d: B.Octets) -> AmlResource:
202	  match t:
203	    case 5n:
204	      AmlRMem32{F.AcpiF.u8(d, 0n), F.AcpiF.u32(d, 1n), F.AcpiF.u32(d, 5n), F.AcpiF.u32(d, 9n), F.AcpiF.u32(d, 13n)}
205	    case 6n:
206	      AmlRMem32Fixed{F.AcpiF.u8(d, 0n), F.AcpiF.u32(d, 1n), F.AcpiF.u32(d, 5n)}
207	    case 7n:
208	      res.addr(32, 4n, d)
209	    case 8n:
210	      res.addr(16, 2n, d)
211	    case 10n:
212	      res.addr(64, 8n, d)
213	    case 9n:
214	      AmlRExtIrq{F.AcpiF.u8(d, 0n), res.irqs(U32.to_nat(F.AcpiF.u8(d, 1n)), d, 2n)}
215	    case _:
216	      AmlROther{U32.add(128, U32.from_nat(t)), d}
217	
218	def res.large.fit(ok: Bool, +t: Nat, +n: Nat, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
219	  match ok:
220	    case False{}:
221	      Fail{E.AcpiBadEntry{0n, U32.add(128, U32.from_nat(t))}}
222	    case True{}:
223	      Done{AmlResMore{res.large(t, B.Octets.take(n, o)), B.Octets.drop(n, o)}}
224	
225	def res.large.go(+t: Nat, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
226	  +n = U32.to_nat(F.AcpiF.u16(o, 0n))
227	  res.large.fit(Bool.and(Nat.is_le(Nat.add(2n, n), B.Octets.len(o)), Nat.is_le(res.min.large(t), n)), t, n, B.Octets.drop(2n, o))
228	
229	def res.tag.pick(small: Bool, +b: U32, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
230	  match small:
231	    case True{}:
232	      res.small.go(U32.to_nat(U32.and(U32.shrn(b, 3n), 15)), U32.to_nat(U32.and(b, 7)), o)
233	    case False{}:
234	      res.large.go(U32.to_nat(U32.and(b, 127)), o)
235	
236	def res.tag(+b: U32, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
237	  res.tag.pick(U32.is_eq(U32.and(b, 128), 0), b, o)
238	
239	def res.step.pick(m: Maybe<&2, U32>, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
240	  match m:
241	    case None{}:
242	      Done{AmlResEnd{}}
243	    case Some{+b}:
244	      res.tag(b, B.Octets.drop(1n, o))
245	
246	def res.step(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
247	  res.step.pick(B.Octets.at(o, 0n), o)
248	
249	def res.loop(fuel: Nat, r: Result<&2, &2, E.AcpiError, AmlResNext>, acc: List<&2, AmlResource>) -> Result<&2, &2, E.AcpiError, List<&2, AmlResource>>:
250	  match fuel:
251	    case 0n:
252	      Done{List.reverse(&2, AmlResource, acc)}
253	    case 1n+p:
254	      match r:
255	        case Fail{e}:
256	          Fail{e}
257	        case Done{AmlResEnd{}}:
258	          Done{List.reverse(&2, AmlResource, acc)}
259	        case Done{AmlResMore{x, +rest}}:
260	          res.loop(p, res.step(rest), Con{x, acc})
261	
262	# the descriptors of a resource template, up to its End Tag (or its end);
263	# AcpiBadEntry for a descriptor shorter than its type needs or that runs
264	# past the buffer
265	def AmlResource.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, List<&2, AmlResource>>:
266	  res.loop(Nat.add(B.Octets.len(o), 1n), res.step(o), Nil{})
267	
268	def res.addr.tag.go(+n: Nat) -> U32:
269	  match n:
270	    case 16n:
271	      136
272	    case 32n:
273	      135
274	    case _:
275	      138
276	
277	def res.addr.tag(+width: U32) -> U32:
278	  res.addr.tag.go(U32.to_nat(width))
279	
280	def res.irqs.enc(xs: List<&2, U32>) -> B.Octets:
281	  match xs:
282	    case Nil{}:
283	      B.Octets.empty()
284	    case Con{x, t}:
285	      B.Octets.append(B.Octets.le32(x), res.irqs.enc(t))
286	
287	def res.other(small: Bool, +t: U32, +d: B.Octets) -> B.Octets:
288	  match small:
289	    case True{}:
290	      B.Octets.append(res.b([U32.or(t, U32.from_nat(B.Octets.len(d)))]), d)
291	    case False{}:
292	      res.lenc(t, d)
293	
294	def AmlResource.encode(r: AmlResource) -> B.Octets:
295	  match r:
296	    case AmlRIrq{m, f}:
297	      B.Octets.append(res.b([35]), B.Octets.append(B.Octets.le16(m), res.b([f])))
298	    case AmlRDma{m, f}:
299	      res.b([42, m, f])
300	    case AmlRIo{dc, mn, mx, al, l}:
301	      B.Octets.concat([res.b([71, dc]), B.Octets.le16(mn), B.Octets.le16(mx), res.b([al, l])])
302	    case AmlRFixedIo{b, l}:
303	      B.Octets.concat([res.b([75]), B.Octets.le16(b), res.b([l])])
304	    case AmlRMem32{wr, mn, mx, al, l}:
305	      res.lenc(133, B.Octets.concat([res.b([wr]), B.Octets.le32(mn), B.Octets.le32(mx), B.Octets.le32(al), B.Octets.le32(l)]))
306	    case AmlRMem32Fixed{wr, b, l}:
307	      res.lenc(134, B.Octets.concat([res.b([wr]), B.Octets.le32(b), B.Octets.le32(l)]))
308	    case AmlRAddr{+bits, k, f, tf, AmlRange{g, mn, mx, t, l}}:
309	      res.lenc(res.addr.tag(bits), B.Octets.concat([res.b([k, f, tf]), res.w(bits, g), res.w(bits, mn), res.w(bits, mx), res.w(bits, t), res.w(bits, l)]))
310	    case AmlRExtIrq{f, +irqs}:
311	      res.lenc(137, B.Octets.concat([res.b([f, U32.from_nat(List.length(&2, U32, irqs))]), res.irqs.enc(irqs)]))
312	    case AmlROther{+t, +d}:
313	      res.other(U32.is_lt(t, 128), t, d)
314	
315	def res.enc.all(rs: List<&2, AmlResource>) -> B.Octets:
316	  match rs:
317	    case Nil{}:
318	      res.b([121, 0])
319	    case Con{r, t}:
320	      B.Octets.append(AmlResource.encode(r), res.enc.all(t))
321	
322	# a resource template: the descriptors, then the End Tag
323	def AmlResource.template(rs: List<&2, AmlResource>) -> B.Octets:
324	  res.enc.all(rs)