Skip to content

Commit

Permalink
cmd/compile: in prove, fix fence-post implications for unsigned domain
Browse files Browse the repository at this point in the history
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 <[email protected]>
  • Loading branch information
rasky committed Aug 31, 2018
1 parent 8a2b5f1 commit 09ea3c0
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 3 deletions.
9 changes: 7 additions & 2 deletions src/cmd/compile/internal/ssa/prove.go
Original file line number Diff line number Diff line change
Expand Up @@ -425,13 +425,13 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
//
// Useful for i > 0; s[i-1].
lim, ok := ft.limits[x.ID]
if ok && lim.min > opMin[v.Op] {
if ok && ((d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0)) {
ft.update(parent, x, w, d, gt)
}
} else if x, delta := isConstDelta(w); x != nil && delta == 1 {
// v >= x+1 && x < max ⇒ v > x
lim, ok := ft.limits[x.ID]
if ok && lim.max < opMax[w.Op] {
if ok && ((d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op])) {
ft.update(parent, v, x, d, gt)
}
}
Expand Down Expand Up @@ -527,6 +527,11 @@ var opMax = map[Op]int64{
OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
}

var opUMax = map[Op]uint64{
OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64,
OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32,
}

// isNonNegative reports whether v is known to be non-negative.
func (ft *factsTable) isNonNegative(v *Value) bool {
if isNonNegative(v) {
Expand Down
24 changes: 24 additions & 0 deletions test/fixedbugs/issue27289.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
// 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)
}
4 changes: 3 additions & 1 deletion test/prove.go
Original file line number Diff line number Diff line change
Expand Up @@ -542,7 +542,7 @@ func fence2(x, y int) {
}
}

func fence3(b []int, x, y int64) {
func fence3(b, c []int, x, y int64) {
if x-1 >= y {
if x <= y { // Can't prove because x may have wrapped.
return
Expand All @@ -555,6 +555,8 @@ func fence3(b []int, x, y int64) {
}
}

c[len(c)-1] = 0 // Can't prove because len(c) might be 0

if n := len(b); n > 0 {
b[n-1] = 0 // ERROR "Proved IsInBounds$"
}
Expand Down

0 comments on commit 09ea3c0

Please sign in to comment.