def bpf_check.op

bend-osdev-bpf@0.1.0.0 · validate.bend:80

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

80# the checks of one instruction at index pc, with r instructions after it
81def bpf_check.op(op: I.BpfOp, +pc: Nat, +r: Nat) -> Result<&2, &2, I.BpfError, Unit>:
82  match op:
83    case I.BpfLdMem{k}:
84      bpf_check.mem(k, pc, r)
85    case I.BpfLdxMem{k}:
86      bpf_check.mem(k, pc, r)
87    case I.BpfSt{k}:
88      bpf_check.mem(k, pc, r)
89    case I.BpfStx{k}:
90      bpf_check.mem(k, pc, r)
91    case I.BpfAlu{o, src}:
92      bpf_both(bpf_check.div(o, src, pc), bpf_check.next(pc, r))
93    case I.BpfJa{k}:
94      bpf_chk(Nat.is_lt(U32.to_nat(k), r), I.BpfErrJump{pc})
95    case I.BpfJmp{c, src, jt, jf}:
96      bpf_check.jmp(jt, jf, pc, r)
97    case I.BpfRet{v}:
98      Done{Unit{}}
99    case other:
100      bpf_check.next(pc, r)