[RFC,bpf-next,0/2] propagate nullness information for reg to reg comparisons

Message

Eduard Zingerman Aug. 22, 2022, 9:43 a.m. UTC

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                         |  39 +++-
 .../bpf/verifier/jeq_infer_not_null.c         | 186 ++++++++++++++++++
 2 files changed, 224 insertions(+), 1 deletion(-)
 create mode 100644 tools/testing/selftests/bpf/verifier/jeq_infer_not_null.c

Signed-off-by: Eduard Zingerman <[e-mail]>