@@ -1350,66 +1350,28 @@ module Make<LocationSig Location, InputSig<Location> Input> {
13501350
13511351 /** Provides a set of consistency queries. */
13521352 module Consistency {
1353- /** A definition that is relevant for the consistency queries. */
1354- abstract class RelevantDefinition extends Definition {
1355- /** Override this predicate to ensure locations in consistency results. */
1356- abstract predicate hasLocationInfo (
1357- string filepath , int startline , int startcolumn , int endline , int endcolumn
1358- ) ;
1359- }
1360-
1361- /** A definition that is relevant for the consistency queries. */
1362- abstract class RelevantDefinitionExt extends DefinitionExt {
1363- /** Override this predicate to ensure locations in consistency results. */
1364- abstract predicate hasLocationInfo (
1365- string filepath , int startline , int startcolumn , int endline , int endcolumn
1366- ) ;
1367- }
1368-
13691353 /** Holds if a read can be reached from multiple definitions. */
1370- query predicate nonUniqueDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
1354+ query predicate nonUniqueDef ( Definition def , SourceVariable v , BasicBlock bb , int i ) {
13711355 ssaDefReachesRead ( v , def , bb , i ) and
13721356 not exists ( unique( Definition def0 | ssaDefReachesRead ( v , def0 , bb , i ) ) )
13731357 }
13741358
1375- /** Holds if a read can be reached from multiple definitions. */
1376- query predicate nonUniqueDefExt (
1377- RelevantDefinitionExt def , SourceVariable v , BasicBlock bb , int i
1378- ) {
1379- ssaDefReachesReadExt ( v , def , bb , i ) and
1380- not exists ( unique( DefinitionExt def0 | ssaDefReachesReadExt ( v , def0 , bb , i ) ) )
1381- }
1382-
13831359 /** Holds if a read cannot be reached from a definition. */
13841360 query predicate readWithoutDef ( SourceVariable v , BasicBlock bb , int i ) {
13851361 variableRead ( bb , i , v , _) and
13861362 not ssaDefReachesRead ( v , _, bb , i )
13871363 }
13881364
1389- /** Holds if a read cannot be reached from a definition. */
1390- query predicate readWithoutDefExt ( SourceVariable v , BasicBlock bb , int i ) {
1391- variableRead ( bb , i , v , _) and
1392- not ssaDefReachesReadExt ( v , _, bb , i )
1393- }
1394-
13951365 /** Holds if a definition cannot reach a read. */
1396- query predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
1366+ query predicate deadDef ( Definition def , SourceVariable v ) {
13971367 v = def .getSourceVariable ( ) and
13981368 not ssaDefReachesRead ( _, def , _, _) and
13991369 not phiHasInputFromBlock ( _, def , _) and
14001370 not uncertainWriteDefinitionInput ( _, def )
14011371 }
14021372
1403- /** Holds if a definition cannot reach a read. */
1404- query predicate deadDefExt ( RelevantDefinitionExt def , SourceVariable v ) {
1405- v = def .getSourceVariable ( ) and
1406- not ssaDefReachesReadExt ( _, def , _, _) and
1407- not phiHasInputFromBlockExt ( _, def , _) and
1408- not uncertainWriteDefinitionInput ( _, def )
1409- }
1410-
14111373 /** Holds if a read is not dominated by a definition. */
1412- query predicate notDominatedByDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
1374+ query predicate notDominatedByDef ( Definition def , SourceVariable v , BasicBlock bb , int i ) {
14131375 exists ( BasicBlock bbDef , int iDef | def .definesAt ( v , bbDef , iDef ) |
14141376 ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
14151377 ( bb != bbDef or i < iDef )
@@ -1419,20 +1381,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
14191381 not def .definesAt ( v , getImmediateBasicBlockDominator * ( bb ) , _)
14201382 )
14211383 }
1422-
1423- /** Holds if a read is not dominated by a definition. */
1424- query predicate notDominatedByDefExt (
1425- RelevantDefinitionExt def , SourceVariable v , BasicBlock bb , int i
1426- ) {
1427- exists ( BasicBlock bbDef , int iDef | def .definesAt ( v , bbDef , iDef , _) |
1428- ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
1429- ( bb != bbDef or i < iDef )
1430- or
1431- ssaDefReachesReadExt ( v , def , bb , i ) and
1432- not ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
1433- not def .definesAt ( v , getImmediateBasicBlockDominator * ( bb ) , _, _)
1434- )
1435- }
14361384 }
14371385
14381386 /** Provides the input to `DataFlowIntegration`. */
0 commit comments