aml_name.bend
bend-osdev-acpi@0.1.0.0 · 425 lines · 0 definitions
1# bend-osdev-acpi, aml_name.bend: AML name strings (ACPI 6.5, sections
2# 20.2.2, Name Objects Encoding, and 5.3, ACPI Namespace):
3#
4# NameSeg := <LeadNameChar NameChar NameChar NameChar>
5# LeadNameChar := 'A'-'Z' | '_'
6# NameChar := DigitChar | LeadNameChar (DigitChar: '0'-'9')
7# NameString := <RootChar NamePath> | <PrefixPath NamePath>
8# RootChar := '\' (0x5C)
9# PrefixPath := Nothing | <'^' PrefixPath> ('^' is 0x5E)
10# NamePath := NameSeg | DualNamePath | MultiNamePath | NullName
11# DualNamePath := DualNamePrefix NameSeg NameSeg (DualNamePrefix: 0x2E)
12# MultiNamePath := MultiNamePrefix SegCount NameSeg(SegCount)
13# (MultiNamePrefix: 0x2F; SegCount: a byte, 1 to 255)
14# NullName := 0x00
15#
16# A name is AmlName{root, up, segs}: rooted at '\', or up some number of
17# parents, then its segments (4 bytes each, as Octets). The encoder writes
18# the shortest NamePath (a NameSeg for one segment, DualNamePath for two,
19# MultiNamePath for three or more); the decoder reads every form, and
20# refuses a SegCount of 0.
21import Base
22import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23import bend-osdev-acpi@0.1.0.0/error.bend as E
24
25type AmlName is Data:
26 AmlName{root: Bool, up: Nat, segs: List<&2, B.Octets>}
27
28# a name read from a list of bytes: the name and what follows
29type AmlNameL is Data:
30 AmlNameL{name: AmlName, rest: List<&2, U32>}
31
32# a name read from Octets
33type AmlNameParsed is Data:
34 AmlNameParsed{name: AmlName, rest: B.Octets}
35
36def AmlName.root(n: AmlName) -> Bool:
37 match n:
38 case AmlName{r, u, s}:
39 r
40
41def AmlName.up(n: AmlName) -> Nat:
42 match n:
43 case AmlName{r, u, s}:
44 u
45
46def AmlName.segs(n: AmlName) -> List<&2, B.Octets>:
47 match n:
48 case AmlName{r, u, s}:
49 s
50
51# What a byte can begin
52
53type AmlLeadKind is Data:
54 AmlLRoot{}
55 AmlLParent{}
56 AmlLDual{}
57 AmlLMulti{}
58 AmlLNull{}
59 AmlLSeg{}
60 AmlLOther{}
61
62def nm.alpha(+c: U32) -> Bool:
63 Bool.or(Bool.and(U32.is_le(65, c), U32.is_le(c, 90)), U32.is_eq(c, 95))
64
65def nm.cls.c(seg: Bool) -> AmlLeadKind:
66 match seg:
67 case True{}:
68 AmlLSeg{}
69 case False{}:
70 AmlLOther{}
71
72def nm.cls.b(z: Bool, +c: U32) -> AmlLeadKind:
73 match z:
74 case True{}:
75 AmlLNull{}
76 case False{}:
77 nm.cls.c(nm.alpha(c))
78
79def nm.cls.a(m: Bool, +c: U32) -> AmlLeadKind:
80 match m:
81 case True{}:
82 AmlLMulti{}
83 case False{}:
84 nm.cls.b(U32.is_eq(c, 0), c)
85
86def nm.cls.n9(d: Bool, +c: U32) -> AmlLeadKind:
87 match d:
88 case True{}:
89 AmlLDual{}
90 case False{}:
91 nm.cls.a(U32.is_eq(c, 47), c)
92
93def nm.cls.n8(p: Bool, +c: U32) -> AmlLeadKind:
94 match p:
95 case True{}:
96 AmlLParent{}
97 case False{}:
98 nm.cls.n9(U32.is_eq(c, 46), c)
99
100def nm.cls.r(r: Bool, +c: U32) -> AmlLeadKind:
101 match r:
102 case True{}:
103 AmlLRoot{}
104 case False{}:
105 nm.cls.n8(U32.is_eq(c, 94), c)
106
107# the kind of name element a byte begins
108def AmlLead.classify(+c: U32) -> AmlLeadKind:
109 nm.cls.r(U32.is_eq(c, 92), c)
110
111def AmlLead.is_seg(k: AmlLeadKind) -> Bool:
112 match k:
113 case AmlLSeg{}:
114 True{}
115 case _:
116 False{}
117
118# a NameChar: a LeadNameChar or a digit
119def AmlName.name_char(+c: U32) -> Bool:
120 Bool.or(nm.alpha(c), Bool.and(U32.is_le(48, c), U32.is_le(c, 57)))
121
122def nm.seg_ok4(+c0: U32, +c1: U32, +c2: U32, +c3: U32) -> Bool:
123 Bool.and(AmlLead.is_seg(AmlLead.classify(c0)), Bool.and(AmlName.name_char(c1), Bool.and(AmlName.name_char(c2), AmlName.name_char(c3))))
124
125def nm.seg_ok.list(xs: List<&2, U32>) -> Bool:
126 match xs:
127 case Con{c0, Con{c1, Con{c2, Con{c3, Nil{}}}}}:
128 nm.seg_ok4(c0, c1, c2, c3)
129 case _:
130 False{}
131
132# a NameSeg: four bytes, a LeadNameChar then three NameChars
133def AmlName.seg_ok(s: B.Octets) -> Bool:
134 nm.seg_ok.list(B.Octets.to_list(s))
135
136def AmlName.segs_ok(ss: List<&2, B.Octets>) -> Bool:
137 match ss:
138 case Nil{}:
139 True{}
140 case Con{s, t}:
141 Bool.and(AmlName.seg_ok(s), AmlName.segs_ok(t))
142
143def nm.root_up_ok(root: Bool, up: Nat) -> Bool:
144 match root:
145 case True{}:
146 Nat.is_eq(up, 0n)
147 case False{}:
148 True{}
149
150def nm.len(ss: List<&2, B.Octets>) -> Nat:
151 List.length(&2, B.Octets, ss)
152
153# the names a NameString can hold: not both rooted and going up, every
154# segment a NameSeg, at most 255 segments
155def AmlName.valid(n: AmlName) -> Bool:
156 match n:
157 case AmlName{r, u, +ss}:
158 Bool.and(nm.root_up_ok(r, u), Bool.and(AmlName.segs_ok(ss), Nat.is_lt(nm.len(ss), 256n)))
159
160# Encoding (list layer)
161
162def nm.carets(n: Nat) -> List<&2, U32>:
163 match n:
164 case 0n:
165 Nil{}
166 case 1n+p:
167 Con{94, nm.carets(p)}
168
169def nm.prefix(root: Bool, up: Nat) -> List<&2, U32>:
170 match root:
171 case True{}:
172 [92]
173 case False{}:
174 nm.carets(up)
175
176def nm.segs.list(ss: List<&2, B.Octets>) -> List<&2, U32>:
177 match ss:
178 case Nil{}:
179 Nil{}
180 case Con{s, t}:
181 B.append(B.Octets.to_list(s), nm.segs.list(t))
182
183def nm.path(ss: List<&2, B.Octets>) -> List<&2, U32>:
184 match ss:
185 case Nil{}:
186 [0]
187 case Con{s, Nil{}}:
188 nm.segs.list([s])
189 case Con{s1, Con{s2, Nil{}}}:
190 Con{46, nm.segs.list([s1, s2])}
191 case Con{s1, Con{s2, Con{s3, +t}}}:
192 Con{47, Con{U32.from_nat(Nat.add(3n, nm.len(t))), nm.segs.list(Con{s1, Con{s2, Con{s3, t}}})}}
193
194def nm.enc(n: AmlName) -> List<&2, U32>:
195 match n:
196 case AmlName{r, u, ss}:
197 B.append(nm.prefix(r, u), nm.path(ss))
198
199# the name as a NameString (AmlName.valid names read back: LAWS.bend,
200# namestring_round_trip)
201def AmlName.encode(n: AmlName) -> B.Octets:
202 B.Octets.of_list(nm.enc(n))
203
204# its size in bytes
205def AmlName.size(n: AmlName) -> Nat:
206 B.len.fast(nm.enc(n))
207
208# Decoding (list layer)
209
210type AmlSegL is Data:
211 AmlSegL{seg: B.Octets, rest: List<&2, U32>}
212
213type AmlSegsL is Data:
214 AmlSegsL{segs: List<&2, B.Octets>, rest: List<&2, U32>}
215
216def nm.seg.pick(ok: Bool, c0: U32, c1: U32, c2: U32, c3: U32, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegL>:
217 match ok:
218 case True{}:
219 Done{AmlSegL{B.Octets.of_list([c0, c1, c2, c3]), t}}
220 case False{}:
221 Fail{E.AcpiAmlBadName{}}
222
223def nm.seg(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegL>:
224 match xs:
225 case Con{+c0, Con{+c1, Con{+c2, Con{+c3, t}}}}:
226 nm.seg.pick(nm.seg_ok4(c0, c1, c2, c3), c0, c1, c2, c3, t)
227 case _:
228 Fail{E.AcpiAmlTruncated{}}
229
230def nm.cons(s: B.Octets, r: Result<&2, &2, E.AcpiError, AmlSegsL>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
231 match r:
232 case Fail{e}:
233 Fail{e}
234 case Done{AmlSegsL{ss, rest}}:
235 Done{AmlSegsL{Con{s, ss}, rest}}
236
237# the segment in r, then p more
238def nm.segs.go(p: Nat, r: Result<&2, &2, E.AcpiError, AmlSegL>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
239 match p:
240 case 0n:
241 match r:
242 case Fail{e}:
243 Fail{e}
244 case Done{AmlSegL{s, rest}}:
245 Done{AmlSegsL{[s], rest}}
246 case 1n+q:
247 match r:
248 case Fail{e}:
249 Fail{e}
250 case Done{AmlSegL{s, rest}}:
251 nm.cons(s, nm.segs.go(q, nm.seg(rest)))
252
253# n segments
254def nm.segs(n: Nat, xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
255 match n:
256 case 0n:
257 Done{AmlSegsL{Nil{}, xs}}
258 case 1n+p:
259 nm.segs.go(p, nm.seg(xs))
260
261def nm.multi.k(zero: Bool, n: Nat, r: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
262 match zero:
263 case True{}:
264 Fail{E.AcpiAmlBadName{}}
265 case False{}:
266 nm.segs(n, r)
267
268def nm.multi(t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
269 match t:
270 case Nil{}:
271 Fail{E.AcpiAmlTruncated{}}
272 case Con{c, r}:
273 +n = U32.to_nat(c)
274 nm.multi.k(Nat.is_eq(n, 0n), n, r)
275
276def nm.path.k(k: AmlLeadKind, c: U32, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
277 match k:
278 case AmlLNull{}:
279 Done{AmlSegsL{Nil{}, t}}
280 case AmlLDual{}:
281 nm.segs(2n, t)
282 case AmlLMulti{}:
283 nm.multi(t)
284 case AmlLSeg{}:
285 nm.segs(1n, Con{c, t})
286 case _:
287 Fail{E.AcpiAmlBadName{}}
288
289def nm.dpath(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>:
290 match xs:
291 case Nil{}:
292 Fail{E.AcpiAmlTruncated{}}
293 case Con{+c, t}:
294 nm.path.k(AmlLead.classify(c), c, t)
295
296def nm.named(root: Bool, up: Nat, r: Result<&2, &2, E.AcpiError, AmlSegsL>) -> Result<&2, &2, E.AcpiError, AmlNameL>:
297 match r:
298 case Fail{e}:
299 Fail{e}
300 case Done{AmlSegsL{ss, rest}}:
301 Done{AmlNameL{AmlName{root, up, ss}, rest}}
302
303def nm.up1(r: Result<&2, &2, E.AcpiError, AmlNameL>) -> Result<&2, &2, E.AcpiError, AmlNameL>:
304 match r:
305 case Fail{e}:
306 Fail{e}
307 case Done{AmlNameL{AmlName{root, up, ss}, rest}}:
308 Done{AmlNameL{AmlName{root, 1n+up, ss}, rest}}
309
310def nm.head_kind(xs: List<&2, U32>) -> AmlLeadKind:
311 match xs:
312 case Nil{}:
313 AmlLOther{}
314 case Con{+c, t}:
315 AmlLead.classify(c)
316
317# parent prefixes, then a path; k is the kind of the first byte
318def nm.ups(xs: List<&2, U32>, k: AmlLeadKind) -> Result<&2, &2, E.AcpiError, AmlNameL>:
319 match xs:
320 case Nil{}:
321 Fail{E.AcpiAmlTruncated{}}
322 case Con{c, +t}:
323 match k:
324 case AmlLParent{}:
325 nm.up1(nm.ups(t, nm.head_kind(t)))
326 case _:
327 nm.named(False{}, 0n, nm.path.k(k, c, t))
328
329def nm.dec.k(k: AmlLeadKind, c: U32, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlNameL>:
330 match k:
331 case AmlLRoot{}:
332 nm.named(True{}, 0n, nm.dpath(t))
333 case _:
334 nm.ups(Con{c, t}, k)
335
336# the NameString at the front of a list of bytes
337def nm.dec(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlNameL>:
338 match xs:
339 case Nil{}:
340 Fail{E.AcpiAmlTruncated{}}
341 case Con{+c, t}:
342 nm.dec.k(AmlLead.classify(c), c, t)
343
344def nm.pub(r: Result<&2, &2, E.AcpiError, AmlNameL>) -> Result<&2, &2, E.AcpiError, AmlNameParsed>:
345 match r:
346 case Fail{e}:
347 Fail{e}
348 case Done{AmlNameL{n, rest}}:
349 Done{AmlNameParsed{n, B.Octets.of_list(rest)}}
350
351# the NameString at the front of o, and what follows it
352def AmlName.decode(o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlNameParsed>:
353 nm.pub(nm.dec(B.Octets.to_list(o)))
354
355# Text: "\_SB_.PCI0", "^^_STA", and the null name "" (segments in full)
356
357def nm.show.segs(ss: List<&2, B.Octets>, first: Bool) -> String:
358 match ss:
359 case Nil{}:
360 ""
361 case Con{s, t}:
362 match first:
363 case True{}:
364 B.Octets.to_string(s) ++ nm.show.segs(t, False{})
365 case False{}:
366 "." ++ B.Octets.to_string(s) ++ nm.show.segs(t, False{})
367
368def nm.show.pre(root: Bool, up: Nat) -> String:
369 match root:
370 case True{}:
371 "\\"
372 case False{}:
373 String.repeat("^", up)
374
375def AmlName.show(n: AmlName) -> String:
376 match n:
377 case AmlName{r, u, ss}:
378 nm.show.pre(r, u) ++ nm.show.segs(ss, True{})
379
380# a segment from text: its first four characters, padded with '_' as ASL
381# does ("_SB" is "_SB_")
382def AmlName.seg(s: String) -> B.Octets:
383 +o = B.Octets.take(4n, B.Octets.of_string(s))
384 B.Octets.append(o, B.Octets.of_string(String.repeat("_", Nat.sub(4n, B.Octets.len(o)))))
385
386def nm.text.segs(ps: List<&2, String>) -> List<&2, B.Octets>:
387 match ps:
388 case Nil{}:
389 Nil{}
390 case Con{p, t}:
391 Con{AmlName.seg(p), nm.text.segs(t)}
392
393def nm.text.split.pick(e: Bool, +s: String) -> List<&2, B.Octets>:
394 match e:
395 case True{}:
396 Nil{}
397 case False{}:
398 nm.text.segs(String.split(s, '.'))
399
400def nm.text.split(+s: String) -> List<&2, B.Octets>:
401 nm.text.split.pick(String.is_empty(s), s)
402
403# leading carets, counted; isc: s starts with one
404def nm.text.ups(s: String, isc: Bool, n: Nat) -> AmlName:
405 match s:
406 case SNil{}:
407 AmlName{False{}, n, Nil{}}
408 case SCon{h, +t}:
409 match isc:
410 case True{}:
411 nm.text.ups(t, String.starts_with(t, "^"), 1n+n)
412 case False{}:
413 AmlName{False{}, n, nm.text.split(SCon{h, t})}
414
415def nm.text.root(r: Bool, +s: String) -> AmlName:
416 match r:
417 case True{}:
418 AmlName{True{}, 0n, nm.text.split(String.drop(s, 1n))}
419 case False{}:
420 nm.text.ups(s, String.starts_with(s, "^"), 0n)
421
422# a name from its text: "\_SB.PCI0" (in Bend source), "^^_STA", "LNKA";
423# segments are separated by '.', each padded to four characters with '_'
424def AmlName.of_text(+s: String) -> AmlName:
425 nm.text.root(String.starts_with(s, "\\"), s)