CFG: Change column order in succExit/hasExitScope

This commit is contained in:
Tom Hvitved
2020-12-15 13:29:18 +01:00
parent e784640cca
commit 489b406e2a
2 changed files with 10 additions and 15 deletions

View File

@@ -131,7 +131,7 @@ predicate succEntry(CfgScope scope, AstNode first) {
/** Holds if `last` with completion `c` can exit `scope`. */
pragma[nomagic]
predicate succExit(AstNode last, CfgScope scope, Completion c) {
predicate succExit(CfgScope scope, AstNode last, Completion c) {
exists(AstNode n |
last(scope, n, c) and
succImplIfHidden*(last, n) and

View File

@@ -156,9 +156,9 @@ abstract class SplitImpl extends Split {
* Holds if this split is left when control passes from `last` out of the enclosing
* scope `scope` with completion `c`.
*
* Invariant: `hasExitScope(last, scope, c) implies succExit(last, scope, c)`
* Invariant: `hasExitScope(scope, last, c) implies succExit(scope, last, c)`
*/
abstract predicate hasExitScope(AstNode last, CfgScope scope, Completion c);
abstract predicate hasExitScope(CfgScope scope, AstNode last, Completion c);
/**
* Holds if this split is maintained when control passes from `pred` to `succ` with
@@ -240,9 +240,9 @@ private module ConditionalCompletionSplitting {
if c instanceof ConditionalCompletion then completion = c else any()
}
override predicate hasExitScope(AstNode last, CfgScope scope, Completion c) {
override predicate hasExitScope(CfgScope scope, AstNode last, Completion c) {
this.appliesTo(last) and
succExit(last, scope, c) and
succExit(scope, last, c) and
if c instanceof ConditionalCompletion then completion = c else any()
}
@@ -286,11 +286,6 @@ module EnsureSplitting {
predicate isEntryNode() { first(block.getEnsure(), this) }
}
/** A node that does not belong to an `ensure` block. */
private class NonEnsureNode extends EnsureNode {
NonEnsureNode() { not this = any(Trees::RescueEnsureBlockTree t).getAnEnsureDescendant() }
}
/**
* A split for nodes belonging to an `ensure` block, which determines how to
* continue execution after leaving the `ensure` block. For example, in
@@ -377,7 +372,7 @@ module EnsureSplitting {
*/
private predicate appliesToPredecessor(AstNode pred) {
this.appliesTo(pred) and
(succ(pred, _, _) or succExit(pred, _, _))
(succ(pred, _, _) or succExit(_, pred, _))
}
pragma[noinline]
@@ -463,8 +458,8 @@ module EnsureSplitting {
)
}
override predicate hasExitScope(AstNode last, CfgScope scope, Completion c) {
succExit(last, scope, c) and
override predicate hasExitScope(CfgScope scope, AstNode last, Completion c) {
succExit(scope, last, c) and
(
exit(_, last, c, _)
or
@@ -551,9 +546,9 @@ predicate succExitSplits(AstNode last, Splits predSplits, CfgScope scope, Succes
exists(Reachability::SameSplitsBlock b, Completion c | last = b.getANode() |
b.isReachable(predSplits) and
t = c.getAMatchingSuccessorType() and
succExit(last, scope, c) and
succExit(scope, last, c) and
forall(SplitImpl predSplit | predSplit = predSplits.getASplit() |
predSplit.hasExitScope(last, scope, c)
predSplit.hasExitScope(scope, last, c)
)
)
}