From: Austin Clements <austin@google.com>
Date: Fri, 23 Mar 2018 21:25:26 +0000 (-0400)
Subject: cmd/compile: derive len/cap relations in factsTable.update
X-Git-Tag: go1.11beta1~377
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=4816eface10125bc915c8a0dfff7fe1489827b8c;p=gostls13.git

cmd/compile: derive len/cap relations in factsTable.update

Currently, the prove pass derives implicit relations between len and
cap in the code that adds branch conditions. This is fine right now
because that's the only place we can encounter len and cap, but we're
about to add a second way to add assertions to the facts table that
can also produce facts involving len and cap.

Prepare for this by moving the fact derivation from updateRestrictions
(where it only applies on branches) to factsTable.update, which can
derive these facts no matter where the root facts come from.

Passes toolstash -cmp.

Change-Id: If09692d9eb98ffaa93f4cfa58ed2d8ba0887c111
Reviewed-on: https://go-review.googlesource.com/102602
Run-TryBot: Austin Clements <austin@google.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: David Chase <drchase@google.com>
---

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index b0abe7ce7d..56d8636a04 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -369,6 +369,37 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 		}
 	}
 
+	// Derived facts below here are only about numbers.
+	if d != signed && d != unsigned {
+		return
+	}
+
+	// Additional facts we know given the relationship between len and cap.
+	//
+	// TODO: Since prove now derives transitive relations, it
+	// should be sufficient to learn that len(w) <= cap(w) at the
+	// beginning of prove where we look for all len/cap ops.
+	if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
+		// len(s) > w implies cap(s) > w
+		// len(s) >= w implies cap(s) >= w
+		// len(s) == w implies cap(s) >= w
+		ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
+	}
+	if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
+		// same, length on the RHS.
+		ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
+	}
+	if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
+		// cap(s) < w implies len(s) < w
+		// cap(s) <= w implies len(s) <= w
+		// cap(s) == w implies len(s) <= w
+		ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
+	}
+	if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
+		// same, capacity on the RHS.
+		ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
+	}
+
 	// Process fence-post implications.
 	//
 	// First, make the condition > or >=.
@@ -931,31 +962,6 @@ func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r rel
 			continue
 		}
 		ft.update(parent, v, w, i, r)
-
-		// Additional facts we know given the relationship between len and cap.
-		if i != signed && i != unsigned {
-			continue
-		}
-		if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
-			// len(s) > w implies cap(s) > w
-			// len(s) >= w implies cap(s) >= w
-			// len(s) == w implies cap(s) >= w
-			ft.update(parent, ft.caps[v.Args[0].ID], w, i, r|gt)
-		}
-		if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
-			// same, length on the RHS.
-			ft.update(parent, v, ft.caps[w.Args[0].ID], i, r|lt)
-		}
-		if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
-			// cap(s) < w implies len(s) < w
-			// cap(s) <= w implies len(s) <= w
-			// cap(s) == w implies len(s) <= w
-			ft.update(parent, ft.lens[v.Args[0].ID], w, i, r|lt)
-		}
-		if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
-			// same, capacity on the RHS.
-			ft.update(parent, v, ft.lens[w.Args[0].ID], i, r|gt)
-		}
 	}
 }