diff options
| -rw-r--r-- | src/cmd/compile/internal/ssa/prove.go | 24 | ||||
| -rw-r--r-- | test/loopbce.go | 6 | ||||
| -rw-r--r-- | test/prove.go | 10 |
3 files changed, 23 insertions, 17 deletions
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index c9f75daa67..1083874100 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -2187,24 +2187,22 @@ func (ft *factsTable) detectSubRelations(v *Value) { return // x-y might overflow } - // Subtracting a positive number only makes - // things smaller. - if yLim.min >= 0 { + // Subtracting a positive non-zero number only makes + // things smaller. If it's positive or zero, it might + // also do nothing (x-0 == v). + if yLim.min > 0 { + ft.update(v.Block, v, x, signed, lt) + } else if yLim.min == 0 { ft.update(v.Block, v, x, signed, lt|eq) - // TODO: is this worth it? - //if yLim.min > 0 { - // ft.update(v.Block, v, x, signed, lt) - //} } // Subtracting a number from a bigger one - // can't go below 0. - if ft.orderS.OrderedOrEqual(y, x) { + // can't go below 1. If the numbers might be + // equal, then it can't go below 0. + if ft.orderS.Ordered(y, x) { + ft.signedMin(v, 1) + } else if ft.orderS.OrderedOrEqual(y, x) { ft.setNonNegative(v) - // TODO: is this worth it? - //if ft.orderS.Ordered(y, x) { - // ft.signedMin(v, 1) - //} } } diff --git a/test/loopbce.go b/test/loopbce.go index aabd56c682..ca09e7e7f7 100644 --- a/test/loopbce.go +++ b/test/loopbce.go @@ -17,8 +17,8 @@ func f0a(a []int) int { func f0b(a []int) int { x := 0 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$" - b := a[i:] // ERROR "Proved IsSliceInBounds$" - x += b[0] + b := a[i:] // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$" + x += b[0] // ERROR "Proved IsInBounds$" } return x } @@ -417,7 +417,7 @@ func bce1() { func nobce2(a string) { for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" - useString(a[i:]) // ERROR "Proved IsSliceInBounds$" + useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$" } for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed" diff --git a/test/prove.go b/test/prove.go index e04b510e17..e12b6087d3 100644 --- a/test/prove.go +++ b/test/prove.go @@ -2552,7 +2552,7 @@ func swapbound(v []int) { for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable" v[i], // ERROR "Proved IsInBounds" v[len(v)-1-i] = // ERROR "Proved IsInBounds" - v[len(v)-1-i], + v[len(v)-1-i], // ERROR "Proved IsInBounds" v[i] // ERROR "Proved IsInBounds" } } @@ -2726,6 +2726,14 @@ func issue76688(x, y uint64) uint64 { return x * y } +func issue76429(s []byte, k int) byte { + if k < 0 || k >= len(s) { + return 0 + } + s = s[k:] // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed" + return s[0] // ERROR "Proved IsInBounds" +} + //go:noinline func prove(x int) { } |