fadt.bend
bend-osdev-acpi@0.1.2.0 · 312 lines · 0 definitions
1# bend-osdev-acpi, fadt.bend: the Fixed ACPI Description Table, "FACP"
2# (ACPI 6.5, section 5.2.9). Every field of revision 6 (276
3# bytes), grouped by the version that added it; a group is present when the
4# table's length covers all of it:
5#
6# bytes group since
7# 36-115 AcpiFadtCore: FIRMWARE_CTRL, DSDT, the ACPI 1.0 ACPI 1.0 (116)
8# register blocks and lengths, latencies, RTC
9# alarms, IAPC_BOOT_ARCH, Flags
10# 116-243 AcpiFadtExt: RESET_REG, RESET_VALUE, ACPI 2.0 (244)
11# ARM_BOOT_ARCH, FADT Minor Version, X_FIRMWARE_CTRL,
12# X_DSDT and the eight X_ register blocks
13# 244-267 AcpiFadtSleep: SLEEP_CONTROL_REG, ACPI 5.0 (268)
14# SLEEP_STATUS_REG
15# 268-275 Hypervisor Vendor Identity ACPI 6.0 (276)
16#
17# (ARM_BOOT_ARCH and the minor version came in ACPI 5.1 in bytes that were
18# reserved before, so older tables read 0 there.) Section 5.2.9 says the X_
19# forms supersede the 32-bit ones when their address is non-zero; the
20# AcpiFadt.* queries below choose that way.
21import Base
22import bend-osdev-word64@0.1.1.1/word64.bend as W
23import bend-osdev-bytes@0.1.1.1/bytes.bend as B
24import bend-osdev-acpi@0.1.2.0/error.bend as E
25import bend-osdev-acpi@0.1.2.0/header.bend as H
26import bend-osdev-acpi@0.1.2.0/fields.bend as F
27import bend-osdev-acpi@0.1.2.0/gas.bend as G
28
29# the ACPI 1.0 register blocks: I/O port addresses
30type AcpiFadtBlocks is Data:
31 AcpiFadtBlocks{pm1a_evt: U32, pm1b_evt: U32, pm1a_cnt: U32, pm1b_cnt: U32, pm2_cnt: U32, pm_tmr: U32, gpe0: U32, gpe1: U32}
32
33# their lengths in bytes, and GPE1_BASE
34type AcpiFadtLens is Data:
35 AcpiFadtLens{pm1_evt: U32, pm1_cnt: U32, pm2_cnt: U32, pm_tmr: U32, gpe0: U32, gpe1: U32, gpe1_base: U32}
36
37# bytes 36 to 115. int_model is byte 44, reserved since ACPI 2.0
38type AcpiFadtCore is Data:
39 AcpiFadtCore{firmware_ctrl: U32, dsdt: U32, int_model: U32, pm_profile: U32, sci_int: U32, smi_cmd: U32, acpi_enable: U32, acpi_disable: U32, s4bios_req: U32, pstate_cnt: U32, blocks: AcpiFadtBlocks, lens: AcpiFadtLens, cst_cnt: U32, p_lvl2_lat: U32, p_lvl3_lat: U32, flush_size: U32, flush_stride: U32, duty_offset: U32, duty_width: U32, day_alrm: U32, mon_alrm: U32, century: U32, iapc_boot_arch: U32, flags: U32}
40
41# the X_ register blocks (Generic Address Structures)
42type AcpiFadtX is Data:
43 AcpiFadtX{pm1a_evt: G.AcpiGas, pm1b_evt: G.AcpiGas, pm1a_cnt: G.AcpiGas, pm1b_cnt: G.AcpiGas, pm2_cnt: G.AcpiGas, pm_tmr: G.AcpiGas, gpe0: G.AcpiGas, gpe1: G.AcpiGas}
44
45# bytes 116 to 243
46type AcpiFadtExt is Data:
47 AcpiFadtExt{reset_reg: G.AcpiGas, reset_value: U32, arm_boot_arch: U32, minor_version: U32, x_firmware_ctrl: W.W64, x_dsdt: W.W64, x: AcpiFadtX}
48
49# bytes 244 to 267
50type AcpiFadtSleep is Data:
51 AcpiFadtSleep{control: G.AcpiGas, status: G.AcpiGas}
52
53type AcpiFadt is Data:
54 AcpiFadt{header: H.AcpiHeader, core: AcpiFadtCore, ext: Maybe<&2, AcpiFadtExt>, sleep: Maybe<&2, AcpiFadtSleep>, hypervisor: Maybe<&2, W.W64>}
55
56# Reading (o: the whole table; offsets from its start)
57
58def fadt.core(+o: B.Octets) -> AcpiFadtCore:
59 +blocks = {AcpiFadtBlocks{F.AcpiF.u32(o, 56n), F.AcpiF.u32(o, 60n), F.AcpiF.u32(o, 64n), F.AcpiF.u32(o, 68n), F.AcpiF.u32(o, 72n), F.AcpiF.u32(o, 76n), F.AcpiF.u32(o, 80n), F.AcpiF.u32(o, 84n)} : AcpiFadtBlocks}
60 +lens = {AcpiFadtLens{F.AcpiF.u8(o, 88n), F.AcpiF.u8(o, 89n), F.AcpiF.u8(o, 90n), F.AcpiF.u8(o, 91n), F.AcpiF.u8(o, 92n), F.AcpiF.u8(o, 93n), F.AcpiF.u8(o, 94n)} : AcpiFadtLens}
61 AcpiFadtCore{F.AcpiF.u32(o, 36n), F.AcpiF.u32(o, 40n), F.AcpiF.u8(o, 44n), F.AcpiF.u8(o, 45n), F.AcpiF.u16(o, 46n), F.AcpiF.u32(o, 48n), F.AcpiF.u8(o, 52n), F.AcpiF.u8(o, 53n), F.AcpiF.u8(o, 54n), F.AcpiF.u8(o, 55n), blocks, lens, F.AcpiF.u8(o, 95n), F.AcpiF.u16(o, 96n), F.AcpiF.u16(o, 98n), F.AcpiF.u16(o, 100n), F.AcpiF.u16(o, 102n), F.AcpiF.u8(o, 104n), F.AcpiF.u8(o, 105n), F.AcpiF.u8(o, 106n), F.AcpiF.u8(o, 107n), F.AcpiF.u8(o, 108n), F.AcpiF.u16(o, 109n), F.AcpiF.u32(o, 112n)}
62
63def fadt.x(+o: B.Octets) -> AcpiFadtX:
64 AcpiFadtX{G.AcpiGas.at(o, 148n), G.AcpiGas.at(o, 160n), G.AcpiGas.at(o, 172n), G.AcpiGas.at(o, 184n), G.AcpiGas.at(o, 196n), G.AcpiGas.at(o, 208n), G.AcpiGas.at(o, 220n), G.AcpiGas.at(o, 232n)}
65
66def fadt.ext(has: Bool, +o: B.Octets) -> Maybe<&2, AcpiFadtExt>:
67 match has:
68 case False{}:
69 None{}
70 case True{}:
71 Some{AcpiFadtExt{G.AcpiGas.at(o, 116n), F.AcpiF.u8(o, 128n), F.AcpiF.u16(o, 129n), F.AcpiF.u8(o, 131n), F.AcpiF.u64(o, 132n), F.AcpiF.u64(o, 140n), fadt.x(o)}}
72
73def fadt.sleep(has: Bool, +o: B.Octets) -> Maybe<&2, AcpiFadtSleep>:
74 match has:
75 case False{}:
76 None{}
77 case True{}:
78 Some{AcpiFadtSleep{G.AcpiGas.at(o, 244n), G.AcpiGas.at(o, 256n)}}
79
80def fadt.hyp(has: Bool, +o: B.Octets) -> Maybe<&2, W.W64>:
81 match has:
82 case False{}:
83 None{}
84 case True{}:
85 Some{F.AcpiF.u64(o, 268n)}
86
87def fadt.read(ok: Bool, +h: H.AcpiHeader, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiFadt>:
88 match ok:
89 case False{}:
90 Fail{E.AcpiTooShort{116n, B.Octets.len(o)}}
91 case True{}:
92 +n = B.Octets.len(o)
93 Done{AcpiFadt{h, fadt.core(o), fadt.ext(Nat.is_le(244n, n), o), fadt.sleep(Nat.is_le(268n, n), o), fadt.hyp(Nat.is_le(276n, n), o)}}
94
95# a checked table as an FADT (at least the 116 bytes of ACPI 1.0)
96def AcpiFadt.of_sdt(t: H.AcpiSdt) -> Result<&2, &2, E.AcpiError, AcpiFadt>:
97 match t:
98 case H.AcpiSdt{+h, body}:
99 +o = B.Octets.append(H.AcpiHeader.encode(h), body)
100 fadt.read(Nat.is_le(116n, B.Octets.len(o)), h, o)
101
102def fadt.parse(r: Result<&2, &2, E.AcpiError, H.AcpiSdt>) -> Result<&2, &2, E.AcpiError, AcpiFadt>:
103 match r:
104 case Fail{e}:
105 Fail{e}
106 case Done{t}:
107 AcpiFadt.of_sdt(t)
108
109# the FADT at the front of o: checked (length, checksum, signature "FACP"),
110# then read
111def AcpiFadt.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiFadt>:
112 fadt.parse(H.AcpiSdt.parse_sig(B.Octets.of_string("FACP"), o))
113
114# Fields
115
116def AcpiFadt.core(f: AcpiFadt) -> AcpiFadtCore:
117 match f:
118 case AcpiFadt{h, c, x, s, v}:
119 c
120
121def AcpiFadt.ext(f: AcpiFadt) -> Maybe<&2, AcpiFadtExt>:
122 match f:
123 case AcpiFadt{h, c, x, s, v}:
124 x
125
126def AcpiFadt.sleep(f: AcpiFadt) -> Maybe<&2, AcpiFadtSleep>:
127 match f:
128 case AcpiFadt{h, c, x, s, v}:
129 s
130
131def AcpiFadt.hypervisor(f: AcpiFadt) -> Maybe<&2, W.W64>:
132 match f:
133 case AcpiFadt{h, c, x, s, v}:
134 v
135
136# The fixed register blocks, by name
137type AcpiFadtBlock is Data:
138 AcpiFadtPm1aEvt{}
139 AcpiFadtPm1bEvt{}
140 AcpiFadtPm1aCnt{}
141 AcpiFadtPm1bCnt{}
142 AcpiFadtPm2Cnt{}
143 AcpiFadtPmTmr{}
144 AcpiFadtGpe0{}
145 AcpiFadtGpe1{}
146
147def fadt.legacy(b: AcpiFadtBlocks, l: AcpiFadtLens, k: AcpiFadtBlock) -> G.AcpiGas:
148 match b l:
149 case AcpiFadtBlocks{e1a, e1b, c1a, c1b, c2, tm, g0, g1} AcpiFadtLens{le, lc, l2, lt, lg0, lg1, gb}:
150 match k:
151 case AcpiFadtPm1aEvt{}:
152 G.AcpiGas.io_block(e1a, le)
153 case AcpiFadtPm1bEvt{}:
154 G.AcpiGas.io_block(e1b, le)
155 case AcpiFadtPm1aCnt{}:
156 G.AcpiGas.io_block(c1a, lc)
157 case AcpiFadtPm1bCnt{}:
158 G.AcpiGas.io_block(c1b, lc)
159 case AcpiFadtPm2Cnt{}:
160 G.AcpiGas.io_block(c2, l2)
161 case AcpiFadtPmTmr{}:
162 G.AcpiGas.io_block(tm, lt)
163 case AcpiFadtGpe0{}:
164 G.AcpiGas.io_block(g0, lg0)
165 case AcpiFadtGpe1{}:
166 G.AcpiGas.io_block(g1, lg1)
167
168def fadt.xblock(x: AcpiFadtX, k: AcpiFadtBlock) -> G.AcpiGas:
169 match x:
170 case AcpiFadtX{e1a, e1b, c1a, c1b, c2, tm, g0, g1}:
171 match k:
172 case AcpiFadtPm1aEvt{}:
173 e1a
174 case AcpiFadtPm1bEvt{}:
175 e1b
176 case AcpiFadtPm1aCnt{}:
177 c1a
178 case AcpiFadtPm1bCnt{}:
179 c1b
180 case AcpiFadtPm2Cnt{}:
181 c2
182 case AcpiFadtPmTmr{}:
183 tm
184 case AcpiFadtGpe0{}:
185 g0
186 case AcpiFadtGpe1{}:
187 g1
188
189def fadt.core.flags(c: AcpiFadtCore) -> U32:
190 match c:
191 case AcpiFadtCore{fc, d, im, pp, sci, smi, en, dis, s4, ps, bl, ln, cst, l2, l3, fs, fst, doff, dw, da, ma, ce, ia, fl}:
192 fl
193
194def fadt.core.dsdt(c: AcpiFadtCore) -> U32:
195 match c:
196 case AcpiFadtCore{fc, d, im, pp, sci, smi, en, dis, s4, ps, bl, ln, cst, l2, l3, fs, fst, doff, dw, da, ma, ce, ia, fl}:
197 d
198
199def fadt.core.facs(c: AcpiFadtCore) -> U32:
200 match c:
201 case AcpiFadtCore{fc, d, im, pp, sci, smi, en, dis, s4, ps, bl, ln, cst, l2, l3, fs, fst, doff, dw, da, ma, ce, ia, fl}:
202 fc
203
204def fadt.core.legacy(k: AcpiFadtBlock, c: AcpiFadtCore) -> G.AcpiGas:
205 match c:
206 case AcpiFadtCore{fc, d, im, pp, sci, smi, en, dis, s4, ps, bl, ln, cst, l2, l3, fs, fst, doff, dw, da, ma, ce, ia, fl}:
207 fadt.legacy(bl, ln, k)
208
209def AcpiFadt.flags(f: AcpiFadt) -> U32:
210 fadt.core.flags(AcpiFadt.core(f))
211
212# Flags, bit numbers: 0 WBINVD, 1 WBINVD_FLUSH, 2 PROC_C1,
213# 3 P_LVL2_UP, 4 PWR_BUTTON, 5 SLP_BUTTON, 6 FIX_RTC, 7 RTC_S4,
214# 8 TMR_VAL_EXT, 9 DCK_CAP, 10 RESET_REG_SUP, 11 SEALED_CASE, 12 HEADLESS,
215# 13 CPU_SW_SLP, 14 PCI_EXP_WAK, 15 USE_PLATFORM_CLOCK,
216# 16 S4_RTC_STS_VALID, 17 REMOTE_POWER_ON_CAPABLE, 18 FORCE_APIC_CLUSTER_MODEL,
217# 19 FORCE_APIC_PHYSICAL_DESTINATION_MODE, 20 HW_REDUCED_ACPI,
218# 21 LOW_POWER_S0_IDLE_CAPABLE, 22-23 PERSISTENT_CPU_CACHES
219def AcpiFadt.flag(+f: AcpiFadt, bit: Nat) -> Bool:
220 F.AcpiF.bit(AcpiFadt.flags(f), bit)
221
222def AcpiFadt.hw_reduced(+f: AcpiFadt) -> Bool:
223 AcpiFadt.flag(f, 20n)
224
225def fadt.pick64(nz: Bool, +x: W.W64, lo: U32) -> W.W64:
226 match nz:
227 case True{}:
228 x
229 case False{}:
230 W.W64.from_u32(lo)
231
232def fadt.dsdt.go(m: Maybe<&2, AcpiFadtExt>, +lo: U32) -> W.W64:
233 match m:
234 case None{}:
235 W.W64.from_u32(lo)
236 case Some{AcpiFadtExt{rr, rv, ab, mv, xfc, +xd, xx}}:
237 fadt.pick64(Bool.not(W.W64.is_zero(xd)), xd, lo)
238
239def fadt.facs.go(m: Maybe<&2, AcpiFadtExt>, +lo: U32) -> W.W64:
240 match m:
241 case None{}:
242 W.W64.from_u32(lo)
243 case Some{AcpiFadtExt{rr, rv, ab, mv, +xfc, xd, xx}}:
244 fadt.pick64(Bool.not(W.W64.is_zero(xfc)), xfc, lo)
245
246# the DSDT's address: X_DSDT when present and non-zero, else DSDT
247def AcpiFadt.dsdt_address(+f: AcpiFadt) -> W.W64:
248 fadt.dsdt.go(AcpiFadt.ext(f), fadt.core.dsdt(AcpiFadt.core(f)))
249
250# the FACS's address: X_FIRMWARE_CTRL when present and non-zero, else
251# FIRMWARE_CTRL (zero on hardware-reduced systems without a FACS)
252def AcpiFadt.facs_address(+f: AcpiFadt) -> W.W64:
253 fadt.facs.go(AcpiFadt.ext(f), fadt.core.facs(AcpiFadt.core(f)))
254
255def fadt.choose(nz: Bool, +x: G.AcpiGas, +legacy: G.AcpiGas) -> G.AcpiGas:
256 match nz:
257 case True{}:
258 x
259 case False{}:
260 legacy
261
262def fadt.block.go(+k: AcpiFadtBlock, m: Maybe<&2, AcpiFadtExt>, +legacy: G.AcpiGas) -> G.AcpiGas:
263 match m:
264 case None{}:
265 legacy
266 case Some{AcpiFadtExt{rr, rv, ab, mv, xfc, xd, xx}}:
267 +g = fadt.xblock(xx, k)
268 fadt.choose(Bool.not(G.AcpiGas.is_null(g)), g, legacy)
269
270# a register block as a Generic Address: the X_ block when present and its
271# address is non-zero, else the 32-bit port with its length (a system I/O
272# block; address 0 when the block is absent)
273def AcpiFadt.block(+f: AcpiFadt, +k: AcpiFadtBlock) -> G.AcpiGas:
274 fadt.block.go(k, AcpiFadt.ext(f), fadt.core.legacy(k, AcpiFadt.core(f)))
275
276# Writing: the 276 bytes of revision 6 (absent groups written as zeros)
277
278def fadt.u8(v: U32) -> B.Octets:
279 B.Octets.of_list([v])
280
281def fadt.enc.core(c: AcpiFadtCore) -> B.Octets:
282 match c:
283 case AcpiFadtCore{fc, d, im, pp, sci, smi, en, dis, s4, ps, AcpiFadtBlocks{e1a, e1b, c1a, c1b, c2, tm, g0, g1}, AcpiFadtLens{le, lc, l2, lt, lg0, lg1, gb}, cst, p2, p3, fs, fst, doff, dw, da, ma, ce, ia, fl}:
284 B.Octets.concat([B.Octets.le32(fc), B.Octets.le32(d), fadt.u8(im), fadt.u8(pp), B.Octets.le16(sci), B.Octets.le32(smi), fadt.u8(en), fadt.u8(dis), fadt.u8(s4), fadt.u8(ps), B.Octets.le32(e1a), B.Octets.le32(e1b), B.Octets.le32(c1a), B.Octets.le32(c1b), B.Octets.le32(c2), B.Octets.le32(tm), B.Octets.le32(g0), B.Octets.le32(g1), B.Octets.of_list([le, lc, l2, lt, lg0, lg1, gb, cst]), B.Octets.le16(p2), B.Octets.le16(p3), B.Octets.le16(fs), B.Octets.le16(fst), B.Octets.of_list([doff, dw, da, ma, ce]), B.Octets.le16(ia), B.Octets.zeros(1n), B.Octets.le32(fl)])
285
286def fadt.enc.ext(m: Maybe<&2, AcpiFadtExt>) -> B.Octets:
287 match m:
288 case None{}:
289 B.Octets.zeros(128n)
290 case Some{AcpiFadtExt{rr, rv, ab, mv, xfc, xd, AcpiFadtX{e1a, e1b, c1a, c1b, c2, tm, g0, g1}}}:
291 B.Octets.concat([G.AcpiGas.encode(rr), fadt.u8(rv), B.Octets.le16(ab), fadt.u8(mv), B.Octets.le64(xfc), B.Octets.le64(xd), G.AcpiGas.encode(e1a), G.AcpiGas.encode(e1b), G.AcpiGas.encode(c1a), G.AcpiGas.encode(c1b), G.AcpiGas.encode(c2), G.AcpiGas.encode(tm), G.AcpiGas.encode(g0), G.AcpiGas.encode(g1)])
292
293def fadt.enc.sleep(m: Maybe<&2, AcpiFadtSleep>) -> B.Octets:
294 match m:
295 case None{}:
296 B.Octets.zeros(24n)
297 case Some{AcpiFadtSleep{c, s}}:
298 B.Octets.append(G.AcpiGas.encode(c), G.AcpiGas.encode(s))
299
300def fadt.enc.hyp(m: Maybe<&2, W.W64>) -> B.Octets:
301 match m:
302 case None{}:
303 B.Octets.zeros(8n)
304 case Some{v}:
305 B.Octets.le64(v)
306
307# the table (signature "FACP", revision as in the header, length 276,
308# checksum computed)
309def AcpiFadt.build(f: AcpiFadt) -> B.Octets:
310 match f:
311 case AcpiFadt{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}, core, x, sl, hv}:
312 H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("FACP"), l, r, c, o, t, orv, ci, cr}, B.Octets.concat([fadt.enc.core(core), fadt.enc.ext(x), fadt.enc.sleep(sl), fadt.enc.hyp(hv)]))