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 @@ -294,8 +294,6 @@ module ControlFlow {
}

class Split = Splitting::Split;

class ExceptionHandlerSplit = Splitting::ExceptionHandlerSplitting::ExceptionHandlerSplit;
}

class BasicBlock = BBs::BasicBlock;
Expand Down
182 changes: 2 additions & 180 deletions csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,7 @@ private module Cached {
newtype TSplitKind =
TInitializerSplitKind() or
TConditionalCompletionSplitKind() or
TAssertionSplitKind() or
TExceptionHandlerSplitKind()
TAssertionSplitKind()

cached
newtype TSplit =
Expand All @@ -35,8 +34,7 @@ private module Cached {
TAssertionSplit(AssertionSplitting::Assertion a, int i, boolean success) {
exists(a.getExpr(i)) and
success in [false, true]
} or
TExceptionHandlerSplit(ExceptionClass ec)
}
}

import Cached
Expand Down Expand Up @@ -449,179 +447,3 @@ module AssertionSplitting {
}
}
}

module ExceptionHandlerSplitting {
private newtype TMatch =
TAlways() or
TMaybe() or
TNever()

/**
* A split for elements belonging to a `catch` clause, which determines the type of
* exception to handle. For example, in
*
* ```csharp
* try
* {
* if (M() > 0)
* throw new ArgumentException();
* else if (M() < 0)
* throw new ArithmeticException("negative");
* else
* return;
* }
* catch (ArgumentException e)
* {
* Log.Write("M() positive");
* }
* catch (ArithmeticException e) when (e.Message != null)
* {
* Log.Write($"M() {e.Message}");
* }
* ```
*
* all control flow nodes in
* ```csharp
* catch (ArgumentException e)
* ```
* and
* ```csharp
* catch (ArithmeticException e) when (e.Message != null)
* ```
* have two splits: one representing the `try` block throwing an `ArgumentException`,
* and one representing the `try` block throwing an `ArithmeticException`.
*/
class ExceptionHandlerSplit extends Split, TExceptionHandlerSplit {
private ExceptionClass ec;

ExceptionHandlerSplit() { this = TExceptionHandlerSplit(ec) }

/** Gets the exception type that this split represents. */
ExceptionClass getExceptionClass() { result = ec }

override string toString() { result = "exception: " + ec.toString() }
}

private class ExceptionHandlerSplitKind extends SplitKind, TExceptionHandlerSplitKind {
override int getListOrder() { result = AssertionSplitting::getNextListOrder() }

override string toString() { result = "ExceptionHandler" }
}

int getNextListOrder() { result = AssertionSplitting::getNextListOrder() + 1 }

private class ExceptionHandlerSplitImpl extends SplitImpl instanceof ExceptionHandlerSplit {
override ExceptionHandlerSplitKind getKind() { any() }

override predicate hasEntry(AstNode pred, AstNode succ, Completion c) {
// Entry into first catch clause
exists(Statements::TryStmtTree ts |
super.getExceptionClass() = ts.getAThrownException(pred, c)
|
succ(pred, succ, c) and
succ = ts.(TryStmt).getCatchClause(0).(SpecificCatchClause)
)
}

override predicate hasEntryScope(CfgScope scope, AstNode first) { none() }

/**
* Holds if this split applies to catch clause `scc`. The parameter `match`
* indicates whether the catch clause `scc` may match the exception type of
* this split.
*/
private predicate appliesToCatchClause(SpecificCatchClause scc, TMatch match) {
exists(Statements::TryStmtTree ts, ExceptionClass ec |
ec = super.getExceptionClass() and
ec = ts.getAThrownException(_, _) and
scc = ts.(TryStmt).getACatchClause()
|
if scc.getCaughtExceptionType() = ec.getABaseType*()
then match = TAlways()
else
if scc.getCaughtExceptionType() = ec.getASubType+()
then match = TMaybe()
else match = TNever()
)
}

/**
* Holds if this split applies to control flow element `pred`, where `pred`
* is a valid predecessor with completion `c`.
*/
private predicate appliesToPredecessor(AstNode pred, Completion c) {
this.appliesTo(pred) and
(succ(pred, _, c) or scopeLast(_, pred, c)) and
(
pred instanceof SpecificCatchClause
implies
pred =
any(SpecificCatchClause scc |
if c instanceof MatchingCompletion
then
exists(TMatch match | this.appliesToCatchClause(scc, match) |
c =
any(MatchingCompletion mc |
if mc.isMatch() then match != TNever() else match != TAlways()
)
)
else (
(scc.isLast() and c instanceof ThrowCompletion)
implies
exists(TMatch match | this.appliesToCatchClause(scc, match) | match != TAlways())
)
)
)
}

/**
* Holds if this split applies to `pred`, and `pred` may exit this split
* with throw completion `c`, because it belongs to the last `catch` clause
* in a `try` statement.
*/
private predicate hasLastExit(AstNode pred, ThrowCompletion c) {
this.appliesToPredecessor(pred, c) and
exists(TryStmt ts, SpecificCatchClause scc, int last |
last(ts.getCatchClause(last), pred, c)
|
ts.getCatchClause(last) = scc and
scc.isLast() and
c.getExceptionClass() = super.getExceptionClass()
)
}

override predicate hasExit(AstNode pred, AstNode succ, Completion c) {
this.appliesToPredecessor(pred, c) and
succ(pred, succ, c) and
(
// Exit out to `catch` clause block
first(any(SpecificCatchClause scc).getBlock(), succ)
or
// Exit out to a general `catch` clause
succ instanceof GeneralCatchClause
or
// Exit out from last `catch` clause (no catch clauses match)
this.hasLastExit(pred, c)
)
}

override predicate hasExitScope(CfgScope scope, AstNode last, Completion c) {
// Exit out from last `catch` clause (no catch clauses match)
this.hasLastExit(last, c) and
scopeLast(scope, last, c)
}

override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) {
this.appliesToPredecessor(pred, c) and
this.appliesSucc(pred, succ, c) and
not first(any(SpecificCatchClause scc).getBlock(), succ) and
not succ instanceof GeneralCatchClause and
not exists(TryStmt ts, SpecificCatchClause scc, int last |
last(ts.getCatchClause(last), pred, c)
|
ts.getCatchClause(last) = scc and
scc.isLast()
)
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@
| Assignables.cs:69:13:69:17 | ... = ... | Assignables.cs:69:13:69:17 | ... = ... |
| Assignables.cs:78:22:78:22 | String s | Assignables.cs:78:22:78:22 | String s |
| Assignables.cs:82:21:82:33 | String temp = ... | Assignables.cs:82:21:82:33 | String temp = ... |
| Assignables.cs:84:30:84:30 | Exception e | Assignables.cs:84:30:84:30 | [exception: OutOfMemoryException] Exception e |
| Assignables.cs:84:30:84:30 | Exception e | Assignables.cs:84:30:84:30 | Exception e |
| Assignables.cs:92:9:92:54 | ... = ... | Assignables.cs:92:9:92:54 | ... = ... |
| Assignables.cs:92:9:92:54 | ... = ... | Assignables.cs:92:9:92:54 | ... = ... |
| Assignables.cs:92:9:92:54 | ... = ... | Assignables.cs:92:9:92:54 | ... = ... |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -367,12 +367,10 @@
| ExitMethods.cs:20:10:20:11 | enter M3 | ExitMethods.cs:20:10:20:11 | exit M3 | 7 |
| ExitMethods.cs:26:10:26:11 | enter M4 | ExitMethods.cs:26:10:26:11 | exit M4 | 7 |
| ExitMethods.cs:32:10:32:11 | enter M5 | ExitMethods.cs:32:10:32:11 | exit M5 | 7 |
| ExitMethods.cs:38:10:38:11 | enter M6 | ExitMethods.cs:42:13:42:30 | call to method ErrorAlways | 7 |
| ExitMethods.cs:38:10:38:11 | enter M6 | ExitMethods.cs:44:9:47:9 | catch (...) {...} | 8 |
| ExitMethods.cs:38:10:38:11 | exit M6 (normal) | ExitMethods.cs:38:10:38:11 | exit M6 | 2 |
| ExitMethods.cs:44:9:47:9 | [exception: ArgumentException] catch (...) {...} | ExitMethods.cs:44:9:47:9 | [exception: ArgumentException] catch (...) {...} | 1 |
| ExitMethods.cs:44:9:47:9 | [exception: Exception] catch (...) {...} | ExitMethods.cs:44:9:47:9 | [exception: Exception] catch (...) {...} | 1 |
| ExitMethods.cs:45:9:47:9 | {...} | ExitMethods.cs:46:13:46:19 | return ...; | 2 |
| ExitMethods.cs:48:9:51:9 | [exception: Exception] catch (...) {...} | ExitMethods.cs:48:9:51:9 | [exception: Exception] catch (...) {...} | 1 |
| ExitMethods.cs:48:9:51:9 | catch (...) {...} | ExitMethods.cs:48:9:51:9 | catch (...) {...} | 1 |
| ExitMethods.cs:49:9:51:9 | {...} | ExitMethods.cs:50:13:50:19 | return ...; | 2 |
| ExitMethods.cs:54:10:54:11 | enter M7 | ExitMethods.cs:54:10:54:11 | exit M7 | 6 |
| ExitMethods.cs:60:10:60:11 | enter M8 | ExitMethods.cs:60:10:60:11 | exit M8 | 6 |
Expand Down Expand Up @@ -424,25 +422,26 @@
| Finally.cs:19:10:19:11 | exit M2 (abnormal) | Finally.cs:19:10:19:11 | exit M2 (abnormal) | 1 |
| Finally.cs:19:10:19:11 | exit M2 (normal) | Finally.cs:19:10:19:11 | exit M2 (normal) | 1 |
| Finally.cs:24:13:24:19 | return ...; | Finally.cs:24:13:24:19 | return ...; | 1 |
| Finally.cs:26:9:29:9 | [exception: Exception] catch (...) {...} | Finally.cs:26:9:29:9 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:26:38:26:39 | [exception: Exception] IOException ex | Finally.cs:26:48:26:51 | [exception: Exception] true | 2 |
| Finally.cs:26:9:29:9 | catch (...) {...} | Finally.cs:26:9:29:9 | catch (...) {...} | 1 |
| Finally.cs:26:38:26:39 | IOException ex | Finally.cs:26:48:26:51 | true | 2 |
| Finally.cs:27:9:29:9 | {...} | Finally.cs:28:13:28:18 | throw ...; | 2 |
| Finally.cs:30:9:40:9 | [exception: Exception] catch (...) {...} | Finally.cs:30:9:40:9 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:30:41:30:42 | [exception: Exception] ArgumentException ex | Finally.cs:34:21:34:24 | true | 6 |
| Finally.cs:30:9:40:9 | catch (...) {...} | Finally.cs:30:9:40:9 | catch (...) {...} | 1 |
| Finally.cs:30:41:30:42 | ArgumentException ex | Finally.cs:34:21:34:24 | true | 6 |
| Finally.cs:34:27:34:32 | throw ...; | Finally.cs:38:17:38:44 | throw ...; | 5 |
| Finally.cs:41:9:43:9 | [exception: Exception] catch (...) {...} | Finally.cs:41:9:43:9 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:41:9:43:9 | catch (...) {...} | Finally.cs:41:9:43:9 | catch (...) {...} | 1 |
| Finally.cs:42:9:43:9 | {...} | Finally.cs:42:9:43:9 | {...} | 1 |
| Finally.cs:44:9:47:9 | catch {...} | Finally.cs:46:13:46:19 | return ...; | 3 |
| Finally.cs:49:9:51:9 | {...} | Finally.cs:50:13:50:40 | call to method WriteLine | 4 |
| Finally.cs:54:10:54:11 | enter M3 | Finally.cs:58:13:58:37 | call to method WriteLine | 7 |
| Finally.cs:54:10:54:11 | exit M3 | Finally.cs:54:10:54:11 | exit M3 | 1 |
| Finally.cs:54:10:54:11 | exit M3 (abnormal) | Finally.cs:54:10:54:11 | exit M3 (abnormal) | 1 |
| Finally.cs:54:10:54:11 | exit M3 (normal) | Finally.cs:54:10:54:11 | exit M3 (normal) | 1 |
| Finally.cs:59:13:59:19 | return ...; | Finally.cs:59:13:59:19 | return ...; | 1 |
| Finally.cs:61:9:64:9 | [exception: Exception] catch (...) {...} | Finally.cs:61:9:64:9 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:61:38:61:39 | [exception: Exception] IOException ex | Finally.cs:61:48:61:51 | [exception: Exception] true | 2 |
| Finally.cs:61:9:64:9 | catch (...) {...} | Finally.cs:61:9:64:9 | catch (...) {...} | 1 |
| Finally.cs:61:38:61:39 | IOException ex | Finally.cs:61:48:61:51 | true | 2 |
| Finally.cs:62:9:64:9 | {...} | Finally.cs:63:13:63:18 | throw ...; | 2 |
| Finally.cs:65:9:67:9 | [exception: Exception] catch (...) {...} | Finally.cs:65:9:67:9 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:65:26:65:26 | [exception: Exception] Exception e | Finally.cs:65:35:65:51 | [exception: Exception] ... != ... | 5 |
| Finally.cs:65:9:67:9 | catch (...) {...} | Finally.cs:65:9:67:9 | catch (...) {...} | 1 |
| Finally.cs:65:26:65:26 | Exception e | Finally.cs:65:35:65:51 | ... != ... | 5 |
| Finally.cs:66:9:67:9 | {...} | Finally.cs:66:9:67:9 | {...} | 1 |
| Finally.cs:69:9:71:9 | {...} | Finally.cs:70:13:70:40 | call to method WriteLine | 4 |
| Finally.cs:74:10:74:11 | enter M4 | Finally.cs:77:9:100:9 | while (...) ... | 6 |
Expand Down Expand Up @@ -490,10 +489,8 @@
| Finally.cs:158:36:158:36 | 1 | Finally.cs:158:21:158:36 | ... == ... | 2 |
| Finally.cs:159:21:159:45 | throw ...; | Finally.cs:159:21:159:45 | throw ...; | 1 |
| Finally.cs:159:41:159:43 | "1" | Finally.cs:159:27:159:44 | object creation of type Exception | 2 |
| Finally.cs:161:13:164:13 | [exception: Exception] catch (...) {...} | Finally.cs:161:13:164:13 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:161:13:164:13 | [exception: NullReferenceException] catch (...) {...} | Finally.cs:161:13:164:13 | [exception: NullReferenceException] catch (...) {...} | 1 |
| Finally.cs:161:30:161:30 | [exception: Exception] Exception e | Finally.cs:161:39:161:54 | [exception: Exception] ... == ... | 5 |
| Finally.cs:161:30:161:30 | [exception: NullReferenceException] Exception e | Finally.cs:161:39:161:54 | [exception: NullReferenceException] ... == ... | 5 |
| Finally.cs:161:13:164:13 | catch (...) {...} | Finally.cs:161:13:164:13 | catch (...) {...} | 1 |
| Finally.cs:161:30:161:30 | Exception e | Finally.cs:161:39:161:54 | ... == ... | 5 |
| Finally.cs:162:13:164:13 | {...} | Finally.cs:163:17:163:42 | call to method WriteLine | 6 |
| Finally.cs:165:13:168:13 | catch {...} | Finally.cs:167:17:167:37 | call to method WriteLine | 5 |
| Finally.cs:172:11:172:20 | enter ExceptionA | Finally.cs:172:11:172:20 | exit ExceptionA | 5 |
Expand All @@ -506,11 +503,10 @@
| Finally.cs:180:21:180:43 | throw ...; | Finally.cs:180:21:180:43 | throw ...; | 1 |
| Finally.cs:180:27:180:42 | object creation of type ExceptionA | Finally.cs:180:27:180:42 | object creation of type ExceptionA | 1 |
| Finally.cs:183:9:192:9 | {...} | Finally.cs:186:21:186:22 | access to parameter b2 | 5 |
| Finally.cs:186:25:186:47 | throw ...; | Finally.cs:188:13:191:13 | [exception: ExceptionB] catch (...) {...} | 2 |
| Finally.cs:186:25:186:47 | throw ...; | Finally.cs:186:25:186:47 | throw ...; | 1 |
| Finally.cs:186:31:186:46 | object creation of type ExceptionB | Finally.cs:186:31:186:46 | object creation of type ExceptionB | 1 |
| Finally.cs:188:13:191:13 | [exception: Exception] catch (...) {...} | Finally.cs:188:13:191:13 | [exception: Exception] catch (...) {...} | 1 |
| Finally.cs:188:38:188:39 | [exception: ExceptionB] access to parameter b2 | Finally.cs:188:38:188:39 | [exception: ExceptionB] access to parameter b2 | 1 |
| Finally.cs:188:38:188:39 | [exception: Exception] access to parameter b2 | Finally.cs:188:38:188:39 | [exception: Exception] access to parameter b2 | 1 |
| Finally.cs:188:13:191:13 | catch (...) {...} | Finally.cs:188:13:191:13 | catch (...) {...} | 1 |
| Finally.cs:188:38:188:39 | access to parameter b2 | Finally.cs:188:38:188:39 | access to parameter b2 | 1 |
| Finally.cs:189:13:191:13 | {...} | Finally.cs:190:21:190:22 | access to parameter b1 | 3 |
| Finally.cs:190:31:190:46 | object creation of type ExceptionC | Finally.cs:190:25:190:47 | throw ...; | 2 |
| Finally.cs:195:10:195:12 | enter M10 | Finally.cs:199:17:199:18 | access to parameter b1 | 6 |
Expand Down
Loading