@@ -87,12 +87,30 @@ abstract class Configuration extends string {
8787 /** Holds if data flow into `node` is prohibited. */
8888 predicate isBarrierIn ( Node node ) { none ( ) }
8989
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+
9096 /** Holds if data flow out of `node` is prohibited. */
9197 predicate isBarrierOut ( Node node ) { none ( ) }
9298
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+
93105 /** Holds if data flow through nodes guarded by `guard` is prohibited. */
94106 predicate isBarrierGuard ( BarrierGuard guard ) { none ( ) }
95107
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+
96114 /**
97115 * Holds if the additional flow step from `node1` to `node2` must be taken
98116 * into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
305323 ReturnKindExt getKind ( ) { result = this .asNode ( ) .( ReturnNodeExt ) .getKind ( ) }
306324}
307325
308- private predicate inBarrier ( NodeEx node , Configuration config ) {
326+ private predicate fullInBarrier ( NodeEx node , Configuration config ) {
309327 exists ( Node n |
310328 node .asNode ( ) = n and
311329 config .isBarrierIn ( n )
@@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
314332 )
315333}
316334
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 ) {
318345 exists ( Node n |
319346 node .asNode ( ) = n and
320347 config .isBarrierOut ( n )
@@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
323350 )
324351}
325352
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+
326362pragma [ nomagic]
327363private predicate fullBarrier ( NodeEx node , Configuration config ) {
328364 exists ( Node n | node .asNode ( ) = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
345381
346382pragma [ nomagic]
347383private predicate stateBarrier ( NodeEx node , FlowState state , Configuration config ) {
348- exists ( Node n |
349- node .asNode ( ) = n and
384+ exists ( Node n | node .asNode ( ) = n |
350385 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+ )
351397 )
352398}
353399
@@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
376422/** Provides the relevant barriers for a step from `node1` to `node2`. */
377423pragma [ inline]
378424private 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
381427 not fullBarrier ( node1 , config ) and
382428 not fullBarrier ( node2 , config )
383429}
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
430476 config .isAdditionalFlowStep ( n1 , s1 , n2 , s2 ) and
431477 getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
432478 stepFilter ( node1 , node2 , config ) and
479+ not stateOutBarrier ( node1 , s1 , config ) and
480+ not stateInBarrier ( node2 , s2 , config ) and
433481 not stateBarrier ( node1 , s1 , config ) and
434482 not stateBarrier ( node2 , s2 , config )
435483 )
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
471519 config .isAdditionalFlowStep ( n1 , s1 , n2 , s2 ) and
472520 getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
473521 stepFilter ( node1 , node2 , config ) and
522+ not stateOutBarrier ( node1 , s1 , config ) and
523+ not stateInBarrier ( node2 , s2 , config ) and
474524 not stateBarrier ( node1 , s1 , config ) and
475525 not stateBarrier ( node2 , s2 , config ) and
476526 not config .getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
870920 private predicate throughFlowNodeCand ( NodeEx node , Configuration config ) {
871921 revFlow ( node , true , config ) and
872922 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 )
875925 }
876926
877927 /** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
9661016) {
9671017 viableReturnPosOutNodeCand1 ( call , ret .getReturnPosition ( ) , out , config ) and
9681018 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 )
9711021}
9721022
9731023pragma [ nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
9881038) {
9891039 viableParamArgNodeCand1 ( call , p , arg , config ) and
9901040 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 )
9931043}
9941044
9951045/**
@@ -1706,18 +1756,31 @@ private module LocalFlowBigStep {
17061756 * Holds if `node` can be the first node in a maximal subsequence of local
17071757 * flow steps in a dataflow path.
17081758 */
1709- predicate localFlowEntry ( NodeEx node , FlowState state , Configuration config ) {
1759+ private predicate localFlowEntry ( NodeEx node , FlowState state , Configuration config ) {
17101760 Stage2:: revFlow ( node , state , config ) and
17111761 (
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
17201778 node instanceof FlowCheckNode
1779+ or
1780+ exists ( FlowState s |
1781+ additionalLocalStateStep ( _, s , node , state , config ) and
1782+ s != state
1783+ )
17211784 )
17221785 }
17231786
@@ -1737,6 +1800,9 @@ private module LocalFlowBigStep {
17371800 or
17381801 exists ( NodeEx next , FlowState s | Stage2:: revFlow ( next , s , config ) |
17391802 additionalJumpStateStep ( node , state , next , s , config )
1803+ or
1804+ additionalLocalStateStep ( node , state , next , s , config ) and
1805+ s != state
17401806 )
17411807 or
17421808 Stage2:: revFlow ( node , state , config ) and
@@ -1770,42 +1836,40 @@ private module LocalFlowBigStep {
17701836 */
17711837 pragma [ nomagic]
17721838 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
17751841 ) {
17761842 not isUnreachableInCallCached ( node2 .asNode ( ) , cc .( LocalCallContextSpecificCall ) .getCall ( ) ) and
17771843 (
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
17791845 (
17801846 localFlowStepNodeCand1 ( node1 , node2 , config ) and
1781- state1 = state2 and
17821847 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 ) )
17841850 or
1785- additionalLocalFlowStepNodeCand2 ( node1 , state1 , node2 , state2 , config ) and
1851+ additionalLocalFlowStepNodeCand2 ( node1 , state , node2 , state , config ) and
17861852 preservesValue = false and
17871853 t = node2 .getDataFlowType ( )
17881854 ) and
17891855 node1 != node2 and
17901856 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 ( ) )
17931858 or
17941859 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 ,
17961861 pragma [ only_bind_into ] ( config ) , cc ) and
17971862 localFlowStepNodeCand1 ( mid , node2 , config ) and
17981863 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 ) )
18001865 )
18011866 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
18051870 not mid instanceof FlowCheckNode and
18061871 preservesValue = false and
1807- t = node2 .getDataFlowType ( ) and
1808- Stage2:: revFlow ( node2 , state2 , pragma [ only_bind_into ] ( config ) )
1872+ t = node2 .getDataFlowType ( )
18091873 )
18101874 )
18111875 }
@@ -1819,9 +1883,19 @@ private module LocalFlowBigStep {
18191883 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
18201884 AccessPathFrontNil apf , Configuration config , LocalCallContext callContext
18211885 ) {
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+ )
18251899 }
18261900}
18271901
@@ -2695,10 +2769,10 @@ private module Stage4 {
26952769
26962770 bindingset [ node, cc, config]
26972771 private LocalCc getLocalCc ( NodeEx node , Cc cc , Configuration config ) {
2698- localFlowEntry ( node , _, config ) and
26992772 result =
27002773 getLocalCallContext ( pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( cc ) ) ,
2701- node .getEnclosingCallable ( ) )
2774+ node .getEnclosingCallable ( ) ) and
2775+ exists ( config )
27022776 }
27032777
27042778 private predicate localStep (
0 commit comments