Re: [PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[sdf@google.com]

On 01/05, dthaler1968@googlemail.com wrote:
> From: Dave Thaler <dthaler@microsoft.com>

> Fix modulo zero, division by zero, overflow, and underflow.
> Also clarify how a negative immediate value is used in unsigned division

> Signed-off-by: Dave Thaler <dthaler@microsoft.com>

Acked-by: Stanislav Fomichev <sdf@google.com>

With a small note below.

> ---
>   Documentation/bpf/instruction-set.rst | 15 +++++++++++++--
>   1 file changed, 13 insertions(+), 2 deletions(-)

> diff --git a/Documentation/bpf/instruction-set.rst  
> b/Documentation/bpf/instruction-set.rst
> index e672d5ec6cc..2ba7c618f33 100644
> --- a/Documentation/bpf/instruction-set.rst
> +++ b/Documentation/bpf/instruction-set.rst
> @@ -99,19 +99,26 @@ code      value  description
>   BPF_ADD   0x00   dst += src
>   BPF_SUB   0x10   dst -= src
>   BPF_MUL   0x20   dst \*= src
> -BPF_DIV   0x30   dst /= src
> +BPF_DIV   0x30   dst = (src != 0) ? (dst / src) : 0
>   BPF_OR    0x40   dst \|= src
>   BPF_AND   0x50   dst &= src
>   BPF_LSH   0x60   dst <<= src
>   BPF_RSH   0x70   dst >>= src
>   BPF_NEG   0x80   dst = ~src
> -BPF_MOD   0x90   dst %= src
> +BPF_MOD   0x90   dst = (src != 0) ? (dst % src) : dst
>   BPF_XOR   0xa0   dst ^= src
>   BPF_MOV   0xb0   dst = src
>   BPF_ARSH  0xc0   sign extending shift right
>   BPF_END   0xd0   byte swap operations (see `Byte swap instructions`_  
> below)
>   ========  =====   
> ==========================================================

> +Underflow and overflow are allowed during arithmetic operations,
> +meaning the 64-bit or 32-bit value will wrap.  If
> +eBPF program execution would result in division by zero,
> +the destination register is instead set to zero.
> +If execution would result in modulo by zero,
> +the destination register is instead left unchanged.
> +
>   ``BPF_ADD | BPF_X | BPF_ALU`` means::

>     dst_reg = (u32) dst_reg + (u32) src_reg;
> @@ -128,6 +135,10 @@ BPF_END   0xd0   byte swap operations (see `Byte  
> swap instructions`_ below)

>     dst_reg = dst_reg ^ imm32


[..]

> +Also note that the division and modulo operations are unsigned,
> +where 'imm' is first sign extended to 64 bits and then converted
> +to an unsigned 64-bit value.  There are no instructions for
> +signed division or modulo.

Less sure about this part, but it looks to be true at least by looking at
the interpreter which does:

DST = DST / IMM

where:

DST === (u64) regs[insn->dst_reg]
IMM === (s32) insn->imm

(and s32 is sign-expanded to u64 according to C rules)

>   Byte swap instructions
>   ~~~~~~~~~~~~~~~~~~~~~~
> --
> 2.33.4