The transformation seems right to me, but we are then missing another
transformation like ~X & Y -> X ^ Y when we know that X & ~Y is 0 (the 1
bits of X are included in those of Y). That may not be easy with the
limited bit tracking we have. A version limited to constant Y of the
form 2^n-1 (i.e. 0...01...1) where X has a range included in [0, Y] may
be simpler.
We could also simplify (int)(_Bool)x to x using VRP information that x
is in [0, 1], but apparently when VRP replaces x==0 with y=x^1,(_Bool)y,
it does not compute a range for the new variable y, and by the time the
next VRP pass comes, it is too late.