aml_pkglength.bend
bend-osdev-acpi@0.1.2.0 · 171 lines · 0 definitions
1# bend-osdev-acpi, aml_pkglength.bend: PkgLength, the length that opens every
2# AML package (ACPI 6.5, section 20.2.4, Package Length Encoding):
3#
4# PkgLength := PkgLeadByte |
5# <PkgLeadByte ByteData> |
6# <PkgLeadByte ByteData ByteData> |
7# <PkgLeadByte ByteData ByteData ByteData>
8#
9# Bits 7-6 of PkgLeadByte count the ByteData that follow. With none, bits
10# 5-0 are the length (0 to 63). Otherwise bits 3-0 are its least
11# significant four bits, each following byte the next eight, and bits 5-4
12# must be zero. So a PkgLength holds up to 2^28 - 1. The value counts the
13# PkgLength's own bytes and the package that follows.
14#
15# The decoder reads bits by pattern and builds the value by joining bits,
16# so that its round trip with the encoder computes for a value whose bits
17# are unknown (LAWS.bend: pkglength_round_trip).
18import Base
19import bend-osdev-bytes@0.1.1.1/bytes.bend as B
20import bend-osdev-acpi@0.1.2.0/error.bend as E
21
22# the value, its size in bytes (1 to 4) and what follows (list layer)
23type AmlPkgL is Data:
24 AmlPkgL{value: U32, size: Nat, rest: List<&2, U32>}
25
26# the value and what follows
27type AmlPkgLen is Data:
28 AmlPkgLen{value: U32, rest: B.Octets}
29
30# Encoding (list layer): the shortest form
31
32def pk.enc.pick(s1: Bool, s2: Bool, s3: Bool, +v: U32) -> List<&2, U32>:
33 match s1:
34 case True{}:
35 [U32.and(63, v)]
36 case False{}:
37 match s2:
38 case True{}:
39 [U32.or(64, U32.and(15, v)), U32.and(255, U32.shrn(v, 4n))]
40 case False{}:
41 match s3:
42 case True{}:
43 [U32.or(128, U32.and(15, v)), U32.and(255, U32.shrn(v, 4n)), U32.and(255, U32.shrn(v, 12n))]
44 case False{}:
45 [U32.or(192, U32.and(15, v)), U32.and(255, U32.shrn(v, 4n)), U32.and(255, U32.shrn(v, 12n)), U32.and(255, U32.shrn(v, 20n))]
46
47def pk.enc(+v: U32) -> List<&2, U32>:
48 pk.enc.pick(U32.is_eq(U32.shrn(v, 6n), 0), U32.is_eq(U32.shrn(v, 12n), 0), U32.is_eq(U32.shrn(v, 20n), 0), v)
49
50# Decoding (list layer)
51
52def pk.v2(l0: Bool, l1: Bool, l2: Bool, l3: Bool, a: U32) -> U32:
53 match a:
54 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, ah}}}}}}}}}:
55 U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, Word.zero(20n)}}}}}}}}}}}}}
56
57def pk.v3(l0: Bool, l1: Bool, l2: Bool, l3: Bool, a: U32, b: U32) -> U32:
58 match a b:
59 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, ah}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, bh}}}}}}}}}:
60 U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, Word.zero(12n)}}}}}}}}}}}}}}}}}}}}}
61
62def pk.v4(l0: Bool, l1: Bool, l2: Bool, l3: Bool, a: U32, b: U32, c: U32) -> U32:
63 match a b c:
64 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, ah}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, bh}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, ch}}}}}}}}}:
65 U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(4n)}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
66
67def pk.d2(l0: Bool, l1: Bool, l2: Bool, l3: Bool, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlPkgL>:
68 match t:
69 case Con{a, r}:
70 Done{AmlPkgL{pk.v2(l0, l1, l2, l3, a), 2n, r}}
71 case Nil{}:
72 Fail{E.AcpiAmlTruncated{}}
73
74def pk.d3(l0: Bool, l1: Bool, l2: Bool, l3: Bool, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlPkgL>:
75 match t:
76 case Con{a, Con{b, r}}:
77 Done{AmlPkgL{pk.v3(l0, l1, l2, l3, a, b), 3n, r}}
78 case _:
79 Fail{E.AcpiAmlTruncated{}}
80
81def pk.d4(l0: Bool, l1: Bool, l2: Bool, l3: Bool, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlPkgL>:
82 match t:
83 case Con{a, Con{b, Con{c, r}}}:
84 Done{AmlPkgL{pk.v4(l0, l1, l2, l3, a, b, c), 4n, r}}
85 case _:
86 Fail{E.AcpiAmlTruncated{}}
87
88# bits 5-4 must be zero in the multi-byte forms; n: how many bytes follow
89def pk.multi(l4: Bool, l5: Bool, n: Nat, l0: Bool, l1: Bool, l2: Bool, l3: Bool, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlPkgL>:
90 match l4 l5:
91 case False{} False{}:
92 match n:
93 case 1n:
94 pk.d2(l0, l1, l2, l3, t)
95 case 2n:
96 pk.d3(l0, l1, l2, l3, t)
97 case _:
98 pk.d4(l0, l1, l2, l3, t)
99 case _ _:
100 Fail{E.AcpiAmlBadPkgLength{}}
101
102def pk.lead(l7: Bool, l6: Bool, l0: Bool, l1: Bool, l2: Bool, l3: Bool, l4: Bool, l5: Bool, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlPkgL>:
103 match l7:
104 case False{}:
105 match l6:
106 case False{}:
107 Done{AmlPkgL{U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, WCon{l4, WCon{l5, Word.zero(26n)}}}}}}}, 1n, t}}
108 case True{}:
109 pk.multi(l4, l5, 1n, l0, l1, l2, l3, t)
110 case True{}:
111 match l6:
112 case False{}:
113 pk.multi(l4, l5, 2n, l0, l1, l2, l3, t)
114 case True{}:
115 pk.multi(l4, l5, 3n, l0, l1, l2, l3, t)
116
117# the PkgLength at the front of a list of bytes
118def pk.dec(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlPkgL>:
119 match xs:
120 case Nil{}:
121 Fail{E.AcpiAmlTruncated{}}
122 case Con{U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, WCon{l4, WCon{l5, WCon{l6, WCon{l7, lh}}}}}}}}}, t}:
123 pk.lead(l7, l6, l0, l1, l2, l3, l4, l5, t)
124
125# The public interface, on Octets
126
127# the values a PkgLength holds: below 2^28
128def AmlPkgLength.fits(v: U32) -> Bool:
129 U32.is_eq(U32.shrn(v, 28n), 0)
130
131# v in the shortest form (the low 28 bits of v)
132def AmlPkgLength.encode(+v: U32) -> B.Octets:
133 B.Octets.of_list(pk.enc(v))
134
135def pk.pub(r: Result<&2, &2, E.AcpiError, AmlPkgL>) -> Result<&2, &2, E.AcpiError, AmlPkgLen>:
136 match r:
137 case Fail{e}:
138 Fail{e}
139 case Done{AmlPkgL{v, n, rest}}:
140 Done{AmlPkgLen{v, B.Octets.of_list(rest)}}
141
142# the PkgLength at the front of o, and what follows it; AcpiAmlTruncated if
143# o ends inside it, AcpiAmlBadPkgLength if bits 5-4 are set in a
144# multi-byte form
145def AmlPkgLength.decode(o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlPkgLen>:
146 pk.pub(pk.dec(B.Octets.to_list(o)))
147
148def pk.size.pick(a: Bool, b: Bool, c: Bool) -> Nat:
149 match a:
150 case True{}:
151 1n
152 case False{}:
153 match b:
154 case True{}:
155 2n
156 case False{}:
157 match c:
158 case True{}:
159 3n
160 case False{}:
161 4n
162
163# the size of the PkgLength that covers a package whose contents (after
164# the PkgLength) are n bytes
165def AmlPkgLength.size_for(+n: Nat) -> Nat:
166 pk.size.pick(Nat.is_lt(n, 63n), Nat.is_lt(n, 4094n), Nat.is_lt(n, 1048573n))
167
168# a package: the PkgLength covering it, then its contents
169def AmlPkgLength.wrap(+body: B.Octets) -> B.Octets:
170 +n = B.Octets.len(body)
171 B.Octets.append(AmlPkgLength.encode(U32.from_nat(Nat.add(n, AmlPkgLength.size_for(n)))), body)