Commit b16463c9 authored by Giovanni Bajo's avatar Giovanni Bajo

cmd/compile: in prove, give a different name to each poset

Instead of using a two-slot array and having to remember which
index is the signed poset, and which is the unsigned one, just
use two different variables.

Change-Id: Ic7f7676436c51bf43a182e999a926f8b7f69434b
Reviewed-on: https://go-review.googlesource.com/c/go/+/196678Reviewed-by: default avatarKeith Randall <khr@golang.org>
parent e4c39259
...@@ -164,7 +164,8 @@ type factsTable struct { ...@@ -164,7 +164,8 @@ type factsTable struct {
// order is a couple of partial order sets that record information // order is a couple of partial order sets that record information
// about relations between SSA values in the signed and unsigned // about relations between SSA values in the signed and unsigned
// domain. // domain.
order [2]*poset orderS *poset
orderU *poset
// known lower and upper bounds on individual values. // known lower and upper bounds on individual values.
limits map[ID]limit limits map[ID]limit
...@@ -187,10 +188,10 @@ var checkpointBound = limitFact{} ...@@ -187,10 +188,10 @@ var checkpointBound = limitFact{}
func newFactsTable(f *Func) *factsTable { func newFactsTable(f *Func) *factsTable {
ft := &factsTable{} ft := &factsTable{}
ft.order[0] = f.newPoset() // signed ft.orderS = f.newPoset()
ft.order[1] = f.newPoset() // unsigned ft.orderU = f.newPoset()
ft.order[0].SetUnsigned(false) ft.orderS.SetUnsigned(false)
ft.order[1].SetUnsigned(true) ft.orderU.SetUnsigned(true)
ft.facts = make(map[pair]relation) ft.facts = make(map[pair]relation)
ft.stack = make([]fact, 4) ft.stack = make([]fact, 4)
ft.limits = make(map[ID]limit) ft.limits = make(map[ID]limit)
...@@ -221,23 +222,23 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) { ...@@ -221,23 +222,23 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
if d == signed || d == unsigned { if d == signed || d == unsigned {
var ok bool var ok bool
idx := 0 order := ft.orderS
if d == unsigned { if d == unsigned {
idx = 1 order = ft.orderU
} }
switch r { switch r {
case lt: case lt:
ok = ft.order[idx].SetOrder(v, w) ok = order.SetOrder(v, w)
case gt: case gt:
ok = ft.order[idx].SetOrder(w, v) ok = order.SetOrder(w, v)
case lt | eq: case lt | eq:
ok = ft.order[idx].SetOrderOrEqual(v, w) ok = order.SetOrderOrEqual(v, w)
case gt | eq: case gt | eq:
ok = ft.order[idx].SetOrderOrEqual(w, v) ok = order.SetOrderOrEqual(w, v)
case eq: case eq:
ok = ft.order[idx].SetEqual(v, w) ok = order.SetEqual(v, w)
case lt | gt: case lt | gt:
ok = ft.order[idx].SetNonEqual(v, w) ok = order.SetNonEqual(v, w)
default: default:
panic("unknown relation") panic("unknown relation")
} }
...@@ -588,6 +589,7 @@ func (ft *factsTable) isNonNegative(v *Value) bool { ...@@ -588,6 +589,7 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
} }
// Check if the recorded limits can prove that the value is positive // Check if the recorded limits can prove that the value is positive
if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= uint64(max)) { if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= uint64(max)) {
return true return true
} }
...@@ -610,7 +612,7 @@ func (ft *factsTable) isNonNegative(v *Value) bool { ...@@ -610,7 +612,7 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
} }
// Check if the signed poset can prove that the value is >= 0 // Check if the signed poset can prove that the value is >= 0
return ft.order[0].OrderedOrEqual(ft.zero, v) return ft.orderS.OrderedOrEqual(ft.zero, v)
} }
// checkpoint saves the current state of known relations. // checkpoint saves the current state of known relations.
...@@ -621,8 +623,8 @@ func (ft *factsTable) checkpoint() { ...@@ -621,8 +623,8 @@ func (ft *factsTable) checkpoint() {
} }
ft.stack = append(ft.stack, checkpointFact) ft.stack = append(ft.stack, checkpointFact)
ft.limitStack = append(ft.limitStack, checkpointBound) ft.limitStack = append(ft.limitStack, checkpointBound)
ft.order[0].Checkpoint() ft.orderS.Checkpoint()
ft.order[1].Checkpoint() ft.orderU.Checkpoint()
} }
// restore restores known relation to the state just // restore restores known relation to the state just
...@@ -658,8 +660,8 @@ func (ft *factsTable) restore() { ...@@ -658,8 +660,8 @@ func (ft *factsTable) restore() {
ft.limits[old.vid] = old.limit ft.limits[old.vid] = old.limit
} }
} }
ft.order[0].Undo() ft.orderS.Undo()
ft.order[1].Undo() ft.orderU.Undo()
} }
func lessByID(v, w *Value) bool { func lessByID(v, w *Value) bool {
...@@ -922,7 +924,7 @@ func prove(f *Func) { ...@@ -922,7 +924,7 @@ func prove(f *Func) {
ft.restore() ft.restore()
// Return the posets to the free list // Return the posets to the free list
for _, po := range ft.order { for _, po := range []*poset{ft.orderS, ft.orderU} {
// Make sure it's empty as it should be. A non-empty poset // Make sure it's empty as it should be. A non-empty poset
// might cause errors and miscompilations if reused. // might cause errors and miscompilations if reused.
if checkEnabled { if checkEnabled {
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment