Been playing with a relational bitvector abstract domain. Every bit of a value is 0, 1, or a (potentially inverted) fixed bit from another value. It's similar to LLVM's collectBitParts or Hexagon BitTracker. The domain makes it possible to detect all kinds of bit twiddling shenanigans. Eg when a value is split into pieces and reassembled: lo = x & 0x0000ffff hi = x >> 16 result = lo | (hi << 16) here we can directly conclude that result == x, without having this patterns as a peephole rule.