languages/go
languages/go
1
0
Fork 0
mirror of https://github.com/golang/go synced 2024-11-05 18:36:08 +00:00
Code Issues Projects Releases Packages Wiki Activity

cmd/compile: fix deriving from x+d >= w on overflow in prove pass

Browse source 
In the case of x+d >= w, where d and w are constants, we are
deriving x is within the bound of min=w-d and max=maxInt-d. When
there is an overflow (min >= max), we know only one of x >= min
or x <= max is true, and we derive this by excluding the other.
When excluding x >= min, we did not consider the equal case, so
we could incorrectly derive x <= max when x == min.

Fixes #29502.

Change-Id: Ia9f7d814264b1a3ddf78f52e2ce23377450e6e8a
Reviewed-on: https://go-review.googlesource.com/c/156019
Reviewed-by: David Chase <drchase@google.com>
This commit is contained in:
Cherry Zhang 2019-01-02 12:27:55 -05:00
parent 1f035d036c
commit 2e217fa726
2 changed files with 29 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/cmd/compile/internal/ssa/prove.go
View file

@ -197,6 +197,9 @@ func newFactsTable(f *Func) *factsTable {
// update updates the set of relations between v and w in domain d
// restricting it to r.
func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
if parent.Func.pass.debug > 2 {
parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
}
// No need to do anything else if we already found unsat.
if ft.unsat {
return
@ -234,6 +237,9 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
panic("unknown relation")
}
if !ok {
if parent.Func.pass.debug > 2 {
parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
}
ft.unsat = true
return
}
@ -260,6 +266,9 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
ft.facts[p] = oldR & r
// If this relation is not satisfiable, mark it and exit right away
if oldR&r == 0 {
if parent.Func.pass.debug > 2 {
parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
}
ft.unsat = true
return
}
@ -361,7 +370,7 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
lim = old.intersect(lim)
ft.limits[v.ID] = lim
if v.Block.Func.pass.debug > 2 {
v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s %s", parent, v, w, r, lim.String())
}
if lim.min > lim.max || lim.umin > lim.umax {
ft.unsat = true
@ -442,7 +451,7 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
if r == gt || r == gt|eq {
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)
parent.Func.Warnl(parent.Pos, "x+d %s w; x:%v %v delta:%v w:%v d:%v", r, x, parent.String(), delta, w.AuxInt, d)
}
if !w.isGenericIntConst() {
// If we know that x+delta > w but w is not constant, we can derive:
@ -503,8 +512,10 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
// 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)
if r&eq == 0 || l.max < min {
// x>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)

14
test/prove.go
View file

@ -488,6 +488,20 @@ func f18(b []int, x int, y uint) {
}
}
func f19() (e int64, err error) {
// Issue 29502: slice[:0] is incorrectly disproved.
var stack []int64
stack = append(stack, 123)
if len(stack) > 1 {
panic("too many elements")
}
last := len(stack) - 1
e = stack[last]
// Buggy compiler prints "Disproved Geq64" for the next line.
stack = stack[:last] // ERROR "Proved IsSliceInBounds"
return e, nil
}
func sm1(b []int, x int) {
// Test constant argument to slicemask.
useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"