-
Notifications
You must be signed in to change notification settings - Fork 1.9k
Shared: Use edge dominance terminology in basic block library #18696
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from 3 commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
820d2cb
Shared: Use edge dominance in basic block library
paldepind 7c57962
Merge branch 'main' into shared-bb-dominates
paldepind 532ca17
C#/Ruby/Swift: Add change note for deprecated basic block methods
paldepind 8eadd11
C#/Swift/Ruby: Fix grammar in change note
paldepind d6e8acd
C#/Ruby/Swift: Tweaks to documentation
paldepind 003058c
Shared/Ruby: Use `e` for edges in documentation
paldepind File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,6 @@ | ||
| --- | ||
| category: deprecated | ||
| --- | ||
| * The predicates `immediatelyControls` and `controls` on the `ConditionBlock` | ||
| class has been deprecated in favor of the newly added `dominatingEdge` | ||
| predicate. | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,6 @@ | ||
| --- | ||
| category: deprecated | ||
| --- | ||
| * The predicates `immediatelyControls` and `controls` on the `ConditionBlock` | ||
| class has been deprecated in favor of the newly added `dominatingEdge` | ||
paldepind marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| predicate. | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -168,6 +168,29 @@ final class BasicBlock extends BasicBlocksImpl::BasicBlock { | |
| */ | ||
| BasicBlock getImmediateDominator() { result = super.getImmediateDominator() } | ||
|
|
||
| /** | ||
| * Holds if the edge with successor type `s` out of this basic block is a | ||
| * dominating edge for `dominated`. | ||
| * | ||
| * That is, all paths reaching `dominated` from the entry point basic | ||
| * block must go through the `s` edge out of this basic block. | ||
| * | ||
| * Edge dominance is similar to node dominance except it concerns edges | ||
| * instead of nodes: A basic block is dominated by a _basic block_ `bb` if it | ||
| * can only be reached through `bb` and dominated by an _edge_ `s` if it can | ||
| * only be reached through `s`. | ||
|
||
| * | ||
| * Note that where all basic blocks (except the entry basic block) are | ||
| * strictly dominated by at least one basic block, a basic block may not be | ||
| * dominated by any edge. If an edge dominates a basic block `bb`, then | ||
| * both endpoints of the edge dominates `bb`. The converse is not the case, | ||
| * as there may be multiple paths between the endpoints with none of them | ||
| * dominating. | ||
| */ | ||
| predicate edgeDominates(BasicBlock dominated, SuccessorType s) { | ||
| super.edgeDominates(dominated, s) | ||
| } | ||
|
|
||
| /** | ||
| * Holds if this basic block strictly post-dominates basic block `bb`. | ||
| * | ||
|
|
@@ -248,21 +271,26 @@ final class JoinBlockPredecessor extends BasicBlock, BasicBlocksImpl::JoinPredec | |
| */ | ||
| final class ConditionBlock extends BasicBlock, BasicBlocksImpl::ConditionBasicBlock { | ||
| /** | ||
| * DEPRECATED: Use `edgeDominates` instead. | ||
| * | ||
| * Holds if basic block `succ` is immediately controlled by this basic | ||
| * block with conditional value `s`. That is, `succ` is an immediate | ||
| * successor of this block, and `succ` can only be reached from | ||
| * the callable entry point by going via the `s` edge out of this basic block. | ||
| */ | ||
| predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) { | ||
| super.immediatelyControls(succ, s) | ||
| deprecated predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) { | ||
| this.getASuccessor(s) = succ and | ||
| BasicBlocksImpl::dominatingEdge(this, succ) | ||
| } | ||
|
|
||
| /** | ||
| * DEPRECATED: Use `edgeDominates` instead. | ||
| * | ||
| * Holds if basic block `controlled` is controlled by this basic block with | ||
| * conditional value `s`. That is, `controlled` can only be reached from the | ||
| * callable entry point by going via the `s` edge out of this basic block. | ||
| */ | ||
| predicate controls(BasicBlock controlled, ConditionalSuccessor s) { | ||
| super.controls(controlled, s) | ||
| deprecated predicate controls(BasicBlock controlled, ConditionalSuccessor s) { | ||
| super.edgeDominates(controlled, s) | ||
| } | ||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -169,90 +169,59 @@ module Make<LocationSig Location, InputSig<Location> Input> { | |
| BasicBlock getImmediateDominator() { bbIDominates(result, this) } | ||
|
|
||
| /** | ||
| * Holds if basic block `succ` is immediately controlled by this basic | ||
| * block with successor type `s`. | ||
| * Holds if the edge with successor type `s` out of this basic block is a | ||
| * dominating edge for `dominated`. | ||
| * | ||
| * That is, `succ` is an immediate successor of this block, and `succ` can | ||
| * only be reached from the entry block by going via the `s` edge out of | ||
| * this basic block. | ||
| */ | ||
| pragma[nomagic] | ||
| predicate immediatelyControls(BasicBlock succ, SuccessorType s) { | ||
| succ = this.getASuccessor(s) and | ||
| bbIDominates(this, succ) and | ||
| // The above is not sufficient to ensure that `succ` can only be reached | ||
| // through `s`. To see why, consider this example corresponding to an | ||
| // `if` statement without an `else` block and whe `A` is the basic block | ||
| // following the `if` statement: | ||
| // ``` | ||
| // ... --> cond --[true]--> ... --> A | ||
| // \ / | ||
| // ----[false]----------- | ||
| // ``` | ||
| // Here `A` is a direct successor of `cond` along the `false` edge and it | ||
| // is immediately dominated by `cond`, but `A` is not controlled by the | ||
| // `false` edge since it is also possible to reach `A` via the `true` | ||
| // edge. | ||
| // | ||
| // Note that the first and third conjunct implies the second. But | ||
| // explicitly including the second conjunct leads to a better join order. | ||
| forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this | | ||
| succ.dominates(pred) | ||
| ) | ||
| } | ||
|
|
||
| /** | ||
| * Holds if basic block `controlled` is controlled by this basic block with | ||
| * successor type `s`. | ||
| * | ||
| * That is, all paths reaching `controlled` from the entry point basic | ||
| * That is, all paths reaching `dominated` from the entry point basic | ||
| * block must go through the `s` edge out of this basic block. | ||
| * | ||
| * Control is similar to dominance except it concerns edges instead of | ||
| * nodes: A basic block is _dominated_ by a _basic block_ `bb` if it can | ||
| * only be reached through `bb` and _controlled_ by an _edge_ `s` if it can | ||
| * only be reached through `s`. | ||
| * Edge dominance is similar to node dominance except it concerns edges | ||
| * instead of nodes: A basic block is dominated by a _basic block_ `bb` if | ||
| * it can only be reached through `bb` and dominated by an _edge_ `s` if it | ||
| * can only be reached through `s`. | ||
|
||
| * | ||
| * Note that where all basic blocks (except the entry basic block) are | ||
| * strictly dominated by at least one basic block, a basic block may not be | ||
| * controlled by any edge. If an edge controls a basic block `bb`, then | ||
| * dominated by any edge. If an edge dominates a basic block `bb`, then | ||
| * both endpoints of the edge dominates `bb`. The converse is not the case, | ||
| * as there may be multiple paths between the endpoints with none of them | ||
| * dominating. | ||
| */ | ||
| predicate controls(BasicBlock controlled, SuccessorType s) { | ||
| // For this block to control the block `controlled` with `s` the following must be true: | ||
| // 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`. | ||
| predicate edgeDominates(BasicBlock dominated, SuccessorType s) { | ||
| // For this block to control the block `dominated` with `s` the following must be true: | ||
| // 1/ Execution must have passed through the test i.e. `this` must strictly dominate `dominated`. | ||
| // 2/ Execution must have passed through the `s` edge leaving `this`. | ||
| // | ||
| // Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `controlled`, | ||
| // Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `dominated`, | ||
| // the reverse is not true, as flow may have passed through another edge to get to `this.getASuccessor(s)` | ||
| // so we need to assert that `this.getASuccessor(s)` dominates `controlled` *and* that | ||
| // so we need to assert that `this.getASuccessor(s)` dominates `dominated` *and* that | ||
| // all predecessors of `this.getASuccessor(s)` are either `this` or dominated by `this.getASuccessor(s)`. | ||
| // | ||
| // For example, in the following C# snippet: | ||
| // ```csharp | ||
| // if (x) | ||
| // controlled; | ||
| // dominated; | ||
| // false_successor; | ||
| // uncontrolled; | ||
| // ``` | ||
| // `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`) | ||
| // or dominated by itself. Whereas in the following code: | ||
| // ```csharp | ||
| // if (x) | ||
| // while (controlled) | ||
| // while (dominated) | ||
| // also_controlled; | ||
| // false_successor; | ||
| // uncontrolled; | ||
| // ``` | ||
| // the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`) | ||
| // the block `while dominated` is dominated because all of its predecessors are `this` (`if (x)`) | ||
| // or (in the case of `also_controlled`) dominated by itself. | ||
| // | ||
| // The additional constraint on the predecessors of the test successor implies | ||
| // that `this` strictly dominates `controlled` so that isn't necessary to check | ||
| // that `this` strictly dominates `dominated` so that isn't necessary to check | ||
| // directly. | ||
| exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled)) | ||
| exists(BasicBlock succ | | ||
| succ = this.getASuccessor(s) and dominatingEdge(this, succ) and succ.dominates(dominated) | ||
| ) | ||
| } | ||
|
|
||
| /** | ||
|
|
@@ -282,6 +251,38 @@ module Make<LocationSig Location, InputSig<Location> Input> { | |
| string toString() { result = this.getFirstNode().toString() } | ||
| } | ||
|
|
||
| /** | ||
| * Holds if `bb1` has `bb2` as a direct successor and the edge between `bb1` | ||
| * and `bb2` is a dominating edge. | ||
| * | ||
| * An edge `(bb1, bb2)` is dominating if there exists a basic block that can | ||
| * only be reached from the entry block by going through `(bb1, bb2)`. This | ||
| * implies that `(bb1, bb2)` dominates its endpoint `bb2`. I.e., `bb2` can | ||
| * only be reached from the entry block by going via `(bb1, bb2)`. | ||
| */ | ||
| pragma[nomagic] | ||
| predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { | ||
| bb1.getASuccessor(_) = bb2 and | ||
| bbIDominates(bb1, bb2) and | ||
| // The above is not sufficient to ensure that `bb1` can only be reached | ||
paldepind marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| // through `(bb1, bb2)`. To see why, consider this example corresponding to | ||
| // an `if` statement without an `else` block and whe `A` is the basic block | ||
paldepind marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| // following the `if` statement: | ||
| // ``` | ||
| // ... --> cond --[true]--> ... --> A | ||
| // \ / | ||
paldepind marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| // ----[false]----------- | ||
| // ``` | ||
| // Here `A` is a direct successor of `cond` along the `false` edge and it | ||
| // is immediately dominated by `cond`, but `A` is not controlled by the | ||
paldepind marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| // `false` edge since it is also possible to reach `A` via the `true` | ||
| // edge. | ||
| // | ||
| // Note that the first and third conjunct implies the second. But | ||
| // explicitly including the second conjunct leads to a better join order. | ||
| forall(BasicBlock pred | pred = bb2.getAPredecessor() and pred != bb1 | bb2.dominates(pred)) | ||
| } | ||
|
|
||
| cached | ||
| private module Cached { | ||
| /** | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,6 @@ | ||
| --- | ||
| category: deprecated | ||
| --- | ||
| * The predicates `immediatelyControls` and `controls` on the `ConditionBlock` | ||
| class has been deprecated in favor of the newly added `dominatingEdge` | ||
paldepind marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| predicate. | ||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.