mirror of
https://github.com/golang/go
synced 2024-11-02 08:01:26 +00:00
cmd/compile: derive unsigned limits from signed limits in prove
This adds a few simple deductions to the prove pass' fact table to derive unsigned concrete limits from signed concrete limits where possible. This tweak lets the pass prove 70 additional branch conditions in std and cmd. This is based on a comment from the recently-deleted factsTable.get: "// TODO: also use signed data if lim.min >= 0". Change-Id: Ib4340249e7733070f004a0aa31254adf5df8a392 Reviewed-on: https://go-review.googlesource.com/87479 Reviewed-by: Alexandru Moșoi <alexandru@mosoi.ro> Reviewed-by: Keith Randall <khr@golang.org>
This commit is contained in:
parent
669db2cef5
commit
941fc129e2
2 changed files with 36 additions and 2 deletions
|
@ -248,6 +248,16 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
|
|||
lim.min = c
|
||||
lim.max = c
|
||||
}
|
||||
if lim.min >= 0 {
|
||||
// int(x) >= 0 && int(x) >= N ⇒ uint(x) >= N
|
||||
lim.umin = uint64(lim.min)
|
||||
}
|
||||
if lim.max != noLimit.max && old.min >= 0 && lim.max >= 0 {
|
||||
// 0 <= int(x) <= N ⇒ 0 <= uint(x) <= N
|
||||
// This is for a max update, so the lower bound
|
||||
// comes from what we already know (old).
|
||||
lim.umax = uint64(lim.max)
|
||||
}
|
||||
case unsigned:
|
||||
var uc uint64
|
||||
switch w.Op {
|
||||
|
@ -281,6 +291,9 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
|
|||
lim.umin = uc
|
||||
lim.umax = uc
|
||||
}
|
||||
// We could use the contrapositives of the
|
||||
// signed implications to derive signed facts,
|
||||
// but it turns out not to matter.
|
||||
}
|
||||
ft.limitStack = append(ft.limitStack, limitFact{v.ID, old})
|
||||
lim = old.intersect(lim)
|
||||
|
|
|
@ -479,12 +479,33 @@ func sm1(b []int, x int) {
|
|||
// Test constant argument to slicemask.
|
||||
useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
|
||||
// Test non-constant argument with known limits.
|
||||
// Right now prove only uses the unsigned limit.
|
||||
if uint(cap(b)) > 10 {
|
||||
if cap(b) > 10 {
|
||||
useSlice(b[2:]) // ERROR "Proved slicemask not needed$"
|
||||
}
|
||||
}
|
||||
|
||||
func lim1(x, y, z int) {
|
||||
// Test relations between signed and unsigned limits.
|
||||
if x > 5 {
|
||||
if uint(x) > 5 { // ERROR "Proved Greater64U$"
|
||||
return
|
||||
}
|
||||
}
|
||||
if y >= 0 && y < 4 {
|
||||
if uint(y) > 4 { // ERROR "Disproved Greater64U$"
|
||||
return
|
||||
}
|
||||
if uint(y) < 5 { // ERROR "Proved Less64U$"
|
||||
return
|
||||
}
|
||||
}
|
||||
if z < 4 {
|
||||
if uint(z) > 4 { // Not provable without disjunctions.
|
||||
return
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//go:noinline
|
||||
func useInt(a int) {
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue