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

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

[dthaler1968]

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>
---
 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.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4

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

[sdf]

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

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

[Daniel Borkmann]

On 1/5/23 8:01 PM, sdf@google.com wrote:
> 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)

Yeap, the actual operation is in the target width, so for 32 bit it's casted
to u32, e.g. for modulo (note that the verifier rewrites it into `(src != 0) ?
(dst % src) : dst` form, so here is just the extract of the plain mod insn and
it's similar for div):

         ALU64_MOD_X:
                 div64_u64_rem(DST, SRC, &AX);
                 DST = AX;
                 CONT;
         ALU_MOD_X:
                 AX = (u32) DST;
                 DST = do_div(AX, (u32) SRC);
                 CONT;
         ALU64_MOD_K:
                 div64_u64_rem(DST, IMM, &AX);
                 DST = AX;
                 CONT;
         ALU_MOD_K:
                 AX = (u32) DST;
                 DST = do_div(AX, (u32) IMM);
                 CONT;

So in above phrasing the middle part needs to be adapted or just removed.

Thanks,
Daniel

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

[Dave Thaler]

Daniel Borkmann wrote:
[...]
> >> +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)
> 
> Yeap, the actual operation is in the target width, so for 32 bit it's casted to
> u32, e.g. for modulo (note that the verifier rewrites it into `(src != 0) ?
> (dst % src) : dst` form, so here is just the extract of the plain mod insn and it's
> similar for div):
> 
>          ALU64_MOD_X:
>                  div64_u64_rem(DST, SRC, &AX);
>                  DST = AX;
>                  CONT;
>          ALU_MOD_X:
>                  AX = (u32) DST;
>                  DST = do_div(AX, (u32) SRC);
>                  CONT;
>          ALU64_MOD_K:
>                  div64_u64_rem(DST, IMM, &AX);
>                  DST = AX;
>                  CONT;
>          ALU_MOD_K:
>                  AX = (u32) DST;
>                  DST = do_div(AX, (u32) IMM);
>                  CONT;
> 
> So in above phrasing the middle part needs to be adapted or just removed.

The phrasing was based on the earlier discussion on this list (see
https://lore.kernel.org/bpf/CAADnVQJ387tWd7WgxqfoB44xMe17bY0RRp_Sng3xMnKsywFpxg@mail.gmail.com/) where
Alexei wrote "imm32 is _sign_ extended everywhere",
and I cited the div_k tests in lib/test_bpf.c that assume sign extension
not zero extension.

So I don't know how to reconcile your comments with that thread.
If you do, please educate me :)

Dave

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

[Daniel Borkmann]

On 1/6/23 7:11 PM, Dave Thaler wrote:
> Daniel Borkmann wrote:
> [...]
>>>> +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)
>>
>> Yeap, the actual operation is in the target width, so for 32 bit it's casted to
>> u32, e.g. for modulo (note that the verifier rewrites it into `(src != 0) ?
>> (dst % src) : dst` form, so here is just the extract of the plain mod insn and it's
>> similar for div):
>>
>>           ALU64_MOD_X:
>>                   div64_u64_rem(DST, SRC, &AX);
>>                   DST = AX;
>>                   CONT;
>>           ALU_MOD_X:
>>                   AX = (u32) DST;
>>                   DST = do_div(AX, (u32) SRC);
>>                   CONT;
>>           ALU64_MOD_K:
>>                   div64_u64_rem(DST, IMM, &AX);
>>                   DST = AX;
>>                   CONT;
>>           ALU_MOD_K:
>>                   AX = (u32) DST;
>>                   DST = do_div(AX, (u32) IMM);
>>                   CONT;
>>
>> So in above phrasing the middle part needs to be adapted or just removed.
> 
> The phrasing was based on the earlier discussion on this list (see
> https://lore.kernel.org/bpf/CAADnVQJ387tWd7WgxqfoB44xMe17bY0RRp_Sng3xMnKsywFpxg@mail.gmail.com/) where
> Alexei wrote "imm32 is _sign_ extended everywhere",
> and I cited the div_k tests in lib/test_bpf.c that assume sign extension
> not zero extension.

`Where 'imm' is first sign extended to 64 bits and then converted to an unsigned
64-bit value` is true for the 64 bit operation, for the 32-bit it's just converted
to an unsigned 32-bit value, see the (u32)IMM which is (u32)(s32) insn->imm. From
the phrasing, it was a bit less clear perhaps.

Thanks,
Daniel

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

[patchwork-bot+netdevbpf]

Hello:

This patch was applied to bpf/bpf-next.git (master)
by Daniel Borkmann <daniel@iogearbox.net>:

On Tue, 24 Jan 2023 00:12:18 +0000 you 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
> 
> Changes from last submission: addressed comments from Daniel.
> 
> [...]

Here is the summary with links:
  - bpf, docs: Fix modulo zero, division by zero, overflow, and underflow
    https://git.kernel.org/bpf/bpf-next/c/0eb9d19e2201

You are awesome, thank you!
-- 
Deet-doot-dot, I am a bot.
https://korg.docs.kernel.org/patchwork/pwbot.html

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

[dthaler1968]

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

Changes from last submission: addressed comments from Daniel.

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 Documentation/bpf/instruction-set.rst | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
index e672d5ec6cc..a7f4574562c 100644
--- a/Documentation/bpf/instruction-set.rst
+++ b/Documentation/bpf/instruction-set.rst
@@ -99,19 +99,27 @@ 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, for ``BPF_ALU64``
+the value of the destination register is unchanged whereas for
+``BPF_ALU`` the upper 32 bits of the destination register are zeroed.
+
 ``BPF_ADD | BPF_X | BPF_ALU`` means::
 
   dst_reg = (u32) dst_reg + (u32) src_reg;
@@ -128,6 +136,11 @@ 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.
+Thus, for ``BPF_ALU``, 'imm' is first interpreted as an unsigned
+32-bit value, whereas for ``BPF_ALU64``, 'imm' is first sign extended
+to 64 bits and the result interpreted as an unsigned 64-bit value.
+There are no instructions for signed division or modulo.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4

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

[Daniel Borkmann]

On 1/20/23 9:16 PM, dthaler1968@googlemail.com wrote:
[...]
> -BPF_MOD   0x90   dst %= src
> +BPF_MOD   0x90   dst = (src != 0) ? (dst % src) : dst   
[...]
> +If execution would result in modulo by zero,
> +the destination register is instead set to the source register
> +as ``BPF_MOV`` would do, meaning that for ``BPF_ALU64`` the value
> +is unchanged whereas for ``BPF_ALU`` the upper 32 bits are zeroed.

I think the "the destination register is instead set to the source register
as ``BPF_MOV`` would do" is a bit ambiguous. Could we just simplify it to the
following:

If execution would result in modulo by zero, for ``BPF_ALU64`` the value of
the destination register is unchanged whereas for ``BPF_ALU`` the upper 32 bits
of the destination register are zeroed.

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

[dthaler1968]

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

Changes from last submission: addressed comments from Alexei.

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 Documentation/bpf/instruction-set.rst | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
index e672d5ec6cc..2546630fcbd 100644
--- a/Documentation/bpf/instruction-set.rst
+++ b/Documentation/bpf/instruction-set.rst
@@ -99,19 +99,28 @@ 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 set to the source register
+as ``BPF_MOV`` would do, meaning that for ``BPF_ALU64`` the value
+is unchanged whereas for ``BPF_ALU`` the upper 32 bits are zeroed.
+
 ``BPF_ADD | BPF_X | BPF_ALU`` means::
 
   dst_reg = (u32) dst_reg + (u32) src_reg;
@@ -128,6 +137,11 @@ 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.
+Thus, for ``BPF_ALU``, 'imm' is first interpreted as an unsigned
+32-bit value, whereas for ``BPF_ALU64``, 'imm' is first sign extended
+to 64 bits and the result interpreted as an unsigned 64-bit value.
+There are no instructions for signed division or modulo.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4

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

[Alexei Starovoitov]

On Thu, Jan 19, 2023 at 2:25 PM <dthaler1968@googlemail.com> wrote:
> -BPF_MOD   0x90   dst %= src
> +BPF_MOD   0x90   dst = (src != 0) ? (dst % src) : dst

...

> +If execution would result in modulo by zero,
> +the destination register is instead set to the source register
> +as ``BPF_MOV`` would do, meaning that for ``BPF_ALU64`` the value
> +is unchanged whereas for ``BPF_ALU`` the value is truncated to 32 bits.

These two don't match.
Probably should say that for ALU64 dst doesn't change
and for alu32 it's upper 32-bits are zeroed.

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

[dthaler1968]

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

Changes from last submission: addressed comments from Daniel.

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 Documentation/bpf/instruction-set.rst | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
index e672d5ec6cc..dd37cc5c0bf 100644
--- a/Documentation/bpf/instruction-set.rst
+++ b/Documentation/bpf/instruction-set.rst
@@ -99,19 +99,28 @@ 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 set to the source register
+as ``BPF_MOV`` would do, meaning that for ``BPF_ALU64`` the value
+is unchanged whereas for ``BPF_ALU`` the value is truncated to 32 bits.
+
 ``BPF_ADD | BPF_X | BPF_ALU`` means::
 
   dst_reg = (u32) dst_reg + (u32) src_reg;
@@ -128,6 +137,11 @@ 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.
+Thus, for ``BPF_ALU``, 'imm' is first interpreted as an unsigned
+32-bit value, whereas for ``BPF_ALU64``, 'imm' is first sign extended
+to 64 bits and the result interpreted as an unsigned 64-bit value.
+There are no instructions for signed division or modulo.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4

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

[Daniel Borkmann]

On 1/18/23 4:23 PM, 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
> 
> Changes from last submission: addressed conversion comment from
> Jose.
> 
> Signed-off-by: Dave Thaler <dthaler@microsoft.com>
> ---
>   Documentation/bpf/instruction-set.rst | 16 ++++++++++++++--
>   1 file changed, 14 insertions(+), 2 deletions(-)
> 
> diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
> index e672d5ec6cc..f79dae527ad 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.

Looks good to go with one small nit for the previous sentence which could be
misinterpreted. The rewrites from verifier for modulo op are:

       mod32:                            mod64:

       (16) if w0 == 0x0 goto pc+2       (15) if r0 == 0x0 goto pc+1
       (9c) w1 %= w0                     (9f) r1 %= r0
       (05) goto pc+1
       (bc) w1 = w1

So for BPF_ALU as 32-bit op, it is expected that the result is 32-bit
value, too. So for 32-bit op the destination register is truncated to
32-bit value. (Related commit 9b00f1b78809 ("bpf: Fix truncation handling
for mod32 dst reg wrt zero")).

>   ``BPF_ADD | BPF_X | BPF_ALU`` means::
>   
>     dst_reg = (u32) dst_reg + (u32) src_reg;
> @@ -128,6 +135,11 @@ 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.
> +Thus, for `BPF_ALU`, 'imm' is first interpreted as an unsigned
> +32-bit value, whereas for `BPF_ALU64`, 'imm' is first sign extended
> +to 64 bits and the result interpreted as an unsigned 64-bit value.
> +There are no instructions for signed division or modulo.
>   
>   Byte swap instructions
>   ~~~~~~~~~~~~~~~~~~~~~~
> 

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

[dthaler1968]

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

Changes from last submission: addressed conversion comment from
Jose.

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 Documentation/bpf/instruction-set.rst | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
index e672d5ec6cc..f79dae527ad 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,11 @@ 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.
+Thus, for `BPF_ALU`, 'imm' is first interpreted as an unsigned
+32-bit value, whereas for `BPF_ALU64`, 'imm' is first sign extended
+to 64 bits and the result interpreted as an unsigned 64-bit value.
+There are no instructions for signed division or modulo.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4

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

[Jose E. Marchesi]

> +Also note that the division and modulo operations are unsigned.
> +Thus, for `BPF_ALU`, 'imm' is first converted to an unsigned
> +32-bit value, whereas for `BPF_ALU64`, '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.

English is not my native language, but I think "converted" may be too
generic for this paragraph: are the same bits reinterpreted as unsigned?
Or an actual conversion like absolute value is performed?

Wouldn't it be better to say "interpreted as" instead of "converted to"
in this case?

Something like this:

  "Also note that the division and modulo operations are unsigned.
   Thus, for `BPF_ALU`, 'imm' is interpreted as an unsigned 32-bit
   value, whereas for `BPF_ALU64`, 'imm' is first sign extended to 64
   bits and the result interpreted as an unsigned 64-bit value.  There
   are no instructions for signed division or modulo."

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

[dthaler1968]

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

Changes from last submission: addressed 32-bit comments from
Daniel and Stanislav.

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 Documentation/bpf/instruction-set.rst | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
index e672d5ec6cc..fcd4db45717 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,11 @@ 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.
+Thus, for `BPF_ALU`, 'imm' is first converted to an unsigned
+32-bit value, whereas for `BPF_ALU64`, '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.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4