From 6d379add0fefcc17ed7b763078526800a3c1d705 Mon Sep 17 00:00:00 2001 From: Giovanni Bajo Date: Sun, 15 Apr 2018 16:03:30 +0200 Subject: [PATCH] cmd/compile: in prove, detect loops with negative increments To be effective, this also requires being able to relax constraints on min/max bound inclusiveness; they are now exposed through a flags, and prove has been updated to handle it correctly. Change-Id: I3490e54461b7b9de8bc4ae40d3b5e2fa2d9f0556 Reviewed-on: https://go-review.googlesource.com/104041 Run-TryBot: Giovanni Bajo TryBot-Result: Gobot Gobot Reviewed-by: David Chase --- src/cmd/compile/internal/ssa/loopbce.go | 61 +++++++++++++++++++++---- src/cmd/compile/internal/ssa/prove.go | 13 +++++- test/loopbce.go | 34 ++++++++++++++ 3 files changed, 96 insertions(+), 12 deletions(-) diff --git a/src/cmd/compile/internal/ssa/loopbce.go b/src/cmd/compile/internal/ssa/loopbce.go index 403aed6b20..d484d12a78 100644 --- a/src/cmd/compile/internal/ssa/loopbce.go +++ b/src/cmd/compile/internal/ssa/loopbce.go @@ -2,13 +2,21 @@ package ssa import "fmt" +type indVarFlags uint8 + +const ( + indVarMinExc indVarFlags = 1 << iota // minimum value is exclusive (default: inclusive) + indVarMaxInc // maximum value is inclusive (default: exclusive) +) + type indVar struct { ind *Value // induction variable inc *Value // increment, a constant nxt *Value // ind+inc variable - min *Value // minimum value. inclusive, - max *Value // maximum value. exclusive. + min *Value // minimum value, inclusive/exclusive depends on flags + max *Value // maximum value, inclusive/exclusive depends on flags entry *Block // entry block in the loop. + flags indVarFlags // Invariants: for all blocks dominated by entry: // min <= ind < max // min <= nxt <= max @@ -43,15 +51,22 @@ nextb: continue } + var flags indVarFlags var ind, max *Value // induction, and maximum entry := -1 // which successor of b enters the loop - // Check thet the control if it either ind < max or max > ind. - // TODO: Handle Leq64, Geq64. + // Check thet the control if it either ind />= ind. + // TODO: Handle 32-bit comparisons. switch b.Control.Op { + case OpLeq64: + flags |= indVarMaxInc + fallthrough case OpLess64: entry = 0 ind, max = b.Control.Args[0], b.Control.Args[1] + case OpGeq64: + flags |= indVarMaxInc + fallthrough case OpGreater64: entry = 0 ind, max = b.Control.Args[1], b.Control.Args[0] @@ -59,6 +74,11 @@ nextb: continue nextb } + // See if the arguments are reversed (i < len() <=> len() > i) + if max.Op == OpPhi { + ind, max = max, ind + } + // Check that the induction variable is a phi that depends on itself. if ind.Op != OpPhi { continue @@ -84,12 +104,24 @@ nextb: panic("unreachable") // one of the cases must be true from the above. } - // Expect the increment to be a positive constant. - // TODO: handle negative increment. - if inc.Op != OpConst64 || inc.AuxInt <= 0 { + // Expect the increment to be a constant. + if inc.Op != OpConst64 { continue } + // If the increment is negative, swap min/max and their flags + if inc.AuxInt <= 0 { + min, max = max, min + oldf := flags + flags = 0 + if oldf&indVarMaxInc == 0 { + flags |= indVarMinExc + } + if oldf&indVarMinExc == 0 { + flags |= indVarMaxInc + } + } + // Up to now we extracted the induction variable (ind), // the increment delta (inc), the temporary sum (nxt), // the mininum value (min) and the maximum value (max). @@ -126,8 +158,8 @@ nextb: } // 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 { + // if the increment is ±1 or when the limits are constants. + if inc.AuxInt != 1 && inc.AuxInt != -1 { ok := false if min.Op == OpConst64 && max.Op == OpConst64 { if max.AuxInt > min.AuxInt && max.AuxInt%inc.AuxInt == min.AuxInt%inc.AuxInt { // handle overflow @@ -140,6 +172,14 @@ nextb: } if f.pass.debug >= 1 { + mb1, mb2 := "[", "]" + if flags&indVarMinExc != 0 { + mb1 = "(" + } + if flags&indVarMaxInc == 0 { + mb2 = ")" + } + mlim1, mlim2 := fmt.Sprint(min.AuxInt), fmt.Sprint(max.AuxInt) if !min.isGenericIntConst() { if f.pass.debug >= 2 { @@ -155,7 +195,7 @@ nextb: mlim2 = "?" } } - b.Func.Warnl(b.Pos, "Induction variable: limits [%v,%v), increment %d", mlim1, mlim2, inc.AuxInt) + b.Func.Warnl(b.Pos, "Induction variable: limits %v%v,%v%v, increment %d", mb1, mlim1, mlim2, mb2, inc.AuxInt) } iv = append(iv, indVar{ @@ -165,6 +205,7 @@ nextb: min: min, max: max, entry: b.Succs[entry].b, + flags: flags, }) b.Logf("found induction variable %v (inc = %v, min = %v, max = %v)\n", ind, inc, min, max) } diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 536cfcebf0..0767be7d57 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -799,8 +799,17 @@ func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) { d |= unsigned } - addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq) - addRestrictions(b, ft, d, iv.ind, iv.max, lt) + if iv.flags&indVarMinExc == 0 { + addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq) + } else { + addRestrictions(b, ft, d, iv.min, iv.ind, lt) + } + + if iv.flags&indVarMaxInc == 0 { + addRestrictions(b, ft, d, iv.ind, iv.max, lt) + } else { + addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq) + } } // addBranchRestrictions updates the factsTables ft with the facts learned when diff --git a/test/loopbce.go b/test/loopbce.go index 95dd6ff58f..6ef183dea8 100644 --- a/test/loopbce.go +++ b/test/loopbce.go @@ -84,6 +84,22 @@ func g0b(a string) int { return x } +func g0c(a string) int { + x := 0 + for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment -1$" + x += int(a[i-1]) // ERROR "Proved IsInBounds$" + } + return x +} + +func g0d(a string) int { + x := 0 + for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment -1$" + x += int(a[i-1]) // ERROR "Proved IsInBounds$" + } + return x +} + func g1() int { a := "evenlength" x := 0 @@ -190,6 +206,24 @@ func k3(a [100]int) [100]int { return a } +func k3neg(a [100]int) [100]int { + for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment -1$" + a[i+9] = i + a[i+10] = i // ERROR "Proved IsInBounds$" + a[i+11] = i + } + return a +} + +func k3neg2(a [100]int) [100]int { + for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment -1$" + a[i+9] = i + a[i+10] = i // ERROR "Proved IsInBounds$" + a[i+11] = i + } + return a +} + func k4(a [100]int) [100]int { min := (-1) << 63 for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"