qbit/go
1
0
Fork 0
mirror of https://github.com/golang/go synced 2024-11-18 11:44:45 -07:00
Code Releases Activity

cmd/compile: derive len/cap relations in factsTable.update

Browse Source 
Currently, the prove pass derives implicit relations between len and
cap in the code that adds branch conditions. This is fine right now
because that's the only place we can encounter len and cap, but we're
about to add a second way to add assertions to the facts table that
can also produce facts involving len and cap.

Prepare for this by moving the fact derivation from updateRestrictions
(where it only applies on branches) to factsTable.update, which can
derive these facts no matter where the root facts come from.

Passes toolstash -cmp.

Change-Id: If09692d9eb98ffaa93f4cfa58ed2d8ba0887c111
Reviewed-on: https://go-review.googlesource.com/102602
Run-TryBot: Austin Clements <austin@google.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: David Chase <drchase@google.com>
This commit is contained in:
Austin Clements 2018-03-23 17:25:26 -04:00
parent 8d8f620f68
commit 4816eface1
1 changed files with 31 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -369,6 +369,37 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
}
}
// Derived facts below here are only about numbers.
if d != signed && d != unsigned {
return
}
// Additional facts we know given the relationship between len and cap.
//
// TODO: Since prove now derives transitive relations, it
// should be sufficient to learn that len(w) <= cap(w) at the
// beginning of prove where we look for all len/cap ops.
if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
// len(s) > w implies cap(s) > w
// len(s) >= w implies cap(s) >= w
// len(s) == w implies cap(s) >= w
ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
}
if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
// same, length on the RHS.
ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
}
if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
// cap(s) < w implies len(s) < w
// cap(s) <= w implies len(s) <= w
// cap(s) == w implies len(s) <= w
ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
}
if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
// same, capacity on the RHS.
ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
}
// Process fence-post implications.
//
// First, make the condition > or >=.
@ -931,31 +962,6 @@ func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r rel
continue
}
ft.update(parent, v, w, i, r)
// Additional facts we know given the relationship between len and cap.
if i != signed && i != unsigned {
continue
}
if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
// len(s) > w implies cap(s) > w
// len(s) >= w implies cap(s) >= w
// len(s) == w implies cap(s) >= w
ft.update(parent, ft.caps[v.Args[0].ID], w, i, r|gt)
}
if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
// same, length on the RHS.
ft.update(parent, v, ft.caps[w.Args[0].ID], i, r|lt)
}
if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
// cap(s) < w implies len(s) < w
// cap(s) <= w implies len(s) <= w
// cap(s) == w implies len(s) <= w
ft.update(parent, ft.lens[v.Args[0].ID], w, i, r|lt)
}
if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
// same, capacity on the RHS.
ft.update(parent, v, ft.lens[w.Args[0].ID], i, r|gt)
}
}
}