cmd/compile: support unsigned induction variables

src/cmd/compile/internal/ssacompile/downward_counting_loop.go

@@ -98,9 +98,9 @@ func maybeRewriteLoopToDownwardCountingLoop(f *ssa.Func, v indVar) {
 			return
 		}
 	case ssaop.OpLess8U, ssaop.OpLess16U, ssaop.OpLess32U, ssaop.OpLess64U, ssaop.OpLeq8U, ssaop.OpLeq16U, ssaop.OpLeq32U, ssaop.OpLeq64U:
-		panic(`parseIndVar didn't yet support unsigned induction variables, this code doesn't yet support them either.
-If you are seeing this it is probably because you've fixed https://go.dev/issue/65918.
-You need to update this code and add tests then.`)
+		// Unsigned induction variables are tracked for BCE, but loop inversion
+		// still relies on signed bounds and is intentionally skipped.
+		return
 	case ssaop.OpEq8, ssaop.OpEq16, ssaop.OpEq32, ssaop.OpEq64, ssaop.OpNeq8, ssaop.OpNeq16, ssaop.OpNeq32, ssaop.OpNeq64:
 		panic(`parseIndVar didn't yet support induction variables using == or !=.
 If you are seeing this it is probably because you've added support for them.

src/cmd/compile/internal/ssacompile/loopbce.go

@@ -6,6 +6,7 @@ package ssacompile
 
 import (
 	"fmt"
+	"math"
 
 	"cmd/compile/internal/base"
 	"cmd/compile/internal/ssa"
@@ -22,13 +23,14 @@ const (
 )
 
 type indVar struct {
-	ind   *ssa.Value // induction variable
-	nxt   *ssa.Value // the incremented variable
-	min   *ssa.Value // minimum value, inclusive/exclusive depends on flags
-	max   *ssa.Value // maximum value, inclusive/exclusive depends on flags
-	entry *ssa.Block // the block where the edge from the succeeded comparison of the induction variable goes to, means when the bound check has passed.
-	step  int64      // it will always be positive.
-	flags indVarFlags
+	ind      *ssa.Value // induction variable
+	nxt      *ssa.Value // the incremented variable
+	min      *ssa.Value // minimum value, inclusive/exclusive depends on flags
+	max      *ssa.Value // maximum value, inclusive/exclusive depends on flags
+	entry    *ssa.Block // the block where the edge from the succeeded comparison of the induction variable goes to, means when the bound check has passed.
+	step     int64      // it will always be positive.
+	flags    indVarFlags
+	unsigned bool
 	// Invariant: for all blocks dominated by entry:
 	//	min <= ind <  max    [if flags == 0]
 	//	min <  ind <  max    [if flags == indVarMinExc]
@@ -130,12 +132,17 @@ nextblock:
 		c := b.Controls[0]
 		for idx := range 2 {
 			// Check that the control if it either ind </<= limit or limit </<= ind.
-			// TODO: Handle unsigned comparisons?
 			inclusive := false
+			unsigned := false
 			switch c.Op {
 			case ssaop.OpLeq64, ssaop.OpLeq32, ssaop.OpLeq16, ssaop.OpLeq8:
 				inclusive = true
 			case ssaop.OpLess64, ssaop.OpLess32, ssaop.OpLess16, ssaop.OpLess8:
+			case ssaop.OpLeq64U, ssaop.OpLeq32U, ssaop.OpLeq16U, ssaop.OpLeq8U:
+				inclusive = true
+				unsigned = true
+			case ssaop.OpLess64U, ssaop.OpLess32U, ssaop.OpLess16U, ssaop.OpLess8U:
+				unsigned = true
 			default:
 				continue nextblock
 			}
@@ -163,6 +170,10 @@ nextblock:
 			if step == 0 {
 				continue
 			}
+			if unsigned && inc.AuxUnsigned() > math.MaxInt64 {
+				// indVar.step is signed; don't reinterpret a wrapped constant.
+				continue
+			}
 			// step == minInt64 cannot be safely negated below, because -step
 			// overflows back to minInt64. The later underflow checks need a
 			// positive magnitude, so reject this case here.
@@ -230,6 +241,32 @@ nextblock:
 			// We use a function wrapper here for easy return true / return false / keep going logic.
 			// This function returns true if the increment will never overflow/underflow.
 			ok := func() bool {
+				if unsigned {
+					max := maxUintForConstType(ind.Type)
+					if step > 0 {
+						if limit.IsGenericIntConst() {
+							room := max - limit.AuxUnsigned()
+							if (!inclusive && room >= uint64(step-1)) || (inclusive && room >= uint64(step)) {
+								return true
+							}
+						}
+						if step == 1 && !inclusive {
+							return true
+						}
+					} else {
+						if limit.IsGenericIntConst() {
+							bound := uint64(-step)
+							if (!inclusive && limit.AuxUnsigned() >= bound-1) || (inclusive && limit.AuxUnsigned() >= bound) {
+								return true
+							}
+						}
+						if step == -1 && !inclusive {
+							return true
+						}
+					}
+					return false
+				}
+
 				if step > 0 {
 					if limit.IsGenericIntConst() {
 						// Figure out the actual largest value.
@@ -349,9 +386,10 @@ nextblock:
 					// This is startBody.b, where startBody is the edge from the comparison for the
 					// induction variable, not necessarily the in-loop edge from the loop header.
 					// Induction variable bounds are not valid in the loop before this edge.
-					entry: startBody.B,
-					step:  step,
-					flags: flags,
+					entry:    startBody.B,
+					step:     step,
+					flags:    flags,
+					unsigned: unsigned,
 				})
 				b.Logf("found induction variable %v (inc = %v, min = %v, max = %v)\n", ind, inc, min, max)
 			}
@@ -361,6 +399,21 @@ nextblock:
 	return iv
 }
 
+func maxUintForConstType(t *types.Type) uint64 {
+	switch t.Size() {
+	case 8:
+		return math.MaxUint64
+	case 4:
+		return math.MaxUint32
+	case 2:
+		return math.MaxUint16
+	case 1:
+		return math.MaxUint8
+	default:
+		panic("unreachable")
+	}
+}
+
 // subWillUnderflow checks if x - y underflows the min value.
 // y must be positive.
 func subWillUnderflow(x, y int64, min int64) bool {

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

@@ -1773,8 +1773,11 @@ func getBranch(sdom ssa.SparseTree, p *ssa.Block, b *ssa.Block) branch {
 // starting in Block b.
 func addIndVarRestrictions(ft *factsTable, b *ssa.Block, iv indVar) {
 	d := signed
+	if iv.unsigned {
+		d = unsigned
+	}
 	if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
-		d |= unsigned
+		d |= signed | unsigned
 	}
 
 	if iv.flags&indVarMinExc == 0 {

test/prove.go

@@ -74,12 +74,19 @@ func f2(a []int) int {
 }
 
 func f3(a []uint) int {
-	for i := uint(0); i < uint(len(a)); i++ {
+	for i := uint(0); i < uint(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 		a[i] = i // ERROR "Proved IsInBounds$"
 	}
 	return 41
 }
 
+func f3step(a []uint) int {
+	for i := uint(0); i < uint(len(a))-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
+		a[i] = i // ERROR "Proved IsInBounds$"
+	}
+	return 42
+}
+
 func f4a(a, b, c int) int {
 	if a < b {
 		if a == b { // ERROR "Disproved Eq64$"

test/prove_invert_loop_with_unused_iterators.go

@@ -9,3 +9,15 @@ func invert(b func(), n int) {
 		b()
 	}
 }
+
+func invertu(b func(), n uint) {
+	for i := uint(0); i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+		b()
+	}
+}
+
+func invertudown(b func(), n uint) {
+	for i := n; i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1"
+		b()
+	}
+}