cmd/compile: in prove, infer unsigned relations while branching

When a branch is followed, we apply the relation as described
in the domain relation table. In case the relation is in the
positive domain, we can also infer an unsigned relation if,
by that point, we know that both operands are non-negative.

Fixes #20393

Change-Id: Ieaf0c81558b36d96616abae3eb834c788dd278d5
Reviewed-on: https://go-review.googlesource.com/100278
Run-TryBot: Giovanni Bajo <[email protected]>
TryBot-Result: Gobot Gobot <[email protected]>
Reviewed-by: Giovanni Bajo <[email protected]>
Reviewed-by: David Chase <[email protected]>

Author: rasky

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

@@ -704,6 +704,9 @@ func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
 		// When we branched from parent we learned a new set of
 		// restrictions. Update the factsTable accordingly.
 		d := tr.d
+		if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) {
+			d |= unsigned
+		}
 		switch br {
 		case negative:
 			switch b.Control.Op { // Special cases

test/prove.go

@@ -605,6 +605,15 @@ func trans2(a, b []int, i int) {
 	_ = b[i] // ERROR "Proved IsInBounds$"
 }
 
+func trans3(a, b []int, i int) {
+	if len(a) > len(b) {
+		return
+	}
+
+	_ = a[i]
+	_ = b[i] // ERROR "Proved IsInBounds$"
+}
+
 //go:noinline
 func useInt(a int) {
 }