11/**
2- * This modules provides an implementation of a basic block class based based
3- * on a control flow graph implementation.
2+ * This modules provides an implementation of a basic block class based on a
3+ * control flow graph implementation.
44 *
55 * INTERNAL use only. This is an experimental API subject to change without
66 * notice.
77 */
88
9+ private import codeql.util.Location
10+
911/** Provides the language-specific input specification. */
10- signature module InputSig {
12+ signature module InputSig< LocationSig Location > {
1113 class SuccessorType ;
1214
1315 /** Hold if `t` represents a conditional successor type. */
@@ -16,21 +18,31 @@ signature module InputSig {
1618 /** The class of control flow nodes. */
1719 class Node {
1820 string toString ( ) ;
21+
22+ /** Gets the location of this control flow node. */
23+ Location getLocation ( ) ;
1924 }
2025
26+ /** Gets an immediate successor of this node. */
2127 Node nodeGetASuccessor ( Node node , SuccessorType t ) ;
2228
23- /** Holds if `node` is the beginning of an entry basic block. */
24- predicate nodeIsEntry ( Node node ) ;
29+ /**
30+ * Holds if `node` represents an entry node to be used when calculating
31+ * dominance.
32+ */
33+ predicate nodeIsDominanceEntry ( Node node ) ;
2534
26- /** Holds if `node` is the beginning of an entry basic block. */
27- predicate nodeIsExit ( Node node ) ;
35+ /**
36+ * Holds if `node` represents an exit node to be used when calculating
37+ * post dominance.
38+ */
39+ predicate nodeIsPostDominanceExit ( Node node ) ;
2840}
2941
3042/**
3143 * Provides a basic block construction on top of a control flow graph.
3244 */
33- module Make< InputSig Input> {
45+ module Make< LocationSig Location , InputSig< Location > Input> {
3446 private import Input
3547
3648 final class BasicBlock = BasicBlockImpl ;
@@ -42,13 +54,17 @@ module Make<InputSig Input> {
4254 /** Holds if this node has more than one predecessor. */
4355 private predicate nodeIsJoin ( Node node ) { strictcount ( nodeGetAPredecessor ( node , _) ) > 1 }
4456
57+ /** Holds if this node has more than one successor. */
4558 private predicate nodeIsBranch ( Node node ) { strictcount ( nodeGetASuccessor ( node , _) ) > 1 }
4659
4760 /**
4861 * A basic block, that is, a maximal straight-line sequence of control flow nodes
4962 * without branches or joins.
5063 */
5164 private class BasicBlockImpl extends TBasicBlockStart {
65+ /** Gets the location of this basic block. */
66+ Location getLocation ( ) { result = this .getFirstNode ( ) .getLocation ( ) }
67+
5268 /** Gets an immediate successor of this basic block, if any. */
5369 BasicBlock getASuccessor ( ) { result = this .getASuccessor ( _) }
5470
@@ -64,6 +80,7 @@ module Make<InputSig Input> {
6480 BasicBlock getAPredecessor ( SuccessorType t ) { result .getASuccessor ( t ) = this }
6581
6682 /** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
83+ cached
6784 Node getNode ( int pos ) { bbIndex ( this .getFirstNode ( ) , result , pos ) }
6885
6986 /** Gets a control flow node in this basic block. */
@@ -166,52 +183,6 @@ module Make<InputSig Input> {
166183 cached
167184 newtype TBasicBlock = TBasicBlockStart ( Node cfn ) { startsBB ( cfn ) }
168185
169- /** Holds if `cfn` starts a new basic block. */
170- private predicate startsBB ( Node cfn ) {
171- not exists ( nodeGetAPredecessor ( cfn , _) ) and exists ( nodeGetASuccessor ( cfn , _) )
172- or
173- nodeIsJoin ( cfn )
174- or
175- nodeIsBranch ( nodeGetAPredecessor ( cfn , _) )
176- or
177- // In cases such as
178- //
179- // ```rb
180- // if x or y
181- // foo
182- // else
183- // bar
184- // ```
185- //
186- // we have a CFG that looks like
187- //
188- // x --false--> [false] x or y --false--> bar
189- // \ |
190- // --true--> y --false--
191- // \
192- // --true--> [true] x or y --true--> foo
193- //
194- // and we want to ensure that both `foo` and `bar` start a new basic block.
195- exists ( nodeGetAPredecessor ( cfn , any ( SuccessorType s | successorTypeIsCondition ( s ) ) ) )
196- }
197-
198- /**
199- * Holds if `succ` is a control flow successor of `pred` within
200- * the same basic block.
201- */
202- private predicate intraBBSucc ( Node pred , Node succ ) {
203- succ = nodeGetASuccessor ( pred , _) and
204- not startsBB ( succ )
205- }
206-
207- /**
208- * Holds if `bbStart` is the first node in a basic block and `cfn` is the
209- * `i`th node in the same basic block.
210- */
211- cached
212- predicate bbIndex ( Node bbStart , Node cfn , int i ) =
213- shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
214-
215186 /**
216187 * Holds if the first node of basic block `succ` is a control flow
217188 * successor of the last node of basic block `pred`.
@@ -227,7 +198,7 @@ module Make<InputSig Input> {
227198 private predicate predBB ( BasicBlock succ , BasicBlock pred ) { succBB ( pred , succ ) }
228199
229200 /** Holds if `bb` is an exit basic block that represents normal exit. */
230- private predicate exitBB ( BasicBlock bb ) { nodeIsExit ( bb .getANode ( ) ) }
201+ private predicate exitBB ( BasicBlock bb ) { nodeIsPostDominanceExit ( bb .getANode ( ) ) }
231202
232203 /** Holds if `dom` is an immediate post-dominator of `bb`. */
233204 cached
@@ -237,6 +208,51 @@ module Make<InputSig Input> {
237208
238209 private import Cached
239210
211+ /** Holds if `cfn` starts a new basic block. */
212+ private predicate startsBB ( Node cfn ) {
213+ not exists ( nodeGetAPredecessor ( cfn , _) ) and exists ( nodeGetASuccessor ( cfn , _) )
214+ or
215+ nodeIsJoin ( cfn )
216+ or
217+ nodeIsBranch ( nodeGetAPredecessor ( cfn , _) )
218+ or
219+ // In cases such as
220+ //
221+ // ```rb
222+ // if x or y
223+ // foo
224+ // else
225+ // bar
226+ // ```
227+ //
228+ // we have a CFG that looks like
229+ //
230+ // x --false--> [false] x or y --false--> bar
231+ // \ |
232+ // --true--> y --false--
233+ // \
234+ // --true--> [true] x or y --true--> foo
235+ //
236+ // and we want to ensure that both `foo` and `bar` start a new basic block.
237+ exists ( nodeGetAPredecessor ( cfn , any ( SuccessorType s | successorTypeIsCondition ( s ) ) ) )
238+ }
239+
240+ /**
241+ * Holds if `succ` is a control flow successor of `pred` within
242+ * the same basic block.
243+ */
244+ predicate intraBBSucc ( Node pred , Node succ ) {
245+ succ = nodeGetASuccessor ( pred , _) and
246+ not startsBB ( succ )
247+ }
248+
249+ /**
250+ * Holds if `bbStart` is the first node in a basic block and `cfn` is the
251+ * `i`th node in the same basic block.
252+ */
253+ private predicate bbIndex ( Node bbStart , Node cfn , int i ) =
254+ shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
255+
240256 /** Holds if `bb` is an entry basic block. */
241- private predicate entryBB ( BasicBlock bb ) { nodeIsEntry ( bb .getFirstNode ( ) ) }
257+ private predicate entryBB ( BasicBlock bb ) { nodeIsDominanceEntry ( bb .getFirstNode ( ) ) }
242258}
0 commit comments