diff --git a/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll b/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll index 3e33807991a9..a05aee1745b2 100644 --- a/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll +++ b/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll @@ -287,6 +287,18 @@ private module LogicInput implements GuardsImpl::LogicInputSig { g2 = g1.(NullCoalescingExpr).getAnOperand() and v1.isNullValue() and v2 = v1 + or + exists(Assertion assert, AssertMethod target, int i | + assert.getAssertMethod() = target and + g1 = assert and + v1.getDualValue().isThrowsException() and + g2 = assert.getExpr(i) + | + target.(BooleanAssertMethod).getAnAssertionIndex(v2.asBooleanValue()) = i + or + target.(NullnessAssertMethod).getAnAssertionIndex(any(boolean isNull | v2.isNullness(isNull))) = + i + ) } } diff --git a/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Completion.qll b/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Completion.qll index b1afbaed8ef0..ab8bb233e2cc 100644 --- a/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Completion.qll +++ b/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Completion.qll @@ -390,11 +390,6 @@ private predicate invalidCastCandidate(CastExpr ce) { ce.getExpr().getType() = getACastExprBaseType(ce) } -private predicate assertion(Assertion a, int i, AssertMethod am, Expr e) { - e = a.getExpr(i) and - am = a.getAssertMethod() -} - /** Gets a valid completion when argument `i` fails in assertion `a`. */ Completion assertionCompletion(Assertion a, int i) { exists(AssertMethod am | am = a.getAssertMethod() | @@ -429,11 +424,6 @@ private predicate inBooleanContext(Expr e) { or e = any(SpecificCatchClause scc).getFilterClause() or - exists(BooleanAssertMethod m, int i | - assertion(_, i, m, e) and - i = m.getAnAssertionIndex(_) - ) - or e = any(LogicalNotExpr lne | inBooleanContext(lne)).getAnOperand() or exists(LogicalAndExpr lae | @@ -481,11 +471,6 @@ private predicate inNullnessContext(Expr e) { or exists(QualifiableExpr qe | qe.isConditional() | e = qe.getChildExpr(-1)) or - exists(NullnessAssertMethod m, int i | - assertion(_, i, m, e) and - i = m.getAnAssertionIndex(_) - ) - or exists(ConditionalExpr ce | inNullnessContext(ce) | (e = ce.getThen() or e = ce.getElse())) or exists(NullCoalescingExpr nce | inNullnessContext(nce) | e = nce.getRightOperand()) diff --git a/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll b/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll index 210326b987ce..63d2c181da45 100644 --- a/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll +++ b/csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll @@ -24,17 +24,12 @@ private module Cached { cached newtype TSplitKind = TInitializerSplitKind() or - TConditionalCompletionSplitKind() or - TAssertionSplitKind() + TConditionalCompletionSplitKind() cached newtype TSplit = TInitializerSplit(Constructor c) { InitializerSplitting::constructorInitializes(c, _) } or - TConditionalCompletionSplit(ConditionalCompletion c) or - TAssertionSplit(AssertionSplitting::Assertion a, int i, boolean success) { - exists(a.getExpr(i)) and - success in [false, true] - } + TConditionalCompletionSplit(ConditionalCompletion c) } import Cached @@ -320,130 +315,3 @@ module ConditionalCompletionSplitting { int getNextListOrder() { result = InitializerSplitting::getNextListOrder() + 1 } } - -module AssertionSplitting { - import semmle.code.csharp.commons.Assertions - private import semmle.code.csharp.ExprOrStmtParent - - private AstNode getAnAssertionDescendant(Assertion a) { - result = a - or - result = getAnAssertionDescendant(a).getAChild() - } - - /** - * A split for assertions. For example, in - * - * ```csharp - * void M(int i) - * { - * Debug.Assert(i >= 0); - * System.Console.WriteLine("i is positive") - * } - * ``` - * - * we record whether `i >= 0` evaluates to `true` or `false`, and restrict the - * edges out of the assertion accordingly. - */ - class AssertionSplit extends Split, TAssertionSplit { - Assertion a; - boolean success; - int i; - - AssertionSplit() { this = TAssertionSplit(a, i, success) } - - /** Gets the assertion. */ - Assertion getAssertion() { result = a } - - /** Holds if this split represents a successful assertion. */ - predicate isSuccess() { success = true } - - override string toString() { - success = true and result = "assertion success" - or - success = false and result = "assertion failure" - } - } - - private class AssertionSplitKind extends SplitKind, TAssertionSplitKind { - override int getListOrder() { result = ConditionalCompletionSplitting::getNextListOrder() } - - override predicate isEnabled(AstNode cfe) { this.appliesTo(cfe) } - - override string toString() { result = "Assertion" } - } - - int getNextListOrder() { result = ConditionalCompletionSplitting::getNextListOrder() + 1 } - - private class AssertionSplitImpl extends SplitImpl instanceof AssertionSplit { - Assertion a; - boolean success; - int i; - - AssertionSplitImpl() { this = TAssertionSplit(a, i, success) } - - override AssertionSplitKind getKind() { any() } - - override predicate hasEntry(AstNode pred, AstNode succ, Completion c) { - exists(AssertMethod m | - last(a.getExpr(i), pred, c) and - succ(pred, succ, c) and - m = a.getAssertMethod() and - // The assertion only succeeds when all asserted arguments succeeded, so - // we only enter a "success" state after the last argument has succeeded. - // - // The split is only entered if we are not already in a "failing" state - // for one of the previous arguments, which ensures that the "success" - // state is only entered when all arguments succeed. This also means - // that if multiple arguments fail, then the first failing argument - // will determine the exception being thrown by the assertion. - if success = true then i = max(int j | exists(a.getExpr(j))) else any() - | - exists(boolean b | i = m.(BooleanAssertMethod).getAnAssertionIndex(b) | - c instanceof TrueCompletion and success = b - or - c instanceof FalseCompletion and success = b.booleanNot() - ) - or - exists(boolean b | i = m.(NullnessAssertMethod).getAnAssertionIndex(b) | - c.(NullnessCompletion).isNull() and success = b - or - c.(NullnessCompletion).isNonNull() and success = b.booleanNot() - ) - ) - } - - override predicate hasEntryScope(CfgScope scope, AstNode first) { none() } - - override predicate hasExit(AstNode pred, AstNode succ, Completion c) { - this.appliesTo(pred) and - pred = a and - succ(pred, succ, c) and - ( - success = true and - c instanceof NormalCompletion - or - success = false and - c = assertionCompletion(a, i) - ) - } - - override predicate hasExitScope(CfgScope scope, AstNode last, Completion c) { - this.appliesTo(last) and - last = a and - scopeLast(scope, last, c) and - ( - success = true and - c instanceof NormalCompletion - or - success = false and - c = assertionCompletion(a, i) - ) - } - - override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) { - this.appliesSucc(pred, succ, c) and - succ = getAnAssertionDescendant(a) - } - } -} diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 74fefbb4e39c..d03d4624f963 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -297,7 +297,7 @@ module Make< */ predicate isIntRange(int bound, boolean upper) { this = TIntRange(bound, upper) } - /** Holds if this value represents throwing an exception. */ + /** Holds if this value represents throwing an exception (or exiting). */ predicate isThrowsException() { this = TException(true) } /** Gets a textual representation of this value. */ @@ -362,12 +362,19 @@ module Make< v.asConstantValue() = c.asConstantValue() } + /** Holds if `t` is an exception-like successor type. */ + private predicate exceptionLike(SuccessorType t) { + t instanceof ExceptionSuccessor or + t instanceof ExitSuccessor + } + private predicate exceptionBranchPoint(BasicBlock bb1, BasicBlock normalSucc, BasicBlock excSucc) { - exists(SuccessorType norm, ExceptionSuccessor exc | + exists(SuccessorType norm, SuccessorType exc | bb1.getASuccessor(norm) = normalSucc and bb1.getASuccessor(exc) = excSucc and normalSucc != excSucc and - not norm instanceof ExceptionSuccessor + exceptionLike(exc) and + not exceptionLike(norm) ) }