mirror of
https://github.com/golang/go
synced 2024-11-14 07:40:21 -07:00
09ea3c08e8
Fence-post implications of the form "x-1 >= w && x > min ⇒ x > w" were not correctly handling unsigned domain, by always checking signed limits. This bug was uncovered once we taught prove that len(x) is always >= 0 in the signed domain. In the code being miscompiled (s[len(s)-1]), prove checks whether len(s)-1 >= len(s) in the unsigned domain; if it proves that this is always false, it can remove the bound check. Notice that len(s)-1 >= len(s) can be true for len(s) = 0 because of the wrap-around, so this is something prove should not be able to deduce. But because of the bug, the gate condition for the fence-post implication was len(s) > MinInt64 instead of len(s) > 0; that condition would be good in the signed domain but not in the unsigned domain. And since in CL105635 we taught prove that len(s) >= 0, the condition incorrectly triggered (len(s) >= 0 > MinInt64) and things were going downfall. Fixes #27251 Fixes #27289 Change-Id: I3dbcb1955ac5a66a0dcbee500f41e8d219409be5 Reviewed-on: https://go-review.googlesource.com/132495 Reviewed-by: Keith Randall <khr@golang.org>
25 lines
437 B
Go
25 lines
437 B
Go
// run
|
|
|
|
// Copyright 2018 The Go Authors. All rights reserved.
|
|
// Use of this source code is governed by a BSD-style
|
|
// license that can be found in the LICENSE file.
|
|
|
|
// Make sure we don't prove that the bounds check failure branch is unreachable.
|
|
|
|
package main
|
|
|
|
//go:noinline
|
|
func f(a []int) {
|
|
_ = a[len(a)-1]
|
|
}
|
|
|
|
func main() {
|
|
defer func() {
|
|
if err := recover(); err != nil {
|
|
return
|
|
}
|
|
panic("f should panic")
|
|
}()
|
|
f(nil)
|
|
}
|