@@ -1508,53 +1508,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15081508 module DataFlowIntegration< DataFlowIntegrationInputSig DfInput> {
15091509 private import codeql.util.Boolean
15101510
1511- pragma [ nomagic]
1512- private predicate adjacentDefReachesReadExt (
1513- DefinitionExt def , SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
1514- ) {
1515- adjacentDefReadExt ( def , v , bb1 , i1 , bb2 , i2 ) and
1516- (
1517- def .definesAt ( v , bb1 , i1 , _)
1518- or
1519- variableRead ( bb1 , i1 , v , true )
1520- )
1521- or
1522- exists ( BasicBlock bb3 , int i3 |
1523- adjacentDefReachesReadExt ( def , v , bb1 , i1 , bb3 , i3 ) and
1524- variableRead ( bb3 , i3 , v , false ) and
1525- adjacentDefReadExt ( def , v , bb3 , i3 , bb2 , i2 )
1526- )
1527- }
1528-
1529- pragma [ nomagic]
1530- private predicate adjacentDefReachesUncertainReadExt (
1531- DefinitionExt def , SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
1532- ) {
1533- adjacentDefReachesReadExt ( def , v , bb1 , i1 , bb2 , i2 ) and
1534- variableRead ( bb2 , i2 , v , false )
1535- }
1536-
1537- /**
1538- * Holds if the reference to `def` at index `i` in basic block `bb` can reach
1539- * another definition `next` of the same underlying source variable, without
1540- * passing through another write or non-pseudo read.
1541- *
1542- * The reference is either a read of `def` or `def` itself.
1543- */
1544- pragma [ nomagic]
1545- private predicate lastRefBeforeRedefExt (
1546- DefinitionExt def , SourceVariable v , BasicBlock bb , int i , BasicBlock input ,
1547- DefinitionExt next
1548- ) {
1549- lastRefRedefExt ( def , v , bb , i , input , next ) and
1550- not variableRead ( bb , i , v , false )
1551- or
1552- exists ( BasicBlock bb0 , int i0 |
1553- lastRefRedefExt ( def , v , bb0 , i0 , input , next ) and
1554- adjacentDefReachesUncertainReadExt ( def , v , bb , i , bb0 , i0 )
1555- )
1556- }
1557-
15581511 final private class DefinitionExtFinal = DefinitionExt ;
15591512
15601513 /** An SSA definition into which another SSA definition may flow. */
@@ -1564,13 +1517,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15641517 or
15651518 this instanceof PhiReadNode
15661519 }
1567-
1568- /** Holds if `def` may flow into this definition via basic block `input`. */
1569- predicate hasInputFromBlock (
1570- DefinitionExt def , SourceVariable v , BasicBlock bb , int i , BasicBlock input
1571- ) {
1572- lastRefBeforeRedefExt ( def , v , bb , i , input , this )
1573- }
15741520 }
15751521
15761522 cached
0 commit comments