mirror of
https://github.com/golang/go
synced 2024-09-04 23:44:16 +00:00
cmd/compile: add fence-post implications to prove
This adds four new deductions to the prove pass, all related to adding or subtracting one from a value. This is the first hint of actual arithmetic relations in the prove pass. The most effective of these is x-1 >= w && x > min ⇒ x > w This helps eliminate bounds checks in code like if x > 0 { // do something with s[x-1] } Altogether, these deductions prove an additional 260 branches in std and cmd. Furthermore, they will let us eliminate some tricky compiler-inserted panics in the runtime that are interfering with static analysis. Fixes #23354. Change-Id: I7088223e0e0cd6ff062a75c127eb4bb60e6dce02 Reviewed-on: https://go-review.googlesource.com/87480 Reviewed-by: Keith Randall <khr@golang.org> Reviewed-by: Alexandru Moșoi <alexandru@mosoi.ro>
This commit is contained in:
parent
941fc129e2
commit
6436270dad
|
@ -305,6 +305,53 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
|
|||
v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
|
||||
}
|
||||
}
|
||||
|
||||
// Process fence-post implications.
|
||||
//
|
||||
// First, make the condition > or >=.
|
||||
if r == lt || r == lt|eq {
|
||||
v, w = w, v
|
||||
r = reverseBits[r]
|
||||
}
|
||||
switch r {
|
||||
case gt:
|
||||
if x, delta := isConstDelta(v); x != nil && delta == 1 {
|
||||
// x+1 > w ⇒ x >= w
|
||||
//
|
||||
// This is useful for eliminating the
|
||||
// growslice branch of append.
|
||||
ft.update(parent, x, w, d, gt|eq)
|
||||
} else if x, delta := isConstDelta(w); x != nil && delta == -1 {
|
||||
// v > x-1 ⇒ v >= x
|
||||
ft.update(parent, v, x, d, gt|eq)
|
||||
}
|
||||
case gt | eq:
|
||||
if x, delta := isConstDelta(v); x != nil && delta == -1 {
|
||||
// x-1 >= w && x > min ⇒ x > w
|
||||
//
|
||||
// Useful for i > 0; s[i-1].
|
||||
lim, ok := ft.limits[x.ID]
|
||||
if ok && lim.min > opMin[v.Op] {
|
||||
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] {
|
||||
ft.update(parent, v, x, d, gt)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
var opMin = map[Op]int64{
|
||||
OpAdd64: math.MinInt64, OpSub64: math.MinInt64,
|
||||
OpAdd32: math.MinInt32, OpSub32: math.MinInt32,
|
||||
}
|
||||
|
||||
var opMax = map[Op]int64{
|
||||
OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64,
|
||||
OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
|
||||
}
|
||||
|
||||
// isNonNegative returns true if v is known to be non-negative.
|
||||
|
@ -803,3 +850,29 @@ func isNonNegative(v *Value) bool {
|
|||
}
|
||||
return false
|
||||
}
|
||||
|
||||
// isConstDelta returns non-nil if v is equivalent to w+delta (signed).
|
||||
func isConstDelta(v *Value) (w *Value, delta int64) {
|
||||
cop := OpConst64
|
||||
switch v.Op {
|
||||
case OpAdd32, OpSub32:
|
||||
cop = OpConst32
|
||||
}
|
||||
switch v.Op {
|
||||
case OpAdd64, OpAdd32:
|
||||
if v.Args[0].Op == cop {
|
||||
return v.Args[1], v.Args[0].AuxInt
|
||||
}
|
||||
if v.Args[1].Op == cop {
|
||||
return v.Args[0], v.Args[1].AuxInt
|
||||
}
|
||||
case OpSub64, OpSub32:
|
||||
if v.Args[1].Op == cop {
|
||||
aux := v.Args[1].AuxInt
|
||||
if aux != -aux { // Overflow; too bad
|
||||
return v.Args[0], -aux
|
||||
}
|
||||
}
|
||||
}
|
||||
return nil, 0
|
||||
}
|
||||
|
|
|
@ -506,6 +506,60 @@ func lim1(x, y, z int) {
|
|||
}
|
||||
}
|
||||
|
||||
// fence1–4 correspond to the four fence-post implications.
|
||||
|
||||
func fence1(b []int, x, y int) {
|
||||
// Test proofs that rely on fence-post implications.
|
||||
if x+1 > y {
|
||||
if x < y { // ERROR "Disproved Less64$"
|
||||
return
|
||||
}
|
||||
}
|
||||
if len(b) < cap(b) {
|
||||
// This eliminates the growslice path.
|
||||
b = append(b, 1) // ERROR "Disproved Greater64$"
|
||||
}
|
||||
}
|
||||
|
||||
func fence2(x, y int) {
|
||||
if x-1 < y {
|
||||
if x > y { // ERROR "Disproved Greater64$"
|
||||
return
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
func fence3(b []int, x, y int64) {
|
||||
if x-1 >= y {
|
||||
if x <= y { // Can't prove because x may have wrapped.
|
||||
return
|
||||
}
|
||||
}
|
||||
|
||||
if x != math.MinInt64 && x-1 >= y {
|
||||
if x <= y { // ERROR "Disproved Leq64$"
|
||||
return
|
||||
}
|
||||
}
|
||||
|
||||
if n := len(b); n > 0 {
|
||||
b[n-1] = 0 // ERROR "Proved IsInBounds$"
|
||||
}
|
||||
}
|
||||
|
||||
func fence4(x, y int64) {
|
||||
if x >= y+1 {
|
||||
if x <= y {
|
||||
return
|
||||
}
|
||||
}
|
||||
if y != math.MaxInt64 && x >= y+1 {
|
||||
if x <= y { // ERROR "Disproved Leq64$"
|
||||
return
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//go:noinline
|
||||
func useInt(a int) {
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue