@@ -87,12 +87,30 @@ abstract class Configuration extends string {
87
87
/** Holds if data flow into `node` is prohibited. */
88
88
predicate isBarrierIn ( Node node ) { none ( ) }
89
89
90
+ /**
91
+ * Holds if data flow into `node` is prohibited when the flow state is
92
+ * `state`
93
+ */
94
+ predicate isBarrierIn ( Node node , FlowState state ) { none ( ) }
95
+
90
96
/** Holds if data flow out of `node` is prohibited. */
91
97
predicate isBarrierOut ( Node node ) { none ( ) }
92
98
99
+ /**
100
+ * Holds if data flow out of `node` is prohibited when the flow state is
101
+ * `state`
102
+ */
103
+ predicate isBarrierOut ( Node node , FlowState state ) { none ( ) }
104
+
93
105
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
94
106
predicate isBarrierGuard ( BarrierGuard guard ) { none ( ) }
95
107
108
+ /**
109
+ * Holds if data flow through nodes guarded by `guard` is prohibited when
110
+ * the flow state is `state`
111
+ */
112
+ predicate isBarrierGuard ( BarrierGuard guard , FlowState state ) { none ( ) }
113
+
96
114
/**
97
115
* Holds if the additional flow step from `node1` to `node2` must be taken
98
116
* into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
305
323
ReturnKindExt getKind ( ) { result = this .asNode ( ) .( ReturnNodeExt ) .getKind ( ) }
306
324
}
307
325
308
- private predicate inBarrier ( NodeEx node , Configuration config ) {
326
+ private predicate fullInBarrier ( NodeEx node , Configuration config ) {
309
327
exists ( Node n |
310
328
node .asNode ( ) = n and
311
329
config .isBarrierIn ( n )
@@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
314
332
)
315
333
}
316
334
317
- private predicate outBarrier ( NodeEx node , Configuration config ) {
335
+ private predicate stateInBarrier ( NodeEx node , FlowState state , Configuration config ) {
336
+ exists ( Node n |
337
+ node .asNode ( ) = n and
338
+ config .isBarrierIn ( n , state )
339
+ |
340
+ config .isSource ( n , state )
341
+ )
342
+ }
343
+
344
+ private predicate fullOutBarrier ( NodeEx node , Configuration config ) {
318
345
exists ( Node n |
319
346
node .asNode ( ) = n and
320
347
config .isBarrierOut ( n )
@@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
323
350
)
324
351
}
325
352
353
+ private predicate stateOutBarrier ( NodeEx node , FlowState state , Configuration config ) {
354
+ exists ( Node n |
355
+ node .asNode ( ) = n and
356
+ config .isBarrierOut ( n , state )
357
+ |
358
+ config .isSink ( n , state )
359
+ )
360
+ }
361
+
326
362
pragma [ nomagic]
327
363
private predicate fullBarrier ( NodeEx node , Configuration config ) {
328
364
exists ( Node n | node .asNode ( ) = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
345
381
346
382
pragma [ nomagic]
347
383
private predicate stateBarrier ( NodeEx node , FlowState state , Configuration config ) {
348
- exists ( Node n |
349
- node .asNode ( ) = n and
384
+ exists ( Node n | node .asNode ( ) = n |
350
385
config .isBarrier ( n , state )
386
+ or
387
+ config .isBarrierIn ( n , state ) and
388
+ not config .isSource ( n , state )
389
+ or
390
+ config .isBarrierOut ( n , state ) and
391
+ not config .isSink ( n , state )
392
+ or
393
+ exists ( BarrierGuard g |
394
+ config .isBarrierGuard ( g , state ) and
395
+ n = g .getAGuardedNode ( )
396
+ )
351
397
)
352
398
}
353
399
@@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
376
422
/** Provides the relevant barriers for a step from `node1` to `node2`. */
377
423
pragma [ inline]
378
424
private predicate stepFilter ( NodeEx node1 , NodeEx node2 , Configuration config ) {
379
- not outBarrier ( node1 , config ) and
380
- not inBarrier ( node2 , config ) and
425
+ not fullOutBarrier ( node1 , config ) and
426
+ not fullInBarrier ( node2 , config ) and
381
427
not fullBarrier ( node1 , config ) and
382
428
not fullBarrier ( node2 , config )
383
429
}
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
430
476
config .isAdditionalFlowStep ( n1 , s1 , n2 , s2 ) and
431
477
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
432
478
stepFilter ( node1 , node2 , config ) and
479
+ not stateOutBarrier ( node1 , s1 , config ) and
480
+ not stateInBarrier ( node2 , s2 , config ) and
433
481
not stateBarrier ( node1 , s1 , config ) and
434
482
not stateBarrier ( node2 , s2 , config )
435
483
)
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
471
519
config .isAdditionalFlowStep ( n1 , s1 , n2 , s2 ) and
472
520
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
473
521
stepFilter ( node1 , node2 , config ) and
522
+ not stateOutBarrier ( node1 , s1 , config ) and
523
+ not stateInBarrier ( node2 , s2 , config ) and
474
524
not stateBarrier ( node1 , s1 , config ) and
475
525
not stateBarrier ( node2 , s2 , config ) and
476
526
not config .getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
870
920
private predicate throughFlowNodeCand ( NodeEx node , Configuration config ) {
871
921
revFlow ( node , true , config ) and
872
922
fwdFlow ( node , true , config ) and
873
- not inBarrier ( node , config ) and
874
- not outBarrier ( node , config )
923
+ not fullInBarrier ( node , config ) and
924
+ not fullOutBarrier ( node , config )
875
925
}
876
926
877
927
/** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
966
1016
) {
967
1017
viableReturnPosOutNodeCand1 ( call , ret .getReturnPosition ( ) , out , config ) and
968
1018
Stage1:: revFlow ( ret , config ) and
969
- not outBarrier ( ret , config ) and
970
- not inBarrier ( out , config )
1019
+ not fullOutBarrier ( ret , config ) and
1020
+ not fullInBarrier ( out , config )
971
1021
}
972
1022
973
1023
pragma [ nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
988
1038
) {
989
1039
viableParamArgNodeCand1 ( call , p , arg , config ) and
990
1040
Stage1:: revFlow ( p , config ) and
991
- not outBarrier ( arg , config ) and
992
- not inBarrier ( p , config )
1041
+ not fullOutBarrier ( arg , config ) and
1042
+ not fullInBarrier ( p , config )
993
1043
}
994
1044
995
1045
/**
@@ -1706,18 +1756,31 @@ private module LocalFlowBigStep {
1706
1756
* Holds if `node` can be the first node in a maximal subsequence of local
1707
1757
* flow steps in a dataflow path.
1708
1758
*/
1709
- predicate localFlowEntry ( NodeEx node , FlowState state , Configuration config ) {
1759
+ private predicate localFlowEntry ( NodeEx node , FlowState state , Configuration config ) {
1710
1760
Stage2:: revFlow ( node , state , config ) and
1711
1761
(
1712
- sourceNode ( node , state , config ) or
1713
- jumpStep ( _, node , config ) or
1714
- additionalJumpStep ( _, node , config ) or
1715
- additionalJumpStateStep ( _, _, node , state , config ) or
1716
- node instanceof ParamNodeEx or
1717
- node .asNode ( ) instanceof OutNodeExt or
1718
- store ( _, _, node , _, config ) or
1719
- read ( _, _, node , config ) or
1762
+ sourceNode ( node , state , config )
1763
+ or
1764
+ jumpStep ( _, node , config )
1765
+ or
1766
+ additionalJumpStep ( _, node , config )
1767
+ or
1768
+ additionalJumpStateStep ( _, _, node , state , config )
1769
+ or
1770
+ node instanceof ParamNodeEx
1771
+ or
1772
+ node .asNode ( ) instanceof OutNodeExt
1773
+ or
1774
+ store ( _, _, node , _, config )
1775
+ or
1776
+ read ( _, _, node , config )
1777
+ or
1720
1778
node instanceof FlowCheckNode
1779
+ or
1780
+ exists ( FlowState s |
1781
+ additionalLocalStateStep ( _, s , node , state , config ) and
1782
+ s != state
1783
+ )
1721
1784
)
1722
1785
}
1723
1786
@@ -1737,6 +1800,9 @@ private module LocalFlowBigStep {
1737
1800
or
1738
1801
exists ( NodeEx next , FlowState s | Stage2:: revFlow ( next , s , config ) |
1739
1802
additionalJumpStateStep ( node , state , next , s , config )
1803
+ or
1804
+ additionalLocalStateStep ( node , state , next , s , config ) and
1805
+ s != state
1740
1806
)
1741
1807
or
1742
1808
Stage2:: revFlow ( node , state , config ) and
@@ -1770,42 +1836,40 @@ private module LocalFlowBigStep {
1770
1836
*/
1771
1837
pragma [ nomagic]
1772
1838
private predicate localFlowStepPlus (
1773
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1774
- DataFlowType t , Configuration config , LocalCallContext cc
1839
+ NodeEx node1 , FlowState state , NodeEx node2 , boolean preservesValue , DataFlowType t ,
1840
+ Configuration config , LocalCallContext cc
1775
1841
) {
1776
1842
not isUnreachableInCallCached ( node2 .asNode ( ) , cc .( LocalCallContextSpecificCall ) .getCall ( ) ) and
1777
1843
(
1778
- localFlowEntry ( node1 , pragma [ only_bind_into ] ( state1 ) , pragma [ only_bind_into ] ( config ) ) and
1844
+ localFlowEntry ( node1 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( config ) ) and
1779
1845
(
1780
1846
localFlowStepNodeCand1 ( node1 , node2 , config ) and
1781
- state1 = state2 and
1782
1847
preservesValue = true and
1783
- t = node1 .getDataFlowType ( ) // irrelevant dummy value
1848
+ t = node1 .getDataFlowType ( ) and // irrelevant dummy value
1849
+ Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( config ) )
1784
1850
or
1785
- additionalLocalFlowStepNodeCand2 ( node1 , state1 , node2 , state2 , config ) and
1851
+ additionalLocalFlowStepNodeCand2 ( node1 , state , node2 , state , config ) and
1786
1852
preservesValue = false and
1787
1853
t = node2 .getDataFlowType ( )
1788
1854
) and
1789
1855
node1 != node2 and
1790
1856
cc .relevantFor ( node1 .getEnclosingCallable ( ) ) and
1791
- not isUnreachableInCallCached ( node1 .asNode ( ) , cc .( LocalCallContextSpecificCall ) .getCall ( ) ) and
1792
- Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , pragma [ only_bind_into ] ( config ) )
1857
+ not isUnreachableInCallCached ( node1 .asNode ( ) , cc .( LocalCallContextSpecificCall ) .getCall ( ) )
1793
1858
or
1794
1859
exists ( NodeEx mid |
1795
- localFlowStepPlus ( node1 , state1 , mid , pragma [ only_bind_into ] ( state2 ) , preservesValue , t ,
1860
+ localFlowStepPlus ( node1 , pragma [ only_bind_into ] ( state ) , mid , preservesValue , t ,
1796
1861
pragma [ only_bind_into ] ( config ) , cc ) and
1797
1862
localFlowStepNodeCand1 ( mid , node2 , config ) and
1798
1863
not mid instanceof FlowCheckNode and
1799
- Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , pragma [ only_bind_into ] ( config ) )
1864
+ Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( config ) )
1800
1865
)
1801
1866
or
1802
- exists ( NodeEx mid , FlowState st |
1803
- localFlowStepPlus ( node1 , state1 , mid , st , _, _, pragma [ only_bind_into ] ( config ) , cc ) and
1804
- additionalLocalFlowStepNodeCand2 ( mid , st , node2 , state2 , config ) and
1867
+ exists ( NodeEx mid |
1868
+ localFlowStepPlus ( node1 , state , mid , _, _, pragma [ only_bind_into ] ( config ) , cc ) and
1869
+ additionalLocalFlowStepNodeCand2 ( mid , state , node2 , state , config ) and
1805
1870
not mid instanceof FlowCheckNode and
1806
1871
preservesValue = false and
1807
- t = node2 .getDataFlowType ( ) and
1808
- Stage2:: revFlow ( node2 , state2 , pragma [ only_bind_into ] ( config ) )
1872
+ t = node2 .getDataFlowType ( )
1809
1873
)
1810
1874
)
1811
1875
}
@@ -1819,9 +1883,19 @@ private module LocalFlowBigStep {
1819
1883
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1820
1884
AccessPathFrontNil apf , Configuration config , LocalCallContext callContext
1821
1885
) {
1822
- localFlowStepPlus ( node1 , state1 , node2 , state2 , preservesValue , apf .getType ( ) , config ,
1823
- callContext ) and
1824
- localFlowExit ( node2 , state2 , config )
1886
+ localFlowStepPlus ( node1 , state1 , node2 , preservesValue , apf .getType ( ) , config , callContext ) and
1887
+ localFlowExit ( node2 , state1 , config ) and
1888
+ state1 = state2
1889
+ or
1890
+ additionalLocalFlowStepNodeCand2 ( node1 , state1 , node2 , state2 , config ) and
1891
+ state1 != state2 and
1892
+ preservesValue = false and
1893
+ apf = TFrontNil ( node2 .getDataFlowType ( ) ) and
1894
+ callContext .relevantFor ( node1 .getEnclosingCallable ( ) ) and
1895
+ not exists ( DataFlowCall call | call = callContext .( LocalCallContextSpecificCall ) .getCall ( ) |
1896
+ isUnreachableInCallCached ( node1 .asNode ( ) , call ) or
1897
+ isUnreachableInCallCached ( node2 .asNode ( ) , call )
1898
+ )
1825
1899
}
1826
1900
}
1827
1901
@@ -2695,10 +2769,10 @@ private module Stage4 {
2695
2769
2696
2770
bindingset [ node, cc, config]
2697
2771
private LocalCc getLocalCc ( NodeEx node , Cc cc , Configuration config ) {
2698
- localFlowEntry ( node , _, config ) and
2699
2772
result =
2700
2773
getLocalCallContext ( pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( cc ) ) ,
2701
- node .getEnclosingCallable ( ) )
2774
+ node .getEnclosingCallable ( ) ) and
2775
+ exists ( config )
2702
2776
}
2703
2777
2704
2778
private predicate localStep (
0 commit comments