@@ -1206,12 +1206,12 @@ module Make<
1206
1206
* Holds if this node is an exit node, i.e. after all stores have been performed.
1207
1207
*
1208
1208
* A local flow step should be added from this node to a data flow node representing
1209
- * `sc ` inside `source`.
1209
+ * `s ` inside `source`.
1210
1210
*/
1211
- predicate isExit ( SourceElement source , SummaryComponent sc , string model ) {
1211
+ predicate isExit ( SourceElement source , SummaryComponentStack s , string model ) {
1212
1212
source = source_ and
1213
1213
model = model_ and
1214
- state_ .isSourceOutputState ( source , TSingletonSummaryComponentStack ( sc ) , _, model )
1214
+ state_ .isSourceOutputState ( source , s , _, model )
1215
1215
}
1216
1216
1217
1217
override predicate isHidden ( ) { not this .isEntry ( _, _) }
@@ -1460,7 +1460,7 @@ module Make<
1460
1460
1461
1461
DataFlowType getSyntheticGlobalType ( SyntheticGlobal sg ) ;
1462
1462
1463
- DataFlowType getSourceType ( SourceBase source , SummaryComponent sc ) ;
1463
+ DataFlowType getSourceType ( SourceBase source , SummaryComponentStack sc ) ;
1464
1464
1465
1465
DataFlowType getSinkType ( SinkBase sink , SummaryComponent sc ) ;
1466
1466
}
@@ -1543,9 +1543,9 @@ module Make<
1543
1543
)
1544
1544
or
1545
1545
exists ( SourceElement source |
1546
- exists ( SummaryComponent sc |
1547
- n .( SourceOutputNode ) .isExit ( source , sc , _) and
1548
- result = getSourceType ( source , sc )
1546
+ exists ( SummaryComponentStack s |
1547
+ n .( SourceOutputNode ) .isExit ( source , s , _) and
1548
+ result = getSourceType ( source , s )
1549
1549
)
1550
1550
or
1551
1551
exists ( SummaryComponentStack s , ContentSet cont |
@@ -1574,13 +1574,16 @@ module Make<
1574
1574
/** Gets a call that targets summarized callable `sc`. */
1575
1575
DataFlowCall getACall ( SummarizedCallable sc ) ;
1576
1576
1577
+ /** Gets the enclosing callable of `source`. */
1578
+ DataFlowCallable getSourceNodeEnclosingCallable ( SourceBase source ) ;
1579
+
1577
1580
/**
1578
- * Gets a data flow node corresponding to the `sc ` part of `source`.
1581
+ * Gets a data flow node corresponding to the `s ` part of `source`.
1579
1582
*
1580
- * `sc ` is typically `ReturnValue` and the result is the node that
1583
+ * `s ` is typically `ReturnValue` and the result is the node that
1581
1584
* represents the return value of `source`.
1582
1585
*/
1583
- Node getSourceNode ( SourceBase source , SummaryComponent sc ) ;
1586
+ Node getSourceNode ( SourceBase source , SummaryComponentStack s ) ;
1584
1587
1585
1588
/**
1586
1589
* Gets a data flow node corresponding to the `sc` part of `sink`.
@@ -1622,13 +1625,20 @@ module Make<
1622
1625
)
1623
1626
}
1624
1627
1625
- predicate sourceLocalStep ( SourceOutputNode nodeFrom , Node nodeTo , string model ) {
1626
- exists ( SummaryComponent sc , SourceElement source |
1628
+ predicate sourceStep ( SourceOutputNode nodeFrom , Node nodeTo , string model , boolean local ) {
1629
+ exists ( SummaryComponentStack sc , SourceElement source |
1627
1630
nodeFrom .isExit ( source , sc , model ) and
1628
- nodeTo = StepsInput:: getSourceNode ( source , sc )
1631
+ nodeTo = StepsInput:: getSourceNode ( source , sc ) and
1632
+ if StepsInput:: getSourceNodeEnclosingCallable ( source ) = getNodeEnclosingCallable ( nodeTo )
1633
+ then local = true
1634
+ else local = false
1629
1635
)
1630
1636
}
1631
1637
1638
+ predicate sourceLocalStep ( SourceOutputNode nodeFrom , Node nodeTo , string model ) {
1639
+ sourceStep ( nodeFrom , nodeTo , model , true )
1640
+ }
1641
+
1632
1642
predicate sinkLocalStep ( Node nodeFrom , SinkInputNode nodeTo , string model ) {
1633
1643
exists ( SummaryComponent sc , SinkElement sink |
1634
1644
nodeFrom = StepsInput:: getSinkNode ( sink , sc ) and
@@ -1689,6 +1699,10 @@ module Make<
1689
1699
)
1690
1700
}
1691
1701
1702
+ predicate sourceJumpStep ( SourceOutputNode nodeFrom , Node nodeTo ) {
1703
+ sourceStep ( nodeFrom , nodeTo , _, false )
1704
+ }
1705
+
1692
1706
/**
1693
1707
* Holds if values stored inside content `c` are cleared at `n`. `n` is a
1694
1708
* synthesized summary node, so in order for values to be cleared at calls
0 commit comments