1 # bend-osdev-bpf: classic BPF instructions, raw and decoded. 2 # 3 # A classic BPF program is a list of struct sock_filter {code: u16, jt: u8, 4 # jf: u8, k: u32} (the BSD bpf(4) manual page; McCanne and Jacobson, "The BSD 5 # Packet Filter", USENIX 1993). BpfRaw is that struct, field for field. BpfOp 6 # is the same instruction decoded into what it does, one constructor per 7 # instruction and addressing mode, so code that builds or inspects a program 8 # never handles opcode bits. 9 # 10 # The opcode is class | size | mode for loads, class | op | source for ALU 11 # and jumps, class | rval for returns: 12 # class LD 0, LDX 1, ST 2, STX 3, ALU 4, JMP 5, RET 6, MISC 7 13 # size W 0x00, H 0x08, B 0x10 14 # mode IMM 0x00, ABS 0x20, IND 0x40, MEM 0x60, LEN 0x80, MSH 0xa0 15 # ALU ADD 0x00, SUB 0x10, MUL 0x20, DIV 0x30, OR 0x40, AND 0x50, 16 # LSH 0x60, RSH 0x70, NEG 0x80, MOD 0x90, XOR 0xa0 17 # JMP JA 0x00, JEQ 0x10, JGT 0x20, JGE 0x30, JSET 0x40 18 # source K 0x00, X 0x08; rval K 0x00, A 0x10; MISC TAX 0x00, TXA 0x80 19 import Base 20 import bend-osdev-bytes@0.1.0.0/bytes.bend as B 21 22 # Instructions 23 24 type BpfSize is Data: 25 BpfW{} 26 BpfH{} 27 BpfB{} 28 29 type BpfAluOp is Data: 30 BpfAdd{} 31 BpfSub{} 32 BpfMul{} 33 BpfDiv{} 34 BpfOr{} 35 BpfAnd{} 36 BpfLsh{} 37 BpfRsh{} 38 BpfMod{} 39 BpfXor{} 40 41 type BpfCond is Data: 42 BpfJeq{} 43 BpfJgt{} 44 BpfJge{} 45 BpfJset{} 46 47 # the second operand of an ALU or jump instruction: the constant k, or X 48 type BpfSrc is Data: 49 BpfK{k: U32} 50 BpfX{} 51 52 # what a return instruction answers: the constant k, or A 53 type BpfRval is Data: 54 BpfRetK{k: U32} 55 BpfRetA{} 56 57 # A decoded instruction. Jump offsets count the instructions skipped: a jump 58 # at index i by n goes to index i + 1 + n, so jumps only move forward. 59 type BpfOp is Data: 60 BpfLdAbs{size: BpfSize, k: U32} 61 BpfLdInd{size: BpfSize, k: U32} 62 BpfLdImm{k: U32} 63 BpfLdLen{} 64 BpfLdMem{k: U32} 65 BpfLdxImm{k: U32} 66 BpfLdxMem{k: U32} 67 BpfLdxLen{} 68 BpfLdxMsh{k: U32} 69 BpfSt{k: U32} 70 BpfStx{k: U32} 71 BpfAlu{op: BpfAluOp, src: BpfSrc} 72 BpfNeg{} 73 BpfJa{k: U32} 74 BpfJmp{cond: BpfCond, src: BpfSrc, jt: U32, jf: U32} 75 BpfRet{rval: BpfRval} 76 BpfTax{} 77 BpfTxa{} 78 79 # struct sock_filter; code is 16 bits and jt, jf are 8 bits when stored 80 type BpfRaw is Data: 81 BpfRaw{code: U32, jt: U32, jf: U32, k: U32} 82 83 # the byte order of a stored program, and of a filter's loads 84 type BpfOrder is Data: 85 BpfBig{} 86 BpfLittle{} 87 88 # Every failure: decoding (BadCode, Truncated, StoredTooLong), validation 89 # (Empty to SeccompInsn), installing seccomp filters (PathTooLong), and 90 # running a program that was not validated (FellOff, BadScratch). 91 type BpfError is Data: 92 BpfErrBadCode{pc: Nat, code: U32} 93 BpfErrTruncated{len: Nat} 94 BpfErrStoredTooLong{max: Nat} 95 BpfErrEmpty{} 96 BpfErrTooLong{len: Nat} 97 BpfErrJump{pc: Nat} 98 BpfErrJumpField{pc: Nat} 99 BpfErrNoReturn{pc: Nat} 100 BpfErrScratch{pc: Nat} 101 BpfErrDivZero{pc: Nat} 102 BpfErrMemInit{pc: Nat} 103 BpfErrSeccompLoad{pc: Nat} 104 BpfErrSeccompInsn{pc: Nat} 105 BpfErrPathTooLong{total: Nat} 106 BpfErrFellOff{} 107 BpfErrBadScratch{k: U32} 108 109 # BPF_MEMWORDS: the scratch memory is M[0] to M[15] 110 def bpf_memwords() -> U32: 111 16 112 113 # The C macros BPF_STMT(code, k) and BPF_JUMP(code, k, jt, jf) 114 115 def bpf_stmt(code: U32, k: U32) -> BpfRaw: 116 BpfRaw{code, 0, 0, k} 117 118 def bpf_jump(code: U32, k: U32, jt: U32, jf: U32) -> BpfRaw: 119 BpfRaw{code, jt, jf, k} 120 121 def BpfRaw.code(r: BpfRaw) -> U32: 122 match r: 123 case BpfRaw{code, jt, jf, k}: 124 code 125 126 # Encoding 127 128 def BpfSize.bits(s: BpfSize) -> U32: 129 match s: 130 case BpfW{}: 131 0 132 case BpfH{}: 133 8 134 case BpfB{}: 135 16 136 137 def BpfAluOp.bits(o: BpfAluOp) -> U32: 138 match o: 139 case BpfAdd{}: 140 0 141 case BpfSub{}: 142 16 143 case BpfMul{}: 144 32 145 case BpfDiv{}: 146 48 147 case BpfOr{}: 148 64 149 case BpfAnd{}: 150 80 151 case BpfLsh{}: 152 96 153 case BpfRsh{}: 154 112 155 case BpfMod{}: 156 144 157 case BpfXor{}: 158 160 159 160 def BpfCond.bits(c: BpfCond) -> U32: 161 match c: 162 case BpfJeq{}: 163 16 164 case BpfJgt{}: 165 32 166 case BpfJge{}: 167 48 168 case BpfJset{}: 169 64 170 171 def BpfSrc.bits(s: BpfSrc) -> U32: 172 match s: 173 case BpfK{k}: 174 0 175 case BpfX{}: 176 8 177 178 def BpfSrc.k(s: BpfSrc) -> U32: 179 match s: 180 case BpfK{k}: 181 k 182 case BpfX{}: 183 0 184 185 def BpfRval.encode(r: BpfRval) -> BpfRaw: 186 match r: 187 case BpfRetK{k}: 188 BpfRaw{6, 0, 0, k} 189 case BpfRetA{}: 190 BpfRaw{22, 0, 0, 0} 191 192 # the sock_filter of an instruction; unused fields are 0 193 def BpfOp.encode(op: BpfOp) -> BpfRaw: 194 match op: 195 case BpfLdAbs{size, k}: 196 BpfRaw{U32.or(32, BpfSize.bits(size)), 0, 0, k} 197 case BpfLdInd{size, k}: 198 BpfRaw{U32.or(64, BpfSize.bits(size)), 0, 0, k} 199 case BpfLdImm{k}: 200 BpfRaw{0, 0, 0, k} 201 case BpfLdLen{}: 202 BpfRaw{128, 0, 0, 0} 203 case BpfLdMem{k}: 204 BpfRaw{96, 0, 0, k} 205 case BpfLdxImm{k}: 206 BpfRaw{1, 0, 0, k} 207 case BpfLdxMem{k}: 208 BpfRaw{97, 0, 0, k} 209 case BpfLdxLen{}: 210 BpfRaw{129, 0, 0, 0} 211 case BpfLdxMsh{k}: 212 BpfRaw{177, 0, 0, k} 213 case BpfSt{k}: 214 BpfRaw{2, 0, 0, k} 215 case BpfStx{k}: 216 BpfRaw{3, 0, 0, k} 217 case BpfAlu{o, +src}: 218 BpfRaw{U32.or(4, U32.or(BpfAluOp.bits(o), BpfSrc.bits(src))), 0, 0, BpfSrc.k(src)} 219 case BpfNeg{}: 220 BpfRaw{132, 0, 0, 0} 221 case BpfJa{k}: 222 BpfRaw{5, 0, 0, k} 223 case BpfJmp{c, +src, jt, jf}: 224 BpfRaw{U32.or(5, U32.or(BpfCond.bits(c), BpfSrc.bits(src))), jt, jf, BpfSrc.k(src)} 225 case BpfRet{r}: 226 BpfRval.encode(r) 227 case BpfTax{}: 228 BpfRaw{7, 0, 0, 0} 229 case BpfTxa{}: 230 BpfRaw{135, 0, 0, 0} 231 232 # Decoding: every opcode classic BPF defines, and nothing else 233 234 def BpfRaw.decode.pick(hit: Bool, op: BpfOp, rest: Maybe<&2, BpfOp>) -> Maybe<&2, BpfOp>: 235 match hit: 236 case True{}: 237 Some{op} 238 case False{}: 239 rest 240 241 # the instruction a sock_filter holds, or None for an opcode classic BPF does 242 # not define; fields the instruction does not use are ignored 243 def BpfRaw.decode(r: BpfRaw) -> Maybe<&2, BpfOp>: 244 match r: 245 case BpfRaw{+code, +jt, +jf, +k}: 246 BpfRaw.decode.pick(U32.is_eq(code, 32), BpfLdAbs{BpfW{}, k}, 247 BpfRaw.decode.pick(U32.is_eq(code, 40), BpfLdAbs{BpfH{}, k}, 248 BpfRaw.decode.pick(U32.is_eq(code, 48), BpfLdAbs{BpfB{}, k}, 249 BpfRaw.decode.pick(U32.is_eq(code, 64), BpfLdInd{BpfW{}, k}, 250 BpfRaw.decode.pick(U32.is_eq(code, 72), BpfLdInd{BpfH{}, k}, 251 BpfRaw.decode.pick(U32.is_eq(code, 80), BpfLdInd{BpfB{}, k}, 252 BpfRaw.decode.pick(U32.is_eq(code, 0), BpfLdImm{k}, 253 BpfRaw.decode.pick(U32.is_eq(code, 128), BpfLdLen{}, 254 BpfRaw.decode.pick(U32.is_eq(code, 96), BpfLdMem{k}, 255 BpfRaw.decode.pick(U32.is_eq(code, 1), BpfLdxImm{k}, 256 BpfRaw.decode.pick(U32.is_eq(code, 97), BpfLdxMem{k}, 257 BpfRaw.decode.pick(U32.is_eq(code, 129), BpfLdxLen{}, 258 BpfRaw.decode.pick(U32.is_eq(code, 177), BpfLdxMsh{k}, 259 BpfRaw.decode.pick(U32.is_eq(code, 2), BpfSt{k}, 260 BpfRaw.decode.pick(U32.is_eq(code, 3), BpfStx{k}, 261 BpfRaw.decode.pick(U32.is_eq(code, 4), BpfAlu{BpfAdd{}, BpfK{k}}, 262 BpfRaw.decode.pick(U32.is_eq(code, 12), BpfAlu{BpfAdd{}, BpfX{}}, 263 BpfRaw.decode.pick(U32.is_eq(code, 20), BpfAlu{BpfSub{}, BpfK{k}}, 264 BpfRaw.decode.pick(U32.is_eq(code, 28), BpfAlu{BpfSub{}, BpfX{}}, 265 BpfRaw.decode.pick(U32.is_eq(code, 36), BpfAlu{BpfMul{}, BpfK{k}}, 266 BpfRaw.decode.pick(U32.is_eq(code, 44), BpfAlu{BpfMul{}, BpfX{}}, 267 BpfRaw.decode.pick(U32.is_eq(code, 52), BpfAlu{BpfDiv{}, BpfK{k}}, 268 BpfRaw.decode.pick(U32.is_eq(code, 60), BpfAlu{BpfDiv{}, BpfX{}}, 269 BpfRaw.decode.pick(U32.is_eq(code, 68), BpfAlu{BpfOr{}, BpfK{k}}, 270 BpfRaw.decode.pick(U32.is_eq(code, 76), BpfAlu{BpfOr{}, BpfX{}}, 271 BpfRaw.decode.pick(U32.is_eq(code, 84), BpfAlu{BpfAnd{}, BpfK{k}}, 272 BpfRaw.decode.pick(U32.is_eq(code, 92), BpfAlu{BpfAnd{}, BpfX{}}, 273 BpfRaw.decode.pick(U32.is_eq(code, 100), BpfAlu{BpfLsh{}, BpfK{k}}, 274 BpfRaw.decode.pick(U32.is_eq(code, 108), BpfAlu{BpfLsh{}, BpfX{}}, 275 BpfRaw.decode.pick(U32.is_eq(code, 116), BpfAlu{BpfRsh{}, BpfK{k}}, 276 BpfRaw.decode.pick(U32.is_eq(code, 124), BpfAlu{BpfRsh{}, BpfX{}}, 277 BpfRaw.decode.pick(U32.is_eq(code, 148), BpfAlu{BpfMod{}, BpfK{k}}, 278 BpfRaw.decode.pick(U32.is_eq(code, 156), BpfAlu{BpfMod{}, BpfX{}}, 279 BpfRaw.decode.pick(U32.is_eq(code, 164), BpfAlu{BpfXor{}, BpfK{k}}, 280 BpfRaw.decode.pick(U32.is_eq(code, 172), BpfAlu{BpfXor{}, BpfX{}}, 281 BpfRaw.decode.pick(U32.is_eq(code, 132), BpfNeg{}, 282 BpfRaw.decode.pick(U32.is_eq(code, 5), BpfJa{k}, 283 BpfRaw.decode.pick(U32.is_eq(code, 21), BpfJmp{BpfJeq{}, BpfK{k}, jt, jf}, 284 BpfRaw.decode.pick(U32.is_eq(code, 29), BpfJmp{BpfJeq{}, BpfX{}, jt, jf}, 285 BpfRaw.decode.pick(U32.is_eq(code, 37), BpfJmp{BpfJgt{}, BpfK{k}, jt, jf}, 286 BpfRaw.decode.pick(U32.is_eq(code, 45), BpfJmp{BpfJgt{}, BpfX{}, jt, jf}, 287 BpfRaw.decode.pick(U32.is_eq(code, 53), BpfJmp{BpfJge{}, BpfK{k}, jt, jf}, 288 BpfRaw.decode.pick(U32.is_eq(code, 61), BpfJmp{BpfJge{}, BpfX{}, jt, jf}, 289 BpfRaw.decode.pick(U32.is_eq(code, 69), BpfJmp{BpfJset{}, BpfK{k}, jt, jf}, 290 BpfRaw.decode.pick(U32.is_eq(code, 77), BpfJmp{BpfJset{}, BpfX{}, jt, jf}, 291 BpfRaw.decode.pick(U32.is_eq(code, 6), BpfRet{BpfRetK{k}}, 292 BpfRaw.decode.pick(U32.is_eq(code, 22), BpfRet{BpfRetA{}}, 293 BpfRaw.decode.pick(U32.is_eq(code, 7), BpfTax{}, 294 BpfRaw.decode.pick(U32.is_eq(code, 135), BpfTxa{}, 295 None{}))))))))))))))))))))))))))))))))))))))))))))))))) 296 # Programs. Each program-wide loop is a tail call over an accumulator, 297 # reversed at the end, so a program of any length runs on both lanes. The 298 # structural forms (*.ref) are the references the proofs reason about; 299 # PROOF.bend proves each equal to its tail form for every input (F_encode, 300 # F_decode). 301 302 def bpf_encode.ref(ops: List<&2, BpfOp>) -> List<&2, BpfRaw>: 303 match ops: 304 case Nil{}: 305 Nil{} 306 case Con{op, t}: 307 Con{BpfOp.encode(op), bpf_encode.ref(t)} 308 309 # the encoded instructions, last first, onto acc 310 def bpf_encode.go(ops: List<&2, BpfOp>, acc: List<&2, BpfRaw>) -> List<&2, BpfRaw>: 311 match ops: 312 case Nil{}: 313 acc 314 case Con{op, t}: 315 bpf_encode.go(t, Con{BpfOp.encode(op), acc}) 316 317 def bpf_encode(ops: List<&2, BpfOp>) -> List<&2, BpfRaw>: 318 List.reverse(&2, BpfRaw, bpf_encode.go(ops, Nil{})) 319 320 def bpf_decode.cons(m: Maybe<&2, BpfOp>, e: BpfError, rest: Result<&2, &2, BpfError, List<&2, BpfOp>>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>: 321 match m: 322 case None{}: 323 Fail{e} 324 case Some{op}: 325 match rest: 326 case Fail{f}: 327 Fail{f} 328 case Done{ops}: 329 Done{Con{op, ops}} 330 331 def bpf_decode.ref.go(rs: List<&2, BpfRaw>, +pc: Nat) -> Result<&2, &2, BpfError, List<&2, BpfOp>>: 332 match rs: 333 case Nil{}: 334 Done{Nil{}} 335 case Con{+r, t}: 336 bpf_decode.cons(BpfRaw.decode(r), BpfErrBadCode{pc, BpfRaw.code(r)}, bpf_decode.ref.go(t, 1n+pc)) 337 338 def bpf_decode.ref(rs: List<&2, BpfRaw>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>: 339 bpf_decode.ref.go(rs, 0n) 340 341 # one decoded instruction pushed onto the instructions so far (last first) 342 def bpf_decode.push(m: Maybe<&2, BpfOp>, e: BpfError, acc: List<&2, BpfOp>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>: 343 match m: 344 case None{}: 345 Fail{e} 346 case Some{op}: 347 Done{Con{op, acc}} 348 349 # a: the instructions before pc, last first, or the first failure; the loop 350 # stops at the instruction after a failure 351 def bpf_decode.go(rs: List<&2, BpfRaw>, +pc: Nat, a: Result<&2, &2, BpfError, List<&2, BpfOp>>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>: 352 match rs: 353 case Nil{}: 354 match a: 355 case Fail{e}: 356 Fail{e} 357 case Done{acc}: 358 Done{List.reverse(&2, BpfOp, acc)} 359 case Con{+r, t}: 360 match a: 361 case Fail{e}: 362 Fail{e} 363 case Done{acc}: 364 bpf_decode.go(t, 1n+pc, bpf_decode.push(BpfRaw.decode(r), BpfErrBadCode{pc, BpfRaw.code(r)}, acc)) 365 366 # every instruction decoded, or the first one that is not classic BPF 367 def bpf_decode(rs: List<&2, BpfRaw>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>: 368 bpf_decode.go(rs, 0n, Done{Nil{}}) 369 370 # Stored programs: 8 bytes per instruction, in the given byte order 371 372 def BpfRaw.to_octets(order: BpfOrder, r: BpfRaw) -> B.Octets: 373 match order: 374 case BpfLittle{}: 375 match r: 376 case BpfRaw{code, jt, jf, k}: 377 B.Octets.concat([B.Octets.le16(code), B.Octets.of_list([jt, jf]), B.Octets.le32(k)]) 378 case BpfBig{}: 379 match r: 380 case BpfRaw{code, jt, jf, k}: 381 B.Octets.concat([B.Octets.be16(code), B.Octets.of_list([jt, jf]), B.Octets.be32(k)]) 382 383 # each instruction's 8 bytes, last first, onto acc 384 def bpf_to_octets.go(rs: List<&2, BpfRaw>, +order: BpfOrder, acc: List<&2, B.Octets>) -> List<&2, B.Octets>: 385 match rs: 386 case Nil{}: 387 acc 388 case Con{r, t}: 389 bpf_to_octets.go(t, order, Con{BpfRaw.to_octets(order, r), acc}) 390 391 def bpf_to_octets(+order: BpfOrder, rs: List<&2, BpfRaw>) -> B.Octets: 392 B.Octets.concat(List.reverse(&2, B.Octets, bpf_to_octets.go(rs, order, Nil{}))) 393 394 def bpf_field(m: Maybe<&2, U32>) -> U32: 395 Maybe.default(&2, U32, m, 0) 396 397 def BpfRaw.of_octets(order: BpfOrder, +o: B.Octets) -> BpfRaw: 398 match order: 399 case BpfLittle{}: 400 BpfRaw{bpf_field(B.Octets.le16_at(o, 0n)), bpf_field(B.Octets.at(o, 2n)), bpf_field(B.Octets.at(o, 3n)), bpf_field(B.Octets.le32_at(o, 4n))} 401 case BpfBig{}: 402 BpfRaw{bpf_field(B.Octets.be16_at(o, 0n)), bpf_field(B.Octets.at(o, 2n)), bpf_field(B.Octets.at(o, 3n)), bpf_field(B.Octets.be32_at(o, 4n))} 403 404 # the next n instructions, onto acc (last first), then all of them in order 405 def bpf_of_octets.go(n: Nat, +order: BpfOrder, +o: B.Octets, acc: List<&2, BpfRaw>) -> List<&2, BpfRaw>: 406 match n: 407 case 0n: 408 List.reverse(&2, BpfRaw, acc) 409 case 1n+p: 410 bpf_of_octets.go(p, order, B.Octets.drop(8n, o), Con{BpfRaw.of_octets(order, B.Octets.take(8n, o)), acc}) 411 412 def bpf_of_octets.rem(r: Nat, q: Nat, +order: BpfOrder, +o: B.Octets, +len: Nat) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>: 413 match r: 414 case 0n: 415 Done{bpf_of_octets.go(q, order, o, Nil{})} 416 case 1n+p: 417 Fail{BpfErrTruncated{len}} 418 419 def bpf_of_octets.fin(+order: BpfOrder, +o: B.Octets, +len: Nat, qr: Nat & Nat) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>: 420 (q, r) = qr 421 bpf_of_octets.rem(r, q, order, o, len) 422 423 # over: the input's byte at offset max, if it has one 424 def bpf_of_octets.fits(over: Maybe<&2, U32>, max: Nat, +order: BpfOrder, +o: B.Octets) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>: 425 match over: 426 case Some{b}: 427 Fail{BpfErrStoredTooLong{max}} 428 case None{}: 429 +len = B.Octets.len(o) 430 bpf_of_octets.fin(order, o, len, Nat.divmod(len, 8n)) 431 432 # 8 * BPF_MAXINSNS: the bytes of the longest program validation accepts by 433 # default (LAWS.bend: octets_max_default ties it to bpf_maxinsns) 434 def bpf_octets_max() -> Nat: 435 32768n 436 437 # a stored program's instructions: at most max bytes, a multiple of 8. The 438 # limit is checked first, by looking for the byte at offset max, so a longer 439 # input costs max steps whatever its length 440 def bpf_of_octets_with(+max: Nat, +order: BpfOrder, +o: B.Octets) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>: 441 bpf_of_octets.fits(B.Octets.at(o, max), max, order, o) 442 443 # the same, with the default limit, bpf_octets_max() 444 def bpf_of_octets(+order: BpfOrder, o: B.Octets) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>: 445 bpf_of_octets_with(bpf_octets_max(), order, o) 446 447 # Text 448 449 def BpfError.show(e: BpfError) -> String: 450 match e: 451 case BpfErrBadCode{pc, code}: 452 "bad opcode " ++ U32.show(code) ++ " at " ++ Nat.show(pc) 453 case BpfErrTruncated{len}: 454 "truncated program of " ++ Nat.show(len) ++ " bytes" 455 case BpfErrStoredTooLong{max}: 456 "stored program over " ++ Nat.show(max) ++ " bytes" 457 case BpfErrEmpty{}: 458 "empty program" 459 case BpfErrTooLong{len}: 460 "program too long: " ++ Nat.show(len) 461 case BpfErrJump{pc}: 462 "jump out of range at " ++ Nat.show(pc) 463 case BpfErrJumpField{pc}: 464 "jump offset over 255 at " ++ Nat.show(pc) 465 case BpfErrNoReturn{pc}: 466 "no return after " ++ Nat.show(pc) 467 case BpfErrScratch{pc}: 468 "scratch index out of range at " ++ Nat.show(pc) 469 case BpfErrDivZero{pc}: 470 "division by constant zero at " ++ Nat.show(pc) 471 case BpfErrMemInit{pc}: 472 "scratch read before write at " ++ Nat.show(pc) 473 case BpfErrSeccompLoad{pc}: 474 "load not allowed in seccomp at " ++ Nat.show(pc) 475 case BpfErrSeccompInsn{pc}: 476 "instruction not allowed in seccomp at " ++ Nat.show(pc) 477 case BpfErrPathTooLong{total}: 478 "seccomp filters too long: " ++ Nat.show(total) 479 case BpfErrFellOff{}: 480 "ran past the end" 481 case BpfErrBadScratch{k}: 482 "scratch index " ++ U32.show(k)