[PATCH net][v2] bpf: fix range arithmetic for bpf map access

[PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Josef Bacik]

I made some invalid assumptions with BPF_AND and BPF_MOD that could result in
invalid accesses to bpf map entries.  Fix this up by doing a few things

1) Kill BPF_MOD support.  This doesn't actually get used by the compiler in real
life and just adds extra complexity.

2) Fix the logic for BPF_AND, don't allow AND of negative numbers and set the
minimum value to 0 for positive AND's.

3) Don't do operations on the ranges if they are set to the limits, as they are
by definition undefined, and allowing arithmetic operations on those values
could make them appear valid when they really aren't.

This fixes the testcase provided by Jann as well as a few other theoretical
problems.

Reported-by: Jann Horn <jannh@google.com>
Signed-off-by: Josef Bacik <jbacik@fb.com>
---
V1->V2:
- set the MIN_RANGE to -1 to essentially disable all negative values for the min
  value.
- rebased onto net instead of net-next.

 include/linux/bpf_verifier.h |  5 ++--
 kernel/bpf/verifier.c        | 70 +++++++++++++++++++++++++++++---------------
 2 files changed, 50 insertions(+), 25 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 7035b99..6aaf425 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -14,7 +14,7 @@
   * are obviously wrong for any sort of memory access.
   */
 #define BPF_REGISTER_MAX_RANGE (1024 * 1024 * 1024)
-#define BPF_REGISTER_MIN_RANGE -(1024 * 1024 * 1024)
+#define BPF_REGISTER_MIN_RANGE -1
 
 struct bpf_reg_state {
 	enum bpf_reg_type type;
@@ -22,7 +22,8 @@ struct bpf_reg_state {
 	 * Used to determine if any memory access using this register will
 	 * result in a bad access.
 	 */
-	u64 min_value, max_value;
+	s64 min_value;
+	u64 max_value;
 	union {
 		/* valid when type == CONST_IMM | PTR_TO_STACK | UNKNOWN_VALUE */
 		s64 imm;
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 99a7e5b..6a93615 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -216,8 +216,8 @@ static void print_verifier_state(struct bpf_verifier_state *state)
 				reg->map_ptr->key_size,
 				reg->map_ptr->value_size);
 		if (reg->min_value != BPF_REGISTER_MIN_RANGE)
-			verbose(",min_value=%llu",
-				(unsigned long long)reg->min_value);
+			verbose(",min_value=%lld",
+				(long long)reg->min_value);
 		if (reg->max_value != BPF_REGISTER_MAX_RANGE)
 			verbose(",max_value=%llu",
 				(unsigned long long)reg->max_value);
@@ -758,7 +758,7 @@ static int check_mem_access(struct bpf_verifier_env *env, u32 regno, int off,
 			 * index'es we need to make sure that whatever we use
 			 * will have a set floor within our range.
 			 */
-			if ((s64)reg->min_value < 0) {
+			if (reg->min_value < 0) {
 				verbose("R%d min value is negative, either use unsigned index or do a if (index >=0) check.\n",
 					regno);
 				return -EACCES;
@@ -1468,7 +1468,8 @@ static void check_reg_overflow(struct bpf_reg_state *reg)
 {
 	if (reg->max_value > BPF_REGISTER_MAX_RANGE)
 		reg->max_value = BPF_REGISTER_MAX_RANGE;
-	if ((s64)reg->min_value < BPF_REGISTER_MIN_RANGE)
+	if (reg->min_value < BPF_REGISTER_MIN_RANGE ||
+	    reg->min_value > BPF_REGISTER_MAX_RANGE)
 		reg->min_value = BPF_REGISTER_MIN_RANGE;
 }
 
@@ -1476,7 +1477,8 @@ static void adjust_reg_min_max_vals(struct bpf_verifier_env *env,
 				    struct bpf_insn *insn)
 {
 	struct bpf_reg_state *regs = env->cur_state.regs, *dst_reg;
-	u64 min_val = BPF_REGISTER_MIN_RANGE, max_val = BPF_REGISTER_MAX_RANGE;
+	s64 min_val = BPF_REGISTER_MIN_RANGE;
+	u64 max_val = BPF_REGISTER_MAX_RANGE;
 	bool min_set = false, max_set = false;
 	u8 opcode = BPF_OP(insn->code);
 
@@ -1512,22 +1514,43 @@ static void adjust_reg_min_max_vals(struct bpf_verifier_env *env,
 		return;
 	}
 
+	/* If one of our values was at the end of our ranges then we can't just
+	 * do our normal operations to the register, we need to set the values
+	 * to the min/max since they are undefined.
+	 */
+	if (min_val == BPF_REGISTER_MIN_RANGE)
+		dst_reg->min_value = BPF_REGISTER_MIN_RANGE;
+	if (max_val == BPF_REGISTER_MAX_RANGE)
+		dst_reg->max_value = BPF_REGISTER_MAX_RANGE;
+
 	switch (opcode) {
 	case BPF_ADD:
-		dst_reg->min_value += min_val;
-		dst_reg->max_value += max_val;
+		if (dst_reg->min_value != BPF_REGISTER_MIN_RANGE)
+			dst_reg->min_value += min_val;
+		if (dst_reg->max_value != BPF_REGISTER_MAX_RANGE)
+			dst_reg->max_value += max_val;
 		break;
 	case BPF_SUB:
-		dst_reg->min_value -= min_val;
-		dst_reg->max_value -= max_val;
+		if (dst_reg->min_value != BPF_REGISTER_MIN_RANGE)
+			dst_reg->min_value -= min_val;
+		if (dst_reg->max_value != BPF_REGISTER_MAX_RANGE)
+			dst_reg->max_value -= max_val;
 		break;
 	case BPF_MUL:
-		dst_reg->min_value *= min_val;
-		dst_reg->max_value *= max_val;
+		if (dst_reg->min_value != BPF_REGISTER_MIN_RANGE)
+			dst_reg->min_value *= min_val;
+		if (dst_reg->max_value != BPF_REGISTER_MAX_RANGE)
+			dst_reg->max_value *= max_val;
 		break;
 	case BPF_AND:
-		/* & is special since it could end up with 0 bits set. */
-		dst_reg->min_value &= min_val;
+		/* Disallow AND'ing of negative numbers, ain't nobody got time
+		 * for that.  Otherwise the minimum is 0 and the max is the max
+		 * value we could AND against.
+		 */
+		if (min_val < 0)
+			dst_reg->min_value = BPF_REGISTER_MIN_RANGE;
+		else
+			dst_reg->min_value = 0;
 		dst_reg->max_value = max_val;
 		break;
 	case BPF_LSH:
@@ -1537,24 +1560,25 @@ static void adjust_reg_min_max_vals(struct bpf_verifier_env *env,
 		 */
 		if (min_val > ilog2(BPF_REGISTER_MAX_RANGE))
 			dst_reg->min_value = BPF_REGISTER_MIN_RANGE;
-		else
+		else if (dst_reg->min_value != BPF_REGISTER_MIN_RANGE)
 			dst_reg->min_value <<= min_val;
 
 		if (max_val > ilog2(BPF_REGISTER_MAX_RANGE))
 			dst_reg->max_value = BPF_REGISTER_MAX_RANGE;
-		else
+		else if (dst_reg->max_value != BPF_REGISTER_MAX_RANGE)
 			dst_reg->max_value <<= max_val;
 		break;
 	case BPF_RSH:
-		dst_reg->min_value >>= min_val;
-		dst_reg->max_value >>= max_val;
-		break;
-	case BPF_MOD:
-		/* % is special since it is an unsigned modulus, so the floor
-		 * will always be 0.
+		/* RSH by a negative number is undefined, and the BPF_RSH is an
+		 * unsigned shift, so make the appropriate casts.
 		 */
-		dst_reg->min_value = 0;
-		dst_reg->max_value = max_val - 1;
+		if (min_val < 0 || dst_reg->min_value < 0)
+			dst_reg->min_value = BPF_REGISTER_MIN_RANGE;
+		else
+			dst_reg->min_value =
+				(u64)(dst_reg->min_value) >> min_val;
+		if (dst_reg->max_value != BPF_REGISTER_MAX_RANGE)
+			dst_reg->max_value >>= max_val;
 		break;
 	default:
 		reset_reg_range_values(regs, insn->dst_reg);
-- 
2.5.5

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Alexei Starovoitov]

On Mon, Nov 14, 2016 at 03:45:36PM -0500, Josef Bacik wrote:
> I made some invalid assumptions with BPF_AND and BPF_MOD that could result in
> invalid accesses to bpf map entries.  Fix this up by doing a few things
> 
> 1) Kill BPF_MOD support.  This doesn't actually get used by the compiler in real
> life and just adds extra complexity.
> 
> 2) Fix the logic for BPF_AND, don't allow AND of negative numbers and set the
> minimum value to 0 for positive AND's.
> 
> 3) Don't do operations on the ranges if they are set to the limits, as they are
> by definition undefined, and allowing arithmetic operations on those values
> could make them appear valid when they really aren't.
> 
> This fixes the testcase provided by Jann as well as a few other theoretical
> problems.
> 
> Reported-by: Jann Horn <jannh@google.com>
> Signed-off-by: Josef Bacik <jbacik@fb.com>

lgtm.
Acked-by: Alexei Starovoitov <ast@kernel.org>

Jann, could you please double check the logic.
Thanks!

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Jann Horn]

On Tue, Nov 15, 2016 at 4:10 AM, Alexei Starovoitov
<alexei.starovoitov@gmail.com> wrote:
> On Mon, Nov 14, 2016 at 03:45:36PM -0500, Josef Bacik wrote:
>> I made some invalid assumptions with BPF_AND and BPF_MOD that could result in
>> invalid accesses to bpf map entries.  Fix this up by doing a few things
>>
>> 1) Kill BPF_MOD support.  This doesn't actually get used by the compiler in real
>> life and just adds extra complexity.
>>
>> 2) Fix the logic for BPF_AND, don't allow AND of negative numbers and set the
>> minimum value to 0 for positive AND's.
>>
>> 3) Don't do operations on the ranges if they are set to the limits, as they are
>> by definition undefined, and allowing arithmetic operations on those values
>> could make them appear valid when they really aren't.
>>
>> This fixes the testcase provided by Jann as well as a few other theoretical
>> problems.
>>
>> Reported-by: Jann Horn <jannh@google.com>
>> Signed-off-by: Josef Bacik <jbacik@fb.com>
>
> lgtm.
> Acked-by: Alexei Starovoitov <ast@kernel.org>
>
> Jann, could you please double check the logic.
> Thanks!

I found some more potential issues, maybe Josef and you can tell me whether I
understood these correctly.


/* If the source register is a random pointer then the
* min_value/max_value values represent the range of the known
* accesses into that value, not the actual min/max value of the
* register itself.  In this case we have to reset the reg range
* values so we know it is not safe to look at.
*/
if (regs[insn->src_reg].type != CONST_IMM &&
   regs[insn->src_reg].type != UNKNOWN_VALUE) {
min_val = BPF_REGISTER_MIN_RANGE;
max_val = BPF_REGISTER_MAX_RANGE;
}

Why only the source register? Why not the destination register?


/* We don't know anything about what was done to this register, mark it
* as unknown.
*/
if (min_val == BPF_REGISTER_MIN_RANGE &&
   max_val == BPF_REGISTER_MAX_RANGE) {
reset_reg_range_values(regs, insn->dst_reg);
return;
}

Why have this special case at all? Since min_val and max_val are
basically independent, this code shouldn't be necessary, right?


static void check_reg_overflow(struct bpf_reg_state *reg)
{
if (reg->max_value > BPF_REGISTER_MAX_RANGE)
reg->max_value = BPF_REGISTER_MAX_RANGE;
if (reg->min_value < BPF_REGISTER_MIN_RANGE ||
   reg->min_value > BPF_REGISTER_MAX_RANGE)
reg->min_value = BPF_REGISTER_MIN_RANGE;
}

Why is this asymmetric? Why is `reg->max_value <
BPF_REGISTER_MIN_RANGE` not important, but `reg->min_value >
BPF_REGISTER_MAX_RANGE` is?


In states_equal():
if (rold->type == NOT_INIT ||
   (rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT))   <------------
continue;

I think this is broken in code like the following:

int value;
if (condition) {
  value = 1; // visited first by verifier
} else {
  value = 1000000; // visited second by verifier
}
int dummy = 1; // states seem to converge here, but actually don't
map[value] = 1234;

`value` would be an UNKNOWN_VALUE for both paths, right? So
states_equal() would decide that the states converge after the
conditionally executed code?

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Josef Bacik]

On 11/15/2016 08:47 AM, Jann Horn wrote:
> On Tue, Nov 15, 2016 at 4:10 AM, Alexei Starovoitov
> <alexei.starovoitov@gmail.com> wrote:
>> On Mon, Nov 14, 2016 at 03:45:36PM -0500, Josef Bacik wrote:
>>> I made some invalid assumptions with BPF_AND and BPF_MOD that could result in
>>> invalid accesses to bpf map entries.  Fix this up by doing a few things
>>>
>>> 1) Kill BPF_MOD support.  This doesn't actually get used by the compiler in real
>>> life and just adds extra complexity.
>>>
>>> 2) Fix the logic for BPF_AND, don't allow AND of negative numbers and set the
>>> minimum value to 0 for positive AND's.
>>>
>>> 3) Don't do operations on the ranges if they are set to the limits, as they are
>>> by definition undefined, and allowing arithmetic operations on those values
>>> could make them appear valid when they really aren't.
>>>
>>> This fixes the testcase provided by Jann as well as a few other theoretical
>>> problems.
>>>
>>> Reported-by: Jann Horn <jannh@google.com>
>>> Signed-off-by: Josef Bacik <jbacik@fb.com>
>>
>> lgtm.
>> Acked-by: Alexei Starovoitov <ast@kernel.org>
>>
>> Jann, could you please double check the logic.
>> Thanks!
>
> I found some more potential issues, maybe Josef and you can tell me whether I
> understood these correctly.
>
>
> /* If the source register is a random pointer then the
> * min_value/max_value values represent the range of the known
> * accesses into that value, not the actual min/max value of the
> * register itself.  In this case we have to reset the reg range
> * values so we know it is not safe to look at.
> */
> if (regs[insn->src_reg].type != CONST_IMM &&
>    regs[insn->src_reg].type != UNKNOWN_VALUE) {
> min_val = BPF_REGISTER_MIN_RANGE;
> max_val = BPF_REGISTER_MAX_RANGE;
> }
>
> Why only the source register? Why not the destination register?
>

The destination register is what we are doing arithmetic to, so we don't 
actually care about the type of register it is, as we'll interpret the values at 
a a later point.  If the source register however is a MAP or some other pointer, 
then we know that the min/max values only apply to the range on the actual value 
of the register, rather than the possible range of values.  Said in another way 
if src register is a MAP then the range is [SRC_REG.imm+SRC_REG.min_value, 
SRC_REG.imm+SRC_REG.max_value] instead of [SRC_REG.min_value, SRC_REG.max_value].

So this is the same behavior for the destination register for sure, but we don't 
actually care about it at this point.  If the src_reg meets these criteria then 
we certainly don't know anything about the dest_reg and reset it blow with this

         if (min_val == BPF_REGISTER_MIN_RANGE &&
             max_val == BPF_REGISTER_MAX_RANGE) {
                 reset_reg_range_values(regs, insn->dst_reg);
                 return;
         }

Then in check_alu_op() if we weren't doing our operation on a MAP_PTR then we 
set the register to unknown and carry on.

>
> /* We don't know anything about what was done to this register, mark it
> * as unknown.
> */
> if (min_val == BPF_REGISTER_MIN_RANGE &&
>    max_val == BPF_REGISTER_MAX_RANGE) {
> reset_reg_range_values(regs, insn->dst_reg);
> return;
> }
>
> Why have this special case at all? Since min_val and max_val are
> basically independent, this code shouldn't be necessary, right?
>

They are the value of the source register, as I explained above if we know 
nothing about the source register then don't even bother doing the math, we also 
know nothing about the destination register.  This is a shortcut to keep us from 
doing potentially dangerous things when we already know it's invalid.

>
> static void check_reg_overflow(struct bpf_reg_state *reg)
> {
> if (reg->max_value > BPF_REGISTER_MAX_RANGE)
> reg->max_value = BPF_REGISTER_MAX_RANGE;
> if (reg->min_value < BPF_REGISTER_MIN_RANGE ||
>    reg->min_value > BPF_REGISTER_MAX_RANGE)
> reg->min_value = BPF_REGISTER_MIN_RANGE;
> }
>
> Why is this asymmetric? Why is `reg->max_value <
> BPF_REGISTER_MIN_RANGE` not important, but `reg->min_value >
> BPF_REGISTER_MAX_RANGE` is?

Because max_value is unsigned, so if we do reg->max_value = 
BPF_REGISTER_MIN_RANGE; and then do this we'll still get max_value reset to 
MAX_RANGE.

>
>
> In states_equal():
> if (rold->type == NOT_INIT ||
>    (rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT))   <------------
> continue;
>
> I think this is broken in code like the following:
>
> int value;
> if (condition) {
>   value = 1; // visited first by verifier
> } else {
>   value = 1000000; // visited second by verifier
> }
> int dummy = 1; // states seem to converge here, but actually don't
> map[value] = 1234;
>
> `value` would be an UNKNOWN_VALUE for both paths, right? So
> states_equal() would decide that the states converge after the
> conditionally executed code?
>

Value would be CONST_IMM for both paths, and wouldn't match so they wouldn't 
converge.  I think I understood your question right, let me know if I'm 
addressing the wrong part of it.

Do my explanations make sense?  I'm doing this first thing in the morning so I'm 
still a little foggy, let me know if things still aren't clear.  Thanks,

Josef

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[David Miller]

From: Josef Bacik <jbacik@fb.com>
Date: Mon, 14 Nov 2016 15:45:36 -0500

> I made some invalid assumptions with BPF_AND and BPF_MOD that could result in
> invalid accesses to bpf map entries.  Fix this up by doing a few things
> 
> 1) Kill BPF_MOD support.  This doesn't actually get used by the compiler in real
> life and just adds extra complexity.
> 
> 2) Fix the logic for BPF_AND, don't allow AND of negative numbers and set the
> minimum value to 0 for positive AND's.
> 
> 3) Don't do operations on the ranges if they are set to the limits, as they are
> by definition undefined, and allowing arithmetic operations on those values
> could make them appear valid when they really aren't.
> 
> This fixes the testcase provided by Jann as well as a few other theoretical
> problems.
> 
> Reported-by: Jann Horn <jannh@google.com>
> Signed-off-by: Josef Bacik <jbacik@fb.com>

Applied, thanks.

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Jann Horn]

On Tue, Nov 15, 2016 at 3:20 PM, Josef Bacik <jbacik@fb.com> wrote:
> On 11/15/2016 08:47 AM, Jann Horn wrote:
>> In states_equal():
>> if (rold->type == NOT_INIT ||
>>    (rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT))
>> <------------
>> continue;
>>
>> I think this is broken in code like the following:
>>
>> int value;
>> if (condition) {
>>   value = 1; // visited first by verifier
>> } else {
>>   value = 1000000; // visited second by verifier
>> }
>> int dummy = 1; // states seem to converge here, but actually don't
>> map[value] = 1234;
>>
>> `value` would be an UNKNOWN_VALUE for both paths, right? So
>> states_equal() would decide that the states converge after the
>> conditionally executed code?
>>
>
> Value would be CONST_IMM for both paths, and wouldn't match so they wouldn't
> converge.  I think I understood your question right, let me know if I'm
> addressing the wrong part of it.

Okay, true, but what if you load the values from a map and bounds-check them
instead of hardcoding them? Then they will be of type UNKNOWN_VALUE, right?
Like this:

int value = map[0];
if (condition) {
  value &= 0x1; // visited first by verifier
} else {
  // nothing; visited second by verifier
}
int dummy = 1; // states seem to converge here, but actually don't
map[value] = 1234;

And then `rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT` will be
true in the `dummy = 1` line, and the states converge. Am I missing something?

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Josef Bacik]

On 11/16/2016 01:41 PM, Jann Horn wrote:
> On Tue, Nov 15, 2016 at 3:20 PM, Josef Bacik <jbacik@fb.com> wrote:
>> On 11/15/2016 08:47 AM, Jann Horn wrote:
>>> In states_equal():
>>> if (rold->type == NOT_INIT ||
>>>    (rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT))
>>> <------------
>>> continue;
>>>
>>> I think this is broken in code like the following:
>>>
>>> int value;
>>> if (condition) {
>>>   value = 1; // visited first by verifier
>>> } else {
>>>   value = 1000000; // visited second by verifier
>>> }
>>> int dummy = 1; // states seem to converge here, but actually don't
>>> map[value] = 1234;
>>>
>>> `value` would be an UNKNOWN_VALUE for both paths, right? So
>>> states_equal() would decide that the states converge after the
>>> conditionally executed code?
>>>
>>
>> Value would be CONST_IMM for both paths, and wouldn't match so they wouldn't
>> converge.  I think I understood your question right, let me know if I'm
>> addressing the wrong part of it.
>
> Okay, true, but what if you load the values from a map and bounds-check them
> instead of hardcoding them? Then they will be of type UNKNOWN_VALUE, right?
> Like this:
>
> int value = map[0];
> if (condition) {
>   value &= 0x1; // visited first by verifier
> } else {
>   // nothing; visited second by verifier
> }
> int dummy = 1; // states seem to converge here, but actually don't
> map[value] = 1234;
>
> And then `rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT` will be
> true in the `dummy = 1` line, and the states converge. Am I missing something?
>

Ah ok yeah I see it now you are right.  This is slightly different from this 
particular problem so I'll send a second patch to address this, sound 
reasonable?  Thanks,

Josef

Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

[Jann Horn]

On Wed, Nov 16, 2016 at 9:25 PM, Josef Bacik <jbacik@fb.com> wrote:
> On 11/16/2016 01:41 PM, Jann Horn wrote:
>>
>> On Tue, Nov 15, 2016 at 3:20 PM, Josef Bacik <jbacik@fb.com> wrote:
>>>
>>> On 11/15/2016 08:47 AM, Jann Horn wrote:
>>>>
>>>> In states_equal():
>>>> if (rold->type == NOT_INIT ||
>>>>    (rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT))
>>>> <------------
>>>> continue;
>>>>
>>>> I think this is broken in code like the following:
>>>>
>>>> int value;
>>>> if (condition) {
>>>>   value = 1; // visited first by verifier
>>>> } else {
>>>>   value = 1000000; // visited second by verifier
>>>> }
>>>> int dummy = 1; // states seem to converge here, but actually don't
>>>> map[value] = 1234;
>>>>
>>>> `value` would be an UNKNOWN_VALUE for both paths, right? So
>>>> states_equal() would decide that the states converge after the
>>>> conditionally executed code?
>>>>
>>>
>>> Value would be CONST_IMM for both paths, and wouldn't match so they
>>> wouldn't
>>> converge.  I think I understood your question right, let me know if I'm
>>> addressing the wrong part of it.
>>
>>
>> Okay, true, but what if you load the values from a map and bounds-check
>> them
>> instead of hardcoding them? Then they will be of type UNKNOWN_VALUE,
>> right?
>> Like this:
>>
>> int value = map[0];
>> if (condition) {
>>   value &= 0x1; // visited first by verifier
>> } else {
>>   // nothing; visited second by verifier
>> }
>> int dummy = 1; // states seem to converge here, but actually don't
>> map[value] = 1234;
>>
>> And then `rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT` will be
>> true in the `dummy = 1` line, and the states converge. Am I missing
>> something?
>>
>
> Ah ok yeah I see it now you are right.  This is slightly different from this
> particular problem so I'll send a second patch to address this, sound
> reasonable?  Thanks,

Sure, makes sense.