@@ -54,6 +54,28 @@ private newtype TCompletion =
5454 exists ( boolean b | inner = TBooleanCompletion ( b ) and outer = TBooleanCompletion ( b .booleanNot ( ) ) )
5555 }
5656
57+ pragma [ noinline]
58+ private predicate completionIsValidForStmt ( Stmt s , Completion c ) {
59+ s instanceof BreakStmt and
60+ c = TBreakCompletion ( )
61+ or
62+ s instanceof ContinueStmt and
63+ c = TContinueCompletion ( )
64+ or
65+ s instanceof GotoStmt and
66+ c = TGotoCompletion ( s .( GotoStmt ) .getLabel ( ) )
67+ or
68+ s instanceof ReturnStmt and
69+ c = TReturnCompletion ( )
70+ or
71+ s instanceof YieldBreakStmt and
72+ // `yield break` behaves like a return statement
73+ c = TReturnCompletion ( )
74+ or
75+ mustHaveEmptinessCompletion ( s ) and
76+ c = TEmptinessCompletion ( _)
77+ }
78+
5779/**
5880 * A completion of a statement or an expression.
5981 */
@@ -68,76 +90,59 @@ class Completion extends TCompletion {
6890 * otherwise it is a normal non-Boolean completion.
6991 */
7092 predicate isValidFor ( ControlFlowElement cfe ) {
71- if cfe instanceof NonReturningCall
72- then this = cfe .( NonReturningCall ) .getACompletion ( )
73- else (
74- this = TThrowCompletion ( cfe .( TriedControlFlowElement ) .getAThrownException ( ) )
75- or
76- cfe instanceof ThrowElement and
77- this = TThrowCompletion ( cfe .( ThrowElement ) .getThrownExceptionType ( ) )
78- or
79- cfe instanceof BreakStmt and
80- this = TBreakCompletion ( )
81- or
82- cfe instanceof ContinueStmt and
83- this = TContinueCompletion ( )
84- or
85- cfe instanceof GotoStmt and
86- this = TGotoCompletion ( cfe .( GotoStmt ) .getLabel ( ) )
87- or
88- cfe instanceof ReturnStmt and
89- this = TReturnCompletion ( )
90- or
91- cfe instanceof YieldBreakStmt and
92- // `yield break` behaves like a return statement
93- this = TReturnCompletion ( )
93+ cfe instanceof NonReturningCall and
94+ this = cfe .( NonReturningCall ) .getACompletion ( )
95+ or
96+ this = TThrowCompletion ( cfe .( TriedControlFlowElement ) .getAThrownException ( ) )
97+ or
98+ cfe instanceof ThrowElement and
99+ this = TThrowCompletion ( cfe .( ThrowElement ) .getThrownExceptionType ( ) )
100+ or
101+ completionIsValidForStmt ( cfe , this )
102+ or
103+ mustHaveBooleanCompletion ( cfe ) and
104+ (
105+ exists ( boolean value | isBooleanConstant ( cfe , value ) | this = TBooleanCompletion ( value ) )
94106 or
95- mustHaveBooleanCompletion ( cfe ) and
96- (
97- exists ( boolean value | isBooleanConstant ( cfe , value ) | this = TBooleanCompletion ( value ) )
98- or
99- not isBooleanConstant ( cfe , _) and
100- this = TBooleanCompletion ( _)
101- or
102- // Corner case: In `if (x ?? y) { ... }`, `x` must have both a `true`
103- // completion, a `false` completion, and a `null` completion (but not a
104- // non-`null` completion)
105- mustHaveNullnessCompletion ( cfe ) and
106- this = TNullnessCompletion ( true )
107- )
107+ not isBooleanConstant ( cfe , _) and
108+ this = TBooleanCompletion ( _)
108109 or
110+ // Corner case: In `if (x ?? y) { ... }`, `x` must have both a `true`
111+ // completion, a `false` completion, and a `null` completion (but not a
112+ // non-`null` completion)
109113 mustHaveNullnessCompletion ( cfe ) and
110- not mustHaveBooleanCompletion ( cfe ) and
111- (
112- exists ( boolean value | isNullnessConstant ( cfe , value ) | this = TNullnessCompletion ( value ) )
113- or
114- not isNullnessConstant ( cfe , _) and
115- this = TNullnessCompletion ( _)
116- )
117- or
118- mustHaveMatchingCompletion ( cfe ) and
119- (
120- exists ( boolean value | isMatchingConstant ( cfe , value ) | this = TMatchingCompletion ( value ) )
121- or
122- not isMatchingConstant ( cfe , _) and
123- this = TMatchingCompletion ( _)
124- )
114+ this = TNullnessCompletion ( true )
115+ )
116+ or
117+ mustHaveNullnessCompletion ( cfe ) and
118+ not mustHaveBooleanCompletion ( cfe ) and
119+ (
120+ exists ( boolean value | isNullnessConstant ( cfe , value ) | this = TNullnessCompletion ( value ) )
125121 or
126- mustHaveEmptinessCompletion ( cfe ) and
127- this = TEmptinessCompletion ( _)
122+ not isNullnessConstant ( cfe , _) and
123+ this = TNullnessCompletion ( _)
124+ )
125+ or
126+ mustHaveMatchingCompletion ( cfe ) and
127+ (
128+ exists ( boolean value | isMatchingConstant ( cfe , value ) | this = TMatchingCompletion ( value ) )
128129 or
129- not cfe instanceof ThrowElement and
130- not cfe instanceof BreakStmt and
131- not cfe instanceof ContinueStmt and
132- not cfe instanceof GotoStmt and
133- not cfe instanceof ReturnStmt and
134- not cfe instanceof YieldBreakStmt and
135- not mustHaveBooleanCompletion ( cfe ) and
136- not mustHaveNullnessCompletion ( cfe ) and
137- not mustHaveMatchingCompletion ( cfe ) and
138- not mustHaveEmptinessCompletion ( cfe ) and
139- this = TNormalCompletion ( )
130+ not isMatchingConstant ( cfe , _) and
131+ this = TMatchingCompletion ( _)
140132 )
133+ or
134+ not cfe instanceof NonReturningCall and
135+ not cfe instanceof ThrowElement and
136+ not cfe instanceof BreakStmt and
137+ not cfe instanceof ContinueStmt and
138+ not cfe instanceof GotoStmt and
139+ not cfe instanceof ReturnStmt and
140+ not cfe instanceof YieldBreakStmt and
141+ not mustHaveBooleanCompletion ( cfe ) and
142+ not mustHaveNullnessCompletion ( cfe ) and
143+ not mustHaveMatchingCompletion ( cfe ) and
144+ not mustHaveEmptinessCompletion ( cfe ) and
145+ this = TNormalCompletion ( )
141146 }
142147
143148 /**
@@ -264,7 +269,10 @@ private predicate assemblyCompiledWithCoreLib(Assembly a, CoreLib core) {
264269private class TriedControlFlowElement extends ControlFlowElement {
265270 TryStmt try ;
266271
267- TriedControlFlowElement ( ) { this = try .getATriedElement ( ) }
272+ TriedControlFlowElement ( ) {
273+ this = try .getATriedElement ( ) and
274+ not this instanceof NonReturningCall
275+ }
268276
269277 /**
270278 * Gets an exception class that is potentially thrown by this element, if any.
@@ -372,7 +380,8 @@ private predicate invalidCastCandidate(CastExpr ce) {
372380 */
373381private predicate mustHaveBooleanCompletion ( Expr e ) {
374382 inBooleanContext ( e , _) and
375- not inBooleanContext ( e .getAChildExpr ( ) , true )
383+ not inBooleanContext ( e .getAChildExpr ( ) , true ) and
384+ not e instanceof NonReturningCall
376385}
377386
378387/**
@@ -442,7 +451,8 @@ private predicate inBooleanContext(Expr e, boolean isBooleanCompletionForParent)
442451 */
443452private predicate mustHaveNullnessCompletion ( Expr e ) {
444453 inNullnessContext ( e , _) and
445- not inNullnessContext ( e .getAChildExpr ( ) , true )
454+ not inNullnessContext ( e .getAChildExpr ( ) , true ) and
455+ not e instanceof NonReturningCall
446456}
447457
448458/**
0 commit comments