acpi.bend
bend-osdev-acpi@0.1.2.0 · 276 lines · 0 definitions
1# bend-osdev-acpi: the ACPI tables of a machine, found and read through
2# physical memory (ACPI 6.5, section 5.2: the RSDP leads to the RSDT or
3# XSDT, which lists every other table but the DSDT and the FACS, which the
4# FADT points to).
5#
6# Physical memory is read through a template argument, so any memory works
7# (a mapped window in a kernel, a firmware image, a test image):
8#
9# ~M: Data, ~read: M -> W64 -> Nat -> Result<&2, &2, AcpiError, Octets>
10#
11# read(m, address, n) answers the n bytes at a physical address, or
12# AcpiNotMapped. AcpiMemImage is an in-memory default. Tables are read one
13# at a time: a header's first 8 bytes for its length, then the table.
14import Base
15import bend-osdev-word64@0.1.1.1/word64.bend as W
16import bend-osdev-bytes@0.1.1.1/bytes.bend as B
17import bend-osdev-acpi@0.1.2.0/error.bend as E
18import bend-osdev-acpi@0.1.2.0/header.bend as H
19import bend-osdev-acpi@0.1.2.0/rsdp.bend as P
20import bend-osdev-acpi@0.1.2.0/rsdt.bend as S
21import bend-osdev-acpi@0.1.2.0/fadt.bend as F
22import bend-osdev-acpi@0.1.2.0/facs.bend as FS
23import bend-osdev-acpi@0.1.2.0/registry.bend as R
24
25# An in-memory physical memory: regions at base addresses
26
27type AcpiMemRegion is Data:
28 AcpiMemRegion{base: W.W64, bytes: B.Octets}
29
30type AcpiMemImage is Data:
31 AcpiMemImage{regions: List<&2, AcpiMemRegion>}
32
33def mem.slice(inside: Bool, +off: Nat, +n: Nat, +o: B.Octets) -> Maybe<&2, B.Octets>:
34 match inside:
35 case False{}:
36 None{}
37 case True{}:
38 Some{B.Octets.slice(off, n, o)}
39
40# the offset into the region is computed only once it is known to be small
41# (a Nat holds at most 2^48 - 1 at run time)
42def mem.near(near: Bool, +off: W.W64, +n: Nat, +o: B.Octets) -> Maybe<&2, B.Octets>:
43 match near:
44 case False{}:
45 None{}
46 case True{}:
47 +k = U32.to_nat(W.W64.lo(off))
48 mem.slice(Nat.is_le(Nat.add(k, n), B.Octets.len(o)), k, n, o)
49
50def mem.above(above: Bool, +base: W.W64, +addr: W.W64, +n: Nat, +o: B.Octets) -> Maybe<&2, B.Octets>:
51 match above:
52 case False{}:
53 None{}
54 case True{}:
55 +off = W.W64.sub(addr, base)
56 mem.near(U32.is_eq(W.W64.hi(off), 0), off, n, o)
57
58def mem.try(r: AcpiMemRegion, +addr: W.W64, +n: Nat) -> Maybe<&2, B.Octets>:
59 match r:
60 case AcpiMemRegion{+base, +o}:
61 mem.above(W.W64.is_le(base, addr), base, addr, n, o)
62
63def mem.find(rs: List<&2, AcpiMemRegion>, +addr: W.W64, +n: Nat) -> Maybe<&2, B.Octets>:
64 match rs:
65 case Nil{}:
66 None{}
67 case Con{h, t}:
68 Maybe.or(&2, B.Octets, mem.try(h, addr, n), mem.find(t, addr, n))
69
70def mem.done(m: Maybe<&2, B.Octets>, +addr: W.W64) -> Result<&2, &2, E.AcpiError, B.Octets>:
71 match m:
72 case None{}:
73 Fail{E.AcpiNotMapped{addr}}
74 case Some{o}:
75 Done{o}
76
77# n bytes at a physical address, from the first region holding all of them
78def mem.read(m: AcpiMemImage, +addr: W.W64, +n: Nat) -> Result<&2, &2, E.AcpiError, B.Octets>:
79 match m:
80 case AcpiMemImage{rs}:
81 mem.done(mem.find(rs, addr, n), addr)
82
83# (plain parameters, so that it fits the template type ~read)
84def AcpiMemImage.read(m: AcpiMemImage, addr: W.W64, n: Nat) -> Result<&2, &2, E.AcpiError, B.Octets>:
85 mem.read(m, addr, n)
86
87def AcpiMemImage.of_list(rs: List<&2, AcpiMemRegion>) -> AcpiMemImage:
88 AcpiMemImage{rs}
89
90# Options
91
92type AcpiLoadOptions is Data:
93 # use the XSDT when the RSDP has one (ACPI 6.5, 5.2.5.3: OSPM uses the
94 # XSDT if present); False reads the RSDT
95 AcpiLoadOptions{prefer_xsdt: Bool, registry: R.AcpiRegistry}
96
97def AcpiLoadOptions.default() -> AcpiLoadOptions:
98 AcpiLoadOptions{True{}, R.AcpiRegistry.default()}
99
100# What a machine's tables hold
101
102# a table, by the address it was read from; a table that fails to read
103# does not stop the others
104type AcpiLoaded<-X: Data> is Data:
105 AcpiLoaded{address: W.W64, table: Result<&2, &2, E.AcpiError, R.AcpiTable<X>>}
106
107type AcpiTableSet<-X: Data> is Data:
108 AcpiTableSet{rsdp: P.AcpiRsdp, root: S.AcpiSdtList, tables: List<&2, AcpiLoaded<X>>, facs: Maybe<&2, Result<&2, &2, E.AcpiError, FS.AcpiFacs>>}
109
110# Reading
111
112# the table at a physical address: its length from its header, then all of
113# its bytes
114def ld.whole(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, +m: M, +addr: W.W64, +head: B.Octets) -> Result<&2, &2, E.AcpiError, B.Octets>:
115 read(m, addr, U32.to_nat(Maybe.default(&2, U32, B.Octets.le32_at(head, 4n), 0)))
116
117def AcpiTables.read_table(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, +m: M, +addr: W.W64) -> Result<&2, &2, E.AcpiError, B.Octets>:
118 do Result<&2, &2, E.AcpiError, B.Octets>:
119 head : B.Octets <- read(m, addr, 8n)
120 ld.whole(~M, ~read, m, addr, head)
121
122def ld.rsdp.pick(v1: Bool) -> Nat:
123 match v1:
124 case True{}:
125 20n
126 case False{}:
127 36n
128
129def ld.rsdp.len(+head: B.Octets) -> Nat:
130 ld.rsdp.pick(U32.is_lt(Maybe.default(&2, U32, B.Octets.at(head, 15n), 0), 2))
131
132def AcpiTables.read_rsdp(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, +m: M, +addr: W.W64) -> Result<&2, &2, E.AcpiError, P.AcpiRsdp>:
133 do Result<&2, &2, E.AcpiError, P.AcpiRsdp>:
134 head : B.Octets <- read(m, addr, 20n)
135 o : B.Octets <- read(m, addr, ld.rsdp.len(head))
136 P.AcpiRsdp.parse(o)
137
138def ld.root.parse(xsdt: Bool, +o: B.Octets) -> Result<&2, &2, E.AcpiError, S.AcpiSdtList>:
139 match xsdt:
140 case True{}:
141 S.AcpiXsdt.parse(o)
142 case False{}:
143 S.AcpiRsdt.parse(o)
144
145def ld.root(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, +m: M, +xsdt: Bool, +addr: W.W64) -> Result<&2, &2, E.AcpiError, S.AcpiSdtList>:
146 do Result<&2, &2, E.AcpiError, S.AcpiSdtList>:
147 o : B.Octets <- AcpiTables.read_table(~M, ~read, m, addr)
148 ld.root.parse(xsdt, o)
149
150def ld.one(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, ~X: Data, ~ext: U32 -> H.AcpiSdt -> Result<&2, &2, E.AcpiError, X>, +m: M, +reg: R.AcpiRegistry, +addr: W.W64) -> AcpiLoaded<X>:
151 AcpiLoaded{addr, Result.bind(&2, &2, E.AcpiError, B.Octets, R.AcpiTable<X>, AcpiTables.read_table(~M, ~read, m, addr), o => R.AcpiTable.parse_with(~X, ~ext, reg, o))}
152
153def ld.all(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, ~X: Data, ~ext: U32 -> H.AcpiSdt -> Result<&2, &2, E.AcpiError, X>, as: List<&2, W.W64>, +m: M, +reg: R.AcpiRegistry) -> List<&2, AcpiLoaded<X>>:
154 match as:
155 case Nil{}:
156 Nil{}
157 case Con{a, t}:
158 Con{ld.one(~M, ~read, ~X, ~ext, m, reg, a), ld.all(~M, ~read, ~X, ~ext, t, m, reg)}
159
160# the FADT among the tables read
161def ld.fadt(~X: Data, ts: List<&2, AcpiLoaded<X>>) -> Maybe<&2, F.AcpiFadt>:
162 match ts:
163 case Nil{}:
164 None{}
165 case Con{AcpiLoaded{a, Done{R.AcpiTFadt{f}}}, t}:
166 Some{f}
167 case Con{h, t}:
168 ld.fadt(~X, t)
169
170def ld.nz.pick(z: Bool, +a: W.W64) -> Maybe<&2, W.W64>:
171 match z:
172 case True{}:
173 None{}
174 case False{}:
175 Some{a}
176
177def ld.nz(+a: W.W64) -> Maybe<&2, W.W64>:
178 ld.nz.pick(W.W64.is_zero(a), a)
179
180def ld.list(m: Maybe<&2, W.W64>) -> List<&2, W.W64>:
181 match m:
182 case None{}:
183 Nil{}
184 case Some{a}:
185 [a]
186
187def ld.dsdt(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, ~X: Data, ~ext: U32 -> H.AcpiSdt -> Result<&2, &2, E.AcpiError, X>, f: Maybe<&2, F.AcpiFadt>, +m: M, +reg: R.AcpiRegistry) -> List<&2, AcpiLoaded<X>>:
188 match f:
189 case None{}:
190 Nil{}
191 case Some{+fa}:
192 ld.all(~M, ~read, ~X, ~ext, ld.list(ld.nz(F.AcpiFadt.dsdt_address(fa))), m, reg)
193
194def ld.facs.at(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, +m: M, a: Maybe<&2, W.W64>) -> Maybe<&2, Result<&2, &2, E.AcpiError, FS.AcpiFacs>>:
195 match a:
196 case None{}:
197 None{}
198 case Some{+addr}:
199 Some{Result.bind(&2, &2, E.AcpiError, B.Octets, FS.AcpiFacs, read(m, addr, 64n), o => FS.AcpiFacs.parse(o))}
200
201def ld.facs(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, f: Maybe<&2, F.AcpiFadt>, +m: M) -> Maybe<&2, Result<&2, &2, E.AcpiError, FS.AcpiFacs>>:
202 match f:
203 case None{}:
204 None{}
205 case Some{+fa}:
206 ld.facs.at(~M, ~read, m, ld.nz(F.AcpiFadt.facs_address(fa)))
207
208def ld.use_x(prefer: Bool, +r: P.AcpiRsdp) -> Bool:
209 match prefer:
210 case True{}:
211 Bool.not(W.W64.is_zero(P.AcpiRsdp.xsdt_address(r)))
212 case False{}:
213 False{}
214
215def ld.root_addr(x: Bool, +r: P.AcpiRsdp) -> W.W64:
216 match x:
217 case True{}:
218 P.AcpiRsdp.xsdt_address(r)
219 case False{}:
220 W.W64.from_u32(P.AcpiRsdp.rsdt_address(r))
221
222def ld.finish(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, ~X: Data, ~ext: U32 -> H.AcpiSdt -> Result<&2, &2, E.AcpiError, X>, +m: M, +reg: R.AcpiRegistry, rsdp: P.AcpiRsdp, +root: S.AcpiSdtList) -> AcpiTableSet<X>:
223 +ts = ld.all(~M, ~read, ~X, ~ext, S.AcpiSdtList.entries(root), m, reg)
224 +f = ld.fadt(~X, ts)
225 AcpiTableSet{rsdp, root, List.append(&2, AcpiLoaded<X>, ts, ld.dsdt(~M, ~read, ~X, ~ext, f, m, reg)), ld.facs(~M, ~read, f, m)}
226
227def ld.opts(o: AcpiLoadOptions) -> Bool:
228 match o:
229 case AcpiLoadOptions{p, r}:
230 p
231
232def ld.reg(o: AcpiLoadOptions) -> R.AcpiRegistry:
233 match o:
234 case AcpiLoadOptions{p, r}:
235 r
236
237# every table of the machine whose RSDP is at rsdp_addr: the RSDP, the RSDT
238# or XSDT (Fail if either cannot be read), then each table it lists, the
239# DSDT (from the FADT) and the FACS, each read and parsed on its own
240def AcpiTables.load_with(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, ~X: Data, ~ext: U32 -> H.AcpiSdt -> Result<&2, &2, E.AcpiError, X>, +opts: AcpiLoadOptions, +m: M, +rsdp_addr: W.W64) -> Result<&2, &2, E.AcpiError, AcpiTableSet<X>>:
241 do Result<&2, &2, E.AcpiError, AcpiTableSet<X>>:
242 +r : P.AcpiRsdp <- AcpiTables.read_rsdp(~M, ~read, m, rsdp_addr)
243 +x : Bool = ld.use_x(ld.opts(opts), r)
244 root : S.AcpiSdtList <- ld.root(~M, ~read, m, x, ld.root_addr(x, r))
245 return ld.finish(~M, ~read, ~X, ~ext, m, ld.reg(opts), r, root)
246
247def AcpiTables.load(~M: Data, ~read: M -> W.W64 -> Nat -> Result<&2, &2, E.AcpiError, B.Octets>, +m: M, +rsdp_addr: W.W64) -> Result<&2, &2, E.AcpiError, AcpiTableSet<R.AcpiNoExt>>:
248 AcpiTables.load_with(~M, ~read, ~R.AcpiNoExt, ~R.AcpiNoExt.parse, AcpiLoadOptions.default(), m, rsdp_addr)
249
250# Queries
251
252def AcpiTableSet.tables(~X: Data, s: AcpiTableSet<X>) -> List<&2, AcpiLoaded<X>>:
253 match s:
254 case AcpiTableSet{r, root, ts, f}:
255 ts
256
257def ld.find.pick(~X: Data, hit: Bool, t: R.AcpiTable<X>, rest: Maybe<&2, R.AcpiTable<X>>) -> Maybe<&2, R.AcpiTable<X>>:
258 match hit:
259 case True{}:
260 Some{t}
261 case False{}:
262 rest
263
264def ld.find(~X: Data, ts: List<&2, AcpiLoaded<X>>, +name: String) -> Maybe<&2, R.AcpiTable<X>>:
265 match ts:
266 case Nil{}:
267 None{}
268 case Con{AcpiLoaded{a, Done{+t}}, rest}:
269 ld.find.pick(~X, String.eq(R.AcpiTable.name(~X, t), name), t, ld.find(~X, rest, name))
270 case Con{h, rest}:
271 ld.find(~X, rest, name)
272
273# the first table read whose parser's name (R.AcpiTable.name: the
274# signature) is name
275def AcpiTableSet.find(~X: Data, s: AcpiTableSet<X>, +name: String) -> Maybe<&2, R.AcpiTable<X>>:
276 ld.find(~X, AcpiTableSet.tables(~X, s), name)