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.
21	import Base
22	import bend-osdev-word64@0.1.0.0/word64.bend as W
23	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
24	import ./error.bend as E
25	import ./header.bend as H
26	import ./fields.bend as F
27	import ./gas.bend as G
28	
29	# the ACPI 1.0 register blocks: I/O port addresses
30	type 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
34	type 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
38	type 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)
42	type 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
46	type 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
50	type AcpiFadtSleep is Data:
51	  AcpiFadtSleep{control: G.AcpiGas, status: G.AcpiGas}
52	
53	type 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	
58	def 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	
63	def 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	
66	def 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	
73	def 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	
80	def 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	
87	def 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)
96	def 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	
102	def 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
111	def 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	
116	def AcpiFadt.core(f: AcpiFadt) -> AcpiFadtCore:
117	  match f:
118	    case AcpiFadt{h, c, x, s, v}:
119	      c
120	
121	def AcpiFadt.ext(f: AcpiFadt) -> Maybe<&2, AcpiFadtExt>:
122	  match f:
123	    case AcpiFadt{h, c, x, s, v}:
124	      x
125	
126	def AcpiFadt.sleep(f: AcpiFadt) -> Maybe<&2, AcpiFadtSleep>:
127	  match f:
128	    case AcpiFadt{h, c, x, s, v}:
129	      s
130	
131	def 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
137	type AcpiFadtBlock is Data:
138	  AcpiFadtPm1aEvt{}
139	  AcpiFadtPm1bEvt{}
140	  AcpiFadtPm1aCnt{}
141	  AcpiFadtPm1bCnt{}
142	  AcpiFadtPm2Cnt{}
143	  AcpiFadtPmTmr{}
144	  AcpiFadtGpe0{}
145	  AcpiFadtGpe1{}
146	
147	def 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	
168	def 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	
189	def 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	
194	def 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	
199	def 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	
204	def 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	
209	def 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
219	def AcpiFadt.flag(+f: AcpiFadt, bit: Nat) -> Bool:
220	  F.AcpiF.bit(AcpiFadt.flags(f), bit)
221	
222	def AcpiFadt.hw_reduced(+f: AcpiFadt) -> Bool:
223	  AcpiFadt.flag(f, 20n)
224	
225	def 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	
232	def 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	
239	def 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
247	def 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)
252	def AcpiFadt.facs_address(+f: AcpiFadt) -> W.W64:
253	  fadt.facs.go(AcpiFadt.ext(f), fadt.core.facs(AcpiFadt.core(f)))
254	
255	def 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	
262	def 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)
273	def 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	
278	def fadt.u8(v: U32) -> B.Octets:
279	  B.Octets.of_list([v])
280	
281	def 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	
286	def 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	
293	def 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	
300	def 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)
309	def 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)]))