implied: handle ->implied states differently

implied: handle ->implied states differently

Calling them "->implied states" is a terrible name because I use the word
->implied everywhere to mean everything.  Forget that name because it is
going away.

How smatch implications work is that you have ->left and ->right pointers
that are set when you merge states together and you have a ->pool pointer.
The ->left and ->right pointers branch out to for a tree.  You have leaf
states and trunk states.

Smatch can find implications for several types of conditions.  You could
have comparisons a variable and a number (x < 0) or you could maybe have
a condition that we have seen before and saved.  The stored condition
states are boolean either it's true or false.  But the number states are
more complicated because we have one path where we know x is (-2)-4 and the
(-2)-(-1) range is true but the rest is false.  We have part of a state
which is true and part which is false.

If the state is a leaf state then that was handled by commit
b1c111ba472f ('implied: create fake implication history').  We change the
state to a trunk state and create two new leaf states sprouting out of it,
one for the true part and one for the false part.

The problem for this patch is how do we handle if part of the trunk state
is true and part is false.  Originally what would happen is that we would
create an ->implied state which preserved the true parts.  But the problem
is the next time we had a condition, instead of using these ->implied
states we would look up the whole original state.  Sometimes on this next
visit the ->implied state was false but the whole original state could go
both ways so we couldn't take advantage of the implication.

It means that we missed out on implications where we could have said
exactly what was going on but now we were more general.

Really what the ->left ->right tree is, is that it's paths to the ->pool
pointers.  The problem is that ->implied states potentially created
multiple paths to a pool and some were true and some were false.  With
the implied code we check the false paths first so we would look at the
multiple paths and say that it was false even though some true paths
existed.

So now what this patch does is that it makes a list of all the true, maybe
and false paths.  It removes all the maybes from the true and false list
and it removes all the pools that are both true and false.  Again, the way
it works is that false trumps true, true is used as a short cut only so
that we don't have to check any further down the rest of the branch.

I added back the add_pool() function because otherwise you can get pools
listed multiple times because there can be multiple true paths or multiple
false paths to the same pool.

I moved the pool_in_pools() function to be next to add_pool() and
remove_pool().

This patch only changes how SMATCH_EXTRA implications are handled, it
doesn't change how smatch_stored_condition.c implications are handled
because those are true and false states.  True is true.  False is false.
It's not a range of true and false that can be broken into parts like
SMATCH_EXTRA is range of numbers than can be subdivided.

Signed-off-by: Dan Carpenter <dan.carpenter@oracle.com>