public inbox for bpf@vger.kernel.org
 help / color / mirror / Atom feed
* [PATCH bpf-next 0/2] propagate nullness information for reg to reg comparisons
@ 2022-08-26 17:29 Eduard Zingerman
  2022-08-26 17:29 ` [PATCH bpf-next 1/2] bpf: " Eduard Zingerman
  2022-08-26 17:29 ` [PATCH bpf-next 2/2] selftests/bpf: check nullness propagation " Eduard Zingerman
  0 siblings, 2 replies; 11+ messages in thread
From: Eduard Zingerman @ 2022-08-26 17:29 UTC (permalink / raw)
  To: bpf, ast, andrii, daniel, kernel-team, yhs, john.fastabend
  Cc: Eduard Zingerman

Changes since RFC:
 - newly added if block in `check_cond_jmp_op` is moved down to keep
   `make_ptr_not_null_reg` actions together;
 - tests rewritten to have a single `r0 = 0; exit;` block.

Original message follows:

Hi Everyone,

This patchset adds ability to propagates nullness information for
branches of register to register equality compare instructions. The
following rules are used:
 - suppose register A maybe null
 - suppose register B is not null
 - for JNE A, B, ... - A is not null in the false branch
 - for JEQ A, B, ... - A is not null in the true branch

E.g. for program like below:

  r6 = skb->sk;
  r7 = sk_fullsock(r6);
  r0 = sk_fullsock(r6);
  if (r0 == 0) return 0;    (a)
  if (r0 != r7) return 0;   (b)
  *r7->type;                (c)
  return 0;

It is safe to dereference r7 at point (c), because of (a) and (b).

The utility of this change came up while working on BPF CLang backend
issue [1]. Specifically, while debugging issue with selftest
`test_sk_lookup.c`. This test has the following structure:

    int access_ctx_sk(struct bpf_sk_lookup *ctx __CTX__)
    {
        struct bpf_sock *sk1 = NULL, *sk2 = NULL;
        ...
        sk1 = bpf_map_lookup_elem(&redir_map, &KEY_SERVER_A);
        if (!sk1)           // (a)
            goto out;
        ...
        if (ctx->sk != sk1) // (b)
            goto out;
        ...
        if (ctx->sk->family != AF_INET ||     // (c)
            ctx->sk->type != SOCK_STREAM ||
            ctx->sk->state != BPF_TCP_LISTEN)
            goto out;
            ...
    }

- at (a) `sk1` is checked to be not null;
- at (b) `ctx->sk` is verified to be equal to `sk1`;
- at (c) `ctx->sk` is accessed w/o nullness check.

Currently Global Value Numbering pass considers expressions `sk1` and
`ctx->sk` to be identical at point (c) and replaces `ctx->sk` with
`sk1` (not expressions themselves but corresponding SSA values).
Since `sk1` is known to be not null after (b) verifier allows
execution of the program.

However, such optimization is not guaranteed to happen. When it does
not happen verifier reports an error.

[1] https://reviews.llvm.org/D131633#3722231

Thanks,
Eduard

Eduard Zingerman (2):
  bpf: propagate nullness information for reg to reg comparisons
  selftests/bpf: check nullness propagation for reg to reg comparisons

 kernel/bpf/verifier.c                         |  41 ++++-
 .../bpf/verifier/jeq_infer_not_null.c         | 166 ++++++++++++++++++
 2 files changed, 205 insertions(+), 2 deletions(-)
 create mode 100644 tools/testing/selftests/bpf/verifier/jeq_infer_not_null.c

-- 
2.37.2


^ permalink raw reply	[flat|nested] 11+ messages in thread

end of thread, other threads:[~2022-11-15 20:52 UTC | newest]

Thread overview: 11+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2022-08-26 17:29 [PATCH bpf-next 0/2] propagate nullness information for reg to reg comparisons Eduard Zingerman
2022-08-26 17:29 ` [PATCH bpf-next 1/2] bpf: " Eduard Zingerman
2022-08-29 14:23   ` Daniel Borkmann
2022-08-30 10:41     ` Eduard Zingerman
2022-09-01  8:13       ` Shung-Hsi Yu
2022-09-01  9:01         ` Shung-Hsi Yu
2022-10-27 22:18           ` Eduard Zingerman
2022-08-26 17:29 ` [PATCH bpf-next 2/2] selftests/bpf: check nullness propagation " Eduard Zingerman
2022-11-14 18:01   ` Alexei Starovoitov
2022-11-15 20:31     ` Eduard Zingerman
2022-11-15 20:51       ` Alexei Starovoitov

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox