I got an idea how to make RangeConstraintManager more sofisticated within comparison operations.
I want you speak out, share your vision about this idea. Briefly speaking, RangeConstraintManager shall care about the sanity of comparison expressions sequences and help reasonably to branch an exploded graph.
The idea came to me as a thing which resolves this bug PR13426.
Let's consider the next snippet:
int foo(int x, int y) { int z; if (x == y) { z = 0; } if (x != y) { z = 1; } return z; }
Obviously that z will be initialized, but CSA reports next:
warning: Undefined or garbage value returned to caller [core.uninitialized.UndefReturn] return z;
It happenes because CSA does not take into account that x == y and x != y are just two opposites, as if it was:
if (x == y) { z = 0; } else { z = 1; }
So my improvements are in handling case above and similar ones. Assume for some comparison x < y we look for any other comparisons with the same operands (x > y, y != x, etc.). Then we do logical calculations and refuse impossible branches.
For example:
- x < y and x > y at the same time are impossible.
- x >= y and x != y at the same time makes x > y true only.
- x == y and y == x are just reversed but the same.
It covers all possible combinations and is described in the next table.
< | > | <= | >= | == | != | UnknownX2 | |
< | 1 | 0 | * | 0 | 0 | * | 1 |
> | 0 | 1 | 0 | * | 0 | * | 1 |
<= | 1 | 0 | 1 | * | 1 | * | 0 |
>= | 0 | 1 | * | 1 | 1 | * | 0 |
== | 0 | 0 | * | * | 1 | 0 | 1 |
!= | 1 | 1 | * | * | 0 | 1 | 0 |
The table holds states for the preceding comparison operation assuming the latter is true.
For instance, assume x < y is true that means x != y is surely true:
if (x preciding_operation y) // < | != | > if (x operation y) // != | > | < tristate // True | Unknown | False
Columns stands for a preceding operator. Rows stands for a current operator. Each row has exactly two Unknown cases. UnknownX2 means that both Unknown preceding operators are met in code, and there is a special column for that, for example:
if (x >= y) if (x != y) if (x <= y) False only
As a result of processing an example below, we have
and exploded graphs.void foo(int y, int x) { if (x < y) { if (y > x); if (x > y); if (x <= y); if (y <= x); if (x == y); if (y != x); } }
Please, express your thoughts down here, if it is worth to be.
+1 for this static assert!
It's good to ensure such assumptions, even if those are very unlikely to change