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.
14	import Base
15	import bend-osdev-word64@0.1.1.1/word64.bend as W
16	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
17	import ./error.bend as E
18	import ./header.bend as H
19	import ./rsdp.bend as P
20	import ./rsdt.bend as S
21	import ./fadt.bend as F
22	import ./facs.bend as FS
23	import ./registry.bend as R
24	
25	# An in-memory physical memory: regions at base addresses
26	
27	type AcpiMemRegion is Data:
28	  AcpiMemRegion{base: W.W64, bytes: B.Octets}
29	
30	type AcpiMemImage is Data:
31	  AcpiMemImage{regions: List<&2, AcpiMemRegion>}
32	
33	def 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)
42	def 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	
50	def 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	
58	def 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	
63	def 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	
70	def 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
78	def 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)
84	def AcpiMemImage.read(m: AcpiMemImage, addr: W.W64, n: Nat) -> Result<&2, &2, E.AcpiError, B.Octets>:
85	  mem.read(m, addr, n)
86	
87	def AcpiMemImage.of_list(rs: List<&2, AcpiMemRegion>) -> AcpiMemImage:
88	  AcpiMemImage{rs}
89	
90	# Options
91	
92	type 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	
97	def 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
104	type AcpiLoaded<-X: Data> is Data:
105	  AcpiLoaded{address: W.W64, table: Result<&2, &2, E.AcpiError, R.AcpiTable<X>>}
106	
107	type 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
114	def 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	
117	def 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	
122	def ld.rsdp.pick(v1: Bool) -> Nat:
123	  match v1:
124	    case True{}:
125	      20n
126	    case False{}:
127	      36n
128	
129	def 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	
132	def 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	
138	def 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	
145	def 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	
150	def 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	
153	def 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
161	def 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	
170	def 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	
177	def ld.nz(+a: W.W64) -> Maybe<&2, W.W64>:
178	  ld.nz.pick(W.W64.is_zero(a), a)
179	
180	def 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	
187	def 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	
194	def 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	
201	def 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	
208	def 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	
215	def 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	
222	def 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	
227	def ld.opts(o: AcpiLoadOptions) -> Bool:
228	  match o:
229	    case AcpiLoadOptions{p, r}:
230	      p
231	
232	def 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
240	def 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	
247	def 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	
252	def AcpiTableSet.tables(~X: Data, s: AcpiTableSet<X>) -> List<&2, AcpiLoaded<X>>:
253	  match s:
254	    case AcpiTableSet{r, root, ts, f}:
255	      ts
256	
257	def 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	
264	def 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
275	def AcpiTableSet.find(~X: Data, s: AcpiTableSet<X>, +name: String) -> Maybe<&2, R.AcpiTable<X>>:
276	  ld.find(~X, AcpiTableSet.tables(~X, s), name)