Bpf.bpf_exec: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/bpf.bend as Bpf
Lines 269-316 of bend-osdev-bpf@0.1.0.0/bpf.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&start_line=269&end_line=316

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I

def bpf_exec(op: I.BpfOp, st: BpfState, +inp: BpfInput) -> BpfStep:
  match op:
    case I.BpfLdAbs{size, k}:
      bpf_step.of(bpf_set_a.m(bpf_load(inp, size, k), st))
    case I.BpfLdInd{size, k}:
      match st:
        case BpfState{a, +x, mem}:
          bpf_step.of(bpf_set_a.m(bpf_load.ind(inp, size, x, k), BpfState{a, x, mem}))
    case I.BpfLdImm{k}:
      BpfNext{0n, bpf_set_a(st, k)}
    case I.BpfLdLen{}:
      BpfNext{0n, bpf_set_a(st, bpf_len(inp))}
    case I.BpfLdMem{+k}:
      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.lda(st, k))
    case I.BpfLdxImm{k}:
      BpfNext{0n, bpf_set_x(st, k)}
    case I.BpfLdxMem{+k}:
      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.ldx(st, k))
    case I.BpfLdxLen{}:
      BpfNext{0n, bpf_set_x(st, bpf_len(inp))}
    case I.BpfLdxMsh{k}:
      bpf_step.of(bpf_set_x.m(bpf_load.msh(inp, k), st))
    case I.BpfSt{+k}:
      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.st(st, k))
    case I.BpfStx{+k}:
      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.stx(st, k))
    case I.BpfAlu{o, src}:
      match st:
        case BpfState{+a, +x, mem}:
          bpf_step.of(bpf_set_a.m(bpf_alu(o, a, bpf_src(src, x)), BpfState{a, x, mem}))
    case I.BpfNeg{}:
      BpfNext{0n, bpf_neg(st)}
    case I.BpfJa{k}:
      BpfNext{U32.to_nat(k), st}
    case I.BpfJmp{c, src, jt, jf}:
      match st:
        case BpfState{+a, +x, mem}:
          BpfNext{bpf_jsel(bpf_test(c, a, bpf_src(src, x)), jt, jf), BpfState{a, x, mem}}
    case I.BpfRet{v}:
      match v:
        case I.BpfRetK{k}:
          BpfStop{k}
        case I.BpfRetA{}:
          BpfStop{bpf_get_a(st)}
    case I.BpfTax{}:
      BpfNext{0n, bpf_tax(st)}
    case I.BpfTxa{}:
      BpfNext{0n, bpf_txa(st)}

Uses (30):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=BpfInput
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=BpfState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=BpfStep
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_alu
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_get_a
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_jsel
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_load
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_load.ind
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_load.msh
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.lda
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.ldx
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.st
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.stx
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_neg
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_scratch
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_set_a
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_set_a.m
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_set_x
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_set_x.m
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_src
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_step.of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_tax
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_test
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_txa
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRval
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_memwords