Skip to content

C#: Unify goto completions #1548

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
semmle-qlci merged 3 commits into from
Aug 12, 2019
Merged

C#: Unify goto completions #1548

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8a35813
C#: Unify `goto` completions
hvitved Jul 3, 2019
e6c258c
C#: Restructure `Completion::isValidFor()`
hvitved Jul 3, 2019
f56c17f
C#: Fix bad join-orders in `lastNonRec()`
hvitved Jul 4, 2019
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
13 changes: 8 additions & 5 deletions csharp/ql/src/semmle/code/csharp/Stmt.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -669,7 +669,10 @@ class ContinueStmt extends JumpStmt, @continue_stmt {
* Either a `goto` label (`GotoLabelStmt`), a `goto case` (`GotoCaseStmt`), or
* a `goto default` (`GotoDefaultStmt`).
*/
class GotoStmt extends JumpStmt, @goto_any_stmt { }
class GotoStmt extends JumpStmt, @goto_any_stmt {
/** Gets the label that this `goto` statement jumps to. */
string getLabel() { none() }
}

/**
* A `goto` statement that jumps to a labeled statement, for example line 4 in
Expand All @@ -684,8 +687,7 @@ class GotoStmt extends JumpStmt, @goto_any_stmt { }
* ```
*/
class GotoLabelStmt extends GotoStmt, @goto_stmt {
/** Gets the label that this `goto` statement jumps to. */
string getLabel() { exprorstmt_name(this, result) }
override string getLabel() { exprorstmt_name(this, result) }

override string toString() { result = "goto ...;" }

Expand Down Expand Up @@ -716,8 +718,7 @@ class GotoCaseStmt extends GotoStmt, @goto_case_stmt {
/** Gets the constant expression that this `goto case` statement jumps to. */
Expr getExpr() { result = this.getChild(0) }

/** Gets the label that this `goto case` statement jumps to. */
string getLabel() { result = getExpr().getValue() }
override string getLabel() { result = getExpr().getValue() }

override string toString() { result = "goto case ...;" }
}
Expand All @@ -740,6 +741,8 @@ class GotoCaseStmt extends GotoStmt, @goto_case_stmt {
*/
class GotoDefaultStmt extends GotoStmt, @goto_default_stmt {
override string toString() { result = "goto default;" }

override string getLabel() { result = "default" }
}

/**
Expand Down
52 changes: 22 additions & 30 deletions csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -746,6 +746,10 @@ module ControlFlow {
result = TSelf(any(Completion c | c.isValidFor(cfe)))
}

private TRec specificBoolean(boolean value) {
result = TRec(TLastRecSpecificCompletion(any(BooleanCompletion bc | bc.getValue() = value)))
}

/**
* Gets an element from which the last element of `cfe` can be computed
* (recursively) based on computation specification `c`. The predicate
Expand Down Expand Up @@ -788,7 +792,7 @@ module ControlFlow {
cfe = any(LogicalAndExpr lae |
// Left operand exits with a false completion
result = lae.getLeftOperand() and
c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
c = specificBoolean(false)
or
// Left operand exits abnormally
result = lae.getLeftOperand() and
Expand All @@ -802,7 +806,7 @@ module ControlFlow {
cfe = any(LogicalOrExpr loe |
// Left operand exits with a true completion
result = loe.getLeftOperand() and
c = TRec(TLastRecSpecificCompletion(any(TrueCompletion tc)))
c = specificBoolean(true)
or
// Left operand exits abnormally
result = loe.getLeftOperand() and
Expand Down Expand Up @@ -887,7 +891,7 @@ module ControlFlow {
cfe = any(IfStmt is |
// Condition exits with a false completion and there is no `else` branch
result = is.getCondition() and
c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc))) and
c = specificBoolean(false) and
not exists(is.getElse())
or
// Condition exits abnormally
Expand Down Expand Up @@ -936,7 +940,7 @@ module ControlFlow {
c = TRec(TLastRecSpecificNegCompletion(any(MatchingCompletion mc | mc.isMatch())))
or
result = cs.getCondition() and
c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
c = specificBoolean(false)
)
or
// Last statement exits with any non-break completion
Expand Down Expand Up @@ -966,7 +970,7 @@ module ControlFlow {
cfe = any(Case case |
// Condition exists with a `false` completion
result = case.getCondition() and
c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
c = specificBoolean(false)
or
// Condition exists abnormally
result = case.getCondition() and
Expand All @@ -987,7 +991,7 @@ module ControlFlow {
|
// Condition exits with a false completion
result = ls.getCondition() and
c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
c = specificBoolean(false)
or
// Condition exits abnormally
result = ls.getCondition() and
Expand Down Expand Up @@ -1046,7 +1050,7 @@ module ControlFlow {
or
// Incompatible filter
result = scc.getFilterClause() and
c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
c = specificBoolean(false)
)
)
or
Expand Down Expand Up @@ -1087,6 +1091,12 @@ module ControlFlow {
)
}

pragma[noinline]
private LabeledStmt getLabledStmt(string label, Callable c) {
result.getEnclosingCallable() = c and
label = result.getLabel()
}

/**
* Gets a potential last element executed within control flow element `cfe`,
* as well as its completion.
Expand Down Expand Up @@ -1148,8 +1158,8 @@ module ControlFlow {
rec = TLastRecSwitchAbnormalCompletion() and
not c instanceof BreakCompletion and
not c instanceof NormalCompletion and
not c instanceof GotoDefaultCompletion and
not c instanceof GotoCaseCompletion and
not getLabledStmt(c.(GotoCompletion).getLabel(), cfe.getEnclosingCallable()) instanceof
CaseStmt and
c = c0
or
rec = TLastRecInvalidOperationException() and
Expand Down Expand Up @@ -1515,24 +1525,6 @@ module ControlFlow {
c instanceof NormalCompletion and
result = first(ss.getStmt(i + 1))
)
or
exists(GotoCompletion gc |
cfe = last(ss.getAStmt(), gc) and
gc = c
|
// Flow from last element of a statement with a `goto default` completion
// to first element `default` statement
gc instanceof GotoDefaultCompletion and
result = first(ss.getDefaultCase())
or
// Flow from last element of a statement with a `goto case` completion
// to first element of relevant case
exists(ConstCase cc |
cc = ss.getAConstCase() and
cc.getLabel() = gc.(GotoCaseCompletion).getLabel() and
result = first(cc.getBody())
)
)
)
or
exists(Case case |
Expand Down Expand Up @@ -1766,13 +1758,13 @@ module ControlFlow {
or
// Flow from element with `goto` completion to first element of relevant
// target
c = any(GotoLabelCompletion glc |
cfe = last(_, glc) and
c = any(GotoCompletion gc |
cfe = last(_, gc) and
// Special case: when a `goto` happens inside a `try` statement with a
// `finally` block, flow does not go directly to the target, but instead
// to the `finally` block (and from there possibly to the target)
not cfe = getBlockOrCatchFinallyPred(any(TryStmt ts | ts.hasFinally()), _) and
result = first(glc.getGotoStmt().getTarget())
result = first(getLabledStmt(gc.getLabel(), cfe.getEnclosingCallable()))
)
or
// Standard left-to-right evaluation
Expand Down
Loading