From: Giovanni Bajo <rasky@develer.com>
Date: Mon, 12 Mar 2018 23:25:06 +0000 (+0100)
Subject: cmd/compile: in prove, shortcircuit self-facts
X-Git-Tag: go1.11beta1~1124
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=d54902ece907d55d937b7b2fa294e0cc22b57a32;p=gostls13.git

cmd/compile: in prove, shortcircuit self-facts

Sometimes, we can end up calling update with a self-relation
about a variable (x REL x). In this case, there is no need
to record anything: the relation is unsatisfiable if and only
if it doesn't contain eq.

This also helps avoiding infinite loop in next CL that will
introduce transitive closure of relations.

Passes toolstash -cmp.

Change-Id: Ic408452ec1c13653f22ada35466ec98bc14aaa8e
Reviewed-on: https://go-review.googlesource.com/100276
Reviewed-by: Austin Clements <austin@google.com>
---

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index ec31d46d02..cf0118ac3c 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -193,6 +193,15 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 		return
 	}
 
+	// Self-fact. It's wasteful to register it into the facts
+	// table, so just note whether it's satisfiable
+	if v == w {
+		if r&eq == 0 {
+			ft.unsat = true
+		}
+		return
+	}
+
 	if lessByID(w, v) {
 		v, w = w, v
 		r = reverseBits[r]