We currently are able to prove X is non-zero if there are dominating
compares or assumes directly on X, but we can do a bit better and
also check uses of X s.t Use(X) != 0 implies X != 0.
For example if we have assume(X & Y != 0), we know X != 0.
Likewise if we have a dominating condition:
if(X & Y != 0) { // X is known zero here }
Currently implemented to track through:
- X&Y -- https://alive2.llvm.org/ce/z/zdkf-x
- 0-X -- https://alive2.llvm.org/ce/z/yvEAZx
- bitreverse(X) -- https://alive2.llvm.org/ce/z/zEPy9z
- bswap(X) -- https://alive2.llvm.org/ce/z/i_li18
- ctpop(X) -- https://alive2.llvm.org/ce/z/fXMDTs
- abs(X) -- https://alive2.llvm.org/ce/z/EbP82g https://alive2.llvm.org/ce/z/hfzZuX
'Null' -> 'Zero' ?