aml_resource.bend
bend-osdev-acpi@0.1.2.0 · 324 lines · 0 definitions
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.
15import Base
16import bend-osdev-word64@0.1.1.1/word64.bend as W
17import bend-osdev-bytes@0.1.1.1/bytes.bend as B
18import bend-osdev-acpi@0.1.2.0/error.bend as E
19import bend-osdev-acpi@0.1.2.0/fields.bend as F
20
21type 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
44type 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
50def 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
59def 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
63def 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
66def 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
73def 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
80def res.irq.flags(+d: B.Octets) -> U32:
81 res.irq.flags.pick(Nat.is_le(3n, B.Octets.len(d)), d)
82
83def 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
97def 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
110def 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
129type AmlResNext is Data:
130 AmlResMore{res: AmlResource, rest: B.Octets}
131 AmlResEnd{}
132
133def 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
140def 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
147def 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
152def 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
159def 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
183def res.b(xs: List<&2, U32>) -> B.Octets:
184 B.Octets.of_list(xs)
185
186def 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
195def res.w(+width: U32, +v: W.W64) -> B.Octets:
196 res.w.go(U32.to_nat(width), v)
197
198def 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
201def 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
218def 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
225def 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
229def 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
236def 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
239def 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
246def res.step(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlResNext>:
247 res.step.pick(B.Octets.at(o, 0n), o)
248
249def 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
265def 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
268def 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
277def res.addr.tag(+width: U32) -> U32:
278 res.addr.tag.go(U32.to_nat(width))
279
280def 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
287def 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
294def 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
315def 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
323def AmlResource.template(rs: List<&2, AmlResource>) -> B.Octets:
324 res.enc.all(rs)