C#: Improve a few join-orders in Splitting.qll

This commit is contained in:
Tom Hvitved
2019-10-02 16:23:08 +02:00
parent 39f550b6d2
commit 6ebefbb67d

View File

@@ -527,15 +527,20 @@ module FinallySplitting {
override string toString() { result = "Finally (" + nestLevel + ")" } override string toString() { result = "Finally (" + nestLevel + ")" }
} }
pragma[noinline]
private predicate hasEntry0(
ControlFlowElement pred, FinallyControlFlowElement succ, int nestLevel, Completion c
) {
succ.isEntryNode() and
nestLevel = nestLevel(succ.getTryStmt()) and
succ = succ(pred, c)
}
private class FinallySplitInternal extends SplitInternal, FinallySplitImpl { private class FinallySplitInternal extends SplitInternal, FinallySplitImpl {
override FinallySplitKind getKind() { result.getNestLevel() = this.getNestLevel() } override FinallySplitKind getKind() { result.getNestLevel() = this.getNestLevel() }
override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) { override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
succ = any(FinallyControlFlowElement entry | hasEntry0(pred, succ, this.getNestLevel(), c) and
entry.isEntryNode() and
this.getNestLevel() = nestLevel(entry.getTryStmt())
) and
succ = succ(pred, c) and
this.getType().isSplitForEntryCompletion(c) this.getType().isSplitForEntryCompletion(c)
} }
@@ -550,17 +555,22 @@ module FinallySplitting {
(exists(succ(pred, _)) or exists(succExit(pred, _))) (exists(succ(pred, _)) or exists(succExit(pred, _)))
} }
pragma[noinline]
private predicate exit0(ControlFlowElement pred, TryStmt try, int nestLevel, Completion c) {
this.appliesToPredecessor(pred) and
nestLevel = nestLevel(try) and
pred = last(try, c)
}
/** /**
* Holds if `pred` may exit this split with completion `c`. The Boolean * Holds if `pred` may exit this split with completion `c`. The Boolean
* `inherited` indicates whether `c` is an inherited completion from a `try`/ * `inherited` indicates whether `c` is an inherited completion from a `try`/
* `catch` block. * `catch` block.
*/ */
private predicate exit(ControlFlowElement pred, Completion c, boolean inherited) { private predicate exit(ControlFlowElement pred, Completion c, boolean inherited) {
this.appliesToPredecessor(pred) and
exists(TryStmt try, FinallySplitType type | exists(TryStmt try, FinallySplitType type |
type = this.getType() and exit0(pred, try, this.getNestLevel(), c) and
nestLevel(try) = this.getNestLevel() and type = this.getType()
pred = last(try, c)
| |
if pred = last(try.getFinally(), c) if pred = last(try.getFinally(), c)
then then
@@ -1019,13 +1029,21 @@ module BooleanSplitting {
override string toString() { result = kind.toString() } override string toString() { result = kind.toString() }
} }
pragma[noinline]
private predicate hasEntry0(
ControlFlowElement pred, ControlFlowElement succ, BooleanSplitSubKind kind, boolean b,
Completion c
) {
kind.startsSplit(pred) and
succ = succ(pred, c) and
b = c.getInnerCompletion().(BooleanCompletion).getValue()
}
private class BooleanSplitInternal extends SplitInternal, BooleanSplitImpl { private class BooleanSplitInternal extends SplitInternal, BooleanSplitImpl {
override BooleanSplitKind getKind() { result.getSubKind() = this.getSubKind() } override BooleanSplitKind getKind() { result.getSubKind() = this.getSubKind() }
override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) { override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
succ = succ(pred, c) and hasEntry0(pred, succ, this.getSubKind(), this.getBranch(), c)
this.getSubKind().startsSplit(pred) and
this.getBranch() = c.getInnerCompletion().(BooleanCompletion).getValue()
} }
override predicate hasEntry(Callable c, ControlFlowElement succ) { none() } override predicate hasEntry(Callable c, ControlFlowElement succ) { none() }