@@ -50,7 +50,20 @@ private import SuccessorTypes
5050private import Splitting
5151private import semmle.code.csharp.ExprOrStmtParent
5252
53- abstract private class ControlFlowTree extends ControlFlowElement {
53+ /** An element that defines a new CFG scope. */
54+ class CfgScope extends Element , @top_level_exprorstmt_parent { }
55+
56+ module ControlFlowTree {
57+ private class Range_ = @callable or @control_flow_element;
58+
59+ class Range extends Element , Range_ { }
60+
61+ private predicate id ( Range x , Range y ) { x = y }
62+
63+ predicate idOf ( Range x , int y ) = equivalenceRelation( id / 2 ) ( x , y )
64+ }
65+
66+ abstract private class ControlFlowTree extends ControlFlowTree:: Range {
5467 /**
5568 * Holds if `first` is the first element executed within this control
5669 * flow element.
@@ -96,57 +109,17 @@ predicate last(ControlFlowTree cft, ControlFlowElement last, Completion c) {
96109 )
97110}
98111
99- pragma [ noinline]
100- private LabeledStmt getLabledStmt ( string label , Callable c ) {
101- result .getEnclosingCallable ( ) = c and
102- label = result .getLabel ( )
103- }
104-
105- pragma [ nomagic]
106- private predicate goto ( ControlFlowElement cfe , GotoCompletion gc , string label , Callable enclosing ) {
107- last ( _, cfe , gc ) and
108- // Special case: when a `goto` happens inside a `try` statement with a
109- // `finally` block, flow does not go directly to the target, but instead
110- // to the `finally` block (and from there possibly to the target)
111- not cfe = any ( Statements:: TryStmtTree t | t .hasFinally ( ) ) .getBlockOrCatchFinallyPred ( _) and
112- label = gc .getLabel ( ) and
113- enclosing = cfe .getEnclosingCallable ( )
114- }
115-
116112/**
117113 * Holds if `succ` is a control flow successor for `pred`, given that `pred`
118114 * finishes with completion `c`.
119115 */
120116pragma [ nomagic]
121117predicate succ ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
122118 any ( ControlFlowTree cft ) .succ ( pred , succ , c )
123- or
124- exists ( Constructor con , InitializerSplitting:: InitializedInstanceMember m , int i |
125- last ( m .getInitializer ( ) , pred , c ) and
126- c instanceof NormalCompletion and
127- InitializerSplitting:: constructorInitializeOrder ( con , m , i )
128- |
129- // Flow from one member initializer to the next
130- exists ( InitializerSplitting:: InitializedInstanceMember next |
131- InitializerSplitting:: constructorInitializeOrder ( con , next , i + 1 ) and
132- first ( next .getInitializer ( ) , succ )
133- )
134- or
135- // Flow from last member initializer to constructor body
136- m = InitializerSplitting:: lastConstructorInitializer ( con ) and
137- first ( con .getBody ( ) , succ )
138- )
139- or
140- // Flow from element with `goto` completion to first element of relevant
141- // target
142- exists ( string label , Callable enclosing |
143- goto ( pred , c , label , enclosing ) and
144- first ( getLabledStmt ( label , enclosing ) , succ )
145- )
146119}
147120
148121/** Holds if `first` is first executed when entering `scope`. */
149- predicate succEntry ( @top_level_exprorstmt_parent scope , ControlFlowElement first ) {
122+ predicate scopeFirst ( CfgScope scope , ControlFlowElement first ) {
150123 scope =
151124 any ( Callable c |
152125 if exists ( c .( Constructor ) .getInitializer ( ) )
@@ -166,7 +139,7 @@ predicate succEntry(@top_level_exprorstmt_parent scope, ControlFlowElement first
166139}
167140
168141/** Holds if `scope` is exited when `last` finishes with completion `c`. */
169- predicate succExit ( ControlFlowElement last , Callable scope , Completion c ) {
142+ predicate scopeLast ( Callable scope , ControlFlowElement last , Completion c ) {
170143 last ( scope .getBody ( ) , last , c ) and
171144 not c instanceof GotoCompletion
172145 or
@@ -177,6 +150,33 @@ predicate succExit(ControlFlowElement last, Callable scope, Completion c) {
177150 )
178151}
179152
153+ private class CallableTree extends ControlFlowTree , Callable {
154+ final override predicate propagatesAbnormal ( ControlFlowElement child ) { none ( ) }
155+
156+ final override predicate first ( ControlFlowElement first ) { none ( ) }
157+
158+ final override predicate last ( ControlFlowElement last , Completion c ) { none ( ) }
159+
160+ final override predicate succ ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
161+ exists ( Constructor con , InitializerSplitting:: InitializedInstanceMember m , int i |
162+ this = con and
163+ last ( m .getInitializer ( ) , pred , c ) and
164+ c instanceof NormalCompletion and
165+ InitializerSplitting:: constructorInitializeOrder ( con , m , i )
166+ |
167+ // Flow from one member initializer to the next
168+ exists ( InitializerSplitting:: InitializedInstanceMember next |
169+ InitializerSplitting:: constructorInitializeOrder ( con , next , i + 1 ) and
170+ first ( next .getInitializer ( ) , succ )
171+ )
172+ or
173+ // Flow from last member initializer to constructor body
174+ m = InitializerSplitting:: lastConstructorInitializer ( con ) and
175+ first ( con .getBody ( ) , succ )
176+ )
177+ }
178+ }
179+
180180/**
181181 * A control flow element where the children are evaluated following a
182182 * standard left-to-right evaluation. The actual evaluation order is
@@ -371,7 +371,7 @@ module Expressions {
371371 not this instanceof ConstructorInitializer
372372 }
373373
374- final override ControlFlowTree getChildElement ( int i ) { result = getExprChild ( this , i ) }
374+ final override ControlFlowElement getChildElement ( int i ) { result = getExprChild ( this , i ) }
375375
376376 final override predicate first ( ControlFlowElement first ) {
377377 first ( this .getFirstChild ( ) , first )
@@ -933,18 +933,18 @@ module Statements {
933933 // The following statements need special treatment
934934 not this instanceof IfStmt and
935935 not this instanceof SwitchStmt and
936- ( this instanceof DefaultCase or not this instanceof CaseStmt ) and
936+ not this instanceof CaseStmt and
937937 not this instanceof LoopStmt and
938938 not this instanceof TryStmt and
939939 not this instanceof SpecificCatchClause and
940- not this instanceof JumpStmt
940+ not this instanceof JumpStmt and
941+ not this instanceof LabeledStmt
941942 }
942943
943944 private ControlFlowTree getChildElement0 ( int i ) {
944945 not this instanceof GeneralCatchClause and
945946 not this instanceof FixedStmt and
946947 not this instanceof UsingBlockStmt and
947- not this instanceof DefaultCase and
948948 result = this .getChild ( i )
949949 or
950950 this = any ( GeneralCatchClause gcc | i = 0 and result = gcc .getBlock ( ) )
@@ -967,12 +967,9 @@ module Statements {
967967 result = us .getBody ( ) and
968968 i = max ( [ 1 , count ( us .getVariableDeclExpr ( _) ) ] )
969969 )
970- or
971- result = this .( DefaultCase ) .getStmt ( ) and
972- i = 0
973970 }
974971
975- final override ControlFlowTree getChildElement ( int i ) {
972+ final override ControlFlowElement getChildElement ( int i ) {
976973 result =
977974 rank [ i + 1 ] ( ControlFlowElement cfe , int j | cfe = this .getChildElement0 ( j ) | cfe order by j )
978975 }
@@ -1045,8 +1042,9 @@ module Statements {
10451042 last ( this .getStmt ( _) , last , c ) and
10461043 not c instanceof BreakCompletion and
10471044 not c instanceof NormalCompletion and
1048- not getLabledStmt ( c .( GotoCompletion ) .getLabel ( ) , this .getEnclosingCallable ( ) ) instanceof
1049- CaseStmt
1045+ not any ( LabeledStmtTree t |
1046+ t .hasLabelInCallable ( c .( GotoCompletion ) .getLabel ( ) , this .getEnclosingCallable ( ) )
1047+ ) instanceof CaseStmt
10501048 or
10511049 // Last case exits with a non-match
10521050 exists ( CaseStmt cs , int last_ |
@@ -1355,26 +1353,30 @@ module Statements {
13551353 /**
13561354 * Gets a last element from a `try` or `catch` block of this `try` statement
13571355 * that may finish with completion `c`, such that control may be transferred
1358- * to the `finally` block (if it exists).
1356+ * to the `finally` block (if it exists), but only if `finalizable = true` .
13591357 */
13601358 pragma [ nomagic]
1361- ControlFlowElement getBlockOrCatchFinallyPred ( Completion c ) {
1362- this .lastBlock ( result , c ) and
1359+ ControlFlowElement getAFinallyPredecessor ( Completion c , boolean finalizable ) {
1360+ // Exit completions skip the `finally` block
1361+ ( if c instanceof ExitCompletion then finalizable = false else finalizable = true ) and
13631362 (
1364- // Any non-throw completion from the `try` block will always continue directly
1365- // to the `finally` block
1366- not c instanceof ThrowCompletion
1363+ this .lastBlock ( result , c ) and
1364+ (
1365+ // Any non-throw completion from the `try` block will always continue directly
1366+ // to the `finally` block
1367+ not c instanceof ThrowCompletion
1368+ or
1369+ // Any completion from the `try` block will continue to the `finally` block
1370+ // when there are no catch clauses
1371+ not exists ( this .getACatchClause ( ) )
1372+ )
1373+ or
1374+ // Last element from any of the `catch` clause blocks continues to the `finally` block
1375+ result = lastCatchClauseBlock ( this .getACatchClause ( ) , c )
13671376 or
1368- // Any completion from the `try` block will continue to the `finally` block
1369- // when there are no catch clauses
1370- not exists ( this .getACatchClause ( ) )
1377+ // Last element of last `catch` clause continues to the `finally` block
1378+ result = lastLastCatchClause ( this .getACatchClause ( ) , c )
13711379 )
1372- or
1373- // Last element from any of the `catch` clause blocks continues to the `finally` block
1374- result = lastCatchClauseBlock ( this .getACatchClause ( ) , c )
1375- or
1376- // Last element of last `catch` clause continues to the `finally` block
1377- result = lastLastCatchClause ( this .getACatchClause ( ) , c )
13781380 }
13791381
13801382 pragma [ nomagic]
@@ -1387,19 +1389,19 @@ module Statements {
13871389 ControlFlowElement last , NormalCompletion finally , Completion outer , int nestLevel
13881390 ) {
13891391 this .lastFinally0 ( last , finally ) and
1390- exists ( this .getBlockOrCatchFinallyPred ( any ( Completion c0 | outer = c0 .getOuterCompletion ( ) ) ) ) and
1392+ exists (
1393+ this .getAFinallyPredecessor ( any ( Completion c0 | outer = c0 .getOuterCompletion ( ) ) , true )
1394+ ) and
13911395 nestLevel = this .nestLevel ( )
13921396 }
13931397
13941398 final override predicate last ( ControlFlowElement last , Completion c ) {
1395- last = this .getBlockOrCatchFinallyPred ( c ) and
1396- (
1399+ exists ( boolean finalizable | last = this .getAFinallyPredecessor ( c , finalizable ) |
13971400 // If there is no `finally` block, last elements are from the body, from
13981401 // the blocks of one of the `catch` clauses, or from the last `catch` clause
13991402 not this .hasFinally ( )
14001403 or
1401- // Exit completions ignore the `finally` block
1402- c instanceof ExitCompletion
1404+ finalizable = false
14031405 )
14041406 or
14051407 this .lastFinally ( last , c , any ( NormalCompletion nc ) , _)
@@ -1433,43 +1435,22 @@ module Statements {
14331435 first ( this .getCatchClause ( 0 ) , succ )
14341436 or
14351437 exists ( CatchClause cc , int i | cc = this .getCatchClause ( i ) |
1438+ // Flow from one `catch` clause to the next
14361439 pred = cc and
14371440 last ( this .getCatchClause ( i ) , cc , c ) and
1438- (
1439- // Flow from one `catch` clause to the next
1440- first ( this .getCatchClause ( i + 1 ) , succ ) and
1441- c = any ( MatchingCompletion mc | not mc .isMatch ( ) )
1442- or
1443- // Flow from last `catch` clause to first element of `finally` block
1444- this .getCatchClause ( i ) .isLast ( ) and
1445- first ( this .getFinally ( ) , succ ) and
1446- c instanceof ThrowCompletion // inherited from `try` block
1447- )
1441+ first ( this .getCatchClause ( i + 1 ) , succ ) and
1442+ c = any ( MatchingCompletion mc | not mc .isMatch ( ) )
14481443 or
1444+ // Flow from last element of `catch` clause filter to next `catch` clause
14491445 last ( this .getCatchClause ( i ) , pred , c ) and
14501446 last ( cc .getFilterClause ( ) , pred , _) and
1451- (
1452- // Flow from last element of `catch` clause filter to next `catch` clause
1453- first ( this .getCatchClause ( i + 1 ) , succ ) and
1454- c instanceof FalseCompletion
1455- or
1456- // Flow from last element of `catch` clause filter, of last clause, to first
1457- // element of `finally` block
1458- this .getCatchClause ( i ) .isLast ( ) and
1459- first ( this .getFinally ( ) , succ ) and
1460- c instanceof ThrowCompletion // inherited from `try` block
1461- )
1462- or
1463- // Flow from last element of a `catch` block to first element of `finally` block
1464- pred = lastCatchClauseBlock ( cc , c ) and
1465- first ( this .getFinally ( ) , succ )
1447+ first ( this .getCatchClause ( i + 1 ) , succ ) and
1448+ c instanceof FalseCompletion
14661449 )
14671450 or
1468- // Flow from last element of `try` block to first element of `finally` block
1469- this .lastBlock ( pred , c ) and
1470- first ( this .getFinally ( ) , succ ) and
1471- not c instanceof ExitCompletion and
1472- ( c instanceof ThrowCompletion implies not exists ( this .getACatchClause ( ) ) )
1451+ // Flow into `finally` block
1452+ pred = getAFinallyPredecessor ( c , true ) and
1453+ first ( this .getFinally ( ) , succ )
14731454 }
14741455 }
14751456
@@ -1587,6 +1568,51 @@ module Statements {
15871568 c instanceof NormalCompletion
15881569 }
15891570 }
1571+
1572+ pragma [ nomagic]
1573+ private predicate goto ( ControlFlowElement cfe , GotoCompletion gc , string label , Callable enclosing ) {
1574+ last ( _, cfe , gc ) and
1575+ // Special case: when a `goto` happens inside a `try` statement with a
1576+ // `finally` block, flow does not go directly to the target, but instead
1577+ // to the `finally` block (and from there possibly to the target)
1578+ not cfe = any ( Statements:: TryStmtTree t | t .hasFinally ( ) ) .getAFinallyPredecessor ( _, true ) and
1579+ label = gc .getLabel ( ) and
1580+ enclosing = cfe .getEnclosingCallable ( )
1581+ }
1582+
1583+ private class LabeledStmtTree extends PreOrderTree , LabeledStmt {
1584+ final override predicate propagatesAbnormal ( ControlFlowElement child ) { none ( ) }
1585+
1586+ final override predicate last ( ControlFlowElement last , Completion c ) {
1587+ if this instanceof DefaultCase
1588+ then last ( this .getStmt ( ) , last , c )
1589+ else (
1590+ not this instanceof CaseStmt and
1591+ last = this and
1592+ c .isValidFor ( this )
1593+ )
1594+ }
1595+
1596+ pragma [ noinline]
1597+ predicate hasLabelInCallable ( string label , Callable c ) {
1598+ this .getEnclosingCallable ( ) = c and
1599+ label = this .getLabel ( )
1600+ }
1601+
1602+ final override predicate succ ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1603+ this instanceof DefaultCase and
1604+ pred = this and
1605+ first ( this .getStmt ( ) , succ ) and
1606+ c instanceof SimpleCompletion
1607+ or
1608+ // Flow from element with matching `goto` completion to this statement
1609+ exists ( string label , Callable enclosing |
1610+ goto ( pred , c , label , enclosing ) and
1611+ this .hasLabelInCallable ( label , enclosing ) and
1612+ succ = this
1613+ )
1614+ }
1615+ }
15901616}
15911617
15921618cached
0 commit comments