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.
21	import Base
22	import bend-osdev-word64@0.1.1.0/word64.bend as W
23	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
24	import ./error.bend as E
25	import ./checksum.bend as C
26	import ./fields.bend as F
27	
28	# the revision 2 fields
29	type AcpiRsdpExt is Data:
30	  AcpiRsdpExt{length: U32, xsdt_address: W.W64}
31	
32	type AcpiRsdp is Data:
33	  AcpiRsdp{oem_id: B.Octets, revision: U32, rsdt_address: U32, ext: Maybe<&2, AcpiRsdpExt>}
34	
35	def AcpiRsdp.signature() -> B.Octets:
36	  B.Octets.of_string("RSD PTR ")
37	
38	def AcpiRsdp.revision(r: AcpiRsdp) -> U32:
39	  match r:
40	    case AcpiRsdp{o, v, a, x}:
41	      v
42	
43	def AcpiRsdp.rsdt_address(r: AcpiRsdp) -> U32:
44	  match r:
45	    case AcpiRsdp{o, v, a, x}:
46	      a
47	
48	def AcpiRsdp.ext(r: AcpiRsdp) -> Maybe<&2, AcpiRsdpExt>:
49	  match r:
50	    case AcpiRsdp{o, v, a, x}:
51	      x
52	
53	def 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)
61	def AcpiRsdp.xsdt_address(r: AcpiRsdp) -> W.W64:
62	  rs.xsdt(AcpiRsdp.ext(r))
63	
64	def 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
72	def 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	
79	def 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	
86	def 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	
93	def 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	
101	def 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	
108	def 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	
115	def 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	
122	def 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
130	def 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	
136	def 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	
139	def 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	
146	def 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	
154	def 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	
157	def 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	
169	def 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)