Commit 8d8f620f authored by Austin Clements's avatar Austin Clements

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: default avatarDavid Chase <drchase@google.com>
parent 87a18c61
......@@ -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 {
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment