Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/19/17 4:16 PM, David Miller wrote: From: Alexei Starovoitov Date: Fri, 19 May 2017 14:37:56 -0700 On 5/19/17 1:41 PM, David Miller wrote: From: Edward Cree Date: Fri, 19 May 2017 18:17:42 +0100 One question: is there a way to build the verifier as

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

From: Alexei Starovoitov Date: Fri, 19 May 2017 14:37:56 -0700 > On 5/19/17 1:41 PM, David Miller wrote: >> From: Edward Cree >> Date: Fri, 19 May 2017 18:17:42 +0100 >> >>> One question: is there a way to build the verifier as userland code >>> (or at least

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/19/17 1:41 PM, David Miller wrote: From: Edward Cree Date: Fri, 19 May 2017 18:17:42 +0100 One question: is there a way to build the verifier as userland code (or at least as a module), or will I have to reboot every time I want to test a change? There currently

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

From: Edward Cree Date: Fri, 19 May 2017 18:17:42 +0100 > One question: is there a way to build the verifier as userland code > (or at least as a module), or will I have to reboot every time I > want to test a change? There currently is no such machanism, you will have

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 19/05/17 15:55, Alexei Starovoitov wrote: > On 5/19/17 7:21 AM, Edward Cree wrote: >> I'm currently translating the algos to C. But for the kernel patch, >> I'll need to read & understand the existing verifier code, so it >> might take a while :) (I don't suppose there's any design document

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/19/17 7:21 AM, Edward Cree wrote: I'm currently translating the algos to C. But for the kernel patch, I'll need to read & understand the existing verifier code, so it might take a while :) (I don't suppose there's any design document or hacking-notes you could point me at?) Dave just

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 19/05/17 02:22, Alexei Starovoitov wrote: > In your .py I'd only change __str__(self) to print them in mask,value > as the order they're passed into constructor to make it easier to read. Actually I was going to go the other way and change the ctor to take value,mask. But I agree they're

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/18/17 9:38 AM, Edward Cree wrote: On 18/05/17 15:49, Edward Cree wrote: Here's one idea that seemed to work when I did a couple of experiments: let A = (a;am), B = (b;bm) where the m are the masks Σ = am + bm + a + b χ = Σ ^ (a + b) /* unknown carries */ μ = χ | am | bm /* mask of result

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

Implementations (still in Python for now) at https://gist.github.com/ecree-solarflare/0665d5b46c2d8d08de2377fbd527de8d (I left out division, because it's so weak.) I still can't prove + and - are correct, but they've passed every test case I've come up with so far. * seems pretty obviously

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 18/05/17 15:49, Edward Cree wrote: > Here's one idea that seemed to work when I did a couple of experiments: > let A = (a;am), B = (b;bm) where the m are the masks > Σ = am + bm + a + b > χ = Σ ^ (a + b) /* unknown carries */ > μ = χ | am | bm /* mask of result */ > then A + B = ((a + b) & ~μ;

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 18/05/17 03:48, Alexei Starovoitov wrote: > Would it be easier to represent this logic via (mask_of_unknown, value) > instead of (mask0, mask1) ? Yes, I like this. > As far as upper bits we can tweak the algorithm to eat into > one or more bits of known bits due to carry. > Like > 00xx11 +

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 18/05/17 01:16, David Miller wrote: > So, in C, addition (a += b) is something like: > > struct bpf_reg_bits { > u64 zero_bits; > u64 one_bits; > }; > > static void add_update_bits(struct bpf_reg_bits *a, struct bpf_reg_bits *b) > { > u64 m_zeros, m_ones, m_all; > >

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/17/17 8:33 AM, Edward Cree wrote: On 17/05/17 15:00, Edward Cree wrote: OTOH the 'track known 1s as well' might work in a nice generic way and cover all bases, I'll have to experiment a bit with that. -Ed So I did some experiments (in Python, script follows) and found that indeed this

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/17/17 5:16 PM, David Miller wrote: BTW, we track something similar already in reg->imm which tracks how many high order bits are known to be cleared in the register. It is used to avoid potential overflow for packet pointer accesses. I bet we can subsume that into this facility as well.

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

From: Edward Cree Date: Wed, 17 May 2017 16:33:27 +0100 > So I did some experiments (in Python, script follows) and found that > indeed this does appear to work, at least for addition and shifts. > The idea is that we have a 0s mask and a 1s mask; for bits that are >

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

From: Edward Cree Date: Wed, 17 May 2017 18:00:03 +0100 > Did you see the algorithms I posted with two masks? I'll take a look.

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 17/05/17 17:13, David Miller wrote: > Both cases are common in real BPF programs. The offsets really are > necessary. It's funny because initially I tried to implement this > without the auxiliary offset and it simply doesn't work. :-) > > We always have to track when you've seen the offset

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

From: Edward Cree Date: Wed, 17 May 2017 15:00:04 +0100 > On 16/05/17 23:53, Alexei Starovoitov wrote: >> following this line of thinking it feels that it should be possible >> to get rid of 'aux_off' and 'aux_off_align' and simplify the code. >> I mean we can always do >>

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 17/05/17 15:00, Edward Cree wrote: > OTOH the 'track known 1s as well' might work in a nice generic way > and cover all bases, I'll have to experiment a bit with that. > > -Ed So I did some experiments (in Python, script follows) and found that indeed this does appear to work, at least for

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 16/05/17 23:53, Alexei Starovoitov wrote: > following this line of thinking it feels that it should be possible > to get rid of 'aux_off' and 'aux_off_align' and simplify the code. > I mean we can always do > dst_reg->min_align = min(dst_reg->min_align, src_reg->min_align); > > and don't use

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 5/16/17 5:37 AM, Edward Cree wrote: On 15/05/17 17:04, David Miller wrote: If we use 1<<31, then sequences like: R1 = 0 R1 <<= 2 do silly things. Hmm. It might be a bit late for this, but I wonder if, instead of handling alignments as (1 << align), you could store them

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

From: Edward Cree Date: Tue, 16 May 2017 13:37:42 +0100 > On 15/05/17 17:04, David Miller wrote: >> If we use 1<<31, then sequences like: >> >> R1 = 0 >> R1 <<= 2 >> >> do silly things. > Hmm. It might be a bit late for this, but I wonder if, instead of handling

Re: [PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

On 15/05/17 17:04, David Miller wrote: > If we use 1<<31, then sequences like: > > R1 = 0 > R1 <<= 2 > > do silly things. Hmm. It might be a bit late for this, but I wonder if, instead of handling alignments as (1 << align), you could store them as -(1 << align), i.e. leading 1s

[PATCH v2 1/3] bpf: Use 1<<16 as ceiling for immediate alignment in verifier.

If we use 1<<31, then sequences like: R1 = 0 R1 <<= 2 do silly things. Examples of this actually exist in the MAP tests of test_verifier.c Update test_align.c expectation strings. Signed-off-by: David S. Miller --- kernel/bpf/verifier.c