1 # bend-osdev-acpi, aml_name.bend: AML name strings (ACPI 6.5, sections 2 # 20.2.2, Name Objects Encoding, and 5.3, ACPI Namespace): 3 # 4 # NameSeg := 5 # LeadNameChar := 'A'-'Z' | '_' 6 # NameChar := DigitChar | LeadNameChar (DigitChar: '0'-'9') 7 # NameString := | 8 # RootChar := '\' (0x5C) 9 # PrefixPath := Nothing | <'^' PrefixPath> ('^' is 0x5E) 10 # NamePath := NameSeg | DualNamePath | MultiNamePath | NullName 11 # DualNamePath := DualNamePrefix NameSeg NameSeg (DualNamePrefix: 0x2E) 12 # MultiNamePath := MultiNamePrefix SegCount NameSeg(SegCount) 13 # (MultiNamePrefix: 0x2F; SegCount: a byte, 1 to 255) 14 # NullName := 0x00 15 # 16 # A name is AmlName{root, up, segs}: rooted at '\', or up some number of 17 # parents, then its segments (4 bytes each, as Octets). The encoder writes 18 # the shortest NamePath (a NameSeg for one segment, DualNamePath for two, 19 # MultiNamePath for three or more); the decoder reads every form, and 20 # refuses a SegCount of 0. 21 import Base 22 import bend-osdev-bytes@0.1.1.1/bytes.bend as B 23 import ./error.bend as E 24 25 type AmlName is Data: 26 AmlName{root: Bool, up: Nat, segs: List<&2, B.Octets>} 27 28 # a name read from a list of bytes: the name and what follows 29 type AmlNameL is Data: 30 AmlNameL{name: AmlName, rest: List<&2, U32>} 31 32 # a name read from Octets 33 type AmlNameParsed is Data: 34 AmlNameParsed{name: AmlName, rest: B.Octets} 35 36 def AmlName.root(n: AmlName) -> Bool: 37 match n: 38 case AmlName{r, u, s}: 39 r 40 41 def AmlName.up(n: AmlName) -> Nat: 42 match n: 43 case AmlName{r, u, s}: 44 u 45 46 def AmlName.segs(n: AmlName) -> List<&2, B.Octets>: 47 match n: 48 case AmlName{r, u, s}: 49 s 50 51 # What a byte can begin 52 53 type AmlLeadKind is Data: 54 AmlLRoot{} 55 AmlLParent{} 56 AmlLDual{} 57 AmlLMulti{} 58 AmlLNull{} 59 AmlLSeg{} 60 AmlLOther{} 61 62 def nm.alpha(+c: U32) -> Bool: 63 Bool.or(Bool.and(U32.is_le(65, c), U32.is_le(c, 90)), U32.is_eq(c, 95)) 64 65 def nm.cls.c(seg: Bool) -> AmlLeadKind: 66 match seg: 67 case True{}: 68 AmlLSeg{} 69 case False{}: 70 AmlLOther{} 71 72 def nm.cls.b(z: Bool, +c: U32) -> AmlLeadKind: 73 match z: 74 case True{}: 75 AmlLNull{} 76 case False{}: 77 nm.cls.c(nm.alpha(c)) 78 79 def nm.cls.a(m: Bool, +c: U32) -> AmlLeadKind: 80 match m: 81 case True{}: 82 AmlLMulti{} 83 case False{}: 84 nm.cls.b(U32.is_eq(c, 0), c) 85 86 def nm.cls.n9(d: Bool, +c: U32) -> AmlLeadKind: 87 match d: 88 case True{}: 89 AmlLDual{} 90 case False{}: 91 nm.cls.a(U32.is_eq(c, 47), c) 92 93 def nm.cls.n8(p: Bool, +c: U32) -> AmlLeadKind: 94 match p: 95 case True{}: 96 AmlLParent{} 97 case False{}: 98 nm.cls.n9(U32.is_eq(c, 46), c) 99 100 def nm.cls.r(r: Bool, +c: U32) -> AmlLeadKind: 101 match r: 102 case True{}: 103 AmlLRoot{} 104 case False{}: 105 nm.cls.n8(U32.is_eq(c, 94), c) 106 107 # the kind of name element a byte begins 108 def AmlLead.classify(+c: U32) -> AmlLeadKind: 109 nm.cls.r(U32.is_eq(c, 92), c) 110 111 def AmlLead.is_seg(k: AmlLeadKind) -> Bool: 112 match k: 113 case AmlLSeg{}: 114 True{} 115 case _: 116 False{} 117 118 # a NameChar: a LeadNameChar or a digit 119 def AmlName.name_char(+c: U32) -> Bool: 120 Bool.or(nm.alpha(c), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))) 121 122 def nm.seg_ok4(+c0: U32, +c1: U32, +c2: U32, +c3: U32) -> Bool: 123 Bool.and(AmlLead.is_seg(AmlLead.classify(c0)), Bool.and(AmlName.name_char(c1), Bool.and(AmlName.name_char(c2), AmlName.name_char(c3)))) 124 125 def nm.seg_ok.list(xs: List<&2, U32>) -> Bool: 126 match xs: 127 case Con{c0, Con{c1, Con{c2, Con{c3, Nil{}}}}}: 128 nm.seg_ok4(c0, c1, c2, c3) 129 case _: 130 False{} 131 132 # a NameSeg: four bytes, a LeadNameChar then three NameChars 133 def AmlName.seg_ok(s: B.Octets) -> Bool: 134 nm.seg_ok.list(B.Octets.to_list(s)) 135 136 def AmlName.segs_ok(ss: List<&2, B.Octets>) -> Bool: 137 match ss: 138 case Nil{}: 139 True{} 140 case Con{s, t}: 141 Bool.and(AmlName.seg_ok(s), AmlName.segs_ok(t)) 142 143 def nm.root_up_ok(root: Bool, up: Nat) -> Bool: 144 match root: 145 case True{}: 146 Nat.is_eq(up, 0n) 147 case False{}: 148 True{} 149 150 def nm.len(ss: List<&2, B.Octets>) -> Nat: 151 List.length(&2, B.Octets, ss) 152 153 # the names a NameString can hold: not both rooted and going up, every 154 # segment a NameSeg, at most 255 segments 155 def AmlName.valid(n: AmlName) -> Bool: 156 match n: 157 case AmlName{r, u, +ss}: 158 Bool.and(nm.root_up_ok(r, u), Bool.and(AmlName.segs_ok(ss), Nat.is_lt(nm.len(ss), 256n))) 159 160 # Encoding (list layer) 161 162 def nm.carets(n: Nat) -> List<&2, U32>: 163 match n: 164 case 0n: 165 Nil{} 166 case 1n+p: 167 Con{94, nm.carets(p)} 168 169 def nm.prefix(root: Bool, up: Nat) -> List<&2, U32>: 170 match root: 171 case True{}: 172 [92] 173 case False{}: 174 nm.carets(up) 175 176 def nm.segs.list(ss: List<&2, B.Octets>) -> List<&2, U32>: 177 match ss: 178 case Nil{}: 179 Nil{} 180 case Con{s, t}: 181 B.append(B.Octets.to_list(s), nm.segs.list(t)) 182 183 def nm.path(ss: List<&2, B.Octets>) -> List<&2, U32>: 184 match ss: 185 case Nil{}: 186 [0] 187 case Con{s, Nil{}}: 188 nm.segs.list([s]) 189 case Con{s1, Con{s2, Nil{}}}: 190 Con{46, nm.segs.list([s1, s2])} 191 case Con{s1, Con{s2, Con{s3, +t}}}: 192 Con{47, Con{U32.from_nat(Nat.add(3n, nm.len(t))), nm.segs.list(Con{s1, Con{s2, Con{s3, t}}})}} 193 194 def nm.enc(n: AmlName) -> List<&2, U32>: 195 match n: 196 case AmlName{r, u, ss}: 197 B.append(nm.prefix(r, u), nm.path(ss)) 198 199 # the name as a NameString (AmlName.valid names read back: LAWS.bend, 200 # namestring_round_trip) 201 def AmlName.encode(n: AmlName) -> B.Octets: 202 B.Octets.of_list(nm.enc(n)) 203 204 # its size in bytes 205 def AmlName.size(n: AmlName) -> Nat: 206 B.len.fast(nm.enc(n)) 207 208 # Decoding (list layer) 209 210 type AmlSegL is Data: 211 AmlSegL{seg: B.Octets, rest: List<&2, U32>} 212 213 type AmlSegsL is Data: 214 AmlSegsL{segs: List<&2, B.Octets>, rest: List<&2, U32>} 215 216 def nm.seg.pick(ok: Bool, c0: U32, c1: U32, c2: U32, c3: U32, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegL>: 217 match ok: 218 case True{}: 219 Done{AmlSegL{B.Octets.of_list([c0, c1, c2, c3]), t}} 220 case False{}: 221 Fail{E.AcpiAmlBadName{}} 222 223 def nm.seg(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegL>: 224 match xs: 225 case Con{+c0, Con{+c1, Con{+c2, Con{+c3, t}}}}: 226 nm.seg.pick(nm.seg_ok4(c0, c1, c2, c3), c0, c1, c2, c3, t) 227 case _: 228 Fail{E.AcpiAmlTruncated{}} 229 230 def nm.cons(s: B.Octets, r: Result<&2, &2, E.AcpiError, AmlSegsL>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 231 match r: 232 case Fail{e}: 233 Fail{e} 234 case Done{AmlSegsL{ss, rest}}: 235 Done{AmlSegsL{Con{s, ss}, rest}} 236 237 # the segment in r, then p more 238 def nm.segs.go(p: Nat, r: Result<&2, &2, E.AcpiError, AmlSegL>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 239 match p: 240 case 0n: 241 match r: 242 case Fail{e}: 243 Fail{e} 244 case Done{AmlSegL{s, rest}}: 245 Done{AmlSegsL{[s], rest}} 246 case 1n+q: 247 match r: 248 case Fail{e}: 249 Fail{e} 250 case Done{AmlSegL{s, rest}}: 251 nm.cons(s, nm.segs.go(q, nm.seg(rest))) 252 253 # n segments 254 def nm.segs(n: Nat, xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 255 match n: 256 case 0n: 257 Done{AmlSegsL{Nil{}, xs}} 258 case 1n+p: 259 nm.segs.go(p, nm.seg(xs)) 260 261 def nm.multi.k(zero: Bool, n: Nat, r: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 262 match zero: 263 case True{}: 264 Fail{E.AcpiAmlBadName{}} 265 case False{}: 266 nm.segs(n, r) 267 268 def nm.multi(t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 269 match t: 270 case Nil{}: 271 Fail{E.AcpiAmlTruncated{}} 272 case Con{c, r}: 273 +n = U32.to_nat(c) 274 nm.multi.k(Nat.is_eq(n, 0n), n, r) 275 276 def nm.path.k(k: AmlLeadKind, c: U32, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 277 match k: 278 case AmlLNull{}: 279 Done{AmlSegsL{Nil{}, t}} 280 case AmlLDual{}: 281 nm.segs(2n, t) 282 case AmlLMulti{}: 283 nm.multi(t) 284 case AmlLSeg{}: 285 nm.segs(1n, Con{c, t}) 286 case _: 287 Fail{E.AcpiAmlBadName{}} 288 289 def nm.dpath(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlSegsL>: 290 match xs: 291 case Nil{}: 292 Fail{E.AcpiAmlTruncated{}} 293 case Con{+c, t}: 294 nm.path.k(AmlLead.classify(c), c, t) 295 296 def nm.named(root: Bool, up: Nat, r: Result<&2, &2, E.AcpiError, AmlSegsL>) -> Result<&2, &2, E.AcpiError, AmlNameL>: 297 match r: 298 case Fail{e}: 299 Fail{e} 300 case Done{AmlSegsL{ss, rest}}: 301 Done{AmlNameL{AmlName{root, up, ss}, rest}} 302 303 def nm.up1(r: Result<&2, &2, E.AcpiError, AmlNameL>) -> Result<&2, &2, E.AcpiError, AmlNameL>: 304 match r: 305 case Fail{e}: 306 Fail{e} 307 case Done{AmlNameL{AmlName{root, up, ss}, rest}}: 308 Done{AmlNameL{AmlName{root, 1n+up, ss}, rest}} 309 310 def nm.head_kind(xs: List<&2, U32>) -> AmlLeadKind: 311 match xs: 312 case Nil{}: 313 AmlLOther{} 314 case Con{+c, t}: 315 AmlLead.classify(c) 316 317 # parent prefixes, then a path; k is the kind of the first byte 318 def nm.ups(xs: List<&2, U32>, k: AmlLeadKind) -> Result<&2, &2, E.AcpiError, AmlNameL>: 319 match xs: 320 case Nil{}: 321 Fail{E.AcpiAmlTruncated{}} 322 case Con{c, +t}: 323 match k: 324 case AmlLParent{}: 325 nm.up1(nm.ups(t, nm.head_kind(t))) 326 case _: 327 nm.named(False{}, 0n, nm.path.k(k, c, t)) 328 329 def nm.dec.k(k: AmlLeadKind, c: U32, t: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlNameL>: 330 match k: 331 case AmlLRoot{}: 332 nm.named(True{}, 0n, nm.dpath(t)) 333 case _: 334 nm.ups(Con{c, t}, k) 335 336 # the NameString at the front of a list of bytes 337 def nm.dec(xs: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlNameL>: 338 match xs: 339 case Nil{}: 340 Fail{E.AcpiAmlTruncated{}} 341 case Con{+c, t}: 342 nm.dec.k(AmlLead.classify(c), c, t) 343 344 def nm.pub(r: Result<&2, &2, E.AcpiError, AmlNameL>) -> Result<&2, &2, E.AcpiError, AmlNameParsed>: 345 match r: 346 case Fail{e}: 347 Fail{e} 348 case Done{AmlNameL{n, rest}}: 349 Done{AmlNameParsed{n, B.Octets.of_list(rest)}} 350 351 # the NameString at the front of o, and what follows it 352 def AmlName.decode(o: B.Octets) -> Result<&2, &2, E.AcpiError, AmlNameParsed>: 353 nm.pub(nm.dec(B.Octets.to_list(o))) 354 355 # Text: "\_SB_.PCI0", "^^_STA", and the null name "" (segments in full) 356 357 def nm.show.segs(ss: List<&2, B.Octets>, first: Bool) -> String: 358 match ss: 359 case Nil{}: 360 "" 361 case Con{s, t}: 362 match first: 363 case True{}: 364 B.Octets.to_string(s) ++ nm.show.segs(t, False{}) 365 case False{}: 366 "." ++ B.Octets.to_string(s) ++ nm.show.segs(t, False{}) 367 368 def nm.show.pre(root: Bool, up: Nat) -> String: 369 match root: 370 case True{}: 371 "\\" 372 case False{}: 373 String.repeat("^", up) 374 375 def AmlName.show(n: AmlName) -> String: 376 match n: 377 case AmlName{r, u, ss}: 378 nm.show.pre(r, u) ++ nm.show.segs(ss, True{}) 379 380 # a segment from text: its first four characters, padded with '_' as ASL 381 # does ("_SB" is "_SB_") 382 def AmlName.seg(s: String) -> B.Octets: 383 +o = B.Octets.take(4n, B.Octets.of_string(s)) 384 B.Octets.append(o, B.Octets.of_string(String.repeat("_", Nat.sub(4n, B.Octets.len(o))))) 385 386 def nm.text.segs(ps: List<&2, String>) -> List<&2, B.Octets>: 387 match ps: 388 case Nil{}: 389 Nil{} 390 case Con{p, t}: 391 Con{AmlName.seg(p), nm.text.segs(t)} 392 393 def nm.text.split.pick(e: Bool, +s: String) -> List<&2, B.Octets>: 394 match e: 395 case True{}: 396 Nil{} 397 case False{}: 398 nm.text.segs(String.split(s, '.')) 399 400 def nm.text.split(+s: String) -> List<&2, B.Octets>: 401 nm.text.split.pick(String.is_empty(s), s) 402 403 # leading carets, counted; isc: s starts with one 404 def nm.text.ups(s: String, isc: Bool, n: Nat) -> AmlName: 405 match s: 406 case SNil{}: 407 AmlName{False{}, n, Nil{}} 408 case SCon{h, +t}: 409 match isc: 410 case True{}: 411 nm.text.ups(t, String.starts_with(t, "^"), 1n+n) 412 case False{}: 413 AmlName{False{}, n, nm.text.split(SCon{h, t})} 414 415 def nm.text.root(r: Bool, +s: String) -> AmlName: 416 match r: 417 case True{}: 418 AmlName{True{}, 0n, nm.text.split(String.drop(s, 1n))} 419 case False{}: 420 nm.text.ups(s, String.starts_with(s, "^"), 0n) 421 422 # a name from its text: "\_SB.PCI0" (in Bend source), "^^_STA", "LNKA"; 423 # segments are separated by '.', each padded to four characters with '_' 424 def AmlName.of_text(+s: String) -> AmlName: 425 nm.text.root(String.starts_with(s, "\\"), s)