LAWS.seccomp_example: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/LAWS.bend as LAWS
Lines 252-257 of bend-osdev-bpf@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&start_line=252&end_line=257

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

# seccomp(2), EXAMPLES, install_filter(syscall_nr, t_arch, f_errno) with
# t_arch = AUDIT_ARCH_X86_64, so upper_nr_limit = X32_SYSCALL_BIT - 1: the
# call syscall_nr fails with f_errno, other calls are allowed, and another
# architecture or an x32 call (nr above the limit) kills the process
def seccomp_example(nr: U32, e: U32) -> List<&2, I.BpfOp>:
  [I.BpfLdAbs{I.BpfW{}, 4}, I.BpfJmp{I.BpfJeq{}, I.BpfK{S.seccomp_arch_x86_64()}, 0, 5}, I.BpfLdAbs{I.BpfW{}, 0}, I.BpfJmp{I.BpfJgt{}, I.BpfK{U32.sub(S.seccomp_x32_syscall_bit(), 1)}, 3, 0}, I.BpfJmp{I.BpfJeq{}, I.BpfK{nr}, 0, 1}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompErrno{e})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompAllow{})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompKillProcess{})}}]

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfCond
  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=BpfSize
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfSrc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompAction
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompAction.to_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_arch_x86_64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_x32_syscall_bit