@@ -307,6 +307,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
307307 private predicate inReadDominanceFrontier ( BasicBlock bb , SourceVariable v ) {
308308 exists ( BasicBlock readbb | inDominanceFrontier ( readbb , bb ) |
309309 ssaDefReachesRead ( v , _, readbb , _) and
310+ variableRead ( readbb , _, v , true ) and
310311 not variableWrite ( readbb , _, v , _)
311312 or
312313 synthPhiRead ( readbb , v ) and
@@ -1379,6 +1380,56 @@ module Make<LocationSig Location, InputSig<Location> Input> {
13791380 not def .definesAt ( v , getImmediateBasicBlockDominator * ( bb ) , _)
13801381 )
13811382 }
1383+
1384+ /** Holds if the end of a basic block can be reached by multiple definitions. */
1385+ query predicate nonUniqueDefReachesEndOfBlock ( Definition def , SourceVariable v , BasicBlock bb ) {
1386+ ssaDefReachesEndOfBlock ( bb , def , v ) and
1387+ not exists ( unique( Definition def0 | ssaDefReachesEndOfBlock ( bb , def0 , v ) ) )
1388+ }
1389+
1390+ /** Holds if a phi node has less than two inputs. */
1391+ query predicate uselessPhiNode ( PhiNode phi , int inputs ) {
1392+ inputs = count ( Definition inp | phiHasInputFromBlock ( phi , inp , _) ) and
1393+ inputs < 2
1394+ }
1395+
1396+ /** Holds if a certain read does not have a prior reference. */
1397+ query predicate readWithoutPriorRef ( SourceVariable v , BasicBlock bb , int i ) {
1398+ variableRead ( bb , i , v , true ) and
1399+ not AdjacentSsaRefs:: adjacentRefRead ( _, _, bb , i , v )
1400+ }
1401+
1402+ /**
1403+ * Holds if a certain read has multiple prior references. The introduction
1404+ * of phi reads should make the prior reference unique.
1405+ */
1406+ query predicate readWithMultiplePriorRefs (
1407+ SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
1408+ ) {
1409+ AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
1410+ 2 <=
1411+ strictcount ( BasicBlock bb0 , int i0 | AdjacentSsaRefs:: adjacentRefRead ( bb0 , i0 , bb1 , i1 , v ) )
1412+ }
1413+
1414+ /** Holds if `phi` has less than 2 immediately prior references. */
1415+ query predicate phiWithoutTwoPriorRefs ( PhiNode phi , int inputRefs ) {
1416+ exists ( BasicBlock bbPhi , SourceVariable v |
1417+ phi .definesAt ( v , bbPhi , _) and
1418+ inputRefs =
1419+ count ( BasicBlock bb , int i | AdjacentSsaRefs:: adjacentRefPhi ( bb , i , _, bbPhi , v ) ) and
1420+ inputRefs < 2
1421+ )
1422+ }
1423+
1424+ /**
1425+ * Holds if the phi read for `v` at `bb` has less than 2 immediately prior
1426+ * references.
1427+ */
1428+ query predicate phiReadWithoutTwoPriorRefs ( BasicBlock bbPhi , SourceVariable v , int inputRefs ) {
1429+ synthPhiRead ( bbPhi , v ) and
1430+ inputRefs = count ( BasicBlock bb , int i | AdjacentSsaRefs:: adjacentRefPhi ( bb , i , _, bbPhi , v ) ) and
1431+ inputRefs < 2
1432+ }
13821433 }
13831434
13841435 /** Provides the input to `DataFlowIntegration`. */
0 commit comments