public inbox for bpf@vger.kernel.org
 help / color / mirror / Atom feed
From: Andrii Nakryiko <andrii@kernel.org>
To: <bpf@vger.kernel.org>, <ast@kernel.org>, <daniel@iogearbox.net>,
	<martin.lau@kernel.org>
Cc: <andrii@kernel.org>, <kernel-team@meta.com>,
	Shung-Hsi Yu <shung-hsi.yu@suse.com>
Subject: [PATCH v5 bpf-next 03/23] bpf: derive smin/smax from umin/max bounds
Date: Fri, 27 Oct 2023 11:13:26 -0700	[thread overview]
Message-ID: <20231027181346.4019398-4-andrii@kernel.org> (raw)
In-Reply-To: <20231027181346.4019398-1-andrii@kernel.org>

Add smin/smax derivation from appropriate umin/umax values. Previously the
logic was surprisingly asymmetric, trying to derive umin/umax from smin/smax
(if possible), but not trying to do the same in the other direction. A simple
addition to __reg64_deduce_bounds() fixes this.

Added also generic comment about u64/s64 ranges and their relationship.
Hopefully that helps readers to understand all the bounds deductions
a bit better.

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 70 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 857d76694517..bf4193706744 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2358,6 +2358,76 @@ static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
 
 static void __reg64_deduce_bounds(struct bpf_reg_state *reg)
 {
+	/* If u64 range forms a valid s64 range (due to matching sign bit),
+	 * try to learn from that. Let's do a bit of ASCII art to see when
+	 * this is happening. Let's take u64 range first:
+	 *
+	 * 0             0x7fffffffffffffff 0x8000000000000000        U64_MAX
+	 * |-------------------------------|--------------------------------|
+	 *
+	 * Valid u64 range is formed when umin and umax are anywhere in this
+	 * range [0, U64_MAX] and umin <= umax. u64 is simple and
+	 * straightforward. Let's where s64 range maps to this simple [0,
+	 * U64_MAX] range, annotated below the line for comparison:
+	 *
+	 * 0             0x7fffffffffffffff 0x8000000000000000        U64_MAX
+	 * |-------------------------------|--------------------------------|
+	 * 0                        S64_MAX S64_MIN                        -1
+	 *
+	 * So s64 values basically start in the middle and then are contiguous
+	 * to the right of it, wrapping around from -1 to 0, and then
+	 * finishing as S64_MAX (0x7fffffffffffffff) right before S64_MIN.
+	 * We can try drawing more visually continuity of u64 vs s64 values as
+	 * mapped to just actual hex valued range of values.
+	 *
+	 *  u64 start                                               u64 end
+	 *  _______________________________________________________________
+	 * /                                                               \
+	 * 0             0x7fffffffffffffff 0x8000000000000000        U64_MAX
+	 * |-------------------------------|--------------------------------|
+	 * 0                        S64_MAX S64_MIN                        -1
+	 *                                / \
+	 * >------------------------------   ------------------------------->
+	 * s64 continues...        s64 end   s64 start          s64 "midpoint"
+	 *
+	 * What this means is that in general, we can't always derive
+	 * something new about u64 from any random s64 range, and vice versa.
+	 * But we can do that in two particular cases. One is when entire
+	 * u64/s64 range is *entirely* contained within left half of the above
+	 * diagram or when it is *entirely* contained in the right half. I.e.:
+	 *
+	 * |-------------------------------|--------------------------------|
+	 *     ^                   ^            ^                 ^
+	 *     A                   B            C                 D
+	 *
+	 * [A, B] and [C, D] are contained entirely in their respective halves
+	 * and form valid contiguous ranges as both u64 and s64 values. [A, B]
+	 * will be non-negative both as u64 and s64 (and in fact it will be
+	 * identical ranges no matter the signedness). [C, D] treated as s64
+	 * will be a range of negative values, while in u64 it will be
+	 * non-negative range of values larger than 0x8000000000000000.
+	 *
+	 * Now, any other range here can't be represented in both u64 and s64
+	 * simultaneously. E.g., [A, C], [A, D], [B, C], [B, D] are valid
+	 * contiguous u64 ranges, but they are discontinuous in s64. [B, C]
+	 * in s64 would be properly presented as [S64_MIN, C] and [B, S64_MAX],
+	 * for example. Similarly, valid s64 range [D, A] (going from negative
+	 * to positive values), would be two separate [D, U64_MAX] and [0, A]
+	 * ranges as u64. Currently reg_state can't represent two segments per
+	 * numeric domain, so in such situations we can only derive maximal
+	 * possible range ([0, U64_MAX] for u64, and [S64_MIN, S64_MAX) for s64).
+	 *
+	 * So we use these facts to derive umin/umax from smin/smax and vice
+	 * versa only if they stay within the same "half". This is equivalent
+	 * to checking sign bit: lower half will have sign bit as zero, upper
+	 * half have sign bit 1. Below in code we simplify this by just
+	 * casting umin/umax as smin/smax and checking if they form valid
+	 * range, and vice versa. Those are equivalent checks.
+	 */
+	if ((s64)reg->umin_value <= (s64)reg->umax_value) {
+		reg->smin_value = max_t(s64, reg->smin_value, reg->umin_value);
+		reg->smax_value = min_t(s64, reg->smax_value, reg->umax_value);
+	}
 	/* Learn sign from signed bounds.
 	 * If we cannot cross the sign boundary, then signed and unsigned bounds
 	 * are the same, so combine.  This works even in the negative case, e.g.
-- 
2.34.1


  parent reply	other threads:[~2023-10-27 18:16 UTC|newest]

Thread overview: 77+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-10-27 18:13 [PATCH v5 bpf-next 00/23] BPF register bounds logic and testing improvements Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 01/23] selftests/bpf: fix RELEASE=1 build for tc_opts Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 02/23] selftests/bpf: satisfy compiler by having explicit return in btf test Andrii Nakryiko
2023-10-27 18:13 ` Andrii Nakryiko [this message]
2023-10-31 15:37   ` [PATCH v5 bpf-next 03/23] bpf: derive smin/smax from umin/max bounds Eduard Zingerman
2023-10-31 17:30     ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 04/23] bpf: derive smin32/smax32 from umin32/umax32 bounds Andrii Nakryiko
2023-10-31 15:37   ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 05/23] bpf: derive subreg bounds from full bounds when upper 32 bits are constant Andrii Nakryiko
2023-10-31 15:37   ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 06/23] bpf: add special smin32/smax32 derivation from 64-bit bounds Andrii Nakryiko
2023-10-31 15:37   ` Eduard Zingerman
2023-10-31 17:39     ` Andrii Nakryiko
2023-10-31 18:41       ` Alexei Starovoitov
2023-10-31 18:49         ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 07/23] bpf: improve deduction of 64-bit bounds from 32-bit bounds Andrii Nakryiko
2023-10-31 15:37   ` Eduard Zingerman
2023-10-31 20:26   ` Alexei Starovoitov
2023-10-31 20:33     ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 08/23] bpf: try harder to deduce register bounds from different numeric domains Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 09/23] bpf: drop knowledge-losing __reg_combine_{32,64}_into_{64,32} logic Andrii Nakryiko
2023-10-31 15:38   ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 10/23] selftests/bpf: BPF register range bounds tester Andrii Nakryiko
2023-11-08 22:08   ` Eduard Zingerman
2023-11-08 23:23     ` Andrii Nakryiko
2023-11-09  0:30       ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 11/23] bpf: rename is_branch_taken reg arguments to prepare for the second one Andrii Nakryiko
2023-10-30 19:39   ` Alexei Starovoitov
2023-10-31  5:19     ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 12/23] bpf: generalize is_branch_taken() to work with two registers Andrii Nakryiko
2023-10-31 15:38   ` Eduard Zingerman
2023-10-31 17:41     ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 13/23] bpf: move is_branch_taken() down Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 14/23] bpf: generalize is_branch_taken to handle all conditional jumps in one place Andrii Nakryiko
2023-10-31 15:38   ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 15/23] bpf: unify 32-bit and 64-bit is_branch_taken logic Andrii Nakryiko
2023-10-30 19:52   ` Alexei Starovoitov
2023-10-31  5:28     ` Andrii Nakryiko
2023-10-31 17:35   ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 16/23] bpf: prepare reg_set_min_max for second set of registers Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 17/23] bpf: generalize reg_set_min_max() to handle two sets of two registers Andrii Nakryiko
2023-10-31  2:02   ` Alexei Starovoitov
2023-10-31  6:03     ` Andrii Nakryiko
2023-10-31 16:23       ` Alexei Starovoitov
2023-10-31 17:50         ` Andrii Nakryiko
2023-10-31 17:56           ` Andrii Nakryiko
2023-10-31 18:04             ` Alexei Starovoitov
2023-10-31 18:06               ` Andrii Nakryiko
2023-10-31 18:14   ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 18/23] bpf: generalize reg_set_min_max() to handle non-const register comparisons Andrii Nakryiko
2023-10-31 23:25   ` Eduard Zingerman
2023-11-01 16:35     ` Andrii Nakryiko
2023-11-01 17:12       ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 19/23] bpf: generalize is_scalar_branch_taken() logic Andrii Nakryiko
2023-10-31  2:12   ` Alexei Starovoitov
2023-10-31  6:12     ` Andrii Nakryiko
2023-10-31 16:34       ` Alexei Starovoitov
2023-10-31 18:01         ` Andrii Nakryiko
2023-10-31 20:53           ` Andrii Nakryiko
2023-10-31 20:55             ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 20/23] bpf: enhance BPF_JEQ/BPF_JNE is_branch_taken logic Andrii Nakryiko
2023-10-31  2:20   ` Alexei Starovoitov
2023-10-31  6:16     ` Andrii Nakryiko
2023-10-31 16:36       ` Alexei Starovoitov
2023-10-31 18:04         ` Andrii Nakryiko
2023-10-31 18:06           ` Alexei Starovoitov
2023-10-27 18:13 ` [PATCH v5 bpf-next 21/23] selftests/bpf: adjust OP_EQ/OP_NE handling to use subranges for branch taken Andrii Nakryiko
2023-11-08 18:22   ` Eduard Zingerman
2023-11-08 19:59     ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 22/23] selftests/bpf: add range x range test to reg_bounds Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 23/23] selftests/bpf: add iter test requiring range x range logic Andrii Nakryiko
2023-10-30 17:55 ` [PATCH v5 bpf-next 00/23] BPF register bounds logic and testing improvements Alexei Starovoitov
2023-10-31  5:19   ` Andrii Nakryiko
2023-11-01 12:37     ` Paul Chaignon
2023-11-01 17:13       ` Andrii Nakryiko
2023-11-07  6:37         ` Harishankar Vishwanathan
2023-11-07 16:38           ` Paul Chaignon

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20231027181346.4019398-4-andrii@kernel.org \
    --to=andrii@kernel.org \
    --cc=ast@kernel.org \
    --cc=bpf@vger.kernel.org \
    --cc=daniel@iogearbox.net \
    --cc=kernel-team@meta.com \
    --cc=martin.lau@kernel.org \
    --cc=shung-hsi.yu@suse.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox