implied: overwrite smatch_extra using implied states if possible
commit209b75b277f851ebb591371043f0feebc7883f8d
authorDan Carpenter <dan.carpenter@oracle.com>
Fri, 15 Apr 2016 11:40:23 +0000 (15 14:40 +0300)
committerDan Carpenter <dan.carpenter@oracle.com>
Fri, 15 Apr 2016 11:40:23 +0000 (15 14:40 +0300)
tree5201b4114dd180808f3c108df0f1036eb5481fb6
parent90825e2ca22d40b0f197900d232fce0688c9a9d7
implied: overwrite smatch_extra using implied states if possible

The issue here is this scenario:  We say on one path x is 5 on another
path x is 0-10.  We merge those paths together.  Then we come to a
condition "if (x == 10)".  We know that for that to be true then "x" has to
come from the path where x was "0-10".  In other words, it's implied that
x is 0-10.  It's implied 0-10 but actually in smatch_extra we can further
limit it to just 10.

So there are a couple things that happen.  First is that we actually delete
these states from the implied list using the delete_equiv_stree() function.
The next is that we overwrite the implied state because we first set the
implied states and then call the smatch_extra hook for conditions which
sets the true and false paths.

The problem is that when we overwrite the implied states we use state_state
and not set_sm so all the earlier implications are lost.

Let me explain this patch in the reverse order.  First it says that, let's
do the smatch_extra hook first and then use the implied states.  This should
be fine because we deleted the "x" implications using the call to
delete_equiv_stree().

But then it says let's say that instead of implying x is 0-10, say we have
a different code where it implies something which is clearly either true
or false like x = 10.  Something which the smatch_extra hooks would have
said as well.  In that case don't call delete_equiv_stree() but instead
let's preserve the original implications.

Signed-off-by: Dan Carpenter <dan.carpenter@oracle.com>
smatch_implied.c
validation/sm_implied16.c [new file with mode: 0644]