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 # | 6 # | 7 # 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). 18 import Base 19 import bend-osdev-bytes@0.1.1.1/bytes.bend as B 20 import ./error.bend as E 21 22 # the value, its size in bytes (1 to 4) and what follows (list layer) 23 type AmlPkgL is Data: 24 AmlPkgL{value: U32, size: Nat, rest: List<&2, U32>} 25 26 # the value and what follows 27 type AmlPkgLen is Data: 28 AmlPkgLen{value: U32, rest: B.Octets} 29 30 # Encoding (list layer): the shortest form 31 32 def 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 47 def 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 52 def 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 57 def 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 62 def 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 67 def 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 74 def 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 81 def 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 89 def 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 102 def 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 118 def 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 128 def 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) 132 def AmlPkgLength.encode(+v: U32) -> B.Octets: 133 B.Octets.of_list(pk.enc(v)) 134 135 def 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 145 def AmlPkgLength.decode(o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlPkgLen>: 146 pk.pub(pk.dec(B.Octets.to_list(o))) 147 148 def 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 165 def 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 169 def 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)