Merge pull request #70 from github/hvitved/cfg/rescue-part2

CFG: More adjustments for `rescue`/`ensure`
This commit is contained in:
Arthur Baars
2020-12-15 16:06:26 +01:00
committed by GitHub
5 changed files with 205 additions and 24 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
@@ -1101,12 +1101,26 @@ module Trees {
.lastEnsure(last, nec.getAnInnerCompatibleCompletion(), nec.getOuterCompletion(),
nec.getNestLevel())
)
or
not exists(this.getBodyChild(_, _)) and
not exists(this.getRescue(_)) and
this.lastEnsure0(last, c)
}
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
pred = this and
first(this.getBodyChild(0, _), succ) and
c instanceof SimpleCompletion
c instanceof SimpleCompletion and
(
first(this.getBodyChild(0, _), succ)
or
not exists(this.getBodyChild(_, _)) and
(
first(this.getRescue(0), succ)
or
not exists(this.getRescue(_)) and
first(this.getEnsure(), succ)
)
)
or
// Normal left-to-right evaluation in the body
exists(int i |

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)
)
)
}

View File

@@ -8,6 +8,9 @@ break_ensure.rb:
# 27| enter m3
#-----| -> elements
# 44| enter m4
#-----| -> elements
case.rb:
# 1| enter if_in_case
#-----| -> Case
@@ -128,6 +131,12 @@ raise.rb:
# 128| enter m11
#-----| -> b
# 142| enter m12
#-----| -> b
# 150| enter m13
#-----| -> Ensure
break_ensure.rb:
# 1| elements
#-----| -> elements
@@ -143,13 +152,13 @@ break_ensure.rb:
#-----| -> For
# 3| If
#-----| -> x
#-----| -> element
# 3| Binary
#-----| false -> For
#-----| true -> Break
# 3| x
# 3| element
#-----| -> 0
# 3| 0
@@ -197,13 +206,13 @@ break_ensure.rb:
#-----| -> For
# 16| If
#-----| -> x
#-----| -> element
# 16| Binary
#-----| true -> Break
#-----| false -> Ensure
# 16| x
# 16| element
#-----| -> 0
# 16| 0
@@ -348,6 +357,85 @@ break_ensure.rb:
# 41| String
#-----| -> puts
# 44| elements
#-----| -> elements
# 45| For
#-----| non-empty -> element
#-----| empty -> exit m4 (normal)
# 45| element
#-----| -> If
# 45| elements
#-----| -> For
# 47| If
#-----| -> element
# 47| Binary
#-----| true -> String
#-----| false -> Ensure
# 47| element
#-----| -> 1
# 47| 1
#-----| -> Binary
# 48| MethodCall
#-----| raise -> [ensure: raise] Ensure
# 48| raise
#-----| -> MethodCall
# 48| String
#-----| -> raise
# 50| Ensure
#-----| -> If
# 50| [ensure: raise] Ensure
#-----| -> [ensure: raise] If
# 51| If
#-----| -> element
# 51| [ensure: raise] If
#-----| -> [ensure: raise] element
# 51| Binary
#-----| false -> For
#-----| true -> 10
# 51| [ensure: raise] Binary
#-----| true -> [ensure: raise] 10
#-----| raise -> exit m4 (abnormal)
# 51| element
#-----| -> 0
# 51| [ensure: raise] element
#-----| -> [ensure: raise] 0
# 51| 0
#-----| -> Binary
# 51| [ensure: raise] 0
#-----| -> [ensure: raise] Binary
# 52| Break
#-----| break -> exit m4 (normal)
# 52| [ensure: raise] Break
#-----| break -> exit m4 (normal)
# 52| 10
#-----| -> Break
# 52| [ensure: raise] 10
#-----| -> [ensure: raise] Break
case.rb:
# 2| Case
#-----| -> x1
@@ -3149,6 +3237,46 @@ raise.rb:
# 139| String
#-----| -> puts
# 142| b
#-----| -> If
# 143| If
#-----| -> b
# 143| b
#-----| true -> String
#-----| false -> Ensure
# 144| MethodCall
#-----| raise -> [ensure: raise] Ensure
# 144| raise
#-----| -> MethodCall
# 144| String
#-----| -> raise
# 146| Ensure
#-----| -> 3
# 146| [ensure: raise] Ensure
#-----| -> [ensure: raise] 3
# 147| Return
#-----| return -> exit m12 (normal)
# 147| [ensure: raise] Return
#-----| return -> exit m12 (normal)
# 147| 3
#-----| -> Return
# 147| [ensure: raise] 3
#-----| -> [ensure: raise] Return
# 151| Ensure
#-----| -> exit m13 (normal)
break_ensure.rb:
# 1| exit m1
@@ -3156,6 +3284,8 @@ break_ensure.rb:
# 27| exit m3
# 44| exit m4
case.rb:
# 1| exit if_in_case
@@ -3236,6 +3366,10 @@ raise.rb:
# 128| exit m11
# 142| exit m12
# 150| exit m13
break_ensure.rb:
# 1| exit m1 (normal)
#-----| -> exit m1
@@ -3246,6 +3380,12 @@ break_ensure.rb:
# 27| exit m3 (normal)
#-----| -> exit m3
# 44| exit m4 (abnormal)
#-----| -> exit m4
# 44| exit m4 (normal)
#-----| -> exit m4
case.rb:
# 1| exit if_in_case (normal)
#-----| -> exit if_in_case
@@ -3392,3 +3532,9 @@ raise.rb:
# 128| exit m11 (normal)
#-----| -> exit m11
# 142| exit m12 (normal)
#-----| -> exit m12
# 150| exit m13 (normal)
#-----| -> exit m13

View File

@@ -1,6 +1,6 @@
def m1 elements
for element in elements do
if x > 0 then
if element > 0 then
break
end
end
@@ -13,7 +13,7 @@ end
def m2 elements
for element in elements do
begin
if x > 0 then
if element > 0 then
break
end
ensure
@@ -40,3 +40,17 @@ def m3 elements
end
puts "Done"
end
def m4 elements
for element in elements do
begin
if element > 1 then
raise ""
end
ensure
if element > 0 then
break 10;
end
end
end
end

View File

@@ -136,5 +136,17 @@ def m11 b
ensure
puts "Ensure"
end
puts "End m5"
puts "End m11"
end
def m12 b
if b
raise ""
end
ensure
return 3
end
def m13
ensure
end