Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,11 @@ import csharp
private import semmle.code.csharp.commons.Assertions
private import semmle.code.csharp.commons.Constants
private import semmle.code.csharp.frameworks.System
private import ControlFlowGraphImpl
private import NonReturning
private import SuccessorType
private import SuccessorTypes

// Internal representation of completions
private newtype TCompletion =
TSimpleCompletion() or
TBooleanCompletion(boolean b) { b = true or b = false } or
Expand All @@ -40,26 +40,33 @@ private newtype TCompletion =
TGotoCompletion(string label) { label = any(GotoStmt gs).getLabel() } or
TThrowCompletion(ExceptionClass ec) or
TExitCompletion() or
TNestedCompletion(Completion inner, Completion outer) {
inner instanceof NormalCompletion and
(
outer = TReturnCompletion()
or
outer = TBreakCompletion()
or
outer = TContinueCompletion()
or
outer = TGotoCompletion(_)
or
outer = TThrowCompletion(_)
or
outer = TExitCompletion()
)
or
TNestedCompletion(Completion inner, Completion outer, int nestLevel) {
inner = TBreakCompletion() and
outer instanceof NonNestedNormalCompletion
outer instanceof NonNestedNormalCompletion and
nestLevel = 0
or
inner instanceof NormalCompletion and
nestedFinallyCompletion(outer, nestLevel)
}

pragma[noinline]
private predicate nestedFinallyCompletion(Completion outer, int nestLevel) {
(
outer = TReturnCompletion()
or
outer = TBreakCompletion()
or
outer = TContinueCompletion()
or
outer = TGotoCompletion(_)
or
outer = TThrowCompletion(_)
or
outer = TExitCompletion()
) and
nestLevel = any(Statements::TryStmtTree t).nestLevel()
}

pragma[noinline]
private predicate completionIsValidForStmt(Stmt s, Completion c) {
s instanceof BreakStmt and
Expand Down Expand Up @@ -674,21 +681,25 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
class NestedCompletion extends Completion, TNestedCompletion {
Completion inner;
Completion outer;
int nestLevel;

NestedCompletion() { this = TNestedCompletion(inner, outer) }
NestedCompletion() { this = TNestedCompletion(inner, outer, nestLevel) }

/** Gets a completion that is compatible with the inner completion. */
Completion getAnInnerCompatibleCompletion() {
result.getOuterCompletion() = this.getInnerCompletion()
}

/** Gets the level of this nested completion. */
int getNestLevel() { result = nestLevel }

override Completion getInnerCompletion() { result = inner }

override Completion getOuterCompletion() { result = outer }

override SuccessorType getAMatchingSuccessorType() { none() }

override string toString() { result = outer + " [" + inner + "]" }
override string toString() { result = outer + " [" + inner + "] (" + nestLevel + ")" }
}

/**
Expand Down Expand Up @@ -725,13 +736,13 @@ class NestedBreakCompletion extends NormalCompletion, NestedCompletion {

override BreakCompletion getInnerCompletion() { result = inner }

override SimpleCompletion getOuterCompletion() { result = outer }
override NonNestedNormalCompletion getOuterCompletion() { result = outer }

override Completion getAnInnerCompatibleCompletion() {
result = inner and
outer = TSimpleCompletion()
or
result = TNestedCompletion(outer, inner)
result = TNestedCompletion(outer, inner, _)
}

override SuccessorType getAMatchingSuccessorType() {
Expand All @@ -749,7 +760,7 @@ class NestedBreakCompletion extends NormalCompletion, NestedCompletion {
class ReturnCompletion extends Completion {
ReturnCompletion() {
this = TReturnCompletion() or
this = TNestedCompletion(_, TReturnCompletion())
this = TNestedCompletion(_, TReturnCompletion(), _)
}

override ReturnSuccessor getAMatchingSuccessorType() { any() }
Expand All @@ -768,7 +779,7 @@ class ReturnCompletion extends Completion {
class BreakCompletion extends Completion {
BreakCompletion() {
this = TBreakCompletion() or
this = TNestedCompletion(_, TBreakCompletion())
this = TNestedCompletion(_, TBreakCompletion(), _)
}

override BreakSuccessor getAMatchingSuccessorType() { any() }
Expand All @@ -787,7 +798,7 @@ class BreakCompletion extends Completion {
class ContinueCompletion extends Completion {
ContinueCompletion() {
this = TContinueCompletion() or
this = TNestedCompletion(_, TContinueCompletion())
this = TNestedCompletion(_, TContinueCompletion(), _)
}

override ContinueSuccessor getAMatchingSuccessorType() { any() }
Expand All @@ -807,7 +818,7 @@ class GotoCompletion extends Completion {

GotoCompletion() {
this = TGotoCompletion(label) or
this = TNestedCompletion(_, TGotoCompletion(label))
this = TNestedCompletion(_, TGotoCompletion(label), _)
}

/** Gets the label of the `goto` completion. */
Expand All @@ -830,7 +841,7 @@ class ThrowCompletion extends Completion {

ThrowCompletion() {
this = TThrowCompletion(ec) or
this = TNestedCompletion(_, TThrowCompletion(ec))
this = TNestedCompletion(_, TThrowCompletion(ec), _)
}

/** Gets the type of the exception being thrown. */
Expand All @@ -856,7 +867,7 @@ class ThrowCompletion extends Completion {
class ExitCompletion extends Completion {
ExitCompletion() {
this = TExitCompletion() or
this = TNestedCompletion(_, TExitCompletion())
this = TNestedCompletion(_, TExitCompletion(), _)
}

override ExitSuccessor getAMatchingSuccessorType() { any() }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -858,6 +858,7 @@ module Expressions {
(cc.(MatchingCompletion).isNonMatch() or cc instanceof FalseCompletion) and
c =
any(NestedCompletion nc |
nc.getNestLevel() = 0 and
nc.getInnerCompletion() = cc and
nc.getOuterCompletion()
.(ThrowCompletion)
Expand Down Expand Up @@ -1300,13 +1301,53 @@ module Statements {
last(cc.getBlock(), result, c)
}

/** Gets a child of `cfe` that is in CFG scope `scope`. */
pragma[noinline]
private ControlFlowElement getAChildInScope(ControlFlowElement cfe, Callable scope) {
result = cfe.getAChild() and
scope = result.getEnclosingCallable()
}

class TryStmtTree extends PreOrderTree, TryStmt {
ControlFlowTree body;

final override predicate propagatesAbnormal(ControlFlowElement child) {
child = this.getFinally()
}

/**
* Gets a descendant that belongs to the `finally` block of this try statement.
*/
ControlFlowElement getAFinallyDescendant() {
result = this.getFinally()
or
exists(ControlFlowElement mid |
mid = this.getAFinallyDescendant() and
result = getAChildInScope(mid, mid.getEnclosingCallable()) and
not exists(TryStmtTree nestedTry |
result = nestedTry.getFinally() and
nestedTry != this
)
)
}

/**
* Holds if `innerTry` has a `finally` block and is immediately nested inside the
* `finally` block of this `try` statement.
*/
private predicate nestedFinally(TryStmtTree innerTry) {
exists(ControlFlowElement innerFinally |
innerFinally = getAChildInScope(this.getAFinallyDescendant(), this.getEnclosingCallable()) and
innerFinally = innerTry.getFinally()
)
}

/**
* Gets the `finally`-nesting level of this `try` statement. That is, the number of
* `finally` blocks that this `try` statement is nested under.
*/
int nestLevel() { result = count(TryStmtTree outer | outer.nestedFinally+(this)) }

/** Holds if `last` is a last element of the block of this `try` statement. */
pragma[nomagic]
predicate lastBlock(ControlFlowElement last, Completion c) { last(this.getBlock(), last, c) }
Expand Down Expand Up @@ -1343,10 +1384,11 @@ module Statements {

pragma[nomagic]
private predicate lastFinally(
ControlFlowElement last, NormalCompletion finally, Completion outer
ControlFlowElement last, NormalCompletion finally, Completion outer, int nestLevel
) {
this.lastFinally0(last, finally) and
exists(this.getBlockOrCatchFinallyPred(any(Completion c0 | outer = c0.getOuterCompletion())))
exists(this.getBlockOrCatchFinallyPred(any(Completion c0 | outer = c0.getOuterCompletion()))) and
nestLevel = this.nestLevel()
}

final override predicate last(ControlFlowElement last, Completion c) {
Expand All @@ -1360,13 +1402,14 @@ module Statements {
c instanceof ExitCompletion
)
or
this.lastFinally(last, c, any(NormalCompletion nc))
this.lastFinally(last, c, any(NormalCompletion nc), _)
or
// If the `finally` block completes normally, it inherits any non-normal
// completion that was current before the `finally` block was entered
c =
any(NestedCompletion nc |
this.lastFinally(last, nc.getAnInnerCompatibleCompletion(), nc.getOuterCompletion())
this.lastFinally(last, nc.getAnInnerCompatibleCompletion(), nc.getOuterCompletion(),
nc.getNestLevel())
)
}

Expand Down Expand Up @@ -1481,6 +1524,7 @@ module Statements {
this.isLast() and
c =
any(NestedCompletion nc |
nc.getNestLevel() = 0 and
this.throwMayBeUncaught(nc.getOuterCompletion().(ThrowCompletion)) and
(
// Incompatible exception type: clause itself
Expand Down
Loading