From: Austin Clements <austin@google.com>
Date: Fri, 23 Mar 2018 21:21:33 +0000 (-0400)
Subject: cmd/compile: teach prove about relations between constants
X-Git-Tag: go1.11beta1~378
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=8d8f620f686f596a34d75d0bc251b46d8c476891;p=gostls13.git

cmd/compile: teach prove about relations between constants

Currently, we never add a relation between two constants to prove's
fact table because these are eliminated before prove runs, so it
currently doesn't handle facts like this very well even though they're
easy to prove.

We're about to start asserting some conditions that don't appear in
the SSA, but are constructed from existing SSA values that may both be
constants.

Hence, improve the fact table to understand relations between
constants by initializing the constant bounds of constant values to
the value itself, rather than noLimit.

Passes toolstash -cmp.

Change-Id: I71f8dc294e59f19433feab1c10b6d3c99b7f1e26
Reviewed-on: https://go-review.googlesource.com/102601
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 8e24834088..b0abe7ce7d 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -279,6 +279,21 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 		old, ok := ft.limits[v.ID]
 		if !ok {
 			old = noLimit
+			if v.isGenericIntConst() {
+				switch d {
+				case signed:
+					old.min, old.max = v.AuxInt, v.AuxInt
+					if v.AuxInt >= 0 {
+						old.umin, old.umax = uint64(v.AuxInt), uint64(v.AuxInt)
+					}
+				case unsigned:
+					old.umin = v.AuxUnsigned()
+					old.umax = old.umin
+					if int64(old.umin) >= 0 {
+						old.min, old.max = int64(old.umin), int64(old.umin)
+					}
+				}
+			}
 		}
 		lim := noLimit
 		switch d {