entries.bend
bend-osdev-acpi@0.1.0.0 · 81 lines · 0 definitions
1# bend-osdev-acpi, entries.bend: the variable-length sub-structures that the
2# MADT (ACPI 6.5, section 5.2.12) and the SRAT (5.2.16) carry after their
3# fixed fields. Each begins with a type byte and a length byte (the
4# structure's whole length, these two bytes included).
5import Base
6import bend-osdev-bytes@0.1.0.0/bytes.bend as B
7import bend-osdev-acpi@0.1.0.0/error.bend as E
8import bend-osdev-acpi@0.1.0.0/fields.bend as F
9
10# one structure: its type, its offset from the start of the table, and its
11# bytes (the type and length bytes included)
12type AcpiRawEntry is Data:
13 AcpiRawEntry{kind: U32, offset: Nat, data: B.Octets}
14
15def AcpiRawEntry.kind(e: AcpiRawEntry) -> U32:
16 match e:
17 case AcpiRawEntry{k, off, d}:
18 k
19
20def AcpiRawEntry.data(e: AcpiRawEntry) -> B.Octets:
21 match e:
22 case AcpiRawEntry{k, off, d}:
23 d
24
25# what comes next in the bytes: nothing, a structure of type k and length l,
26# or a structure of type k whose length is bad
27type AcpiEntNext is Data:
28 AcpiEntEnd{}
29 AcpiEntOk{kind: U32, len: Nat}
30 AcpiEntBad{kind: U32}
31
32def ent.next.pick(ok: Bool, +k: U32, l: Nat) -> AcpiEntNext:
33 match ok:
34 case True{}:
35 AcpiEntOk{k, l}
36 case False{}:
37 AcpiEntBad{k}
38
39def ent.next.go(empty: Bool, +o: B.Octets, +n: Nat) -> AcpiEntNext:
40 match empty:
41 case True{}:
42 AcpiEntEnd{}
43 case False{}:
44 +l = U32.to_nat(F.AcpiF.u8(o, 1n))
45 ent.next.pick(Bool.and(Nat.is_le(2n, l), Nat.is_le(l, n)), F.AcpiF.u8(o, 0n), l)
46
47def ent.next(+o: B.Octets) -> AcpiEntNext:
48 +n = B.Octets.len(o)
49 ent.next.go(Nat.is_eq(n, 0n), o, n)
50
51def ent.rev(xs: List<&2, AcpiRawEntry>, acc: List<&2, AcpiRawEntry>) -> List<&2, AcpiRawEntry>:
52 match xs:
53 case Nil{}:
54 acc
55 case Con{h, t}:
56 ent.rev(t, Con{h, acc})
57
58# every structure consumes at least 2 bytes, so len(o) steps are enough
59def ent.go(fuel: Nat, nx: AcpiEntNext, +o: B.Octets, +off: Nat, acc: List<&2, AcpiRawEntry>) -> Result<&2, &2, E.AcpiError, List<&2, AcpiRawEntry>>:
60 match fuel:
61 case 0n:
62 Done{ent.rev(acc, Nil{})}
63 case 1n+p:
64 match nx:
65 case AcpiEntEnd{}:
66 Done{ent.rev(acc, Nil{})}
67 case AcpiEntBad{k}:
68 Fail{E.AcpiBadEntry{off, k}}
69 case AcpiEntOk{k, +l}:
70 +rest = B.Octets.drop(l, o)
71 ent.go(p, ent.next(rest), rest, Nat.add(off, l), Con{AcpiRawEntry{k, off, B.Octets.take(l, o)}, acc})
72
73# the structures in o, which starts at offset off of its table; AcpiBadEntry
74# names the first one whose length is below 2 or runs past the end
75def AcpiRawEntry.split(+o: B.Octets, +off: Nat) -> Result<&2, &2, E.AcpiError, List<&2, AcpiRawEntry>>:
76 ent.go(B.Octets.len(o), ent.next(o), o, off, Nil{})
77
78# the structure as bytes: its type, its length, then body (the bytes after
79# the two header bytes)
80def AcpiRawEntry.encode(+k: U32, +body: B.Octets) -> B.Octets:
81 B.Octets.append(B.Octets.of_list([k, U32.from_nat(Nat.add(2n, B.Octets.len(body)))]), body)