On Wed, Nov 13, 2019 at 06:30:04PM +0000, Edward Cree wrote:
> > There is also
> > no way to place extern into a section. Currently SEC("..") is a standard way to
> > annotate bpf programs.
> While the symbol itself doesn't have a section, each _use_ of the symbol has a
> reloc, and the SHT_REL[A] in which that reloc resides has a sh_info specifying
> "the section header index of the section to which the relocation applies." So
> can't that be used if symbol visibility needs to depend on section? Tbh I
> can't exactly see why externs need placing in a section in the first place.
I think section for extern can give a scope of search and make libbpf decisions
more predictable? May be we can live without it for now, but we need BTF of
extern symbols. See my example in reply to John.
> > I think we need to be able to specify something like section to
> > extern variables and functions.
> It seems unnecessary to have the user code specify this. Another a bad
> analogy: in userland C code you don't have to annotate the function protos in
> your header files to say whether they come from another .o file, a random
> library or the libc. You just declare "a function called this exists somewhere
> and we'll find it at link time".
yeah. good analogy.
> > I was imagining that the verifier will do per-function verification
> > of program with sub-programs instead of analyzing from root.
> Ah I see. Yes, that's a very attractive design.
>
> If we make it from a sufficiently generic idea of pre/postconditions, then it
> could also be useful for e.g. loop bodies (user-supplied annotations that allow
> us to walk the body only once instead of N times); then a function call just
> gets standard pre/postconditions generated from its argument types if the user
> didn't specify something else.
regarding pre/post conditions.
I think we have them already. These conditions are the function prototypes.
Instead of making the verifier figuring the conditions it's simpler to use
function prototypes instead. If program author is saying that argument to the
function is 'struct xpd_md *' the verifier will check that the function is safe
when such pointer is passed into it. Then to verify the callsite the verifier
only need to check that what is passed into such function matches the type. I
think it's easy to see when such type is context. Like 'struct __sk_buff *'.
But the idea applies to pointer to int too. I believe you were arguing that
instead of tnum_unknown there could be cases with tnum_range(0-2) as
pre-condition is useful. May be. I think it will simplify the verifier logic
quite a bit if we avoid going fine grain.
Say we have a function:
int foo(struct __sk_buff *skb, int arg)
{
if (arg > 2)
return 0;
// do safe stuff with skb depending whether arg is 0, 1, or 2.
}
That first 'if' is enough to turn pre-conditions into 'any skb' and 'any arg'.
That is exactly what BTF says about this function.
