madt.bend
bend-osdev-acpi@0.1.1.0 · 315 lines · 32 definitions
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28import Base
29import bend-osdev-word64@0.1.1.0/word64.bend as W
30import bend-osdev-bytes@0.1.1.0/bytes.bend as B
31import bend-osdev-acpi@0.1.1.0/error.bend as E
32import bend-osdev-acpi@0.1.1.0/header.bend as H
33import bend-osdev-acpi@0.1.1.0/fields.bend as F
34import bend-osdev-acpi@0.1.1.0/entries.bend as N
35
36
37type AcpiGiccAddrs is Data:
38 AcpiGiccAddrs{parked: W.W64, base: W.W64, gicv: W.W64, gich: W.W64, gicr: W.W64}
39
40type AcpiMadtEntry is Data:
41
42 AcpiMadtLapic{uid: U32, apic_id: U32, flags: U32}
43 AcpiMadtIoApic{id: U32, address: U32, gsi_base: U32}
44
45 AcpiMadtIso{bus: U32, source: U32, gsi: U32, flags: U32}
46 AcpiMadtNmiSource{flags: U32, gsi: U32}
47
48 AcpiMadtLapicNmi{uid: U32, flags: U32, lint: U32}
49 AcpiMadtLapicOverride{address: W.W64}
50 AcpiMadtX2apic{x2apic_id: U32, flags: U32, uid: U32}
51
52 AcpiMadtX2apicNmi{flags: U32, uid: U32, lint: U32}
53 AcpiMadtGicc{cpu_interface: U32, uid: U32, flags: U32, parking_version: U32, perf_gsiv: U32, vgic_gsiv: U32, addrs: AcpiGiccAddrs, mpidr: W.W64, efficiency_class: U32, spe_gsiv: U32, trbe_gsiv: U32}
54 AcpiMadtGicd{gic_id: U32, base: W.W64, version: U32}
55 AcpiMadtGicMsi{id: U32, base: W.W64, flags: U32, spi_count: U32, spi_base: U32}
56 AcpiMadtGicr{base: W.W64, length: U32}
57 AcpiMadtGicIts{id: U32, base: W.W64}
58 AcpiMadtWakeup{version: U32, mailbox: W.W64}
59
60 AcpiMadtOther{kind: U32, data: B.Octets}
61
62type AcpiMadt is Data:
63 AcpiMadt{header: H.AcpiHeader, lapic_address: U32, flags: U32, entries: List<&2, AcpiMadtEntry>}
64
65def AcpiMadt.entries(m: AcpiMadt) -> List<&2, AcpiMadtEntry>:
66 match m:
67 case AcpiMadt{h, a, f, es}:
68 es
69
70def AcpiMadt.lapic_address32(m: AcpiMadt) -> U32:
71 match m:
72 case AcpiMadt{h, a, f, es}:
73 a
74
75def AcpiMadt.flags(m: AcpiMadt) -> U32:
76 match m:
77 case AcpiMadt{h, a, f, es}:
78 f
79
80
81
82
83def madt.min.go(k: Nat) -> Nat:
84 match k:
85 case 0n:
86 8n
87 case 1n:
88 12n
89 case 2n:
90 10n
91 case 3n:
92 8n
93 case 4n:
94 6n
95 case 5n:
96 12n
97 case 9n:
98 16n
99 case 10n:
100 12n
101 case 11n:
102 76n
103 case 12n:
104 24n
105 case 13n:
106 24n
107 case 14n:
108 16n
109 case 15n:
110 20n
111 case 16n:
112 16n
113 case _:
114 2n
115
116def madt.min(+k: U32) -> Nat:
117 madt.min.go(U32.to_nat(k))
118
119def madt.gicc(+d: B.Octets) -> AcpiMadtEntry:
120 AcpiMadtGicc{F.AcpiF.u32(d, 4n), F.AcpiF.u32(d, 8n), F.AcpiF.u32(d, 12n), F.AcpiF.u32(d, 16n), F.AcpiF.u32(d, 20n), F.AcpiF.u32(d, 56n), AcpiGiccAddrs{F.AcpiF.u64(d, 24n), F.AcpiF.u64(d, 32n), F.AcpiF.u64(d, 40n), F.AcpiF.u64(d, 48n), F.AcpiF.u64(d, 60n)}, F.AcpiF.u64(d, 68n), F.AcpiF.u8(d, 76n), F.AcpiF.u16(d, 78n), F.AcpiF.u16(d, 80n)}
121
122def madt.typed(k: Nat, +d: B.Octets) -> AcpiMadtEntry:
123 match k:
124 case 0n:
125 AcpiMadtLapic{F.AcpiF.u8(d, 2n), F.AcpiF.u8(d, 3n), F.AcpiF.u32(d, 4n)}
126 case 1n:
127 AcpiMadtIoApic{F.AcpiF.u8(d, 2n), F.AcpiF.u32(d, 4n), F.AcpiF.u32(d, 8n)}
128 case 2n:
129 AcpiMadtIso{F.AcpiF.u8(d, 2n), F.AcpiF.u8(d, 3n), F.AcpiF.u32(d, 4n), F.AcpiF.u16(d, 8n)}
130 case 3n:
131 AcpiMadtNmiSource{F.AcpiF.u16(d, 2n), F.AcpiF.u32(d, 4n)}
132 case 4n:
133 AcpiMadtLapicNmi{F.AcpiF.u8(d, 2n), F.AcpiF.u16(d, 3n), F.AcpiF.u8(d, 5n)}
134 case 5n:
135 AcpiMadtLapicOverride{F.AcpiF.u64(d, 4n)}
136 case 9n:
137 AcpiMadtX2apic{F.AcpiF.u32(d, 4n), F.AcpiF.u32(d, 8n), F.AcpiF.u32(d, 12n)}
138 case 10n:
139 AcpiMadtX2apicNmi{F.AcpiF.u16(d, 2n), F.AcpiF.u32(d, 4n), F.AcpiF.u8(d, 8n)}
140 case 11n:
141 madt.gicc(d)
142 case 12n:
143 AcpiMadtGicd{F.AcpiF.u32(d, 4n), F.AcpiF.u64(d, 8n), F.AcpiF.u8(d, 20n)}
144 case 13n:
145 AcpiMadtGicMsi{F.AcpiF.u32(d, 4n), F.AcpiF.u64(d, 8n), F.AcpiF.u32(d, 16n), F.AcpiF.u16(d, 20n), F.AcpiF.u16(d, 22n)}
146 case 14n:
147 AcpiMadtGicr{F.AcpiF.u64(d, 4n), F.AcpiF.u32(d, 12n)}
148 case 15n:
149 AcpiMadtGicIts{F.AcpiF.u32(d, 4n), F.AcpiF.u64(d, 8n)}
150 case 16n:
151 AcpiMadtWakeup{F.AcpiF.u16(d, 2n), F.AcpiF.u64(d, 8n)}
152 case _:
153 AcpiMadtOther{F.AcpiF.u8(d, 0n), B.Octets.drop(2n, d)}
154
155def madt.entry.pick(ok: Bool, +k: U32, +off: Nat, +d: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiMadtEntry>:
156 match ok:
157 case True{}:
158 Done{madt.typed(U32.to_nat(k), d)}
159 case False{}:
160 Fail{E.AcpiBadEntry{off, k}}
161
162def AcpiMadtEntry.of_raw(e: N.AcpiRawEntry) -> Result<&2, &2, E.AcpiError, AcpiMadtEntry>:
163 match e:
164 case N.AcpiRawEntry{+k, off, +d}:
165 madt.entry.pick(Nat.is_le(madt.min(k), B.Octets.len(d)), k, off, d)
166
167def madt.rev(xs: List<&2, AcpiMadtEntry>, acc: List<&2, AcpiMadtEntry>) -> List<&2, AcpiMadtEntry>:
168 match xs:
169 case Nil{}:
170 acc
171 case Con{h, t}:
172 madt.rev(t, Con{h, acc})
173
174def madt.push(acc: Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>, r: Result<&2, &2, E.AcpiError, AcpiMadtEntry>) -> Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>:
175 match acc r:
176 case Fail{e} _:
177 Fail{e}
178 case Done{xs} Done{x}:
179 Done{Con{x, xs}}
180 case Done{xs} Fail{e}:
181 Fail{e}
182
183def madt.fin(r: Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>) -> Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>:
184 match r:
185 case Fail{e}:
186 Fail{e}
187 case Done{xs}:
188 Done{madt.rev(xs, Nil{})}
189
190def madt.all(es: List<&2, N.AcpiRawEntry>, acc: Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>) -> Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>:
191 match es:
192 case Nil{}:
193 madt.fin(acc)
194 case Con{h, t}:
195 madt.all(t, madt.push(acc, AcpiMadtEntry.of_raw(h)))
196
197def madt.mk2(+h: H.AcpiHeader, +a: U32, +f: U32, r: Result<&2, &2, E.AcpiError, List<&2, AcpiMadtEntry>>) -> Result<&2, &2, E.AcpiError, AcpiMadt>:
198 match r:
199 case Fail{e}:
200 Fail{e}
201 case Done{es}:
202 Done{AcpiMadt{h, a, f, es}}
203
204def madt.mk(+h: H.AcpiHeader, +a: U32, +f: U32, r: Result<&2, &2, E.AcpiError, List<&2, N.AcpiRawEntry>>) -> Result<&2, &2, E.AcpiError, AcpiMadt>:
205 match r:
206 case Fail{e}:
207 Fail{e}
208 case Done{es}:
209 madt.mk2(h, a, f, madt.all(es, Done{Nil{}}))
210
211def madt.body(ok: Bool, +h: H.AcpiHeader, +body: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiMadt>:
212 match ok:
213 case False{}:
214 Fail{E.AcpiTooShort{44n, Nat.add(36n, B.Octets.len(body))}}
215 case True{}:
216 madt.mk(h, F.AcpiF.u32(body, 0n), F.AcpiF.u32(body, 4n), N.AcpiRawEntry.split(B.Octets.drop(8n, body), 44n))
217
218
219def AcpiMadt.of_sdt(t: H.AcpiSdt) -> Result<&2, &2, E.AcpiError, AcpiMadt>:
220 match t:
221 case H.AcpiSdt{h, +body}:
222 madt.body(Nat.is_le(8n, B.Octets.len(body)), h, body)
223
224def madt.parse(r: Result<&2, &2, E.AcpiError, H.AcpiSdt>) -> Result<&2, &2, E.AcpiError, AcpiMadt>:
225 match r:
226 case Fail{e}:
227 Fail{e}
228 case Done{t}:
229 AcpiMadt.of_sdt(t)
230
231
232
233def AcpiMadt.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiMadt>:
234 madt.parse(H.AcpiSdt.parse_sig(B.Octets.of_string("APIC"), o))
235
236
237
238def madt.override(es: List<&2, AcpiMadtEntry>, +dflt: W.W64) -> W.W64:
239 match es:
240 case Nil{}:
241 dflt
242 case Con{AcpiMadtLapicOverride{a}, t}:
243 a
244 case Con{e, t}:
245 madt.override(t, dflt)
246
247
248
249def AcpiMadt.lapic_address(m: AcpiMadt) -> W.W64:
250 match m:
251 case AcpiMadt{h, a, f, es}:
252 madt.override(es, W.W64.from_u32(a))
253
254
255
256def madt.u16(v: U32) -> B.Octets:
257 B.Octets.le16(v)
258
259def madt.u32(v: U32) -> B.Octets:
260 B.Octets.le32(v)
261
262def madt.u64(v: W.W64) -> B.Octets:
263 B.Octets.le64(v)
264
265def madt.u8(v: U32) -> B.Octets:
266 B.Octets.of_list([v])
267
268def madt.z(n: Nat) -> B.Octets:
269 B.Octets.zeros(n)
270
271def AcpiMadtEntry.encode(e: AcpiMadtEntry) -> B.Octets:
272 match e:
273 case AcpiMadtLapic{u, a, f}:
274 N.AcpiRawEntry.encode(0, B.Octets.concat([madt.u8(u), madt.u8(a), madt.u32(f)]))
275 case AcpiMadtIoApic{i, a, g}:
276 N.AcpiRawEntry.encode(1, B.Octets.concat([madt.u8(i), madt.z(1n), madt.u32(a), madt.u32(g)]))
277 case AcpiMadtIso{b, s, g, f}:
278 N.AcpiRawEntry.encode(2, B.Octets.concat([madt.u8(b), madt.u8(s), madt.u32(g), madt.u16(f)]))
279 case AcpiMadtNmiSource{f, g}:
280 N.AcpiRawEntry.encode(3, B.Octets.concat([madt.u16(f), madt.u32(g)]))
281 case AcpiMadtLapicNmi{u, f, l}:
282 N.AcpiRawEntry.encode(4, B.Octets.concat([madt.u8(u), madt.u16(f), madt.u8(l)]))
283 case AcpiMadtLapicOverride{a}:
284 N.AcpiRawEntry.encode(5, B.Octets.concat([madt.z(2n), madt.u64(a)]))
285 case AcpiMadtX2apic{x, f, u}:
286 N.AcpiRawEntry.encode(9, B.Octets.concat([madt.z(2n), madt.u32(x), madt.u32(f), madt.u32(u)]))
287 case AcpiMadtX2apicNmi{f, u, l}:
288 N.AcpiRawEntry.encode(10, B.Octets.concat([madt.u16(f), madt.u32(u), madt.u8(l), madt.z(3n)]))
289 case AcpiMadtGicc{ci, u, f, pv, pg, vg, AcpiGiccAddrs{pk, b, gv, gh, gr}, mp, ec, sp, tr}:
290 N.AcpiRawEntry.encode(11, B.Octets.concat([madt.z(2n), madt.u32(ci), madt.u32(u), madt.u32(f), madt.u32(pv), madt.u32(pg), madt.u64(pk), madt.u64(b), madt.u64(gv), madt.u64(gh), madt.u32(vg), madt.u64(gr), madt.u64(mp), madt.u8(ec), madt.z(1n), madt.u16(sp), madt.u16(tr)]))
291 case AcpiMadtGicd{i, b, v}:
292 N.AcpiRawEntry.encode(12, B.Octets.concat([madt.z(2n), madt.u32(i), madt.u64(b), madt.z(4n), madt.u8(v), madt.z(3n)]))
293 case AcpiMadtGicMsi{i, b, f, c, s}:
294 N.AcpiRawEntry.encode(13, B.Octets.concat([madt.z(2n), madt.u32(i), madt.u64(b), madt.u32(f), madt.u16(c), madt.u16(s)]))
295 case AcpiMadtGicr{b, l}:
296 N.AcpiRawEntry.encode(14, B.Octets.concat([madt.z(2n), madt.u64(b), madt.u32(l)]))
297 case AcpiMadtGicIts{i, b}:
298 N.AcpiRawEntry.encode(15, B.Octets.concat([madt.z(2n), madt.u32(i), madt.u64(b), madt.z(4n)]))
299 case AcpiMadtWakeup{v, m}:
300 N.AcpiRawEntry.encode(16, B.Octets.concat([madt.u16(v), madt.z(4n), madt.u64(m)]))
301 case AcpiMadtOther{k, d}:
302 N.AcpiRawEntry.encode(k, d)
303
304def madt.enc(es: List<&2, AcpiMadtEntry>) -> List<&2, B.Octets>:
305 match es:
306 case Nil{}:
307 Nil{}
308 case Con{h, t}:
309 Con{AcpiMadtEntry.encode(h), madt.enc(t)}
310
311
312def AcpiMadt.build(m: AcpiMadt) -> B.Octets:
313 match m:
314 case AcpiMadt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, a, f, es}:
315 H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("APIC"), l, r, c, o, t, orv, ci, cr}, B.Octets.append(B.Octets.append(madt.u32(a), madt.u32(f)), B.Octets.concat(madt.enc(es))))