From 29162ec9a7d4ee08a558729236cd9bf50febee09 Mon Sep 17 00:00:00 2001 From: Giovanni Bajo Date: Tue, 3 Apr 2018 18:59:44 +0200 Subject: [PATCH] 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 TryBot-Result: Gobot Gobot Reviewed-by: Giovanni Bajo Reviewed-by: David Chase --- src/cmd/compile/internal/ssa/prove.go | 3 +++ test/prove.go | 9 +++++++++ 2 files changed, 12 insertions(+) diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index a11b46566d..371009a57d 100644 --- 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 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) { } -- 2.50.0