On Sat, Aug 3, 2019 at 8:19 PM Alexei Starovoitov <ast@xxxxxxxxxx> wrote:
>
> Add a test that returns a 'random' number between [0, 2^20)
> If state pruning is not working correctly for loop body the number of
> processed insns will be 2^20 * num_of_insns_in_loop_body and the program
> will be rejected.
>
> Signed-off-by: Alexei Starovoitov <ast@xxxxxxxxxx>
> ---
> .../bpf/prog_tests/bpf_verif_scale.c | 1 +
> tools/testing/selftests/bpf/progs/loop4.c | 23 +++++++++++++++++++
> 2 files changed, 24 insertions(+)
> create mode 100644 tools/testing/selftests/bpf/progs/loop4.c
>
> diff --git a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
> index b4be96162ff4..757e39540eda 100644
> --- a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
> +++ b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
> @@ -71,6 +71,7 @@ void test_bpf_verif_scale(void)
>
> { "loop1.o", BPF_PROG_TYPE_RAW_TRACEPOINT },
> { "loop2.o", BPF_PROG_TYPE_RAW_TRACEPOINT },
> + { "loop4.o", BPF_PROG_TYPE_RAW_TRACEPOINT },
>
> /* partial unroll. 19k insn in a loop.
> * Total program size 20.8k insn.
> diff --git a/tools/testing/selftests/bpf/progs/loop4.c b/tools/testing/selftests/bpf/progs/loop4.c
> new file mode 100644
> index 000000000000..3e7ee14fddbd
> --- /dev/null
> +++ b/tools/testing/selftests/bpf/progs/loop4.c
> @@ -0,0 +1,23 @@
> +// SPDX-License-Identifier: GPL-2.0
> +// Copyright (c) 2019 Facebook
> +#include <linux/sched.h>
> +#include <linux/ptrace.h>
> +#include <stdint.h>
> +#include <stddef.h>
> +#include <stdbool.h>
> +#include <linux/bpf.h>
> +#include "bpf_helpers.h"
> +
> +char _license[] SEC("license") = "GPL";
> +
> +SEC("socket")
> +int combinations(volatile struct __sk_buff* skb)
> +{
> + int ret = 0, i;
> +
> +#pragma nounroll
> + for (i = 0; i < 20; i++)
> + if (skb->len)
> + ret |= 1 << i;
So I think the idea is that because verifier shouldn't know whether
skb->len is zero or not, then you have two outcomes on every iteration
leading to 2^20 states, right?
But I'm afraid that verifier can eventually be smart enough (if it's
not already, btw), to figure out that ret can be either 0 or ((1 <<
21) - 1), actually. If skb->len is put into separate register, then
that register's bounds will be established on first loop iteration as
either == 0 on one branch or (0, inf) on another branch, after which
all subsequent iterations will not branch at all (one or the other
branch will be always taken).
It's also possible that LLVM/Clang is smart enough already to figure
this out on its own and optimize loop into.
if (skb->len) {
for (i = 0; i < 20; i++)
ret |= 1 << i;
}
So two complains:
1. Let's obfuscate this a bit more, e.g., with testing (skb->len &
(1<<i)) instead, so that result really depends on actual length of the
packet.
2. Is it possible to somehow turn off this precision tracking (e.g.,
running not under root, maybe?) and see that this same program fails
in that case? That way we'll know test actually validates what we
think it validates.
Thoughts?
> + return ret;
> +}
> --
> 2.20.0
>
