From 385d936fb287cfe3a491ced2d77d52d71b7705a8 Mon Sep 17 00:00:00 2001 From: Giovanni Bajo Date: Tue, 13 Mar 2018 00:21:57 +0100 Subject: [PATCH] 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 --- src/cmd/compile/internal/ssa/prove.go | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index d90f0cad33..ec31d46d02 100644 --- 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. -- 2.50.0