https://gcc.gnu.org/bugzilla/show_bug.cgi?id=115392
--- Comment #7 from Daniel Petrovic <daniel-dev at hotmail dot de> ---
(In reply to Jakub Jelinek from comment #5)
> (In reply to Daniel Petrovic from comment #4)
> > The following generalizatin applies:
> >
> > let op = { |, ^ }
> >
> > Case 1:
> >
> > (a op b) <=//> C <=> b <=//> C
> >
> > if:
> > a = 2^m-1
>
> If op is |, it can be actually anything with [0, 2^m-1] range and then check
> if (2^m-1 & C) == 2^m-1 (but don't we need C to contain at least one bit
> above it too?). I'm not sure about the xor case.
Good point. IMO this broader generalization holds for both | and ^ without
requiring C to have more bits set above m
Since 'a' is in range [0, 2^m - 1] 'a' has bits set only below position m, so
neither a | b or a ^ b can alter b's bits at or above position m
Let x_L and x_H be "low" and "high" parts defined as : x_L = x & 2^m-1 and x_H
= x & ~(2^m-1)
Assuming C_L == 2^m-1 (all lower m bits are set in C):
The claim is: (a op b) <= C <-> b <= C
To show equivalence <-> we have to show both implications -> and <-
->:
Lets assume (a op b) <= C.
Because of C_L == 2^m-1 we have b_L <= C_L.
If b_H > C_H then (a op b)_H == b_H > C_H which implies (a op b) > C.
Contradiction.
So it has to be b_H <= C_H.
But then we have b_L <= C_L and b_H <= C_H -> b <= C
<-:
let assume b <= C
Then we cannot have b_H > C_H, otherwise it would be b >= b_H > C_H. This
would imply b > C. Contradiction.
So it must be b_H <= C_H
if (b_H < C_H):
since (a op b)_H = b_H -> the high bits guarantee that also (a op b) <
C_H < C
if (b_H == C_H):
Then (a op b)_H = b_H == C_H
Because of C_L == 2^m-1 => (a op b)_L <= C_L
So overall: (a op b) <= C
So (a op b) <= C should be equivalent to b <= C under these conditions.
I've also constructed and attached a z3 script formal verifying the claim.
