@@ -470,10 +470,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
470470 private module Stage1 {
471471 private import Stage1Common
472472
473- class Ap = Unit ;
474-
475- class ApNil = Ap ;
476-
477473 private class Cc = boolean ;
478474
479475 /* Begin: Stage 1 logic. */
@@ -954,14 +950,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
954950 c = ret .getEnclosingCallable ( )
955951 }
956952
957- predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
958- callEdgeArgParam ( call , c , _, _, _)
959- }
960-
961- predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
962- callEdgeReturn ( call , c , _, _, _, _)
963- }
964-
965953 predicate stats (
966954 boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges
967955 ) {
@@ -991,6 +979,10 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
991979 private module Stage1Common {
992980 predicate isRelevantSourceSinkPair = SourceSinkFiltering:: isRelevantSourceSinkPair / 2 ;
993981
982+ class Ap = Unit ;
983+
984+ class ApNil = Ap ;
985+
994986 predicate hasSourceCallCtx ( ) {
995987 exists ( FlowFeature feature | feature = Config:: getAFeature ( ) |
996988 feature instanceof FeatureHasSourceCallContext or
@@ -1004,6 +996,20 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1004996 feature instanceof FeatureEqualSourceSinkCallContext
1005997 )
1006998 }
999+
1000+ predicate revFlowIsReadAndStored = Stage1:: revFlowIsReadAndStored / 1 ;
1001+
1002+ predicate callMayFlowThroughRev = Stage1:: callMayFlowThroughRev / 1 ;
1003+
1004+ predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
1005+ Stage1:: callEdgeArgParam ( call , c , _, _, _)
1006+ }
1007+
1008+ predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
1009+ Stage1:: callEdgeReturn ( call , c , _, _, _, _)
1010+ }
1011+
1012+ predicate stats = Stage1:: stats / 7 ;
10071013 }
10081014
10091015 pragma [ nomagic]
@@ -1294,6 +1300,235 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
12941300 predicate localStateStepNodeCand1 = localStateStepNodeCand1Alias / 7 ;
12951301 }
12961302
1303+ // TODO: implements Stage1Output<FlowState>
1304+ module Stage1WithState {
1305+ private predicate flowState ( NodeEx node , FlowState state ) {
1306+ Stage1:: revFlow ( node ) and
1307+ Stage1:: revFlowState ( state ) and
1308+ not stateBarrier ( node , state ) and
1309+ (
1310+ sourceNode ( node , state )
1311+ or
1312+ exists ( NodeEx mid , FlowState state0 | flowState ( mid , state0 ) |
1313+ additionalLocalStateStep ( mid , state0 , node , state , _) or
1314+ additionalJumpStateStep ( mid , state0 , node , state , _)
1315+ )
1316+ or
1317+ exists ( NodeEx mid | flowState ( mid , state ) |
1318+ localFlowStepEx ( mid , node , _) or
1319+ additionalLocalFlowStep ( mid , node , _) or
1320+ jumpStepExAlias ( mid , node ) or
1321+ additionalJumpStepAlias ( mid , node , _) or
1322+ store ( mid , _, node , _, _) or
1323+ readSetEx ( mid , _, node ) or
1324+ flowIntoCallNodeCand1 ( _, mid , node ) or
1325+ flowOutOfCallNodeCand1 ( _, mid , _, node )
1326+ )
1327+ )
1328+ }
1329+
1330+ private newtype TNd = TNodeState ( NodeEx node , FlowState state ) { flowState ( node , state ) }
1331+
1332+ class Nd extends TNd {
1333+ NodeEx node ;
1334+
1335+ Nd ( ) { this = TNodeState ( node , _) }
1336+
1337+ NodeEx getNodeEx ( ) { result = node }
1338+
1339+ FlowState getState ( ) { this = TNodeState ( _, result ) }
1340+
1341+ string toString ( ) { result = node .toString ( ) }
1342+
1343+ Location getLocation ( ) { result = node .getLocation ( ) }
1344+
1345+ DataFlowType getDataFlowType ( ) { result = node .getDataFlowType ( ) }
1346+
1347+ DataFlowCallable getEnclosingCallable ( ) { result = node .getEnclosingCallable ( ) }
1348+ }
1349+
1350+ class ArgNd extends Nd {
1351+ ArgNd ( ) { node instanceof ArgNodeEx }
1352+ }
1353+
1354+ class ParamNd extends Nd {
1355+ ParamNd ( ) { node instanceof ParamNodeEx }
1356+ }
1357+
1358+ class RetNd extends Nd {
1359+ override RetNodeEx node ;
1360+
1361+ ReturnPosition getReturnPosition ( ) { result = node .getReturnPosition ( ) }
1362+
1363+ ReturnKindExt getKind ( ) { result = node .getKind ( ) }
1364+ }
1365+
1366+ class OutNd extends Nd {
1367+ OutNd ( ) { node instanceof OutNodeEx }
1368+ }
1369+
1370+ class CastingNd extends Nd {
1371+ CastingNd ( ) { node instanceof CastingNodeEx }
1372+ }
1373+
1374+ // inline to reduce fan-out via `getAReadContent`
1375+ bindingset [ c]
1376+ predicate expectsContentEx ( Nd n , Content c ) {
1377+ Stage1NoState:: expectsContentEx ( n .getNodeEx ( ) , c )
1378+ }
1379+
1380+ pragma [ nomagic]
1381+ predicate notExpectsContent ( Nd n ) { Stage1NoState:: notExpectsContent ( n .getNodeEx ( ) ) }
1382+
1383+ bindingset [ p, kind]
1384+ pragma [ inline_late]
1385+ predicate parameterFlowThroughAllowed ( ParamNd p , ReturnKindExt kind ) {
1386+ parameterFlowThroughAllowedEx ( p .getNodeEx ( ) , kind )
1387+ }
1388+
1389+ import Stage1Common
1390+
1391+ predicate revFlow ( Nd node ) { Stage1:: revFlow ( node .getNodeEx ( ) ) }
1392+
1393+ predicate revFlow ( Nd node , Ap ap ) { Stage1:: revFlow ( node .getNodeEx ( ) ) and exists ( ap ) }
1394+
1395+ predicate parameterMayFlowThrough ( ParamNd p , boolean emptyAp ) {
1396+ Stage1:: parameterMayFlowThrough ( p .getNodeEx ( ) , emptyAp )
1397+ }
1398+
1399+ predicate returnMayFlowThrough ( RetNd ret , ReturnKindExt kind ) {
1400+ Stage1:: returnMayFlowThrough ( ret .getNodeEx ( ) , kind )
1401+ }
1402+
1403+ pragma [ nomagic]
1404+ predicate storeStepCand (
1405+ Nd node1 , Content c , Nd node2 , DataFlowType contentType , DataFlowType containerType
1406+ ) {
1407+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1408+ Stage1:: storeStepCand ( n1 , c , n2 , contentType , containerType ) and
1409+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1410+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1411+ not outBarrier ( n1 , s ) and
1412+ not inBarrier ( n2 , s )
1413+ )
1414+ }
1415+
1416+ pragma [ nomagic]
1417+ predicate readStepCand ( Nd node1 , Content c , Nd node2 ) {
1418+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1419+ Stage1:: readStepCand ( n1 , c , n2 ) and
1420+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1421+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1422+ not outBarrier ( n1 , s ) and
1423+ not inBarrier ( n2 , s )
1424+ )
1425+ }
1426+
1427+ predicate callEdgeArgParam (
1428+ DataFlowCall call , DataFlowCallable c , ArgNd arg , ParamNd p , boolean emptyAp
1429+ ) {
1430+ exists ( ArgNodeEx arg0 , ParamNodeEx p0 , FlowState s |
1431+ Stage1:: callEdgeArgParam ( call , c , arg0 , p0 , emptyAp ) and
1432+ arg = TNodeState ( arg0 , pragma [ only_bind_into ] ( s ) ) and
1433+ p = TNodeState ( p0 , pragma [ only_bind_into ] ( s ) ) and
1434+ not outBarrier ( arg0 , s ) and
1435+ not inBarrier ( p0 , s )
1436+ )
1437+ }
1438+
1439+ predicate callEdgeReturn (
1440+ DataFlowCall call , DataFlowCallable c , RetNd ret , ReturnKindExt kind , Nd out ,
1441+ boolean allowsFieldFlow
1442+ ) {
1443+ exists ( RetNodeEx ret0 , NodeEx out0 , FlowState s |
1444+ Stage1:: callEdgeReturn ( call , c , ret0 , kind , out0 , allowsFieldFlow ) and
1445+ ret = TNodeState ( ret0 , pragma [ only_bind_into ] ( s ) ) and
1446+ out = TNodeState ( out0 , pragma [ only_bind_into ] ( s ) ) and
1447+ not outBarrier ( ret0 , s ) and
1448+ not inBarrier ( out0 , s )
1449+ )
1450+ }
1451+
1452+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
1453+ Nd toNormalSinkNode ( Nd node ) {
1454+ exists ( NodeEx res , NodeEx n , FlowState s |
1455+ res = toNormalSinkNodeEx ( n ) and
1456+ node = TNodeState ( n , pragma [ only_bind_into ] ( s ) ) and
1457+ result = TNodeState ( res , pragma [ only_bind_into ] ( s ) )
1458+ )
1459+ }
1460+
1461+ predicate sourceNode ( Nd node ) {
1462+ exists ( NodeEx n , FlowState state |
1463+ sourceNode ( n , state ) and
1464+ node = TNodeState ( n , state )
1465+ )
1466+ }
1467+
1468+ predicate sinkNode ( Nd node ) {
1469+ exists ( NodeEx n , FlowState state |
1470+ Stage1:: sinkNode ( n , state ) and
1471+ node = TNodeState ( n , state )
1472+ )
1473+ }
1474+
1475+ predicate jumpStepEx ( Nd node1 , Nd node2 ) {
1476+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1477+ jumpStepExAlias ( n1 , n2 ) and
1478+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1479+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1480+ not outBarrier ( n1 , s ) and
1481+ not inBarrier ( n2 , s )
1482+ )
1483+ }
1484+
1485+ predicate additionalJumpStep ( Nd node1 , Nd node2 , string model ) {
1486+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1487+ additionalJumpStepAlias ( n1 , n2 , model ) and
1488+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1489+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1490+ not outBarrier ( n1 , s ) and
1491+ not inBarrier ( n2 , s )
1492+ )
1493+ or
1494+ exists ( NodeEx n1 , FlowState s1 , NodeEx n2 , FlowState s2 |
1495+ additionalJumpStateStep ( n1 , s1 , n2 , s2 , model ) and
1496+ node1 = TNodeState ( n1 , s1 ) and
1497+ node2 = TNodeState ( n2 , s2 )
1498+ )
1499+ }
1500+
1501+ pragma [ nomagic]
1502+ predicate localStep1 (
1503+ Nd node1 , Nd node2 , boolean preservesValue , DataFlowType t , LocalCallContext lcc ,
1504+ string label
1505+ ) {
1506+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1507+ localStepNodeCand1 ( n1 , n2 , preservesValue , t , lcc , label ) and
1508+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1509+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1510+ not outBarrier ( n1 , s ) and
1511+ not inBarrier ( n2 , s )
1512+ )
1513+ or
1514+ exists ( NodeEx n1 , NodeEx n2 , FlowState s1 , FlowState s2 |
1515+ localStateStepNodeCand1 ( n1 , s1 , n2 , s2 , t , lcc , label ) and
1516+ preservesValue = false and
1517+ node1 = TNodeState ( n1 , s1 ) and
1518+ node2 = TNodeState ( n2 , s2 )
1519+ )
1520+ }
1521+
1522+ predicate isStateStep ( Nd node1 , Nd node2 ) {
1523+ exists ( NodeEx n1 , NodeEx n2 , FlowState s1 , FlowState s2 |
1524+ localStateStepNodeCand1 ( n1 , s1 , n2 , s2 , _, _, _) and
1525+ s1 != s2 and
1526+ node1 = TNodeState ( n1 , s1 ) and
1527+ node2 = TNodeState ( n2 , s2 )
1528+ )
1529+ }
1530+ }
1531+
12971532 private signature predicate flag ( ) ;
12981533
12991534 private predicate flagEnable ( ) { any ( ) }
0 commit comments