rsdp.bend

bend-osdev-acpi@0.1.1.0 · 170 lines · 24 definitions

1# bend-osdev-acpi, rsdp.bend: the Root System Description Pointer (ACPI
2# 6.5, section 5.2.5.3), the structure that leads to every other
3# table:
4#
5#   offset  size  field
6#        0     8  Signature "RSD PTR "
7#        8     1  Checksum (bytes 0 to 19 sum to 0 mod 256)
8#        9     6  OEMID
9#       15     1  Revision (0 for ACPI 1.0, 2 from ACPI 2.0)
10#       16     4  RsdtAddress (32-bit physical address of the RSDT)
11#   from revision 2:
12#       20     4  Length (of the whole structure, 36)
13#       24     8  XsdtAddress (64-bit physical address of the XSDT)
14#       32     1  Extended Checksum (all Length bytes sum to 0 mod 256)
15#       33     3  Reserved
16#
17# Section 5.2.5.1 says where firmware puts it on IA-PC systems (the first
18# KB of the EBDA, or 0xE0000 to 0xFFFFF, on a 16-byte boundary);
19# AcpiRsdp.find searches a region's bytes, and UEFI systems hand the
20# address over in the EFI configuration table instead.
21import Base
22import bend-osdev-word64@0.1.1.0/word64.bend as W
23import bend-osdev-bytes@0.1.1.0/bytes.bend as B
24import bend-osdev-acpi@0.1.1.0/error.bend as E
25import bend-osdev-acpi@0.1.1.0/checksum.bend as C
26import bend-osdev-acpi@0.1.1.0/fields.bend as F
27
28# the revision 2 fields
29type AcpiRsdpExt is Data:
30  AcpiRsdpExt{length: U32, xsdt_address: W.W64}
31
32type AcpiRsdp is Data:
33  AcpiRsdp{oem_id: B.Octets, revision: U32, rsdt_address: U32, ext: Maybe<&2, AcpiRsdpExt>}
34
35def AcpiRsdp.signature() -> B.Octets:
36  B.Octets.of_string("RSD PTR ")
37
38def AcpiRsdp.revision(r: AcpiRsdp) -> U32:
39  match r:
40    case AcpiRsdp{o, v, a, x}:
41      v
42
43def AcpiRsdp.rsdt_address(r: AcpiRsdp) -> U32:
44  match r:
45    case AcpiRsdp{o, v, a, x}:
46      a
47
48def AcpiRsdp.ext(r: AcpiRsdp) -> Maybe<&2, AcpiRsdpExt>:
49  match r:
50    case AcpiRsdp{o, v, a, x}:
51      x
52
53def rs.xsdt(m: Maybe<&2, AcpiRsdpExt>) -> W.W64:
54  match m:
55    case None{}:
56      W.W64.zero()
57    case Some{AcpiRsdpExt{l, a}}:
58      a
59
60# the XSDT's address (zero for a revision 0 RSDP)
61def AcpiRsdp.xsdt_address(r: AcpiRsdp) -> W.W64:
62  rs.xsdt(AcpiRsdp.ext(r))
63
64def rs.checked(m: Maybe<&2, AcpiRsdpExt>) -> Nat:
65  match m:
66    case None{}:
67      20n
68    case Some{AcpiRsdpExt{l, a}}:
69      U32.to_nat(l)
70
71# how many bytes the checksums covered: 20 for revision 0, Length after
72def AcpiRsdp.checked(r: AcpiRsdp) -> Nat:
73  rs.checked(AcpiRsdp.ext(r))
74
75# Reading, checked in order: at least 20 bytes, the signature, the first
76# checksum; for revision 2 or later: at least 36 bytes, a Length from 36 to
77# the bytes given, the extended checksum
78
79def rs.p7(ok: Bool, +l: U32, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
80  match ok:
81    case False{}:
82      Fail{E.AcpiRsdpBadExtChecksum{C.AcpiChecksum.sum(B.Octets.take(U32.to_nat(l), o))}}
83    case True{}:
84      Done{AcpiRsdp{F.AcpiF.bytes(o, 9n, 6n), F.AcpiF.u8(o, 15n), F.AcpiF.u32(o, 16n), Some{AcpiRsdpExt{l, F.AcpiF.u64(o, 24n)}}}}
85
86def rs.p6(ok: Bool, +l: U32, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
87  match ok:
88    case False{}:
89      Fail{E.AcpiBadLength{l}}
90    case True{}:
91      rs.p7(C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)), l, o)
92
93def rs.p5(ok: Bool, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
94  match ok:
95    case False{}:
96      Fail{E.AcpiTooShort{36n, B.Octets.len(o)}}
97    case True{}:
98      +l = F.AcpiF.u32(o, 20n)
99      rs.p6(Bool.and(Nat.is_le(36n, U32.to_nat(l)), Nat.is_le(U32.to_nat(l), B.Octets.len(o))), l, o)
100
101def rs.p4(v1: Bool, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
102  match v1:
103    case True{}:
104      Done{AcpiRsdp{F.AcpiF.bytes(o, 9n, 6n), F.AcpiF.u8(o, 15n), F.AcpiF.u32(o, 16n), None{}}}
105    case False{}:
106      rs.p5(Nat.is_le(36n, B.Octets.len(o)), o)
107
108def rs.p3(ok: Bool, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
109  match ok:
110    case False{}:
111      Fail{E.AcpiRsdpBadChecksum{C.AcpiChecksum.sum(B.Octets.take(20n, o))}}
112    case True{}:
113      rs.p4(U32.is_lt(F.AcpiF.u8(o, 15n), 2), o)
114
115def rs.p2(ok: Bool, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
116  match ok:
117    case False{}:
118      Fail{E.AcpiBadSignature{B.Octets.take(8n, o)}}
119    case True{}:
120      rs.p3(C.AcpiChecksum.ok(B.Octets.take(20n, o)), o)
121
122def rs.p1(ok: Bool, +o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
123  match ok:
124    case False{}:
125      Fail{E.AcpiTooShort{20n, B.Octets.len(o)}}
126    case True{}:
127      rs.p2(B.Octets.is_eq(B.Octets.take(8n, o), AcpiRsdp.signature()), o)
128
129# the RSDP at the front of o
130def AcpiRsdp.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiRsdp>:
131  rs.p1(Nat.is_le(20n, B.Octets.len(o)), o)
132
133# Writing: 20 bytes for revision 0 or 1, 36 after (Length written as 36),
134# with both checksums computed
135
136def rs.v1(oem: B.Octets, +rev: U32, rsdt: U32) -> B.Octets:
137  C.AcpiChecksum.fix(8n, B.Octets.concat([AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]))
138
139def rs.build(m: Maybe<&2, AcpiRsdpExt>, +first: B.Octets) -> B.Octets:
140  match m:
141    case None{}:
142      first
143    case Some{AcpiRsdpExt{l, x}}:
144      C.AcpiChecksum.fix(32n, B.Octets.concat([first, B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]))
145
146def AcpiRsdp.build(r: AcpiRsdp) -> B.Octets:
147  match r:
148    case AcpiRsdp{oem, rev, rsdt, x}:
149      rs.build(x, rs.v1(oem, rev, rsdt))
150
151# Finding: the first 16-byte-aligned offset of o holding a signature and a
152# good first checksum
153
154def rs.here(+o: B.Octets, +i: Nat) -> Bool:
155  Bool.and(B.Octets.is_eq(B.Octets.slice(i, 8n, o), AcpiRsdp.signature()), Bool.and(Nat.is_le(Nat.add(i, 20n), B.Octets.len(o)), C.AcpiChecksum.ok(B.Octets.slice(i, 20n, o))))
156
157def rs.find.go(fuel: Nat, hit: Bool, +o: B.Octets, +i: Nat) -> Maybe<&2, Nat>:
158  match fuel:
159    case 0n:
160      None{}
161    case 1n+p:
162      match hit:
163        case True{}:
164          Some{i}
165        case False{}:
166          +j = Nat.add(i, 16n)
167          rs.find.go(p, rs.here(o, j), o, j)
168
169def AcpiRsdp.find(+o: B.Octets) -> Maybe<&2, Nat>:
170  rs.find.go(Nat.add(Nat.div(B.Octets.len(o), 16n), 1n), rs.here(o, 0n), o, 0n)