Re: [RFC bpf-next 04/10] bpf: cfg: detect loop use domination information

[John Fastabend <john.fastabend@gmail.com>]

On 05/07/2018 03:22 AM, Jiong Wang wrote:
> If one bb is dominating its predecessor, then there is loop.
> 
> Signed-off-by: Jiong Wang <jiong.wang@netronome.com>
> ---
>  kernel/bpf/cfg.c      | 22 ++++++++++++++++++++++
>  kernel/bpf/cfg.h      |  1 +
>  kernel/bpf/verifier.c |  8 ++++++++
>  3 files changed, 31 insertions(+)
> 
> diff --git a/kernel/bpf/cfg.c b/kernel/bpf/cfg.c
> index b50937a..90692e4 100644
> --- a/kernel/bpf/cfg.c
> +++ b/kernel/bpf/cfg.c
> @@ -568,6 +568,28 @@ int subprog_build_dom_info(struct bpf_subprog_info *subprog)
>  	return ret;
>  }
>  
> +bool subprog_has_loop(struct bpf_subprog_info *subprog)
> +{
> +	int lane_len = BITS_TO_LONGS(subprog->bb_num - 2);
> +	struct list_head *bb_list = &subprog->bbs;
> +	struct bb_node *bb, *entry_bb;
> +	struct edge_node *e;
> +
> +	entry_bb = entry_bb(bb_list);
> +	bb = bb_next(entry_bb);
> +	list_for_each_entry_from(bb, &exit_bb(bb_list)->l, l)
> +		list_for_each_entry(e, &bb->e_prevs, l) {
> +			struct bb_node *latch = e->src;
> +
> +			if (latch != entry_bb &&
> +			    test_bit(bb->idx,
> +				     subprog->dtree + latch->idx * lane_len))
> +				return true;
> +		}
> +
> +	return false;
> +}
> +

Because we are using this to guard against loops we need to detect
all loops not just reducible loops. And because (assuming my understanding
is correct) Tarjan's algorithm will only detect all loops when the
graph is reducible we need additional tests.

There are a couple options to fix this with varying levels of complexity.
Because I'm using this to build loop info structures to find induction
variables and show termination. After the loop structures are built we
could search for any back-edges not in valid loops. This would be similar
to the existing back-edge detection code but with an extra check to
allow edges that have been validated. I would need to check that this
doesn't have any escapes before actually proposing it though.

The other method would be to properly test for reducibility using one of
the algorithms for this. I think the most intuitive is to remove back-edges
and test the graph is acyclic. This would be run before the dom tree is
built. This is IMO what we should do, it seems the most "correct" way to
do this.

The most complex would be to handle irreducible programs using some of the
more complex methods. I really don't think this is necessary but in theory
at least we could use something like Havlak-Tarjan algorithm and allow
some programs with irreducible loops. This is likely overkill especially
in a first iteration.

Here is a sample that fails without this series, using original back-edge
detection, but is allowed with this patch,

SEC("classifier_tc_mark")
int _tc_mark(struct __sk_buff *ctx)
{
        void *data      = (void *)(unsigned long)ctx->data;
        void *data_end  = (void *)(unsigned long)ctx->data_end;
        void *data_meta = (void *)(unsigned long)ctx->data_meta;
        struct meta_info *meta = data_meta;
        volatile int mark = ctx->mark;

        mark += 1;

        if (meta + 1 > data) {
B:
                mark += 2;

                if (mark < ctx->mark * 3)
                        goto C;
        } else if (meta < data) {
C:
                mark += 1;
                if (mark < 1000)
                        goto  B;
        }

        return TC_ACT_OK;
}

A more concise example could be made but I just hacked on one of the
sample programs. This generates the CFG as follows (I have a patch
on top of your stack to print the CFG and DOM tables)

CFG:  65535[-1,-1] -> 0[0,9]  0[0,9] -> 3[20,20]  0[0,9] -> 1[10,18]  1[10,18] -> 4[21,28]  1[10,18] -> 2[19,19]  2[19,19] -> 5[29,30]  3[20,20] -> 5[29,30]  3[20,20] -> 4[21,28]  4[21,28] -> 1[10,18]  4[21,28] -> 5[29,30]  5[29,30] -> 65534[31,65534] 
DOM:
 1  0  0  0  0  0 
 1  1  0  0  0  0 
 1  1  1  0  0  0 
 1  0  0  1  0  0 
 1  0  0  0  1  0 
 1  0  0  0  0  1 


Here we have the loop 1[10,18]->4[21,28] and the back-edge 4[21,28]->1[10,18].
The notation is #idx[head_insn,tail_insn]. The above can then be imported
into dot notation and graphed if needed.

Jiong, please verify this analysis is correct.

Thanks,
John