@@ -2177,10 +2177,18 @@ func unsignedSubUnderflows(a, b uint64) bool {
21772177// checkForChunkedIndexBounds looks for index expressions of the form
21782178// A[i+delta] where delta < K and i <= len(A)-K. That is, this is a chunked
21792179// iteration where the index is not directly compared to the length.
2180- func checkForChunkedIndexBounds (ft * factsTable , b * Block , index , bound * Value ) bool {
2181- if bound .Op != OpSliceLen {
2180+ // if isReslice, then delta can be equal to K.
2181+ func checkForChunkedIndexBounds (ft * factsTable , b * Block , index , bound * Value , isReslice bool ) bool {
2182+ if bound .Op != OpSliceLen && bound .Op != OpSliceCap {
21822183 return false
21832184 }
2185+
2186+ // this is a slice bounds check against len or capacity,
2187+ // and refers back to a prior check against length, which
2188+ // will also work for the cap since that is not smaller
2189+ // than the length.
2190+
2191+ slice := bound .Args [0 ]
21842192 lim := ft .limits [index .ID ]
21852193 if lim .min < 0 {
21862194 return false
@@ -2206,22 +2214,25 @@ func checkForChunkedIndexBounds(ft *factsTable, b *Block, index, bound *Value) b
22062214 }
22072215 if ow := o .w ; ow .Op == OpAdd64 {
22082216 var lenOffset * Value
2209- if ow .Args [0 ] == bound {
2217+ if bound := ow .Args [0 ]; bound . Op == OpSliceLen && bound . Args [ 0 ] == slice {
22102218 lenOffset = ow .Args [1 ]
2211- } else if ow .Args [1 ] == bound {
2219+ } else if bound := ow .Args [1 ]; bound . Op == OpSliceLen && bound . Args [ 0 ] == slice {
22122220 lenOffset = ow .Args [0 ]
22132221 }
22142222 if lenOffset == nil || lenOffset .Op != OpConst64 {
22152223 continue
22162224 }
22172225 if K := - lenOffset .AuxInt ; K >= 0 {
22182226 or := o .r
2227+ if isReslice {
2228+ K ++
2229+ }
22192230 if or == lt {
22202231 or = lt | eq
22212232 K ++
2222- if K < 0 {
2223- continue
2224- }
2233+ }
2234+ if K < 0 { // We hate thinking about overflow
2235+ continue
22252236 }
22262237
22272238 if delta < K && or == lt | eq {
@@ -2345,12 +2356,19 @@ func addLocalFacts(ft *factsTable, b *Block) {
23452356 ft .update (b , v , v .Args [0 ].Args [2 ], signed , eq )
23462357 }
23472358 case OpIsInBounds :
2348- if checkForChunkedIndexBounds (ft , b , v .Args [0 ], v .Args [1 ]) {
2359+ if checkForChunkedIndexBounds (ft , b , v .Args [0 ], v .Args [1 ], false ) {
23492360 if b .Func .pass .debug > 0 {
23502361 b .Func .Warnl (v .Pos , "Proved %s for blocked indexing" , v .Op )
23512362 }
23522363 ft .booleanTrue (v )
23532364 }
2365+ case OpIsSliceInBounds :
2366+ if checkForChunkedIndexBounds (ft , b , v .Args [0 ], v .Args [1 ], true ) {
2367+ if b .Func .pass .debug > 0 {
2368+ b .Func .Warnl (v .Pos , "Proved %s for blocked reslicing" , v .Op )
2369+ }
2370+ ft .booleanTrue (v )
2371+ }
23542372 case OpPhi :
23552373 addLocalFactsPhi (ft , v )
23562374 }
0 commit comments