Propagating bounds through bitwise operations

[luu]

http://bitmath.blogspot.com/2023/07/propagating-bounds-through-bitwise.html

[o11c]

Some random adjacent thoughts:

* both arithmetic bounds and bitwise bounds are useful for things the other can't do

* you have to trade off "how much useful information am I keeping for optimizations" with "how much memory am I willing to spend on that information"

* if you had infinite memory you could just track the value sets directly.

* if the value set is union-like, even if it just contains a single special value (often -1, but also MAX_INT and others), that often completely ruins the ability to track meaningful arithmetic or bitwise bounds.

* if an enum is involved, often that's a place that already stores the full value set (but beware the numerous variations of what an "enum" is)

[colanderman]

You can propagate bitwise bounds (whether each bit may be 0 or 1) over arithmetic operations efficiently as well. I worked this out a decade ago too, I forget the specifics but I remember for addition/subtraction I think it had something to do with interleaving upper/lower bounds bitmasks. If I can dig up my code I'll post it here.

[someguydave → colanderman]

Yes please!

[colanderman → someguydave]

Took me a while but I found it!! The algorithm is surprisingly simple.

I represented the combined artihmetic and bitwise bounds for each variable as a triple, (arithLow, arithHigh, bitMask). bitMask specified which bits of the variable were fixed/known; these known bits were reflected in the arithmetic bounds. This way, `arithLow | ~bitMask` gives a bitwise lower bound, and `arithLow & bitMask` gives a bitwise upper bound. (Using arithLow or arithHigh doesn't matter here as they are identical in the known bits.)

Summing the arithmetic bounds is as you'd expect (add the lower bounds together, add the upper bounds together, deal with overflow appropriately); I won't detail that here.

The bitmasks can then be summed, for an expression `x+y`, as:

    x.bitMask & y.bitMask &
      ~(((x.arithLow | ~x.bitMask) + (y.arithLow | ~y.bitMask)) ^
        ((x.arithLow & x.bitMask) + (y.arithLow & y.bitMask)))

Essentially, this is using addition of the bitwise bounds to propagate "unknown" bits for both the lower and upper bitwise bounds, and updating the "known bits" mask from that.

I just discovered, this expression looks elegant rewritten in terms of the bitwise bounds:

    ~(x.bitwiseLower ^ x.bitwiseUpper) &
      ~(y.bitwiseLower ^ y.bitwiseUpper) &
      ~((x.bitwiseLower + y.bitwiseLower) ^ (x.bitwiseUpper + y.bitwiseUpper))

Of course these days you'd use BDDs or throw the whole problem at Z3. But this is very efficient and captures most common cases.

[amelius]

Are the integers allowed to be negative? Is this using two's complement?

[dcuthbertson → amelius]

Probably yes for both questions. Ch.4 of Hacker's Delight starts with assuming all quantities are signed integers. A little further along, a lemma about computing b-a when a≤b is introduced:

Lemma. If a and b are signed integers and a≤b, then the computed value b-a correctly represents the arithmetic value b-a, if the computed value is interpreted as unsigned

It's been a while since I worked through any of Hacker's Delight, but I think this means that unsigned values can be used to check bounds of signed and unsigned values. This post is an improvement over that work, so this same property should hold for these new bit-twiddling equations. Still, I'd run a few test to make sure.