cmd/compile: in prove, add transitive closure of relations

Implement it through a partial order datastructure, which
keeps the relations between SSA values in a forest of DAGs
and is able to discover contradictions.

In make.bash, this patch is able to prove hundreds of conditions
which were not proved before.

Compilebench:

name       old time/op       new time/op       delta
Template         371ms ± 2%        368ms ± 1%    ~     (p=0.222 n=5+5)
Unicode          203ms ± 6%        199ms ± 3%    ~     (p=0.421 n=5+5)
GoTypes          1.17s ± 4%        1.18s ± 1%    ~     (p=0.151 n=5+5)
Compiler         5.54s ± 2%        5.59s ± 1%    ~     (p=0.548 n=5+5)
SSA              12.9s ± 2%        13.2s ± 1%  +2.96%  (p=0.032 n=5+5)
Flate            245ms ± 2%        247ms ± 3%    ~     (p=0.690 n=5+5)
GoParser         302ms ± 6%        302ms ± 4%    ~     (p=0.548 n=5+5)
Reflect          764ms ± 4%        773ms ± 3%    ~     (p=0.095 n=5+5)
Tar              354ms ± 6%        361ms ± 3%    ~     (p=0.222 n=5+5)
XML              434ms ± 3%        429ms ± 1%    ~     (p=0.421 n=5+5)
StdCmd           22.6s ± 1%        22.9s ± 1%  +1.40%  (p=0.032 n=5+5)

name       old user-time/op  new user-time/op  delta
Template         436ms ± 8%        426ms ± 5%    ~     (p=0.579 n=5+5)
Unicode          219ms ±15%        219ms ±12%    ~     (p=1.000 n=5+5)
GoTypes          1.47s ± 6%        1.53s ± 6%    ~     (p=0.222 n=5+5)
Compiler         7.26s ± 4%        7.40s ± 2%    ~     (p=0.389 n=5+5)
SSA              17.7s ± 4%        18.5s ± 4%  +4.13%  (p=0.032 n=5+5)
Flate            257ms ± 5%        268ms ± 9%    ~     (p=0.333 n=5+5)
GoParser         354ms ± 6%        348ms ± 6%    ~     (p=0.913 n=5+5)
Reflect          904ms ± 2%        944ms ± 4%    ~     (p=0.056 n=5+5)
Tar              398ms ±11%        430ms ± 7%    ~     (p=0.079 n=5+5)
XML              501ms ± 7%        489ms ± 5%    ~     (p=0.444 n=5+5)

name       old text-bytes    new text-bytes    delta
HelloSize        670kB ± 0%        670kB ± 0%  +0.00%  (p=0.008 n=5+5)
CmdGoSize       7.22MB ± 0%       7.21MB ± 0%  -0.07%  (p=0.008 n=5+5)

name       old data-bytes    new data-bytes    delta
HelloSize       9.88kB ± 0%       9.88kB ± 0%    ~     (all equal)
CmdGoSize        248kB ± 0%        248kB ± 0%  -0.06%  (p=0.008 n=5+5)

name       old bss-bytes     new bss-bytes     delta
HelloSize        125kB ± 0%        125kB ± 0%    ~     (all equal)
CmdGoSize        145kB ± 0%        144kB ± 0%  -0.20%  (p=0.008 n=5+5)

name       old exe-bytes     new exe-bytes     delta
HelloSize       1.43MB ± 0%       1.43MB ± 0%    ~     (all equal)
CmdGoSize       14.5MB ± 0%       14.5MB ± 0%  -0.06%  (p=0.008 n=5+5)

Fixes #19714
Updates #20393

Change-Id: Ia090f5b5dc1bcd274ba8a39b233c1e1ace1b330e
Reviewed-on: https://go-review.googlesource.com/100277
Run-TryBot: Giovanni Bajo <rasky@develer.com>
Reviewed-by: David Chase <drchase@google.com>

1 files changed, 61 insertions, 22 deletions

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 11efbb516b..a11b46566d 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -160,6 +160,11 @@ type factsTable struct {
 	facts map[pair]relation // current known set of relation
 	stack []fact            // previous sets of relations
 
+	// order is a couple of partial order sets that record information
+	// about relations between SSA values in the signed and unsigned
+	// domain.
+	order [2]*poset
+
 	// known lower and upper bounds on individual values.
 	limits     map[ID]limit
 	limitStack []limitFact // previous entries
@@ -178,6 +183,8 @@ var checkpointBound = limitFact{}
 
 func newFactsTable() *factsTable {
 	ft := &factsTable{}
+	ft.order[0] = newPoset(false) // signed
+	ft.order[1] = newPoset(true)  // unsigned
 	ft.facts = make(map[pair]relation)
 	ft.stack = make([]fact, 4)
 	ft.limits = make(map[ID]limit)
@@ -202,30 +209,58 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 		return
 	}
 
-	if lessByID(w, v) {
-		v, w = w, v
-		r = reverseBits[r]
-	}
+	if d == signed || d == unsigned {
+		var ok bool
+		idx := 0
+		if d == unsigned {
+			idx = 1
+		}
+		switch r {
+		case lt:
+			ok = ft.order[idx].SetOrder(v, w)
+		case gt:
+			ok = ft.order[idx].SetOrder(w, v)
+		case lt | eq:
+			ok = ft.order[idx].SetOrderOrEqual(v, w)
+		case gt | eq:
+			ok = ft.order[idx].SetOrderOrEqual(w, v)
+		case eq:
+			ok = ft.order[idx].SetEqual(v, w)
+		case lt | gt:
+			ok = ft.order[idx].SetNonEqual(v, w)
+		default:
+			panic("unknown relation")
+		}
+		if !ok {
+			ft.unsat = true
+			return
+		}
+	} else {
+		if lessByID(w, v) {
+			v, w = w, v
+			r = reverseBits[r]
+		}
 
-	p := pair{v, w, d}
-	oldR, ok := ft.facts[p]
-	if !ok {
-		if v == w {
-			oldR = eq
-		} else {
-			oldR = lt | eq | gt
+		p := pair{v, w, d}
+		oldR, ok := ft.facts[p]
+		if !ok {
+			if v == w {
+				oldR = eq
+			} else {
+				oldR = lt | eq | gt
+			}
+		}
+		// No changes compared to information already in facts table.
+		if oldR == r {
+			return
+		}
+		ft.stack = append(ft.stack, fact{p, oldR})
+		ft.facts[p] = oldR & r
+		// If this relation is not satisfiable, mark it and exit right away
+		if oldR&r == 0 {
+			ft.unsat = true
+			return
 		}
-	}
-	// No changes compared to information already in facts table.
-	if oldR == r {
-		return
-	}
-	ft.stack = append(ft.stack, fact{p, oldR})
-	ft.facts[p] = oldR & r
-	// If this relation is not satisfiable, mark it and exit right away
-	if oldR&r == 0 {
-		ft.unsat = true
-		return
 	}
 
 	// Extract bounds when comparing against constants
@@ -382,6 +417,8 @@ func (ft *factsTable) checkpoint() {
 	}
 	ft.stack = append(ft.stack, checkpointFact)
 	ft.limitStack = append(ft.limitStack, checkpointBound)
+	ft.order[0].Checkpoint()
+	ft.order[1].Checkpoint()
 }
 
 // restore restores known relation to the state just
@@ -417,6 +454,8 @@ func (ft *factsTable) restore() {
 			ft.limits[old.vid] = old.limit
 		}
 	}
+	ft.order[0].Undo()
+	ft.order[1].Undo()
 }
 
 func lessByID(v, w *Value) bool {