cybercyst/go
1
0
Fork 0
mirror of https://github.com/golang/go.git synced 2025-05-29 19:35:42 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

cmd/compile: in prove, simplify logic of branch pushing

Browse Source 
prove used a complex logic when trying to prove branch conditions:
tryPushBranch() was sometimes leaving a checkpoint on the factsTable,
sometimes not, and the caller was supposed to check the return value
to know what to do.

Since we're going to make the prove descend logic a little bit more
complex by adding also induction variables, simplify the tryPushBranch
logic, by removing any factsTable checkpoint handling from it.

Passes toolstash -cmp.

Change-Id: Idfb1703df8a455f612f93158328b36c461560781
Reviewed-on: https://go-review.googlesource.com/104035
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Austin Clements <austin@google.com>
This commit is contained in:
Giovanni Bajo 2018-04-02 01:39:03 +02:00
parent 26e0e8a840
commit 321bd8c93b
1 changed files with 18 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
src/cmd/compile/internal/ssa/prove.go
View File

@ -594,12 +594,15 @@ func prove(f *Func) {
switch node.state { switch node.state {
case descend: case descend:
ft.checkpoint()
if branch != unknown { if branch != unknown {
if !tryPushBranch(ft, parent, branch) { addBranchRestrictions(ft, parent, branch)
if ft.unsat {
// node.block is unreachable. // node.block is unreachable.
// Remove it and don't visit // Remove it and don't visit
// its children. // its children.
removeBranch(parent, branch) removeBranch(parent, branch)
ft.restore()
break break
} }
// Otherwise, we can now commit to // Otherwise, we can now commit to
@ -620,10 +623,7 @@ func prove(f *Func) {
case simplify: case simplify:
simplifyBlock(sdom, ft, node.block) simplifyBlock(sdom, ft, node.block)
ft.restore()
if branch != unknown {
popBranch(ft)
}
} }
} }
} }
@ -649,41 +649,22 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch {
return unknown return unknown
} }
// tryPushBranch tests whether it is possible to branch from Block b // addBranchRestrictions updates the factsTables ft with the facts learned when
// in direction br and, if so, pushes the branch conditions in the // branching from Block b in direction br.
// factsTable and returns true. A successful tryPushBranch must be func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
// paired with a popBranch.
func tryPushBranch(ft *factsTable, b *Block, br branch) bool {
ft.checkpoint()
c := b.Control c := b.Control
updateRestrictions(b, ft, boolean, nil, c, lt|gt, br) addRestrictions(b, ft, boolean, nil, c, lt|gt, br)
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.
updateRestrictions(b, ft, tr.d, c.Args[0], c.Args[1], tr.r, br) addRestrictions(b, ft, tr.d, c.Args[0], c.Args[1], tr.r, br)
} }
if ft.unsat {
// This branch's conditions contradict some known
// fact, so it cannot be taken. Unwind the facts.
//
// (Since we never checkpoint an unsat factsTable, we
// don't really need factsTable.unsatDepth, but
// there's no cost to keeping checkpoint/restore more
// general.)
ft.restore()
return false
}
return true
} }
// popBranch undoes the effects of a successful tryPushBranch. // addRestrictions updates restrictions from the immediate
func popBranch(ft *factsTable) {
ft.restore()
}
// updateRestrictions updates restrictions from the immediate
// dominating block (p) using r. r is adjusted according to the branch taken. // dominating block (p) using r. r is adjusted according to the branch taken.
func updateRestrictions(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, branch branch) {
if t == 0 || branch == unknown { if t == 0 || branch == unknown {
// Trivial case: nothing to do, or branch unknown. // Trivial case: nothing to do, or branch unknown.
// Shoult not happen, but just in case. // Shoult not happen, but just in case.
@ -797,7 +778,11 @@ func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
} }
// For edges to other blocks, this can trim a branch // For edges to other blocks, this can trim a branch
// even if we couldn't get rid of the child itself. // even if we couldn't get rid of the child itself.
if !tryPushBranch(ft, parent, branch) { ft.checkpoint()
addBranchRestrictions(ft, parent, branch)
unsat := ft.unsat
ft.restore()
if unsat {
// This branch is impossible, so remove it // This branch is impossible, so remove it
// from the block. // from the block.
removeBranch(parent, branch) removeBranch(parent, branch)
@ -808,7 +793,6 @@ func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
// BlockExit, but it doesn't seem worth it.) // BlockExit, but it doesn't seem worth it.)
break break
} }
popBranch(ft)
} }
} }