1	# bend-osdev-acpi, entries.bend: the variable-length sub-structures that the
2	# MADT (ACPI 6.5, section 5.2.12) and the SRAT (5.2.16) carry after their
3	# fixed fields. Each begins with a type byte and a length byte (the
4	# structure's whole length, these two bytes included).
5	import Base
6	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
7	import ./error.bend as E
8	import ./fields.bend as F
9	
10	# one structure: its type, its offset from the start of the table, and its
11	# bytes (the type and length bytes included)
12	type AcpiRawEntry is Data:
13	  AcpiRawEntry{kind: U32, offset: Nat, data: B.Octets}
14	
15	def AcpiRawEntry.kind(e: AcpiRawEntry) -> U32:
16	  match e:
17	    case AcpiRawEntry{k, off, d}:
18	      k
19	
20	def AcpiRawEntry.data(e: AcpiRawEntry) -> B.Octets:
21	  match e:
22	    case AcpiRawEntry{k, off, d}:
23	      d
24	
25	# what comes next in the bytes: nothing, a structure of type k and length l,
26	# or a structure of type k whose length is bad
27	type AcpiEntNext is Data:
28	  AcpiEntEnd{}
29	  AcpiEntOk{kind: U32, len: Nat}
30	  AcpiEntBad{kind: U32}
31	
32	def ent.next.pick(ok: Bool, +k: U32, l: Nat) -> AcpiEntNext:
33	  match ok:
34	    case True{}:
35	      AcpiEntOk{k, l}
36	    case False{}:
37	      AcpiEntBad{k}
38	
39	def ent.next.go(empty: Bool, +o: B.Octets, +n: Nat) -> AcpiEntNext:
40	  match empty:
41	    case True{}:
42	      AcpiEntEnd{}
43	    case False{}:
44	      +l = U32.to_nat(F.AcpiF.u8(o, 1n))
45	      ent.next.pick(Bool.and(Nat.is_le(2n, l), Nat.is_le(l, n)), F.AcpiF.u8(o, 0n), l)
46	
47	def ent.next(+o: B.Octets) -> AcpiEntNext:
48	  +n = B.Octets.len(o)
49	  ent.next.go(Nat.is_eq(n, 0n), o, n)
50	
51	def ent.rev(xs: List<&2, AcpiRawEntry>, acc: List<&2, AcpiRawEntry>) -> List<&2, AcpiRawEntry>:
52	  match xs:
53	    case Nil{}:
54	      acc
55	    case Con{h, t}:
56	      ent.rev(t, Con{h, acc})
57	
58	# every structure consumes at least 2 bytes, so len(o) steps are enough
59	def ent.go(fuel: Nat, nx: AcpiEntNext, +o: B.Octets, +off: Nat, acc: List<&2, AcpiRawEntry>) -> Result<&2, &2, E.AcpiError, List<&2, AcpiRawEntry>>:
60	  match fuel:
61	    case 0n:
62	      Done{ent.rev(acc, Nil{})}
63	    case 1n+p:
64	      match nx:
65	        case AcpiEntEnd{}:
66	          Done{ent.rev(acc, Nil{})}
67	        case AcpiEntBad{k}:
68	          Fail{E.AcpiBadEntry{off, k}}
69	        case AcpiEntOk{k, +l}:
70	          +rest = B.Octets.drop(l, o)
71	          ent.go(p, ent.next(rest), rest, Nat.add(off, l), Con{AcpiRawEntry{k, off, B.Octets.take(l, o)}, acc})
72	
73	# the structures in o, which starts at offset off of its table; AcpiBadEntry
74	# names the first one whose length is below 2 or runs past the end
75	def AcpiRawEntry.split(+o: B.Octets, +off: Nat) -> Result<&2, &2, E.AcpiError, List<&2, AcpiRawEntry>>:
76	  ent.go(B.Octets.len(o), ent.next(o), o, off, Nil{})
77	
78	# the structure as bytes: its type, its length, then body (the bytes after
79	# the two header bytes)
80	def AcpiRawEntry.encode(+k: U32, +body: B.Octets) -> B.Octets:
81	  B.Octets.append(B.Octets.of_list([k, U32.from_nat(Nat.add(2n, B.Octets.len(body)))]), body)