@@ -60,6 +60,18 @@ signature module UniversalFlowInput<LocationSig Location> {
6060 * the null analysis determines that `n` is always null.
6161 */
6262 default predicate isExcludedFromNullAnalysis ( FlowNode n ) { none ( ) }
63+
64+ /**
65+ * Holds if the evaluator is currently evaluating with an overlay. The
66+ * implementation of this predicate needs to be `overlay[local]`. For a
67+ * language with no overlay support, `none()` is a valid implementation.
68+ *
69+ * When called from a local predicate, this predicate holds if we are in the
70+ * overlay-only local evaluation. When called from a global predicate, this
71+ * predicate holds if we are evaluating globally with overlay and base both
72+ * visible.
73+ */
74+ predicate isEvaluatingInOverlay ( ) ;
6375}
6476
6577/**
@@ -68,23 +80,46 @@ signature module UniversalFlowInput<LocationSig Location> {
6880module Make< LocationSig Location, UniversalFlowInput< Location > I> {
6981 private import I
7082
83+ overlay [ local?]
84+ private predicate overlayNode ( FlowNode n ) { isEvaluatingInOverlay ( ) and exists ( n ) }
85+
86+ overlay [ global]
87+ private predicate canReachOverlay ( FlowNode n ) {
88+ overlayNode ( n )
89+ or
90+ exists ( FlowNode mid | canReachOverlay ( mid ) and step ( n , mid ) )
91+ }
92+
93+ bindingset [ n]
94+ private predicate relevantNode ( FlowNode n ) {
95+ not isEvaluatingInOverlay ( )
96+ or
97+ canReachOverlay ( n )
98+ }
99+
71100 /**
72101 * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
73102 * functionally determined by `n2`.
74103 */
75- private predicate uniqStep ( FlowNode n1 , FlowNode n2 ) { n1 = unique( FlowNode n | step ( n , n2 ) ) }
104+ private predicate uniqStep ( FlowNode n1 , FlowNode n2 ) {
105+ n1 = unique( FlowNode n | step ( n , n2 ) ) and relevantNode ( n2 )
106+ }
76107
77108 /**
78109 * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
79110 * functionally determined by `n2`.
80111 */
81- private predicate joinStep ( FlowNode n1 , FlowNode n2 ) { step ( n1 , n2 ) and not uniqStep ( n1 , n2 ) }
112+ private predicate joinStep ( FlowNode n1 , FlowNode n2 ) {
113+ step ( n1 , n2 ) and not uniqStep ( n1 , n2 ) and relevantNode ( n2 )
114+ }
82115
83116 /** Holds if `null` is the only value that flows to `n`. */
84117 private predicate isNull ( FlowNode n ) {
85- isNullValue ( n )
118+ isNullValue ( n ) and
119+ relevantNode ( n )
86120 or
87121 not isExcludedFromNullAnalysis ( n ) and
122+ relevantNode ( n ) and
88123 (
89124 exists ( FlowNode mid | isNull ( mid ) and uniqStep ( mid , n ) )
90125 or
@@ -256,21 +291,24 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
256291 private module Propagation implements PropPropagation {
257292 class Prop = Unit ;
258293
259- predicate candProp ( FlowNode n , Unit u ) { hasProperty ( n ) and exists ( u ) }
294+ predicate candProp ( FlowNode n , Unit u ) { hasPropertyImpl ( n ) and exists ( u ) }
260295
261296 predicate supportsProp = candProp / 2 ;
262297 }
263298
264299 /**
265300 * Holds if all flow reaching `n` originates from nodes in
266301 * `hasPropertyBase`.
302+ *
303+ * When evaluated in an overlay-merged context, this is restricted to nodes
304+ * that can reach the overlay.
267305 */
268- predicate hasProperty ( FlowNode n ) {
306+ private predicate hasPropertyImpl ( FlowNode n ) {
269307 P:: hasPropertyBase ( n )
270308 or
271309 not P:: barrier ( n ) and
272310 (
273- exists ( FlowNode mid | hasProperty ( mid ) and uniqStepNotNull ( mid , n ) )
311+ exists ( FlowNode mid | hasPropertyImpl ( mid ) and uniqStepNotNull ( mid , n ) )
274312 or
275313 // The following is an optimized version of
276314 // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
@@ -284,6 +322,13 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
284322 )
285323 )
286324 }
325+
326+ /**
327+ * Holds if all flow reaching `n` originates from nodes in
328+ * `hasPropertyBase`.
329+ */
330+ overlay [ local?]
331+ predicate hasProperty ( FlowNode n ) = forceLocal( hasPropertyImpl / 1 ) ( n )
287332 }
288333
289334 signature module PropertySig {
@@ -305,25 +350,28 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
305350 private module Propagation implements PropPropagation {
306351 class Prop = P:: Prop ;
307352
308- predicate candProp = hasProperty / 2 ;
353+ predicate candProp = hasPropertyImpl / 2 ;
309354
310355 bindingset [ t]
311356 predicate supportsProp ( FlowNode n , Prop t ) {
312- exists ( Prop t0 | hasProperty ( n , t0 ) and P:: propImplies ( t0 , t ) )
357+ exists ( Prop t0 | hasPropertyImpl ( n , t0 ) and P:: propImplies ( t0 , t ) )
313358 }
314359 }
315360
316361 /**
317362 * Holds if all flow reaching `n` originates from nodes in
318363 * `hasPropertyBase`. The property `t` is taken from one of those origins
319364 * such that all other origins imply `t`.
365+ *
366+ * When evaluated in an overlay-merged context, this is restricted to nodes
367+ * that can reach the overlay.
320368 */
321- predicate hasProperty ( FlowNode n , P:: Prop t ) {
369+ private predicate hasPropertyImpl ( FlowNode n , P:: Prop t ) {
322370 P:: hasPropertyBase ( n , t )
323371 or
324372 not P:: barrier ( n ) and
325373 (
326- exists ( FlowNode mid | hasProperty ( mid , t ) and uniqStepNotNull ( mid , n ) )
374+ exists ( FlowNode mid | hasPropertyImpl ( mid , t ) and uniqStepNotNull ( mid , n ) )
327375 or
328376 // The following is an optimized version of
329377 // ```
@@ -349,5 +397,13 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
349397 )
350398 )
351399 }
400+
401+ /**
402+ * Holds if all flow reaching `n` originates from nodes in
403+ * `hasPropertyBase`. The property `t` is taken from one of those origins
404+ * such that all other origins imply `t`.
405+ */
406+ overlay [ local?]
407+ predicate hasProperty ( FlowNode n , P:: Prop t ) = forceLocal( hasPropertyImpl / 2 ) ( n , t )
352408 }
353409}
0 commit comments