Commit b846edfd authored by Giovanni Bajo's avatar Giovanni Bajo

cmd/compile: in prove, make addRestrictions more generic

addRestrictions was taking a branch parameter, binding its logic
to that of addBranchRestrictions. Since we will need to use it
for updating the facts table for induction variables, refactor it
to remove the branch parameter.

Passes toolstash -cmp.

Change-Id: Iaaec350a8becd1919d03d8574ffd1bbbd906d068
Reviewed-on: https://go-review.googlesource.com/104036
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: 's avatarAustin Clements <austin@google.com>
parent 02952ad7
...@@ -653,27 +653,34 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch { ...@@ -653,27 +653,34 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch {
// branching from Block b in direction br. // branching from Block b in direction br.
func addBranchRestrictions(ft *factsTable, b *Block, br branch) { func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
c := b.Control c := b.Control
addRestrictions(b, ft, boolean, nil, c, lt|gt, br) switch br {
case negative:
addRestrictions(b, ft, boolean, nil, c, eq)
case positive:
addRestrictions(b, ft, boolean, nil, c, lt|gt)
default:
panic("unknown branch")
}
if tr, has := domainRelationTable[b.Control.Op]; has { if tr, has := domainRelationTable[b.Control.Op]; has {
// When we branched from parent we learned a new set of // When we branched from parent we learned a new set of
// restrictions. Update the factsTable accordingly. // restrictions. Update the factsTable accordingly.
addRestrictions(b, ft, tr.d, c.Args[0], c.Args[1], tr.r, br) switch br {
case negative:
addRestrictions(b, ft, tr.d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
case positive:
addRestrictions(b, ft, tr.d, c.Args[0], c.Args[1], tr.r)
}
} }
} }
// addRestrictions updates restrictions from the immediate // addRestrictions updates restrictions from the immediate
// dominating block (p) using r. r is adjusted according to the branch taken. // dominating block (p) using r.
func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation, branch branch) { func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
if t == 0 || branch == unknown { if t == 0 {
// Trivial case: nothing to do, or branch unknown. // Trivial case: nothing to do.
// Shoult not happen, but just in case. // Shoult not happen, but just in case.
return return
} }
if branch == negative {
// Negative branch taken, complement the relations.
r = (lt | eq | gt) ^ r
}
for i := domain(1); i <= t; i <<= 1 { for i := domain(1); i <= t; i <<= 1 {
if t&i == 0 { if t&i == 0 {
continue continue
......
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