From 09ea3c08e8fd1915515383f8cb4c0bb237d2b87d Mon Sep 17 00:00:00 2001 From: Giovanni Bajo Date: Fri, 31 Aug 2018 02:15:26 +0200 Subject: [PATCH] cmd/compile: in prove, fix fence-post implications for unsigned domain MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/cmd/compile/internal/ssa/prove.go | 9 +++++++-- test/fixedbugs/issue27289.go | 24 ++++++++++++++++++++++++ test/prove.go | 4 +++- 3 files changed, 34 insertions(+), 3 deletions(-) create mode 100644 test/fixedbugs/issue27289.go diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index c20f8b7ebc24f..af2b9ef0ed79c 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -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) } } @@ -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) { diff --git a/test/fixedbugs/issue27289.go b/test/fixedbugs/issue27289.go new file mode 100644 index 0000000000000..293b9d005570f --- /dev/null +++ b/test/fixedbugs/issue27289.go @@ -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) +} diff --git a/test/prove.go b/test/prove.go index 45cee9e8b5803..79256893b3604 100644 --- a/test/prove.go +++ b/test/prove.go @@ -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 @@ -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$" }