From 941fc129e2f059a5fb9f5ab77f5cb12aedecd145 Mon Sep 17 00:00:00 2001 From: Austin Clements Date: Thu, 11 Jan 2018 14:23:01 -0500 Subject: cmd/compile: derive unsigned limits from signed limits in prove MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds a few simple deductions to the prove pass' fact table to derive unsigned concrete limits from signed concrete limits where possible. This tweak lets the pass prove 70 additional branch conditions in std and cmd. This is based on a comment from the recently-deleted factsTable.get: "// TODO: also use signed data if lim.min >= 0". Change-Id: Ib4340249e7733070f004a0aa31254adf5df8a392 Reviewed-on: https://go-review.googlesource.com/87479 Reviewed-by: Alexandru Moșoi Reviewed-by: Keith Randall --- src/cmd/compile/internal/ssa/prove.go | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src') diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 172d210216..10a16917b6 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -248,6 +248,16 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) { lim.min = c lim.max = c } + if lim.min >= 0 { + // int(x) >= 0 && int(x) >= N ⇒ uint(x) >= N + lim.umin = uint64(lim.min) + } + if lim.max != noLimit.max && old.min >= 0 && lim.max >= 0 { + // 0 <= int(x) <= N ⇒ 0 <= uint(x) <= N + // This is for a max update, so the lower bound + // comes from what we already know (old). + lim.umax = uint64(lim.max) + } case unsigned: var uc uint64 switch w.Op { @@ -281,6 +291,9 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) { lim.umin = uc lim.umax = uc } + // We could use the contrapositives of the + // signed implications to derive signed facts, + // but it turns out not to matter. } ft.limitStack = append(ft.limitStack, limitFact{v.ID, old}) lim = old.intersect(lim) -- cgit v1.3-5-g9baa