1	# bend-osdev-acpi, header.bend: the system description table header that
2	# every table but the RSDP and the FACS begins with (ACPI 6.5, section
3	# 5.2.6), and the checks every such table must pass.
4	#
5	#   offset  size  field
6	#        0     4  Signature
7	#        4     4  Length (of the whole table, header included)
8	#        8     1  Revision
9	#        9     1  Checksum (all Length bytes sum to 0 mod 256)
10	#       10     6  OEMID
11	#       16     8  OEM Table ID
12	#       24     4  OEM Revision
13	#       28     4  Creator ID
14	#       32     4  Creator Revision
15	#
16	# Fields are little-endian. The four text fields are kept as Octets, exactly
17	# as stored (ACPI pads them with spaces or NULs; nothing is trimmed).
18	import Base
19	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
20	import ./error.bend as E
21	import ./checksum.bend as C
22	
23	type AcpiHeader is Data:
24	  AcpiHeader{signature: B.Octets, length: U32, revision: U32, checksum: U32, oem_id: B.Octets, oem_table_id: B.Octets, oem_revision: U32, creator_id: B.Octets, creator_revision: U32}
25	
26	def AcpiHeader.size() -> Nat:
27	  36n
28	
29	def AcpiHeader.signature(h: AcpiHeader) -> B.Octets:
30	  match h:
31	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
32	      s
33	
34	def AcpiHeader.length(h: AcpiHeader) -> U32:
35	  match h:
36	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
37	      l
38	
39	def AcpiHeader.revision(h: AcpiHeader) -> U32:
40	  match h:
41	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
42	      r
43	
44	def AcpiHeader.checksum(h: AcpiHeader) -> U32:
45	  match h:
46	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
47	      c
48	
49	def AcpiHeader.oem_id(h: AcpiHeader) -> B.Octets:
50	  match h:
51	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
52	      o
53	
54	def AcpiHeader.oem_table_id(h: AcpiHeader) -> B.Octets:
55	  match h:
56	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
57	      t
58	
59	def AcpiHeader.oem_revision(h: AcpiHeader) -> U32:
60	  match h:
61	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
62	      orv
63	
64	def AcpiHeader.creator_id(h: AcpiHeader) -> B.Octets:
65	  match h:
66	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
67	      ci
68	
69	def AcpiHeader.creator_revision(h: AcpiHeader) -> U32:
70	  match h:
71	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
72	      cr
73	
74	# Writing: the 36 bytes, fields as given (the text fields must have their
75	# sizes, 4, 6, 8 and 4 bytes, and revision and checksum must be bytes, for
76	# decode to give the header back; LAWS.bend: header_round_trip)
77	
78	def hd.byte(v: U32) -> B.Octets:
79	  B.Octets.of_list([v])
80	
81	def AcpiHeader.encode(h: AcpiHeader) -> B.Octets:
82	  match h:
83	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
84	      B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(hd.byte(r), B.Octets.append(hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))
85	
86	# Reading: each field split off the front in turn
87	
88	def hd.short(+o: B.Octets) -> E.AcpiError:
89	  E.AcpiTooShort{36n, B.Octets.len(o)}
90	
91	def hd.u32(o: B.Octets) -> U32:
92	  Maybe.default(&2, U32, B.Octets.le32_at(o, 0n), 0)
93	
94	def hd.u8.list(xs: List<&2, U32>) -> U32:
95	  match xs:
96	    case Nil{}:
97	      0
98	    case Con{x, t}:
99	      x
100	
101	def hd.u8(o: B.Octets) -> U32:
102	  hd.u8.list(B.Octets.to_list(o))
103	
104	def hd.d9(ok: Bool, +all: B.Octets, s: B.Octets, l: U32, r: U32, c: U32, o: B.Octets, t: B.Octets, orv: U32, ci: B.Octets, f: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
105	  match ok:
106	    case False{}:
107	      Fail{hd.short(all)}
108	    case True{}:
109	      Done{AcpiHeader{s, l, r, c, o, t, orv, ci, hd.u32(f)}}
110	
111	def hd.d8(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets, l: U32, r: U32, c: U32, o: B.Octets, t: B.Octets, orv: U32) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
112	  match m:
113	    case None{}:
114	      Fail{hd.short(all)}
115	    case Some{B.OctetsSplit{f, +rest}}:
116	      hd.d9(Nat.is_le(4n, B.Octets.len(rest)), all, s, l, r, c, o, t, orv, f, rest)
117	
118	def hd.d7(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets, l: U32, r: U32, c: U32, o: B.Octets, t: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
119	  match m:
120	    case None{}:
121	      Fail{hd.short(all)}
122	    case Some{B.OctetsSplit{f, rest}}:
123	      hd.d8(B.Octets.split_at(4n, rest), all, s, l, r, c, o, t, hd.u32(f))
124	
125	def hd.d6(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets, l: U32, r: U32, c: U32, o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
126	  match m:
127	    case None{}:
128	      Fail{hd.short(all)}
129	    case Some{B.OctetsSplit{f, rest}}:
130	      hd.d7(B.Octets.split_at(4n, rest), all, s, l, r, c, o, f)
131	
132	def hd.d5(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets, l: U32, r: U32, c: U32) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
133	  match m:
134	    case None{}:
135	      Fail{hd.short(all)}
136	    case Some{B.OctetsSplit{f, rest}}:
137	      hd.d6(B.Octets.split_at(8n, rest), all, s, l, r, c, f)
138	
139	def hd.d4(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets, l: U32, r: U32) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
140	  match m:
141	    case None{}:
142	      Fail{hd.short(all)}
143	    case Some{B.OctetsSplit{f, rest}}:
144	      hd.d5(B.Octets.split_at(6n, rest), all, s, l, r, hd.u8(f))
145	
146	def hd.d3(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets, l: U32) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
147	  match m:
148	    case None{}:
149	      Fail{hd.short(all)}
150	    case Some{B.OctetsSplit{f, rest}}:
151	      hd.d4(B.Octets.split_at(1n, rest), all, s, l, hd.u8(f))
152	
153	def hd.d2(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets, s: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
154	  match m:
155	    case None{}:
156	      Fail{hd.short(all)}
157	    case Some{B.OctetsSplit{f, rest}}:
158	      hd.d3(B.Octets.split_at(1n, rest), all, s, hd.u32(f))
159	
160	def hd.d1(m: Maybe<&2, B.OctetsSplit>, +all: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
161	  match m:
162	    case None{}:
163	      Fail{hd.short(all)}
164	    case Some{B.OctetsSplit{f, rest}}:
165	      hd.d2(B.Octets.split_at(4n, rest), all, f)
166	
167	# the header in the first 36 bytes, fields as stored (unchecked);
168	# AcpiTooShort if there are fewer
169	def AcpiHeader.decode(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiHeader>:
170	  hd.d1(B.Octets.split_at(4n, o), o)
171	
172	# The checks every table passes: a length from 36 bytes to the bytes given,
173	# and a checksum of zero over that length
174	
175	def sdt.c3(ok: Bool, +raw: B.Octets) -> Result<&2, &2, E.AcpiError, B.Octets>:
176	  match ok:
177	    case True{}:
178	      Done{raw}
179	    case False{}:
180	      Fail{E.AcpiBadChecksum{C.AcpiChecksum.sum(raw)}}
181	
182	def sdt.c2(ok: Bool, +l: U32, +o: B.Octets) -> Result<&2, &2, E.AcpiError, B.Octets>:
183	  match ok:
184	    case True{}:
185	      +raw = B.Octets.take(U32.to_nat(l), o)
186	      sdt.c3(C.AcpiChecksum.ok(raw), raw)
187	    case False{}:
188	      Fail{E.AcpiBadLength{l}}
189	
190	def sdt.c1(m: Maybe<&2, U32>, +o: B.Octets) -> Result<&2, &2, E.AcpiError, B.Octets>:
191	  match m:
192	    case None{}:
193	      Fail{E.AcpiTooShort{36n, B.Octets.len(o)}}
194	    case Some{+l}:
195	      sdt.c2(Bool.and(Nat.is_le(36n, U32.to_nat(l)), Nat.is_le(U32.to_nat(l), B.Octets.len(o))), l, o)
196	
197	# a table's bytes, as far as its length field says (all of o if o is
198	# shorter than 8 bytes); bytes after the length are not part of the table
199	def AcpiSdt.bytes(+o: B.Octets) -> B.Octets:
200	  B.Octets.take(U32.to_nat(Maybe.default(&2, U32, B.Octets.le32_at(o, 4n), 4294967295)), o)
201	
202	# the table at the front of o, checked: its length field from 36 to the
203	# bytes given (AcpiTooShort, AcpiBadLength), and its bytes summing to zero
204	# (AcpiBadChecksum). Answers the table's bytes (AcpiSdt.bytes(o)).
205	def AcpiSdt.check(+o: B.Octets) -> Result<&2, &2, E.AcpiError, B.Octets>:
206	  sdt.c1(B.Octets.le32_at(o, 4n), o)
207	
208	# A checked table, split into its header and its body
209	
210	type AcpiSdt is Data:
211	  AcpiSdt{header: AcpiHeader, body: B.Octets}
212	
213	def sdt.split(+raw: B.Octets, r: Result<&2, &2, E.AcpiError, AcpiHeader>) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
214	  match r:
215	    case Fail{e}:
216	      Fail{e}
217	    case Done{h}:
218	      Done{AcpiSdt{h, B.Octets.drop(36n, raw)}}
219	
220	def sdt.parse.go(r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
221	  match r:
222	    case Fail{e}:
223	      Fail{e}
224	    case Done{+raw}:
225	      sdt.split(raw, AcpiHeader.decode(raw))
226	
227	# the table at the front of o, checked, as its header and body
228	def AcpiSdt.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
229	  sdt.parse.go(AcpiSdt.check(o))
230	
231	def AcpiSdt.header(t: AcpiSdt) -> AcpiHeader:
232	  match t:
233	    case AcpiSdt{h, b}:
234	      h
235	
236	def AcpiSdt.body(t: AcpiSdt) -> B.Octets:
237	  match t:
238	    case AcpiSdt{h, b}:
239	      b
240	
241	def sdt.sig.pick(ok: Bool, +s: B.Octets, t: AcpiSdt) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
242	  match ok:
243	    case True{}:
244	      Done{t}
245	    case False{}:
246	      Fail{E.AcpiBadSignature{s}}
247	
248	def sdt.sig.go(+sig: B.Octets, r: Result<&2, &2, E.AcpiError, AcpiSdt>) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
249	  match r:
250	    case Fail{e}:
251	      Fail{e}
252	    case Done{+t}:
253	      +s = AcpiHeader.signature(AcpiSdt.header(t))
254	      sdt.sig.pick(B.Octets.is_eq(s, sig), s, t)
255	
256	# the same, also requiring the signature sig (AcpiBadSignature)
257	def AcpiSdt.parse_sig(+sig: B.Octets, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
258	  sdt.sig.go(sig, AcpiSdt.parse(o))
259	
260	# Building: a header and a body as a table, with the length and checksum
261	# fields computed (the header's own length and checksum are ignored)
262	def AcpiSdt.build(h: AcpiHeader, +body: B.Octets) -> B.Octets:
263	  match h:
264	    case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
265	      +len = U32.from_nat(Nat.add(36n, B.Octets.len(body)))
266	      C.AcpiChecksum.fix(9n, B.Octets.append(AcpiHeader.encode(AcpiHeader{s, len, r, 0, o, t, orv, ci, cr}), body))
267	
268	def hd.spaces(n: Nat) -> List<&2, U32>:
269	  match n:
270	    case 0n:
271	      Nil{}
272	    case 1n+p:
273	      Con{32, hd.spaces(p)}
274	
275	def hd.fit(+n: Nat, +o: B.Octets) -> B.Octets:
276	  +h = B.Octets.take(n, o)
277	  B.Octets.append(h, B.Octets.of_list(hd.spaces(Nat.sub(n, B.Octets.len(h)))))
278	
279	# a header for building: signature, revision, OEMID, OEM table ID, with OEM
280	# revision 1 and creator "BEND" revision 1 (text fields fitted to size)
281	def AcpiHeader.make(sig: B.Octets, r: U32, oem: B.Octets, tid: B.Octets) -> AcpiHeader:
282	  AcpiHeader{hd.fit(4n, sig), 0, r, 0, hd.fit(6n, oem), hd.fit(8n, tid), 1, B.Octets.of_string("BEND"), 1}