acpi.bend

bend-osdev-acpi@0.1.1.0 · 276 lines · 42 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.0/word64.bend as W
16import bend-osdev-bytes@0.1.1.0/bytes.bend as B
17import bend-osdev-acpi@0.1.1.0/error.bend as E
18import bend-osdev-acpi@0.1.1.0/header.bend as H
19import bend-osdev-acpi@0.1.1.0/rsdp.bend as P
20import bend-osdev-acpi@0.1.1.0/rsdt.bend as S
21import bend-osdev-acpi@0.1.1.0/fadt.bend as F
22import bend-osdev-acpi@0.1.1.0/facs.bend as FS
23import bend-osdev-acpi@0.1.1.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)