rsdp.bend
bend-osdev-acpi@0.1.2.0 · 170 lines · 0 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.1/word64.bend as W
23import bend-osdev-bytes@0.1.1.1/bytes.bend as B
24import bend-osdev-acpi@0.1.2.0/error.bend as E
25import bend-osdev-acpi@0.1.2.0/checksum.bend as C
26import bend-osdev-acpi@0.1.2.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)