Skip to content

Commit

Permalink
cmd/compile: teach prove to handle expressions like len(s)-delta
Browse files Browse the repository at this point in the history 
When a loop has bound len(s)-delta, findIndVar detected it and
returned len(s) as (conservative) upper bound. This little lie
allowed loopbce to drop bound checks.

It is obviously more generic to teach prove about relations like
x+d<w for non-constant "w"; we already handled the case for
constant "w", so we just want to learn that if d<0, then x+d<w
proves that x<w.

To be able to remove the code from findIndVar, we also need
to teach prove that len() and cap() are always non-negative.

This CL allows to prove 633 more checks in cmd+std. Most
of them are cases where the code was already testing before
accessing a slice but the compiler didn't know it. For instance,
take strings.HasSuffix:

    func HasSuffix(s, suffix string) bool {
        return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
    }

When suffix is a literal string, the compiler now understands
that the explicit check is enough to not emit a slice check.

I also found a loopbce test that was incorrectly
written to detect an overflow but had a off-by-one (on the
conservative side), so it unexpectly passed with this CL; I
changed it to really trigger the overflow as intended.

Change-Id: Ib5abade337db46b8811425afebad4719b6e46c4a
Reviewed-on: https://go-review.googlesource.com/105635
Run-TryBot: Giovanni Bajo <[email protected]>
TryBot-Result: Gobot Gobot <[email protected]>
Reviewed-by: David Chase <[email protected]>
  • Loading branch information
@rasky
rasky committed Apr 29, 2018
1 parent 6d379ad commit e0d37a3
Show file tree
Hide file tree
Showing 4 changed files with 147 additions and 69 deletions.
7 changes: 0 additions & 7 deletions src/cmd/compile/internal/ssa/loopbce.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,13 +150,6 @@ nextb:
continue
}

// If max is c + SliceLen with c <= 0 then we drop c.
// Makes sure c + SliceLen doesn't overflow when SliceLen == 0.
// TODO: save c as an offset from max.
if w, c := dropAdd64(max); (w.Op == OpStringLen || w.Op == OpSliceLen) && 0 >= c && -c >= 0 {
max = w
}

// We can only guarantee that the loops runs within limits of induction variable
// if the increment is ±1 or when the limits are constants.
if inc.AuxInt != 1 && inc.AuxInt != -1 {
Expand Down
145 changes: 86 additions & 59 deletions src/cmd/compile/internal/ssa/prove.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -389,70 +389,78 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
}
}

// Process: x+delta > w (with delta,w constants)
//
// We want to derive: x+delta > w ⇒ x > w-delta
//
// We do this for signed numbers for now, as that allows to prove many
// accesses to slices in loops.
//
// From x+delta > w, we compute (using integers of the correct size):
// min = w - delta
// max = MaxInt - delta
//
// And we prove that:
// if min<max: min < x AND x <= max
// if min>max: min < x OR x <= max
//
// This is always correct, even in case of overflow.
//
// If the initial fact is x+delta >= w instead, the derived conditions are:
// if min<max: min <= x AND x <= max
// if min>max: min <= x OR x <= max
//
// Notice the conditions for max are still <=, as they handle overflows.
// Process: x+delta > w (with delta constant)
// Only signed domain for now (useful for accesses to slices in loops).
if r == gt || r == gt|eq {
if x, delta := isConstDelta(v); x != nil && w.isGenericIntConst() && d == signed {
if x, delta := isConstDelta(v); x != nil && d == signed {
if parent.Func.pass.debug > 1 {
parent.Func.Warnl(parent.Pos, "x+d >= w; x:%v %v delta:%v w:%v d:%v", x, parent.String(), delta, w.AuxInt, d)
}

var min, max int64
var vmin, vmax *Value
switch x.Type.Size() {
case 8:
min = w.AuxInt - delta
max = int64(^uint64(0)>>1) - delta

vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)

case 4:
min = int64(int32(w.AuxInt) - int32(delta))
max = int64(int32(^uint32(0)>>1) - int32(delta))

vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)

default:
panic("unimplemented")
}

if min < max {
// Record that x > min and max >= x
ft.update(parent, x, vmin, d, r)
ft.update(parent, vmax, x, d, r|eq)
if !w.isGenericIntConst() {
// If we know that x+delta > w but w is not constant, we can derive:
// if delta < 0 and x > MinInt - delta, then x > w (because x+delta cannot underflow)
// This is useful for loops with bounds "len(slice)-K" (delta = -K)
if l, has := ft.limits[x.ID]; has && delta < 0 {
if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) ||
(x.Type.Size() == 4 && l.min >= math.MinInt32-delta) {
ft.update(parent, x, w, signed, r)
}
}
} else {
// We know that either x>min OR x<=max. factsTable cannot record OR conditions,
// so let's see if we can already prove that one of them is false, in which case
// the other must be true
if l, has := ft.limits[x.ID]; has {
if l.max <= min {
// x>min is impossible, so it must be x<=max
ft.update(parent, vmax, x, d, r|eq)
} else if l.min > max {
// x<=max is impossible, so it must be x>min
ft.update(parent, x, vmin, d, r)
// With w,delta constants, we want to derive: x+delta > w ⇒ x > w-delta
//
// We compute (using integers of the correct size):
// min = w - delta
// max = MaxInt - delta
//
// And we prove that:
// if min<max: min < x AND x <= max
// if min>max: min < x OR x <= max
//
// This is always correct, even in case of overflow.
//
// If the initial fact is x+delta >= w instead, the derived conditions are:
// if min<max: min <= x AND x <= max
// if min>max: min <= x OR x <= max
//
// Notice the conditions for max are still <=, as they handle overflows.
var min, max int64
var vmin, vmax *Value
switch x.Type.Size() {
case 8:
min = w.AuxInt - delta
max = int64(^uint64(0)>>1) - delta

vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)

case 4:
min = int64(int32(w.AuxInt) - int32(delta))
max = int64(int32(^uint32(0)>>1) - int32(delta))

vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)

default:
panic("unimplemented")
}

if min < max {
// Record that x > min and max >= x
ft.update(parent, x, vmin, d, r)
ft.update(parent, vmax, x, d, r|eq)
} else {
// We know that either x>min OR x<=max. factsTable cannot record OR conditions,
// so let's see if we can already prove that one of them is false, in which case
// the other must be true
if l, has := ft.limits[x.ID]; has {
if l.max <= min {
// x>min is impossible, so it must be x<=max
ft.update(parent, vmax, x, d, r|eq)
} else if l.min > max {
// x<=max is impossible, so it must be x>min
ft.update(parent, x, vmin, d, r)
}
}
}
}
Expand Down Expand Up @@ -661,24 +669,43 @@ func prove(f *Func) {
ft := newFactsTable()

// Find length and capacity ops.
var zero *Value
for _, b := range f.Blocks {
for _, v := range b.Values {
// If we found a zero constant, save it (so we don't have
// to build one later).
if zero == nil && v.Op == OpConst64 && v.AuxInt == 0 {
zero = v
}
if v.Uses == 0 {
// We don't care about dead values.
// (There can be some that are CSEd but not removed yet.)
continue
}
switch v.Op {
case OpStringLen:
if zero == nil {
zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
}
ft.update(b, v, zero, signed, gt|eq)
case OpSliceLen:
if ft.lens == nil {
ft.lens = map[ID]*Value{}
}
ft.lens[v.Args[0].ID] = v
if zero == nil {
zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
}
ft.update(b, v, zero, signed, gt|eq)
case OpSliceCap:
if ft.caps == nil {
ft.caps = map[ID]*Value{}
}
ft.caps[v.Args[0].ID] = v
if zero == nil {
zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
}
ft.update(b, v, zero, signed, gt|eq)
}
}
}
Expand Down
25 changes: 24 additions & 1 deletion test/loopbce.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,22 @@ func g0d(a string) int {
return x
}

func g0e(a string) int {
x := 0
for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment -1$"
x += int(a[i]) // ERROR "Proved IsInBounds$"
}
return x
}

func g0f(a string) int {
x := 0
for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment -1$"
x += int(a[i]) // ERROR "Proved IsInBounds$"
}
return x
}

func g1() int {
a := "evenlength"
x := 0
Expand Down Expand Up @@ -265,7 +281,14 @@ func nobce2(a string) {
useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
}
for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
// tests an overflow of StringLen-MinInt64
useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
}
j := int64(len(a)) - 123
for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
}
for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
useString(a[i:])
}
}
Expand Down
39 changes: 37 additions & 2 deletions test/prove.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ func f1b(a []int, i int, j uint) int {
if i >= 10 && i < len(a) {
return a[i] // ERROR "Proved IsInBounds$"
}
if i >= 10 && i < len(a) { // todo: handle this case
return a[i-10]
if i >= 10 && i < len(a) {
return a[i-10] // ERROR "Proved IsInBounds$"
}
if j < uint(len(a)) {
return a[j] // ERROR "Proved IsInBounds$"
Expand Down Expand Up @@ -613,6 +613,41 @@ func trans3(a, b []int, i int) {
_ = b[i] // ERROR "Proved IsInBounds$"
}

// Derived from nat.cmp
func natcmp(x, y []uint) (r int) {
m := len(x)
n := len(y)
if m != n || m == 0 {
return
}

i := m - 1
for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment -1"
x[i] == // ERROR "Proved IsInBounds$"
y[i] { // ERROR "Proved IsInBounds$"
i--
}

switch {
case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
y[i]: // ERROR "Proved IsInBounds$"
r = -1
case x[i] > // ERROR "Proved IsInBounds$"
y[i]: // ERROR "Proved IsInBounds$"
r = 1
}
return
}

func suffix(s, suffix string) bool {
// todo, we're still not able to drop the bound check here in the general case
return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
}

func constsuffix(s string) bool {
return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
}

//go:noinline
func useInt(a int) {
}
Expand Down

0 comments on commit e0d37a3

Please sign in to comment.