@@ -1178,6 +1178,19 @@ module Make<LocationSig Location, InputSig<Location> Input> {
11781178 predicate hasCfgNode ( BasicBlock bb , int i ) ;
11791179 }
11801180
1181+ /**
1182+ * Gets a read of SSA defintion `def`.
1183+ *
1184+ * Override this with a cached version when applicable.
1185+ */
1186+ default Expr getARead ( Definition def ) {
1187+ exists ( SourceVariable v , BasicBlock bb , int i |
1188+ ssaDefReachesRead ( v , def , bb , i ) and
1189+ variableRead ( bb , i , v , true ) and
1190+ result .hasCfgNode ( bb , i )
1191+ )
1192+ }
1193+
11811194 /** Holds if SSA definition `def` assigns `value` to the underlying variable. */
11821195 predicate ssaDefAssigns ( WriteDefinition def , Expr value ) ;
11831196
@@ -1224,15 +1237,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
12241237 module DataFlowIntegration< DataFlowIntegrationInputSig DfInput> {
12251238 private import codeql.util.Boolean
12261239
1227- pragma [ nomagic]
1228- private DfInput:: Expr getARead ( Definition def ) {
1229- exists ( SourceVariable v , BasicBlock bb , int i |
1230- ssaDefReachesRead ( v , def , bb , i ) and
1231- variableRead ( bb , i , v , true ) and
1232- result .hasCfgNode ( bb , i )
1233- )
1234- }
1235-
12361240 pragma [ nomagic]
12371241 private predicate adjacentDefReachesReadExt (
12381242 DefinitionExt def , SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
@@ -1322,7 +1326,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
13221326 private newtype TNode =
13231327 TParamNode ( DfInput:: Parameter p ) { DfInput:: ssaDefInitializesParam ( _, p ) } or
13241328 TExprNode ( DfInput:: Expr e , Boolean isPost ) {
1325- e = getARead ( _)
1329+ e = DfInput :: getARead ( _)
13261330 or
13271331 DfInput:: ssaDefAssigns ( _, e ) and
13281332 isPost = false
@@ -1545,7 +1549,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15451549 )
15461550 }
15471551
1548- /** Holds if there is a local flow step from `nodeFrom` to `nodeTo`. */
1552+ /**
1553+ * Holds if there is a local flow step from `nodeFrom` to `nodeTo`.
1554+ *
1555+ * `isUseStep` is `true` when `nodeFrom` is a (post-update) read node and
1556+ * `nodeTo` is a read node or phi (read) node.
1557+ */
15491558 predicate localFlowStep ( DefinitionExt def , Node nodeFrom , Node nodeTo , boolean isUseStep ) {
15501559 (
15511560 // Flow from assignment into SSA definition
@@ -1594,7 +1603,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15941603 or
15951604 // Flow from SSA definition to read
15961605 nodeFrom .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
1597- nodeTo .( ExprNode ) .getExpr ( ) = getARead ( def )
1606+ nodeTo .( ExprNode ) .getExpr ( ) = DfInput :: getARead ( def )
15981607 }
15991608
16001609 pragma [ nomagic]
@@ -1603,7 +1612,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
16031612 ) {
16041613 exists ( BasicBlock bb , DfInput:: Expr e |
16051614 e = n .getExpr ( ) and
1606- getARead ( def ) = e and
1615+ DfInput :: getARead ( def ) = e and
16071616 DfInput:: guardControlsBlock ( g , bb , branch ) and
16081617 e .hasCfgNode ( bb , _)
16091618 )
0 commit comments