cmd/compile: in prove, fail fast when unsat is found

When an unsatisfiable relation is recorded in the facts table,
there is no need to compute further relations or updates
additional data structures.

Since we're about to transitively propagate relations, make
sure to fail as fast as possible to avoid doing useless work
in dead branches.

Passes toolstash -cmp.

Change-Id: I23eed376d62776824c33088163c7ac9620abce85
Reviewed-on: https://go-review.googlesource.com/100275
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 d90f0cad33cadccc537ce907074abe77094b5e6a..ec31d46d0294f2fdf8635cc2041a67d14f325cb8 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -188,6 +188,11 @@ func newFactsTable() *factsTable {
 // update updates the set of relations between v and w in domain d
 // restricting it to r.
 func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
+       // No need to do anything else if we already found unsat.
+       if ft.unsat {
+               return
+       }
+
        if lessByID(w, v) {
                v, w = w, v
                r = reverseBits[r]
@@ -202,10 +207,16 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
                        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
        }
 
        // Extract bounds when comparing against constants
@@ -298,12 +309,13 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
                ft.limitStack = append(ft.limitStack, limitFact{v.ID, old})
                lim = old.intersect(lim)
                ft.limits[v.ID] = lim
-               if lim.min > lim.max || lim.umin > lim.umax {
-                       ft.unsat = true
-               }
                if v.Block.Func.pass.debug > 2 {
                        v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
                }
+               if lim.min > lim.max || lim.umin > lim.umax {
+                       ft.unsat = true
+                       return
+               }
        }
 
        // Process fence-post implications.