I found a pretty simple case where GCC cannot optimize out a redundant check. I've reduced it to the following minimal test case: unsigned int random_number(void); void eliminate_me(void); void main(void) { unsigned int a = random_number(); unsigned int b = random_number(); if (b > a) return; int x = b - 8; if (x > 0 && x > a) eliminate_me(); } I think it should be really easy to prove that eliminate_me() cannot be called, because x can never be greater than a (otherwise b would have also been greater than a and the function would have terminated earlier). I don't know anything about how compilers do data flow analysis in detail, but GCC can usually figure out so much that I'm surprised it cannot figure out this one.
Confirmed - symbolic range analysis fails here, we do not adjust relations when seeing x = b - 8.
=========== BB 2 ============ <bb 2> : _1 = random_number (); a_11 = (unsigned int) _1; _2 = random_number (); b_13 = (unsigned int) _2; if (a_11 < b_13) goto <bb 3>; [INV] else goto <bb 4>; [INV] 2->3 (T) _2 : int [-INF, -1][1, +INF] 2->3 (T) b_13 : unsigned int [1, +INF] =========== BB 3 ============ <bb 3> : // predicted unlikely by early return (on trees) predictor. goto <bb 6>; [INV] =========== BB 4 ============ a_11 unsigned int VARYING b_13 unsigned int VARYING <bb 4> : _3 = b_13 + 4294967288; x_14 = (int) _3; _4 = x_14 > 0; _6 = _3 > a_11; _7 = _4 & _6; if (_7 != 0) goto <bb 5>; [INV] else goto <bb 6>; [INV] 4->5 (T) _3 : unsigned int [1, 2147483647] 4->5 (T) _4 : _Bool [1, 1] 4->5 (T) _6 : _Bool [1, 1] 4->5 (T) _7 : _Bool [1, 1] 4->5 (T) a_11 : unsigned int [0, 4294967294] 4->5 (T) b_13 : unsigned int [9, 2147483655] 4->5 (T) x_14 : int [1, +INF] 4->6 (F) _7 : _Bool [0, 0] When relations are implemented, the edge from 2->4 should record a_11 >= b_13 as long as we get it right that x_14 is a cast equivalence of _3, and its > 0, then we should be able to also determine that _3 is < b_13 and therefore < a_11 always, and fold this away. A good testcase to confirm all the parts are working together.. when we get there.. hopefully next release.