cmd/compile: handle sign/zero extensions in prove, via update method

Array accesses with index types smaller than the machine word size may
involve a sign or zero extension of the index value before bounds
checking. Currently, this defeats prove because the facts about the
original index value don't flow through the sign/zero extension.

This CL fixes this by looking back through value-preserving sign/zero
extensions when adding facts via Update and, where appropriate, applying
the same facts using the pre-extension value. This fix is enhanced by
also looking back through value-preserving extensions within
ft.isNonNegative to infer whether the extended value is known to be
non-negative. Without this additional isNonNegative enhancement, this
logic is rendered significantly less effective by the limitation
discussed in the next paragraph.

In Update, the application of facts to pre-extension values is limited
to cases where the domain of the new fact is consistent with the type of
the pre-extension value. There may be cases where this cross-domain
passing of facts is valid, but distinguishing them from the invalid
cases is difficult for me to reason about and to implement.
Assessing which cases to allow requires details about the context and
inferences behind the fact being applied which are not available
within Update. Additional difficulty arises from the fact that the SSA
does not curently differentiate extensions added by the compiler for
indexing operations, extensions added by the compiler for implicit
conversions, or explicit extensions from the source.

Examples of some cases that would need to be filtered correctly for
cross-domain facts:

(1) A uint8 is zero-extended to int for indexing (a value-preserving
zeroExt). When, if ever, can signed domain facts learned about the int be
applied to the uint8?

(2) An int8 is sign-extended to int16 (value-preserving) for an equality
comparison. Equality comparison facts are currently always learned in both
the signed and unsigned domains. When, if ever, can the unsigned facts
learned about the int16, from the int16 != int16 comparison, be applied
to the original int8?

This is an alternative to CL 122695 and CL 174309. Compared to CL 122695,
this CL differs in that the facts added about the pre-extension value will
pass through the Update method, where additional inferences are processed
(e.g. fence-post implications, see #29964). CL 174309 is limited to bounds
checks, so is narrower in application, and makes the code harder to read.

Fixes #26292.
Fixes #29964.
Fixes #15074

Removes 238 bounds checks from std/cmd.

Change-Id: I1f87c32ee672bfb8be397b27eab7a4c2f304893f
Reviewed-on: https://go-review.googlesource.com/c/go/+/174704
Run-TryBot: Zach Jones <zachj1@gmail.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 7c693279906264f3ee16ebc1fcc3e4f8290298be..697862f986d334fcbf9af056bbf0f47b2bc8020e 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -530,6 +530,25 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
                }
        }
 
+       // Look through value-preserving extensions.
+       // If the domain is appropriate for the pre-extension Type,
+       // repeat the update with the pre-extension Value.
+       if isCleanExt(v) {
+               switch {
+               case d == signed && v.Args[0].Type.IsSigned():
+                       fallthrough
+               case d == unsigned && !v.Args[0].Type.IsSigned():
+                       ft.update(parent, v.Args[0], w, d, r)
+               }
+       }
+       if isCleanExt(w) {
+               switch {
+               case d == signed && w.Args[0].Type.IsSigned():
+                       fallthrough
+               case d == unsigned && !w.Args[0].Type.IsSigned():
+                       ft.update(parent, v, w.Args[0], d, r)
+               }
+       }
 }
 
 var opMin = map[Op]int64{
@@ -584,6 +603,11 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
                }
        }
 
+       // Check if v is a value-preserving extension of a non-negative value.
+       if isCleanExt(v) && ft.isNonNegative(v.Args[0]) {
+               return true
+       }
+
        // Check if the signed poset can prove that the value is >= 0
        return ft.order[0].OrderedOrEqual(ft.zero, v)
 }
@@ -1299,3 +1323,20 @@ func isConstDelta(v *Value) (w *Value, delta int64) {
        }
        return nil, 0
 }
+
+// isCleanExt reports whether v is the result of a value-preserving
+// sign or zero extension
+func isCleanExt(v *Value) bool {
+       switch v.Op {
+       case OpSignExt8to16, OpSignExt8to32, OpSignExt8to64,
+               OpSignExt16to32, OpSignExt16to64, OpSignExt32to64:
+               // signed -> signed is the only value-preserving sign extension
+               return v.Args[0].Type.IsSigned() && v.Type.IsSigned()
+
+       case OpZeroExt8to16, OpZeroExt8to32, OpZeroExt8to64,
+               OpZeroExt16to32, OpZeroExt16to64, OpZeroExt32to64:
+               // unsigned -> signed/unsigned are value-preserving zero extensions
+               return !v.Args[0].Type.IsSigned()
+       }
+       return false
+}

diff --git a/test/prove.go b/test/prove.go
index 6e92b9eec21a7ece724f5dc7ff56931b13014703..7643031c6220749a2af175e0ce02ab3e109f802a 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -853,6 +853,63 @@ func unrollIncMin(a []int) int {
        return x
 }
 
+// The 4 xxxxExtNto64 functions below test whether prove is looking
+// through value-preserving sign/zero extensions of index values (issue #26292).
+
+// Look through all extensions
+func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
+       if len(x) < 22 {
+               return 0
+       }
+       if j8 >= 0 && j8 < 22 {
+               return x[j8]  // ERROR "Proved IsInBounds$"
+       }
+       if j16 >= 0 && j16 < 22 {
+               return x[j16]  // ERROR "Proved IsInBounds$"
+       }
+       if j32 >= 0 && j32 < 22 {
+               return x[j32]  // ERROR "Proved IsInBounds$"
+       }
+       return 0
+}
+
+func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
+       if len(x) < 22 {
+               return 0
+       }
+       if j8 >= 0 && j8 < 22 {
+               return x[j8]  // ERROR "Proved IsInBounds$"
+       }
+       if j16 >= 0 && j16 < 22 {
+               return x[j16]  // ERROR "Proved IsInBounds$"
+       }
+       if j32 >= 0 && j32 < 22 {
+               return x[j32]  // ERROR "Proved IsInBounds$"
+       }
+       return 0
+}
+
+// Process fence-post implications through 32to64 extensions (issue #29964)
+func signExt32to64Fence(x []int, j int32) int {
+       if x[j] != 0 {
+               return 1
+       }
+       if j > 0 && x[j-1] != 0 {  // ERROR "Proved IsInBounds$"
+               return 1
+       }
+       return 0
+}
+
+func zeroExt32to64Fence(x []int, j uint32) int {
+       if x[j] != 0 {
+               return 1
+       }
+       if j > 0 && x[j-1] != 0 {  // ERROR "Proved IsInBounds$"
+               return 1
+       }
+       return 0
+}
+
 //go:noinline
 func useInt(a int) {
 }