cmd/compile: teach prove about len's & cap's max based on the element size

Change-Id: I88056fada1ff488c199fce54cf737dbdd091214d
Reviewed-on: https://go-review.googlesource.com/c/go/+/695095
Auto-Submit: Jorropo <jorropo.pgm@gmail.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: David Chase <drchase@google.com>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Keith Randall <khr@golang.org>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index b9b5d3386d7b1c733add377f657a3f472bf25623..309229b4d753b7268dcc3bdc3d995ccbdba964f0 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -1619,7 +1619,16 @@ func initLimit(v *Value) limit {
                lim = lim.unsignedMax(1)
 
        // length operations
-       case OpStringLen, OpSliceLen, OpSliceCap:
+       case OpSliceLen, OpSliceCap:
+               f := v.Block.Func
+               elemSize := uint64(v.Args[0].Type.Elem().Size())
+               if elemSize > 0 {
+                       heapSize := uint64(1)<<(uint64(f.Config.PtrSize)*8) - 1
+                       maximumElementsFittingInHeap := heapSize / elemSize
+                       lim = lim.unsignedMax(maximumElementsFittingInHeap)
+               }
+               fallthrough
+       case OpStringLen:
                lim = lim.signedMin(0)
        }
 

diff --git a/test/prove.go b/test/prove.go
index ef7690bbde6a3720229c607f2242866dae3cb7ad..70a27865cfd7c32805a5edeee173bd9fa5c0badc 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -2330,6 +2330,18 @@ func issue74473(s []uint) {
        }
 }
 
+func setCapMaxBasedOnElementSize(x []uint64) int {
+       c := uintptr(cap(x))
+       max := ^uintptr(0) >> 3
+       if c > max { // ERROR "Disproved Less"
+               return 42
+       }
+       if c <= max { // ERROR "Proved Leq"
+               return 1337
+       }
+       return 0
+}
+
 //go:noinline
 func useInt(a int) {
 }