Re: [PATCH bpf-next 1/2] bpf: fix maximum stack depth tracking logic

[Alexei Starovoitov <alexei.starovoitov@gmail.com>]

On Sat, Dec 23, 2017 at 02:38:29AM +0100, Jann Horn wrote:
> On Fri, Dec 22, 2017 at 10:33 PM, Alexei Starovoitov <ast@kernel.org> wrote:
> > instead of computing max stack depth for current call chain only
> > track the maximum possible stack depth of any function at given
> > frame position. Such algorithm is simple and fast, but conservative,
> > since it overestimates amount of stack used. Consider:
> > main() // stack 32
> > {
> >   A();
> >   B();
> > }
> >
> > A(){} // stack 256
> >
> > B()  // stack 64
> > {
> >   A();
> > }
> >
> > since A() is called at frame[1] and frame[2], the algorithm
> > will estimate the max stack depth as 32 + 256 + 256 and will reject
> > such program, though real max is 32 + 64 + 256.
> >
> > Fortunately the algorithm is good enough in practice. The alternative
> > would be to track max stack of every function in the fast pass through
> > the verifier and then do additional CFG walk just to compute max total.
> >
> > Fixes: f4d7e40a5b71 ("bpf: introduce function calls (verification)")
> > Reported-by: Jann Horn <jannh@google.com>
> > Signed-off-by: Alexei Starovoitov <ast@kernel.org>
> 
> Does this work in cases where multiple invocations of a function have
> different stack access patterns because their inputs have different
> bounds?
> 
> Consider this pseudocode example:
> 
> void main(void) {
>   func1(0);
>   func1(1);
>   func2(1);
> }
> void func1(int alloc_or_recurse) {
>   if (alloc_or_recurse) {
>     frame_pointer[-300] = 1;
>   } else {
>     func2(alloc_or_recurse);
>   }
> }
> void func2(int alloc_or_recurse) {
>   if (alloc_or_recurse) {
>     frame_pointer[-300] = 1;
>   }
> }
> 
> AFAICS this will work as follows:
> 
> Call to func1->func2 runs without any stack accesses because the
> verifier can prove that alloc_or_recurse is 0.

argh. right.
I guess that ruins my attemp to do the stack check inline
with the main verifier pass.
Do you see an algorithm that can do it without extra
cfg walk at the end?