slit.bend

bend-osdev-acpi@0.1.1.0 · 71 lines · 10 definitions

1# bend-osdev-acpi, slit.bend: the System Locality Distance Information
2# Table, "SLIT" (ACPI 6.5, section 5.2.17): after the header, the number of
3# system localities N (8 bytes, offset 36), then the N x N matrix of
4# relative distances, one byte each, row by row, from offset 44. Entry
5# (i, i) is 10 (a locality's distance to itself); 0xFF means unreachable.
6import Base
7import bend-osdev-word64@0.1.1.0/word64.bend as W
8import bend-osdev-bytes@0.1.1.0/bytes.bend as B
9import bend-osdev-acpi@0.1.1.0/error.bend as E
10import bend-osdev-acpi@0.1.1.0/header.bend as H
11import bend-osdev-acpi@0.1.1.0/fields.bend as F
12
13type AcpiSlit is Data:
14  AcpiSlit{header: H.AcpiHeader, count: Nat, matrix: B.Octets}
15
16def AcpiSlit.count(s: AcpiSlit) -> Nat:
17  match s:
18    case AcpiSlit{h, n, m}:
19      n
20
21def slit.mk(ok: Bool, +h: H.AcpiHeader, +n: Nat, +body: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
22  match ok:
23    case False{}:
24      Fail{E.AcpiBadSize{B.Octets.len(body)}}
25    case True{}:
26      Done{AcpiSlit{h, n, B.Octets.slice(8n, Nat.mul(n, n), body)}}
27
28def slit.body(ok: Bool, +h: H.AcpiHeader, +body: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
29  match ok:
30    case False{}:
31      Fail{E.AcpiTooShort{44n, Nat.add(36n, B.Octets.len(body))}}
32    case True{}:
33      +big = F.AcpiF.u64(body, 0n)
34      +n = U32.to_nat(W.W64.lo(big))
35      slit.mk(Bool.and(U32.is_eq(W.W64.hi(big), 0), Bool.and(U32.is_lt(W.W64.lo(big), 65536), Nat.is_le(Nat.add(8n, Nat.mul(n, n)), B.Octets.len(body)))), h, n, body)
36
37# a checked table as an SLIT: the N x N matrix must fit in the body
38# (AcpiBadSize otherwise; N is limited to 65535)
39def AcpiSlit.of_sdt(t: H.AcpiSdt) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
40  match t:
41    case H.AcpiSdt{h, +body}:
42      slit.body(Nat.is_le(8n, B.Octets.len(body)), h, body)
43
44def slit.parse(r: Result<&2, &2, E.AcpiError, H.AcpiSdt>) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
45  match r:
46    case Fail{e}:
47      Fail{e}
48    case Done{t}:
49      AcpiSlit.of_sdt(t)
50
51def AcpiSlit.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
52  slit.parse(H.AcpiSdt.parse_sig(B.Octets.of_string("SLIT"), o))
53
54def slit.at(ok: Bool, +n: Nat, +m: B.Octets, +i: Nat, j: Nat) -> Maybe<&2, U32>:
55  match ok:
56    case False{}:
57      None{}
58    case True{}:
59      B.Octets.at(m, Nat.add(Nat.mul(i, n), j))
60
61# the distance from locality i to locality j, if both are below N
62def AcpiSlit.distance(s: AcpiSlit, +i: Nat, +j: Nat) -> Maybe<&2, U32>:
63  match s:
64    case AcpiSlit{h, +n, m}:
65      slit.at(Bool.and(Nat.is_lt(i, n), Nat.is_lt(j, n)), n, m, i, j)
66
67# the table, from N and the matrix (fitted to N x N bytes)
68def AcpiSlit.build(s: AcpiSlit) -> B.Octets:
69  match s:
70    case AcpiSlit{H.AcpiHeader{sg, l, r, c, o, t, orv, ci, cr}, +n, m}:
71      H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("SLIT"), l, r, c, o, t, orv, ci, cr}, B.Octets.append(B.Octets.le64(W.W64.from_nat(n)), F.AcpiF.fit(Nat.mul(n, n), m)))