header.bend
bend-osdev-acpi@0.1.0.0 · 282 lines · 0 definitions
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).
18import Base
19import bend-osdev-bytes@0.1.0.0/bytes.bend as B
20import bend-osdev-acpi@0.1.0.0/error.bend as E
21import bend-osdev-acpi@0.1.0.0/checksum.bend as C
22
23type 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
26def AcpiHeader.size() -> Nat:
27 36n
28
29def AcpiHeader.signature(h: AcpiHeader) -> B.Octets:
30 match h:
31 case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
32 s
33
34def AcpiHeader.length(h: AcpiHeader) -> U32:
35 match h:
36 case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
37 l
38
39def AcpiHeader.revision(h: AcpiHeader) -> U32:
40 match h:
41 case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
42 r
43
44def AcpiHeader.checksum(h: AcpiHeader) -> U32:
45 match h:
46 case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
47 c
48
49def 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
54def 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
59def AcpiHeader.oem_revision(h: AcpiHeader) -> U32:
60 match h:
61 case AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
62 orv
63
64def 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
69def 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
78def hd.byte(v: U32) -> B.Octets:
79 B.Octets.of_list([v])
80
81def 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
88def hd.short(+o: B.Octets) -> E.AcpiError:
89 E.AcpiTooShort{36n, B.Octets.len(o)}
90
91def hd.u32(o: B.Octets) -> U32:
92 Maybe.default(&2, U32, B.Octets.le32_at(o, 0n), 0)
93
94def hd.u8.list(xs: List<&2, U32>) -> U32:
95 match xs:
96 case Nil{}:
97 0
98 case Con{x, t}:
99 x
100
101def hd.u8(o: B.Octets) -> U32:
102 hd.u8.list(B.Octets.to_list(o))
103
104def 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
111def 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
118def 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
125def 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
132def 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
139def 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
146def 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
153def 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
160def 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
169def 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
175def 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
182def 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
190def 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
199def 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)).
205def 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
210type AcpiSdt is Data:
211 AcpiSdt{header: AcpiHeader, body: B.Octets}
212
213def 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
220def 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
228def AcpiSdt.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSdt>:
229 sdt.parse.go(AcpiSdt.check(o))
230
231def AcpiSdt.header(t: AcpiSdt) -> AcpiHeader:
232 match t:
233 case AcpiSdt{h, b}:
234 h
235
236def AcpiSdt.body(t: AcpiSdt) -> B.Octets:
237 match t:
238 case AcpiSdt{h, b}:
239 b
240
241def 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
248def 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)
257def 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)
262def 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
268def 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
275def 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)
281def 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}