entries.bend

bend-osdev-acpi@0.1.1.0 · 81 lines · 11 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.1.0/bytes.bend as B
7import bend-osdev-acpi@0.1.1.0/error.bend as E
8import bend-osdev-acpi@0.1.1.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)