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>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index a11b46566dd6873522ca681d6493d7575b7f9e1a..371009a57d480376a375f77d14104bdb7a253358 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/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

diff --git a/test/prove.go b/test/prove.go
index b7ef468be63efb1cd55941663abd76593510f545..f7b3ef0847b0748460e0663f35d350999befca22 100644 (file)
--- 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) {
 }