aml_pkglength.bend

bend-osdev-acpi@0.1.1.0 · 171 lines · 20 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.0/bytes.bend as B
20import bend-osdev-acpi@0.1.1.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)