qbit/go
1
0
Fork 0
mirror of https://github.com/golang/go synced 2024-11-26 17:46:57 -07:00
Code Releases Activity

cmd/compile: use transitive relations for slice len/cap in poset

Browse Source 
Currently, we keep track of slice len by mapping from slice ID to
len/cap SSA value. However, slice len/cap can have multiple SSA values,
so when updating fact table for slice len/cap, we only update in one
place.

Instead, we can take advantage of the transitive relations provided by
poset. So all duplicated slice lens are set as equal to one another.
When updating fact table for one, that fact will be reflected to all
others. The same mechanism is applied for slice cap.

Removes 15 bounds checks from std/cmd.

Fixes #42603

Change-Id: I32c07968824cc33765b1e441b3ae2c4b5f5997c3
Reviewed-on: https://go-review.googlesource.com/c/go/+/273670
Trust: Cuong Manh Le <cuong.manhle.vn@gmail.com>
Run-TryBot: Cuong Manh Le <cuong.manhle.vn@gmail.com>
TryBot-Result: Go Bot <gobot@golang.org>
Reviewed-by: Keith Randall <khr@golang.org>
This commit is contained in:
Cuong Manh Le 2020-11-28 02:46:00 +07:00
parent 6a40dd05d8
commit 5e804ba17d
2 changed files with 30 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/cmd/compile/internal/ssa/prove.go
View File

@ -778,7 +778,14 @@ func prove(f *Func) {
if ft.lens == nil { if ft.lens == nil {
ft.lens = map[ID]*Value{} ft.lens = map[ID]*Value{}
} }
ft.lens[v.Args[0].ID] = v // Set all len Values for the same slice as equal in the poset.
// The poset handles transitive relations, so Values related to
// any OpSliceLen for this slice will be correctly related to others.
if l, ok := ft.lens[v.Args[0].ID]; ok {
ft.update(b, v, l, signed, eq)
} else {
ft.lens[v.Args[0].ID] = v
}
ft.update(b, v, ft.zero, signed, gt|eq) ft.update(b, v, ft.zero, signed, gt|eq)
if v.Args[0].Op == OpSliceMake { if v.Args[0].Op == OpSliceMake {
if lensVars == nil { if lensVars == nil {
@ -790,7 +797,12 @@ func prove(f *Func) {
if ft.caps == nil { if ft.caps == nil {
ft.caps = map[ID]*Value{} ft.caps = map[ID]*Value{}
} }
ft.caps[v.Args[0].ID] = v // Same as case OpSliceLen above, but for slice cap.
if c, ok := ft.caps[v.Args[0].ID]; ok {
ft.update(b, v, c, signed, eq)
} else {
ft.caps[v.Args[0].ID] = v
}
ft.update(b, v, ft.zero, signed, gt|eq) ft.update(b, v, ft.zero, signed, gt|eq)
if v.Args[0].Op == OpSliceMake { if v.Args[0].Op == OpSliceMake {
if lensVars == nil { if lensVars == nil {

16
test/prove.go
View File

@ -629,6 +629,22 @@ func trans3(a, b []int, i int) {
_ = b[i] // ERROR "Proved IsInBounds$" _ = b[i] // ERROR "Proved IsInBounds$"
} }
func trans4(b []byte, x int) {
// Issue #42603: slice len/cap transitive relations.
switch x {
case 0:
if len(b) < 20 {
return
}
_ = b[:2] // ERROR "Proved IsSliceInBounds$"
case 1:
if len(b) < 40 {
return
}
_ = b[:2] // ERROR "Proved IsSliceInBounds$"
}
}
// Derived from nat.cmp // Derived from nat.cmp
func natcmp(x, y []uint) (r int) { func natcmp(x, y []uint) (r int) {
m := len(x) m := len(x)