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 <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>
Reviewed-by: David Chase <drchase@google.com>

1 files changed, 9 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index b7ef468be6..f7b3ef0847 100644
--- a/test/prove.go
+++ b/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) {
 }