On 11/16/2016 01:41 PM, Jann Horn wrote:
On Tue, Nov 15, 2016 at 3:20 PM, Josef Bacik <jba...@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
