44
55import csharp
66private import ControlFlow:: SuccessorTypes
7+ private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl
8+ private import CfgImpl:: BasicBlocks as BasicBlocksImpl
79
810/**
911 * A basic block, that is, a maximal straight-line sequence of control flow nodes
1012 * without branches or joins.
1113 */
12- class BasicBlock extends TBasicBlockStart {
13- /** Gets an immediate successor of this basic block, if any. */
14- BasicBlock getASuccessor ( ) { result .getFirstNode ( ) = this .getLastNode ( ) .getASuccessor ( ) }
15-
14+ final class BasicBlock extends BasicBlocksImpl:: BasicBlock {
1615 /** Gets an immediate successor of this basic block of a given type, if any. */
17- BasicBlock getASuccessorByType ( ControlFlow:: SuccessorType t ) {
18- result .getFirstNode ( ) = this .getLastNode ( ) .getASuccessorByType ( t )
19- }
20-
21- /** Gets an immediate predecessor of this basic block, if any. */
22- BasicBlock getAPredecessor ( ) { result .getASuccessor ( ) = this }
16+ BasicBlock getASuccessorByType ( ControlFlow:: SuccessorType t ) { result = this .getASuccessor ( t ) }
2317
2418 /** Gets an immediate predecessor of this basic block of a given type, if any. */
2519 BasicBlock getAPredecessorByType ( ControlFlow:: SuccessorType t ) {
26- result . getASuccessorByType ( t ) = this
20+ result = this . getAPredecessor ( t )
2721 }
2822
2923 /**
@@ -65,23 +59,20 @@ class BasicBlock extends TBasicBlockStart {
6559 }
6660
6761 /** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
68- ControlFlow:: Node getNode ( int pos ) { bbIndex ( this . getFirstNode ( ) , result , pos ) }
62+ ControlFlow:: Node getNode ( int pos ) { result = super . getNode ( pos ) }
6963
7064 /** Gets a control flow node in this basic block. */
71- ControlFlow:: Node getANode ( ) { result = this . getNode ( _ ) }
65+ ControlFlow:: Node getANode ( ) { result = super . getANode ( ) }
7266
7367 /** Gets the first control flow node in this basic block. */
74- ControlFlow:: Node getFirstNode ( ) { this = TBasicBlockStart ( result ) }
68+ ControlFlow:: Node getFirstNode ( ) { result = super . getFirstNode ( ) }
7569
7670 /** Gets the last control flow node in this basic block. */
77- ControlFlow:: Node getLastNode ( ) { result = this . getNode ( this . length ( ) - 1 ) }
71+ ControlFlow:: Node getLastNode ( ) { result = super . getLastNode ( ) }
7872
7973 /** Gets the callable that this basic block belongs to. */
8074 final Callable getCallable ( ) { result = this .getFirstNode ( ) .getEnclosingCallable ( ) }
8175
82- /** Gets the length of this basic block. */
83- int length ( ) { result = strictcount ( this .getANode ( ) ) }
84-
8576 /**
8677 * Holds if this basic block immediately dominates basic block `bb`.
8778 *
@@ -103,7 +94,7 @@ class BasicBlock extends TBasicBlockStart {
10394 * basic block on line 4 (all paths from the entry point of `M`
10495 * to `return s.Length;` must go through the null check).
10596 */
106- predicate immediatelyDominates ( BasicBlock bb ) { bbIDominates ( this , bb ) }
97+ predicate immediatelyDominates ( BasicBlock bb ) { super . immediatelyDominates ( bb ) }
10798
10899 /**
109100 * Holds if this basic block strictly dominates basic block `bb`.
@@ -126,7 +117,7 @@ class BasicBlock extends TBasicBlockStart {
126117 * basic block on line 4 (all paths from the entry point of `M`
127118 * to `return s.Length;` must go through the null check).
128119 */
129- predicate strictlyDominates ( BasicBlock bb ) { bbIDominates + ( this , bb ) }
120+ predicate strictlyDominates ( BasicBlock bb ) { super . strictlyDominates ( bb ) }
130121
131122 /**
132123 * Holds if this basic block dominates basic block `bb`.
@@ -178,15 +169,7 @@ class BasicBlock extends TBasicBlockStart {
178169 * `Console.Write(x);`. Also, the basic block starting on line 2
179170 * does not dominate the basic block on line 6.
180171 */
181- predicate inDominanceFrontier ( BasicBlock df ) {
182- this .dominatesPredecessor ( df ) and
183- not this .strictlyDominates ( df )
184- }
185-
186- /**
187- * Holds if this basic block dominates a predecessor of `df`.
188- */
189- private predicate dominatesPredecessor ( BasicBlock df ) { this .dominates ( df .getAPredecessor ( ) ) }
172+ predicate inDominanceFrontier ( BasicBlock df ) { super .inDominanceFrontier ( df ) }
190173
191174 /**
192175 * Gets the basic block that immediately dominates this basic block, if any.
@@ -208,7 +191,7 @@ class BasicBlock extends TBasicBlockStart {
208191 * the basic block online 4 (all paths from the entry point of `M`
209192 * to `return s.Length;` must go through the null check.
210193 */
211- BasicBlock getImmediateDominator ( ) { bbIDominates ( result , this ) }
194+ BasicBlock getImmediateDominator ( ) { result = super . getImmediateDominator ( ) }
212195
213196 /**
214197 * Holds if this basic block strictly post-dominates basic block `bb`.
@@ -234,7 +217,7 @@ class BasicBlock extends TBasicBlockStart {
234217 * line 3 (all paths to the exit point of `M` from `return s.Length;`
235218 * must go through the `WriteLine` call).
236219 */
237- predicate strictlyPostDominates ( BasicBlock bb ) { bbIPostDominates + ( this , bb ) }
220+ predicate strictlyPostDominates ( BasicBlock bb ) { super . strictlyPostDominates ( bb ) }
238221
239222 /**
240223 * Holds if this basic block post-dominates basic block `bb`.
@@ -262,10 +245,7 @@ class BasicBlock extends TBasicBlockStart {
262245 * This predicate is *reflexive*, so for example `Console.WriteLine("M");`
263246 * post-dominates itself.
264247 */
265- predicate postDominates ( BasicBlock bb ) {
266- this .strictlyPostDominates ( bb ) or
267- this = bb
268- }
248+ predicate postDominates ( BasicBlock bb ) { super .postDominates ( bb ) }
269249
270250 /**
271251 * Holds if this basic block is in a loop in the control flow graph. This
@@ -274,230 +254,44 @@ class BasicBlock extends TBasicBlockStart {
274254 * necessary back edges are unreachable.
275255 */
276256 predicate inLoop ( ) { this .getASuccessor + ( ) = this }
277-
278- /** Gets a textual representation of this basic block. */
279- string toString ( ) { result = this .getFirstNode ( ) .toString ( ) }
280-
281- /** Gets the location of this basic block. */
282- Location getLocation ( ) { result = this .getFirstNode ( ) .getLocation ( ) }
283- }
284-
285- /**
286- * Internal implementation details.
287- */
288- cached
289- private module Internal {
290- /** Internal representation of basic blocks. */
291- cached
292- newtype TBasicBlock = TBasicBlockStart ( ControlFlow:: Node cfn ) { startsBB ( cfn ) }
293-
294- /** Holds if `cfn` starts a new basic block. */
295- private predicate startsBB ( ControlFlow:: Node cfn ) {
296- not exists ( cfn .getAPredecessor ( ) ) and exists ( cfn .getASuccessor ( ) )
297- or
298- cfn .isJoin ( )
299- or
300- cfn .getAPredecessor ( ) .isBranch ( )
301- or
302- /*
303- * In cases such as
304- * ```csharp
305- * if (b)
306- * M()
307- * ```
308- * where the `false` edge out of `b` is not present (because we can prove it
309- * impossible), we still split up the basic block in two, in order to generate
310- * a `ConditionBlock` which can be used by the guards library.
311- */
312-
313- exists ( cfn .getAPredecessorByType ( any ( ControlFlow:: SuccessorTypes:: ConditionalSuccessor s ) ) )
314- }
315-
316- /**
317- * Holds if `succ` is a control flow successor of `pred` within
318- * the same basic block.
319- */
320- private predicate intraBBSucc ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
321- succ = pred .getASuccessor ( ) and
322- not startsBB ( succ )
323- }
324-
325- /**
326- * Holds if `cfn` is the `i`th node in basic block `bb`.
327- *
328- * In other words, `i` is the shortest distance from a node `bb`
329- * that starts a basic block to `cfn` along the `intraBBSucc` relation.
330- */
331- cached
332- predicate bbIndex ( ControlFlow:: Node bbStart , ControlFlow:: Node cfn , int i ) =
333- shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
334-
335- /**
336- * Holds if the first node of basic block `succ` is a control flow
337- * successor of the last node of basic block `pred`.
338- */
339- private predicate succBB ( BasicBlock pred , BasicBlock succ ) { succ = pred .getASuccessor ( ) }
340-
341- /** Holds if `dom` is an immediate dominator of `bb`. */
342- cached
343- predicate bbIDominates ( BasicBlock dom , BasicBlock bb ) =
344- idominance( entryBB / 1 , succBB / 2 ) ( _, dom , bb )
345-
346- /** Holds if `pred` is a basic block predecessor of `succ`. */
347- private predicate predBB ( BasicBlock succ , BasicBlock pred ) { succBB ( pred , succ ) }
348-
349- /** Holds if `bb` is an exit basic block that represents normal exit. */
350- private predicate normalExitBB ( BasicBlock bb ) {
351- bb .getANode ( ) .( ControlFlow:: Nodes:: AnnotatedExitNode ) .isNormal ( )
352- }
353-
354- /** Holds if `dom` is an immediate post-dominator of `bb`. */
355- cached
356- predicate bbIPostDominates ( BasicBlock dom , BasicBlock bb ) =
357- idominance( normalExitBB / 1 , predBB / 2 ) ( _, dom , bb )
358257}
359258
360- private import Internal
361-
362259/**
363260 * An entry basic block, that is, a basic block whose first node is
364- * the entry node of a callable .
261+ * an entry node.
365262 */
366- class EntryBasicBlock extends BasicBlock {
367- EntryBasicBlock ( ) { entryBB ( this ) }
368- }
369-
370- /** Holds if `bb` is an entry basic block. */
371- private predicate entryBB ( BasicBlock bb ) {
372- bb .getFirstNode ( ) instanceof ControlFlow:: Nodes:: EntryNode
373- }
263+ final class EntryBasicBlock extends BasicBlock , BasicBlocksImpl:: EntryBasicBlock { }
374264
375265/**
376- * An annotated exit basic block, that is, a basic block that contains
377- * an annotated exit node.
266+ * An annotated exit basic block, that is, a basic block that contains an
267+ * annotated exit node.
378268 */
379- class AnnotatedExitBasicBlock extends BasicBlock {
380- private boolean isNormal ;
381-
382- AnnotatedExitBasicBlock ( ) {
383- this .getANode ( ) =
384- any ( ControlFlow:: Nodes:: AnnotatedExitNode n |
385- if n .isNormal ( ) then isNormal = true else isNormal = false
386- )
387- }
388-
389- /** Holds if this block represents a normal exit. */
390- predicate isNormal ( ) { isNormal = true }
391- }
269+ final class AnnotatedExitBasicBlock extends BasicBlock , BasicBlocksImpl:: AnnotatedExitBasicBlock { }
392270
393271/**
394272 * An exit basic block, that is, a basic block whose last node is
395- * the exit node of a callable .
273+ * an exit node.
396274 */
397- class ExitBasicBlock extends BasicBlock {
398- ExitBasicBlock ( ) { this .getLastNode ( ) instanceof ControlFlow:: Nodes:: ExitNode }
399- }
400-
401- private module JoinBlockPredecessors {
402- private import ControlFlow:: Nodes
403- private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as Impl
404-
405- int getId ( JoinBlockPredecessor jbp ) {
406- exists ( Impl:: AstNode n | result = n .getId ( ) |
407- n = jbp .getFirstNode ( ) .getAstNode ( )
408- or
409- n = jbp .( EntryBasicBlock ) .getCallable ( )
410- )
411- }
412-
413- string getSplitString ( JoinBlockPredecessor jbp ) {
414- result = jbp .getFirstNode ( ) .( ElementNode ) .getSplitsString ( )
415- or
416- not exists ( jbp .getFirstNode ( ) .( ElementNode ) .getSplitsString ( ) ) and
417- result = ""
418- }
419- }
275+ final class ExitBasicBlock extends BasicBlock , BasicBlocksImpl:: ExitBasicBlock { }
420276
421277/** A basic block with more than one predecessor. */
422- class JoinBlock extends BasicBlock {
423- JoinBlock ( ) { this .getFirstNode ( ) .isJoin ( ) }
424-
425- /**
426- * Gets the `i`th predecessor of this join block, with respect to some
427- * arbitrary order.
428- */
429- cached
430- JoinBlockPredecessor getJoinBlockPredecessor ( int i ) {
431- result =
432- rank [ i + 1 ] ( JoinBlockPredecessor jbp |
433- jbp = this .getAPredecessor ( )
434- |
435- jbp order by JoinBlockPredecessors:: getId ( jbp ) , JoinBlockPredecessors:: getSplitString ( jbp )
436- )
437- }
278+ final class JoinBlock extends BasicBlock , BasicBlocksImpl:: JoinBasicBlock {
279+ JoinBlockPredecessor getJoinBlockPredecessor ( int i ) { result = super .getJoinBlockPredecessor ( i ) }
438280}
439281
440282/** A basic block that is an immediate predecessor of a join block. */
441- class JoinBlockPredecessor extends BasicBlock {
442- JoinBlockPredecessor ( ) { this .getASuccessor ( ) instanceof JoinBlock }
443- }
444-
445- /** A basic block that terminates in a condition, splitting the subsequent control flow. */
446- class ConditionBlock extends BasicBlock {
447- ConditionBlock ( ) { this .getLastNode ( ) .isCondition ( ) }
283+ final class JoinBlockPredecessor extends BasicBlock , BasicBlocksImpl:: JoinPredecessorBasicBlock { }
448284
449- /**
450- * Holds if basic block `succ` is immediately controlled by this basic
451- * block with conditional value `s`. That is, `succ` is an immediate
452- * successor of this block, and `succ` can only be reached from
453- * the callable entry point by going via the `s` edge out of this basic block.
454- */
455- pragma [ nomagic]
285+ /**
286+ * A basic block that terminates in a condition, splitting the subsequent
287+ * control flow.
288+ */
289+ final class ConditionBlock extends BasicBlock , BasicBlocksImpl:: ConditionBasicBlock {
456290 predicate immediatelyControls ( BasicBlock succ , ConditionalSuccessor s ) {
457- succ = this .getASuccessorByType ( s ) and
458- forall ( BasicBlock pred | pred = succ .getAPredecessor ( ) and pred != this | succ .dominates ( pred ) )
291+ super .immediatelyControls ( succ , s )
459292 }
460293
461- /**
462- * Holds if basic block `controlled` is controlled by this basic block with
463- * conditional value `s`. That is, `controlled` can only be reached from
464- * the callable entry point by going via the `s` edge out of this basic block.
465- */
466294 predicate controls ( BasicBlock controlled , ConditionalSuccessor s ) {
467- /*
468- * For this block to control the block `controlled` with `testIsTrue` the following must be true:
469- * Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
470- * Execution must have passed through the `testIsTrue` edge leaving `this`.
471- *
472- * Although "passed through the true edge" implies that `this.getATrueSuccessor()` dominates `controlled`,
473- * the reverse is not true, as flow may have passed through another edge to get to `this.getATrueSuccessor()`
474- * so we need to assert that `this.getATrueSuccessor()` dominates `controlled` *and* that
475- * all predecessors of `this.getATrueSuccessor()` are either `this` or dominated by `this.getATrueSuccessor()`.
476- *
477- * For example, in the following C# snippet:
478- * ```csharp
479- * if (x)
480- * controlled;
481- * false_successor;
482- * uncontrolled;
483- * ```
484- * `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
485- * or dominated by itself. Whereas in the following code:
486- * ```csharp
487- * if (x)
488- * while (controlled)
489- * also_controlled;
490- * false_successor;
491- * uncontrolled;
492- * ```
493- * the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
494- * or (in the case of `also_controlled`) dominated by itself.
495- *
496- * The additional constraint on the predecessors of the test successor implies
497- * that `this` strictly dominates `controlled` so that isn't necessary to check
498- * directly.
499- */
500-
501- exists ( BasicBlock succ | this .immediatelyControls ( succ , s ) | succ .dominates ( controlled ) )
295+ super .controls ( controlled , s )
502296 }
503297}
0 commit comments