cmd/compile: for always negative numbers `int(x) < int(y)` proves `uint(x) < uint(y)`

[Jorropo]

The ssa.limit prove code widely assume that the positive half of the signed domain map to the bottom half of the unsigned domain.

But it also often assume that if a signed number reaches in the negative signed half it has no unsigned mapping while this is not true.
In fact the negative half of the signed domain perfectly maps to the top half of the unsigned domain.

The problem only exists at the discontinuity between maxint & minint.

In other words for always negative number int(x) < int(y) proves uint(x) < uint(y).

For one concrete example, applying the mathematical truth spelled out by the sentence above:

go/src/cmd/compile/internal/ssa/prove.go

Lines 571 to 577 in 0d0d5c9

	// signed <-> unsigned propagation
	if lim.min >= 0 {
	lim = lim.unsignedMinMax(uint64(lim.min), uint64(lim.max))
	}
	if fitsInBitsU(lim.umax, uint(8*v.Type.Size()-1)) {
	lim = lim.signedMinMax(int64(lim.umin), int64(lim.umax))
	}

The perfect* version of this code is:

	// signed <-> unsigned propagation
	bitsize := v.Type.Size()*8
	if sign(lim.min) == sign(lim.max) {
		lim = lim.unsignedMinMax(convertIntWithBitsize[uint64](lim.min, bitsize), convertIntWithBitsize[uint64](lim.max, bitsize))
	}
	intUmin, intUmax := convertIntWithBitsize[int64](lim.umin, bitsize), convertIntWithBitsize[int64](lim.umax, bitsize)
	if sign(intUmin) == sign(intUmax) {
		lim = lim.signedMinMax(intUmin, intUmax)
	}

*within the constraints of what limit can model.

---

I wished we wouldn't have to write workarounds like 03fcb33 does.
It shouldn't be too hard to fix because each occurrence of this "bug" since the current code is never wrong, but it is sometimes too conservative.
So each occurrence can be fixed in a vacuum.

[Jorropo]

I have been working on a patch series which works towards moving some limits code to arcs, arcs are ℤ₂ᵇⁱᵗˢⁱᶻᵉ representations of a cyclic graph that represent the set of possible values that might exists at runtime, the same way limits are two ranges representing the set of possible values that might exists.
https://go-review.googlesource.com/c/go/+/795082/10

And the results are great (see the add implementation comparison below).

There are multiple reasons I went into that direction:

• it's entropically optimal (*rounded up to the nearest bit)
  halves the amount of storage needed from 256bits to 128bits per value
• it allows to represent sets limits can't represent
• it matches my internal ring graph based representation of two's complement arithmetic
• it works: see this perfect implementation of add:

// add uses Minkowski addition to perfectly computes the possible
// result set of all possible pairings of the two sets added together.
func (a arc) add(b arc, bitsize uint) arc {
	mask := uint64(1)<<bitsize - 1
	spanA := (a.end - a.start) & mask
	spanB := (b.end - b.start) & mask
	total, carry := bits.Add64(spanA, spanB, 0)
	if carry != 0 || total >= mask {
		// the result covers the whole space.
		return arc{start: 0, end: mask}
	}
	return arc{start: (a.start + b.start) & mask, end: (a.end + b.end) & mask}
}

For comparison here is our current ¿imperfect? limit implementation:

// add returns the limit obtained by adding a value with limit l
// to a value with limit l2. The result must fit in b bits.
func (l limit) add(l2 limit, b uint) limit {
	var isLConst, isL2Const bool
	var lConst, l2Const uint64
	if l.min == l.max {
		isLConst = true
		lConst = convertIntWithBitsize[uint64](l.min, b)
	} else if l.umin == l.umax {
		isLConst = true
		lConst = l.umin
	}
	if l2.min == l2.max {
		isL2Const = true
		l2Const = convertIntWithBitsize[uint64](l2.min, b)
	} else if l2.umin == l2.umax {
		isL2Const = true
		l2Const = l2.umin
	}
	if isLConst && isL2Const {
		r := lConst + l2Const
		r &= (uint64(1) << b) - 1
		int64r := convertIntWithBitsize[int64](r, b)
		return limit{min: int64r, max: int64r, umin: r, umax: r}
	}

	r := noLimit()
	min, minOk := safeAdd(l.min, l2.min, b)
	max, maxOk := safeAdd(l.max, l2.max, b)
	if minOk && maxOk {
		r.min = min
		r.max = max
	}
	umin, uminOk := safeAddU(l.umin, l2.umin, b)
	umax, umaxOk := safeAddU(l.umax, l2.umax, b)
	if uminOk && umaxOk {
		r.umin = umin
		r.umax = umax
	}
	return r
}

Note: even a perfect limit representation is still not as good as a perfect arc one since limit has no way to represent an arc like [5:3] (in english a set of all possible values that include literally everything except 4); more generally a limit can't express an arc where end < start yet the sign of end and start is identical.

[Jorropo]

While writing arc.intersect I've realized I've made an assumption about limits.

I've assumed that either the unsigned limit was at play or the signed limit was at play.
However you can write let's say limit{-100, 50, 1, umax}.
In my previous assumptions I would have thought the unsigned limit must be 0, umax given the signed limit has both the most negative and the most positive unsigned values.

To be honest I don't even know if prove will do that by itself given I've wrote a CL that keep the whole limit math but does limit → arc and arc → limit when storing data and this never came up. This CL passes trybot, so at worst we are lacking some prove tests in this dual arc edge case.

So infact a limit is equal to two arcs which is way less interesting than I thought.