Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > linux.kernel > #1660678 > unrolled thread

Re: [RFC PATCH net-next 3/5] bpf/verifier: feed pointer-to-unknown-scalar casts into scalar ALU path

Back to article view | Back to linux.kernel

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Alexei Starovoitov <alexei.starovoitov@gmail.com> - 2017-06-08 04:40 +0200
    Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Edward Cree <ecree@solarflare.com> - 2017-06-08 17:30 +0200
      Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Alexei Starovoitov <alexei.starovoitov@gmail.com> - 2017-06-08 19:00 +0200
        Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Edward Cree <ecree@solarflare.com> - 2017-06-08 19:20 +0200
          Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Alexei Starovoitov <alexei.starovoitov@gmail.com> - 2017-06-08 20:50 +0200
            Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Edward Cree <ecree@solarflare.com> - 2017-06-08 21:10 +0200
              Re: [RFC PATCH net-next 3/5] bpf/verifier: feed  pointer-to-unknown-scalar casts into scalar ALU path Alexei Starovoitov <alexei.starovoitov@gmail.com> - 2017-06-08 23:20 +0200

#1660678 — Re: [RFC PATCH net-next 3/5] bpf/verifier: feed pointer-to-unknown-scalar casts into scalar ALU path

On Wed, Jun 07, 2017 at 03:58:50PM +0100, Edward Cree wrote:
> If pointer leaks are allowed, and adjust_ptr_min_max_vals returns -EACCES,
>  treat the pointer as an unknown scalar and try again, because we might be
>  able to conclude something about the result (e.g. pointer & 0x40 is either
>  0 or 0x40).
> 
> Signed-off-by: Edward Cree <ecree@solarflare.com>
> ---
>  kernel/bpf/verifier.c | 244 ++++++++++++++++++++++++++------------------------
>  1 file changed, 127 insertions(+), 117 deletions(-)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index dd06e4e..1ff5b5d 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -1566,6 +1566,8 @@ static void coerce_reg_to_32(struct bpf_reg_state *reg)
>  /* Handles arithmetic on a pointer and a scalar: computes new min/max and align.
>   * Caller must check_reg_overflow all argument regs beforehand.
>   * Caller should also handle BPF_MOV case separately.
> + * If we return -EACCES, caller may want to try again treating pointer as a
> + * scalar.  So we only emit a diagnostic if !env->allow_ptr_leaks.
>   */
>  static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
>  				   struct bpf_insn *insn,
> @@ -1588,43 +1590,29 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
>  
>  	if (BPF_CLASS(insn->code) != BPF_ALU64) {
>  		/* 32-bit ALU ops on pointers produce (meaningless) scalars */
> -		if (!env->allow_ptr_leaks) {
> +		if (!env->allow_ptr_leaks)
>  			verbose("R%d 32-bit pointer arithmetic prohibited\n",
>  				dst);
> -			return -EACCES;
> -		}
> -		__mark_reg_unknown(dst_reg);
> -		/* High bits are known zero */
> -		dst_reg->align.mask = (u32)-1;
> -		return 0;
> +		return -EACCES;
>  	}
>  
>  	if (ptr_reg->type == PTR_TO_MAP_VALUE_OR_NULL) {
> -		if (!env->allow_ptr_leaks) {
> +		if (!env->allow_ptr_leaks)
>  			verbose("R%d pointer arithmetic on PTR_TO_MAP_VALUE_OR_NULL prohibited, null-check it first\n",
>  				dst);
> -			return -EACCES;
> -		}
> -		__mark_reg_unknown(dst_reg);
> -		return 0;
> +		return -EACCES;
>  	}
>  	if (ptr_reg->type == CONST_PTR_TO_MAP) {
> -		if (!env->allow_ptr_leaks) {
> +		if (!env->allow_ptr_leaks)
>  			verbose("R%d pointer arithmetic on CONST_PTR_TO_MAP prohibited\n",
>  				dst);
> -			return -EACCES;
> -		}
> -		__mark_reg_unknown(dst_reg);
> -		return 0;
> +		return -EACCES;
>  	}
>  	if (ptr_reg->type == PTR_TO_PACKET_END) {
> -		if (!env->allow_ptr_leaks) {
> +		if (!env->allow_ptr_leaks)
>  			verbose("R%d pointer arithmetic on PTR_TO_PACKET_END prohibited\n",
>  				dst);
> -			return -EACCES;
> -		}
> -		__mark_reg_unknown(dst_reg);
> -		return 0;
> +		return -EACCES;
>  	}
>  
>  	/* In case of 'scalar += pointer', dst_reg inherits pointer type and id.
> @@ -1648,8 +1636,9 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
>  			break;
>  		}
>  		if (max_val == BPF_REGISTER_MAX_RANGE) {
> -			verbose("R%d tried to add unbounded value to pointer\n",
> -				dst);
> +			if (!env->allow_ptr_leaks)
> +				verbose("R%d tried to add unbounded value to pointer\n",
> +					dst);
>  			return -EACCES;
>  		}
>  		/* A new variable offset is created.  Note that off_reg->off
> @@ -1676,28 +1665,20 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
>  	case BPF_SUB:
>  		if (dst_reg == off_reg) {
>  			/* scalar -= pointer.  Creates an unknown scalar */
> -			if (!env->allow_ptr_leaks) {
> +			if (!env->allow_ptr_leaks)
>  				verbose("R%d tried to subtract pointer from scalar\n",
>  					dst);
> -				return -EACCES;
> -			}
> -			/* Make it an unknown scalar */
> -			__mark_reg_unknown(dst_reg);
> -			break;
> +			return -EACCES;
>  		}
>  		/* We don't allow subtraction from FP, because (according to
>  		 * test_verifier.c test "invalid fp arithmetic", JITs might not
>  		 * be able to deal with it.
>  		 */
>  		if (ptr_reg->type == PTR_TO_STACK) {
> -			if (!env->allow_ptr_leaks) {
> +			if (!env->allow_ptr_leaks)
>  				verbose("R%d subtraction from stack pointer prohibited\n",
>  					dst);
> -				return -EACCES;
> -			}
> -			/* Make it an unknown scalar */
> -			__mark_reg_unknown(dst_reg);
> -			break;
> +			return -EACCES;
>  		}
>  		if (known && (ptr_reg->off - min_val ==
>  			      (s64)(s32)(ptr_reg->off - min_val))) {
> @@ -1713,14 +1694,10 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
>  		 * This can happen if off_reg is an immediate.
>  		 */
>  		if ((s64)max_val < 0) {
> -			if (!env->allow_ptr_leaks) {
> +			if (!env->allow_ptr_leaks)
>  				verbose("R%d tried to subtract negative max_val %lld from pointer\n",
>  					dst, (s64)max_val);
> -				return -EACCES;
> -			}
> -			/* Make it an unknown scalar */
> -			__mark_reg_unknown(dst_reg);
> -			break;
> +			return -EACCES;
>  		}
>  		/* A new variable offset is created.  If the subtrahend is known
>  		 * nonnegative, then any reg->range we had before is still good.
> @@ -1747,99 +1724,37 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
>  		 * (However, in principle we could allow some cases, e.g.
>  		 * ptr &= ~3 which would reduce min_value by 3.)
>  		 */
> -		if (!env->allow_ptr_leaks) {
> +		if (!env->allow_ptr_leaks)
>  			verbose("R%d bitwise operator %s on pointer prohibited\n",
>  				dst, bpf_alu_string[opcode >> 4]);
> -			return -EACCES;
> -		}
> -		/* Make it an unknown scalar */
> -		__mark_reg_unknown(dst_reg);
> +		return -EACCES;
>  	default:
>  		/* other operators (e.g. MUL,LSH) produce non-pointer results */
> -		if (!env->allow_ptr_leaks) {
> +		if (!env->allow_ptr_leaks)
>  			verbose("R%d pointer arithmetic with %s operator prohibited\n",
>  				dst, bpf_alu_string[opcode >> 4]);
> -			return -EACCES;
> -		}
> -		/* Make it an unknown scalar */
> -		__mark_reg_unknown(dst_reg);
> +		return -EACCES;
>  	}
>  
>  	check_reg_overflow(dst_reg);
>  	return 0;
>  }
>  
> -/* Handles ALU ops other than BPF_END, BPF_NEG and BPF_MOV: computes new min/max
> - * and align.
> - * TODO: check this is legit for ALU32, particularly around negatives
> - */
> -static int adjust_reg_min_max_vals(struct bpf_verifier_env *env,
> -				   struct bpf_insn *insn)
> +static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
> +				      struct bpf_insn *insn,
> +				      struct bpf_reg_state *dst_reg,
> +				      struct bpf_reg_state *src_reg)
>  {
> -	struct bpf_reg_state *regs = env->cur_state.regs, *dst_reg, *src_reg;
> -	struct bpf_reg_state *ptr_reg = NULL, off_reg = {0};
> +	struct bpf_reg_state *regs = env->cur_state.regs;
>  	s64 min_val = BPF_REGISTER_MIN_RANGE;
>  	u64 max_val = BPF_REGISTER_MAX_RANGE;
>  	u8 opcode = BPF_OP(insn->code);
>  	bool src_known, dst_known;
>  
> -	dst_reg = &regs[insn->dst_reg];
> -	check_reg_overflow(dst_reg);
> -	src_reg = NULL;
> -	if (dst_reg->type != SCALAR_VALUE)
> -		ptr_reg = dst_reg;
> -	if (BPF_SRC(insn->code) == BPF_X) {
> -		src_reg = &regs[insn->src_reg];
> -		check_reg_overflow(src_reg);
> -
> -		if (src_reg->type != SCALAR_VALUE) {
> -			if (dst_reg->type != SCALAR_VALUE) {
> -				/* Combining two pointers by any ALU op yields
> -				 * an arbitrary scalar.
> -				 */
> -				if (!env->allow_ptr_leaks) {
> -					verbose("R%d pointer %s pointer prohibited\n",
> -						insn->dst_reg,
> -						bpf_alu_string[opcode >> 4]);
> -					return -EACCES;
> -				}
> -				mark_reg_unknown(regs, insn->dst_reg);
> -				return 0;
> -			} else {
> -				/* scalar += pointer
> -				 * This is legal, but we have to reverse our
> -				 * src/dest handling in computing the range
> -				 */
> -				return adjust_ptr_min_max_vals(env, insn,
> -							       src_reg, dst_reg);
> -			}
> -		} else if (ptr_reg) {
> -			/* pointer += scalar */
> -			return adjust_ptr_min_max_vals(env, insn,
> -						       dst_reg, src_reg);
> -		}
> -	} else {
> -		/* Pretend the src is a reg with a known value, since we only
> -		 * need to be able to read from this state.
> -		 */
> -		off_reg.type = SCALAR_VALUE;
> -		off_reg.align = tn_const(insn->imm);
> -		off_reg.min_value = insn->imm;
> -		off_reg.max_value = insn->imm;
> -		src_reg = &off_reg;
> -		if (ptr_reg) /* pointer += K */
> -			return adjust_ptr_min_max_vals(env, insn,
> -						       ptr_reg, src_reg);
> -	}
> -
> -	/* Got here implies adding two SCALAR_VALUEs */
> -	if (WARN_ON_ONCE(ptr_reg)) {
> -		verbose("verifier internal error\n");
> -		return -EINVAL;
> -	}
> -	if (WARN_ON(!src_reg)) {
> -		verbose("verifier internal error\n");
> -		return -EINVAL;

such large back and forth move doesn't help reviewing.
may be just merge it into previous patch?
Or keep that function in the right place in patch 2 already?

[toc] | [next] | [standalone]

#1661389

On 08/06/17 03:35, Alexei Starovoitov wrote:
> such large back and forth move doesn't help reviewing.
> may be just merge it into previous patch?
> Or keep that function in the right place in patch 2 already?
I think 'diff' got a bit confused, and maybe with different options I could
 have got it to produce something more readable.  But I think I will just
 merge this into patch 2; it's only separate because it started out as an
 experiment.

-Ed

[toc] | [prev] | [next] | [standalone]

#1661493

On Thu, Jun 08, 2017 at 04:25:39PM +0100, Edward Cree wrote:
> On 08/06/17 03:35, Alexei Starovoitov wrote:
> > such large back and forth move doesn't help reviewing.
> > may be just merge it into previous patch?
> > Or keep that function in the right place in patch 2 already?
> I think 'diff' got a bit confused, and maybe with different options I could
>  have got it to produce something more readable.  But I think I will just
>  merge this into patch 2; it's only separate because it started out as an
>  experiment.

after sleeping on it I'm not sure we should be allowing such pointer
arithmetic. In normal C code people do fancy tricks with lower 3 bits
of the pointer, but in bpf code I cannot see such use case.
What kind of realistic code will be doing ptr & 0x40 ?

[toc] | [prev] | [next] | [standalone]

#1661504

On 08/06/17 17:50, Alexei Starovoitov wrote:
> On Thu, Jun 08, 2017 at 04:25:39PM +0100, Edward Cree wrote:
>> On 08/06/17 03:35, Alexei Starovoitov wrote:
>>> such large back and forth move doesn't help reviewing.
>>> may be just merge it into previous patch?
>>> Or keep that function in the right place in patch 2 already?
>> I think 'diff' got a bit confused, and maybe with different options I could
>>  have got it to produce something more readable.  But I think I will just
>>  merge this into patch 2; it's only separate because it started out as an
>>  experiment.
> after sleeping on it I'm not sure we should be allowing such pointer
> arithmetic. In normal C code people do fancy tricks with lower 3 bits
> of the pointer, but in bpf code I cannot see such use case.
> What kind of realistic code will be doing ptr & 0x40 ?
Well, I didn't support it because I saw a use case.  I supported it because
 it seemed easy to do and the code came out reasonably elegant-looking.
Since this is guarded by env->allow_ptr_leaks, I can't see any reason _not_
 to let people try fancy tricks with the low bits of pointers.
I agree ptr & 0x40 is a crazy thing with no imaginable use case, but...
"Unix was not designed to stop its users from doing stupid things, as that
 would also stop them from doing clever things." ;-)

-Ed

[toc] | [prev] | [next] | [standalone]

#1661579

On Thu, Jun 08, 2017 at 06:12:39PM +0100, Edward Cree wrote:
> On 08/06/17 17:50, Alexei Starovoitov wrote:
> > On Thu, Jun 08, 2017 at 04:25:39PM +0100, Edward Cree wrote:
> >> On 08/06/17 03:35, Alexei Starovoitov wrote:
> >>> such large back and forth move doesn't help reviewing.
> >>> may be just merge it into previous patch?
> >>> Or keep that function in the right place in patch 2 already?
> >> I think 'diff' got a bit confused, and maybe with different options I could
> >>  have got it to produce something more readable.  But I think I will just
> >>  merge this into patch 2; it's only separate because it started out as an
> >>  experiment.
> > after sleeping on it I'm not sure we should be allowing such pointer
> > arithmetic. In normal C code people do fancy tricks with lower 3 bits
> > of the pointer, but in bpf code I cannot see such use case.
> > What kind of realistic code will be doing ptr & 0x40 ?
> Well, I didn't support it because I saw a use case.  I supported it because
>  it seemed easy to do and the code came out reasonably elegant-looking.
> Since this is guarded by env->allow_ptr_leaks, I can't see any reason _not_
>  to let people try fancy tricks with the low bits of pointers.
> I agree ptr & 0x40 is a crazy thing with no imaginable use case, but...
> "Unix was not designed to stop its users from doing stupid things, as that
>  would also stop them from doing clever things." ;-)

well, I agree with the philosophy :) but I also see few reasons not to allow it:
1. it immediately becomes uapi and if later we find out that it's preventing us
to do something we actually really need we'll be stuck looking for workaround
2. it's the same pruning concern. probably doesn't fully apply here, but
the reason we don't track 'if (reg == 1) ...' is if we mark that
register as known const_imm in the true branch, it will screw up
pruning quite badly. It's trivial to track and may seem useful,
but hurts instead.

[toc] | [prev] | [next] | [standalone]

#1661598

On 08/06/17 19:41, Alexei Starovoitov wrote:
> On Thu, Jun 08, 2017 at 06:12:39PM +0100, Edward Cree wrote:
>> On 08/06/17 17:50, Alexei Starovoitov wrote:
>>> On Thu, Jun 08, 2017 at 04:25:39PM +0100, Edward Cree wrote:
>>>> On 08/06/17 03:35, Alexei Starovoitov wrote:
>>>>> such large back and forth move doesn't help reviewing.
>>>>> may be just merge it into previous patch?
>>>>> Or keep that function in the right place in patch 2 already?
>>>> I think 'diff' got a bit confused, and maybe with different options I could
>>>>  have got it to produce something more readable.  But I think I will just
>>>>  merge this into patch 2; it's only separate because it started out as an
>>>>  experiment.
>>> after sleeping on it I'm not sure we should be allowing such pointer
>>> arithmetic. In normal C code people do fancy tricks with lower 3 bits
>>> of the pointer, but in bpf code I cannot see such use case.
>>> What kind of realistic code will be doing ptr & 0x40 ?
>> Well, I didn't support it because I saw a use case.  I supported it because
>>  it seemed easy to do and the code came out reasonably elegant-looking.
>> Since this is guarded by env->allow_ptr_leaks, I can't see any reason _not_
>>  to let people try fancy tricks with the low bits of pointers.
>> I agree ptr & 0x40 is a crazy thing with no imaginable use case, but...
>> "Unix was not designed to stop its users from doing stupid things, as that
>>  would also stop them from doing clever things." ;-)
> well, I agree with the philosophy :) but I also see few reasons not to allow it:
> 1. it immediately becomes uapi and if later we find out that it's preventing us
> to do something we actually really need we'll be stuck looking for workaround
What could it prevent us from doing, though?  It's basically equivalent to giving
 BPF an opcode that casts a pointer to a u64, which of course is only allowed if
 allow_ptr_leaks is true.  And since we don't feed any knowledge about the pointer
 into the verifier, it's just like any other way of filling a register with
 arbitrary, unknown bits.
I can fully appreciate why you're being cautious, what with uapi and all.  But I
 don't think there's any actual problem here.  Open to being convinced, though.
> 2. it's the same pruning concern. probably doesn't fully apply here, but
> the reason we don't track 'if (reg == 1) ...'
Don't we though?
http://elixir.free-electrons.com/linux/v4.12-rc4/source/kernel/bpf/verifier.c#L2127
> is if we mark that
> register as known const_imm in the true branch, it will screw up
> pruning quite badly. It's trivial to track and may seem useful,
> but hurts instead.
(Thinking out loud...)

What would be really nice is a way to propagate limits backwards as well as
 forwards, so that the verifier can say "when I tested this branch, I used
 this part of the state, I read four bytes past this pointer".  Then when it
 wants to prune, it can say "well, the state this time isn't as strong, but
 it still satisfies everything I actually used".
But that sounds like it would be very hard indeed to do.

Maybe with the basic-block DAG stuff David's been talking about, we could
 find all the paths that reach a block, and take the union of their states,
 and then run through the block feeding it that combined state.  But that
 could reject code that relies on correlation of the state (i.e. if r1 != 0
 then r2 is valid ptr I can access, etc) so would still need the 'walk with
 each individual state' as a fallback.  Though at least you'd have all the
 states at once so you could find out which ones were subsumed, instead of
 hoping you get to them in the right order.

-Ed

[toc] | [prev] | [next] | [standalone]

#1661701

On Thu, Jun 08, 2017 at 08:07:53PM +0100, Edward Cree wrote:
> On 08/06/17 19:41, Alexei Starovoitov wrote:
> > On Thu, Jun 08, 2017 at 06:12:39PM +0100, Edward Cree wrote:
> >> On 08/06/17 17:50, Alexei Starovoitov wrote:
> >>> On Thu, Jun 08, 2017 at 04:25:39PM +0100, Edward Cree wrote:
> >>>> On 08/06/17 03:35, Alexei Starovoitov wrote:
> >>>>> such large back and forth move doesn't help reviewing.
> >>>>> may be just merge it into previous patch?
> >>>>> Or keep that function in the right place in patch 2 already?
> >>>> I think 'diff' got a bit confused, and maybe with different options I could
> >>>>  have got it to produce something more readable.  But I think I will just
> >>>>  merge this into patch 2; it's only separate because it started out as an
> >>>>  experiment.
> >>> after sleeping on it I'm not sure we should be allowing such pointer
> >>> arithmetic. In normal C code people do fancy tricks with lower 3 bits
> >>> of the pointer, but in bpf code I cannot see such use case.
> >>> What kind of realistic code will be doing ptr & 0x40 ?
> >> Well, I didn't support it because I saw a use case.  I supported it because
> >>  it seemed easy to do and the code came out reasonably elegant-looking.
> >> Since this is guarded by env->allow_ptr_leaks, I can't see any reason _not_
> >>  to let people try fancy tricks with the low bits of pointers.
> >> I agree ptr & 0x40 is a crazy thing with no imaginable use case, but...
> >> "Unix was not designed to stop its users from doing stupid things, as that
> >>  would also stop them from doing clever things." ;-)
> > well, I agree with the philosophy :) but I also see few reasons not to allow it:
> > 1. it immediately becomes uapi and if later we find out that it's preventing us
> > to do something we actually really need we'll be stuck looking for workaround
> What could it prevent us from doing, though?  It's basically equivalent to giving
>  BPF an opcode that casts a pointer to a u64, which of course is only allowed if
>  allow_ptr_leaks is true.  And since we don't feed any knowledge about the pointer
>  into the verifier, it's just like any other way of filling a register with
>  arbitrary, unknown bits.
> I can fully appreciate why you're being cautious, what with uapi and all.  But I
>  don't think there's any actual problem here.  Open to being convinced, though.

The leaking is not a concern. It's if we started accepting a certain
class of programs we need to keep accepting them in the future.
Another reason is 'ptr & mask' could have been simply a bug and rejecting it
suppose to help users find issues sooner...
but I don't have a strong opinion here.

> > 2. it's the same pruning concern. probably doesn't fully apply here, but
> > the reason we don't track 'if (reg == 1) ...'
> Don't we though?
> http://elixir.free-electrons.com/linux/v4.12-rc4/source/kernel/bpf/verifier.c#L2127
> > is if we mark that
> > register as known const_imm in the true branch, it will screw up
> > pruning quite badly. It's trivial to track and may seem useful,
> > but hurts instead.
> (Thinking out loud...)
> 
> What would be really nice is a way to propagate limits backwards as well as
>  forwards, so that the verifier can say "when I tested this branch, I used
>  this part of the state, I read four bytes past this pointer".  Then when it
>  wants to prune, it can say "well, the state this time isn't as strong, but
>  it still satisfies everything I actually used".
> But that sounds like it would be very hard indeed to do.

that's more or less what i'm trying to do. liveness info per basic block
will trim the state.

> Maybe with the basic-block DAG stuff David's been talking about, we could
>  find all the paths that reach a block, and take the union of their states,
>  and then run through the block feeding it that combined state.  But that
>  could reject code that relies on correlation of the state (i.e. if r1 != 0
>  then r2 is valid ptr I can access, etc) so would still need the 'walk with
>  each individual state' as a fallback.  Though at least you'd have all the
>  states at once so you could find out which ones were subsumed, instead of
>  hoping you get to them in the right order.

I think it's important to optimize verification speed for good programs.
If bad program takes slightly longer, not a big deal. Right now we have
global lock which needs to go away, but that's a minor fix.
In that sense I see that combining the state can help find bad programs
sooner, but I don't see it's helping good programs.
Also we already have programs like:
if (...) {
  var1 = ptr
  var2 = size
} else {
  var1 = different ptr
  var2 = different size
}
call_helper(...var1, var2)
So the state needs to be considered together. Cannot just mix and match.
Initially I was thinking to build Use/Def chains for all operands
of loads, stores and calls and follow them from Use spot to all Defs
recursively to determine validity, but above use case breaks that.

[toc] | [prev] | [standalone]

Back to top | Article view | linux.kernel

csiph-web