@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
32583258 /** Gets the associated configuration. */
32593259 Configuration getConfiguration ( ) { none ( ) }
32603260
3261- private predicate isHidden ( ) {
3262- hiddenNode ( this .( PathNodeImpl ) .getNodeEx ( ) .asNode ( ) ) and
3263- not this .isSource ( ) and
3264- not this instanceof PathNodeSink
3265- or
3266- this .( PathNodeImpl ) .getNodeEx ( ) instanceof TNodeImplicitRead
3267- }
3268-
32693261 private PathNode getASuccessorIfHidden ( ) {
3270- this .isHidden ( ) and
3262+ this .( PathNodeImpl ) . isHidden ( ) and
32713263 result = this .( PathNodeImpl ) .getASuccessorImpl ( )
32723264 }
32733265
32743266 /** Gets a successor of this node, if any. */
32753267 final PathNode getASuccessor ( ) {
32763268 result = this .( PathNodeImpl ) .getASuccessorImpl ( ) .getASuccessorIfHidden * ( ) and
3277- not this .isHidden ( ) and
3278- not result .isHidden ( )
3269+ not this .( PathNodeImpl ) . isHidden ( ) and
3270+ not result .( PathNodeImpl ) . isHidden ( )
32793271 }
32803272
32813273 /** Holds if this node is a source. */
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
32873279
32883280 abstract NodeEx getNodeEx ( ) ;
32893281
3282+ predicate isHidden ( ) {
3283+ hiddenNode ( this .getNodeEx ( ) .asNode ( ) ) and
3284+ not this .isSource ( ) and
3285+ not this instanceof PathNodeSink
3286+ or
3287+ this .getNodeEx ( ) instanceof TNodeImplicitRead
3288+ }
3289+
32903290 private string ppAp ( ) {
32913291 this instanceof PathNodeSink and result = ""
32923292 or
@@ -3313,10 +3313,15 @@ abstract private class PathNodeImpl extends PathNode {
33133313}
33143314
33153315/** Holds if `n` can reach a sink. */
3316- private predicate reach ( PathNode n ) { n instanceof PathNodeSink or reach ( n .getASuccessor ( ) ) }
3316+ private predicate directReach ( PathNode n ) {
3317+ n instanceof PathNodeSink or directReach ( n .getASuccessor ( ) )
3318+ }
3319+
3320+ /** Holds if `n` can reach a sink or is used in a subpath. */
3321+ private predicate reach ( PathNode n ) { directReach ( n ) or Subpaths:: retReach ( n ) }
33173322
3318- /** Holds if `n1.getSucc () = n2` and `n2` can reach a sink. */
3319- private predicate pathSucc ( PathNode n1 , PathNode n2 ) { n1 .getASuccessor ( ) = n2 and reach ( n2 ) }
3323+ /** Holds if `n1.getASuccessor () = n2` and `n2` can reach a sink. */
3324+ private predicate pathSucc ( PathNode n1 , PathNode n2 ) { n1 .getASuccessor ( ) = n2 and directReach ( n2 ) }
33203325
33213326private predicate pathSuccPlus ( PathNode n1 , PathNode n2 ) = fastTC( pathSucc / 2 ) ( n1 , n2 )
33223327
@@ -3325,12 +3330,14 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
33253330 */
33263331module PathGraph {
33273332 /** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
3328- query predicate edges ( PathNode a , PathNode b ) { pathSucc ( a , b ) }
3333+ query predicate edges ( PathNode a , PathNode b ) { a . getASuccessor ( ) = b and reach ( b ) }
33293334
33303335 /** Holds if `n` is a node in the graph of data flow path explanations. */
33313336 query predicate nodes ( PathNode n , string key , string val ) {
33323337 reach ( n ) and key = "semmle.label" and val = n .toString ( )
33333338 }
3339+
3340+ query predicate subpaths = Subpaths:: subpaths / 4 ;
33343341}
33353342
33363343/**
@@ -3622,6 +3629,86 @@ private predicate pathThroughCallable(PathNodeMid mid, NodeEx out, CallContext c
36223629 )
36233630}
36243631
3632+ private module Subpaths {
3633+ /**
3634+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple and `ret` is determined by
3635+ * `kind`, `sc`, `apout`, and `innercc`.
3636+ */
3637+ pragma [ nomagic]
3638+ private predicate subpaths01 (
3639+ PathNode arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
3640+ NodeEx out , AccessPath apout
3641+ ) {
3642+ pathThroughCallable ( arg , out , _, apout ) and
3643+ pathIntoCallable ( arg , par , _, innercc , sc , _) and
3644+ paramFlowsThrough ( kind , innercc , sc , apout , _, unbindConf ( arg .getConfiguration ( ) ) )
3645+ }
3646+
3647+ /**
3648+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple and `ret` is determined by
3649+ * `kind`, `sc`, `apout`, and `innercc`.
3650+ */
3651+ pragma [ nomagic]
3652+ private predicate subpaths02 (
3653+ PathNode arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
3654+ NodeEx out , AccessPath apout
3655+ ) {
3656+ subpaths01 ( arg , par , sc , innercc , kind , out , apout ) and
3657+ out .asNode ( ) = kind .getAnOutNode ( _)
3658+ }
3659+
3660+ pragma [ nomagic]
3661+ private Configuration getPathNodeConf ( PathNode n ) { result = n .getConfiguration ( ) }
3662+
3663+ /**
3664+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple.
3665+ */
3666+ pragma [ nomagic]
3667+ private predicate subpaths03 (
3668+ PathNode arg , ParamNodeEx par , PathNodeMid ret , NodeEx out , AccessPath apout
3669+ ) {
3670+ exists ( SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind , RetNodeEx retnode |
3671+ subpaths02 ( arg , par , sc , innercc , kind , out , apout ) and
3672+ ret .getNodeEx ( ) = retnode and
3673+ kind = retnode .getKind ( ) and
3674+ innercc = ret .getCallContext ( ) and
3675+ sc = ret .getSummaryCtx ( ) and
3676+ ret .getConfiguration ( ) = unbindConf ( getPathNodeConf ( arg ) ) and
3677+ apout = ret .getAp ( ) and
3678+ not ret .isHidden ( )
3679+ )
3680+ }
3681+
3682+ /**
3683+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3684+ * a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3685+ * `ret -> out` is summarized as the edge `arg -> out`.
3686+ */
3687+ predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeMid ret , PathNodeMid out ) {
3688+ exists ( ParamNodeEx p , NodeEx o , AccessPath apout |
3689+ arg .getASuccessor ( ) = par and
3690+ arg .getASuccessor ( ) = out and
3691+ subpaths03 ( arg , p , ret , o , apout ) and
3692+ par .getNodeEx ( ) = p and
3693+ out .getNodeEx ( ) = o and
3694+ out .getAp ( ) = apout
3695+ )
3696+ }
3697+
3698+ /**
3699+ * Holds if `n` can reach a return node in a summarized subpath.
3700+ */
3701+ predicate retReach ( PathNode n ) {
3702+ subpaths ( _, _, n , _)
3703+ or
3704+ exists ( PathNode mid |
3705+ retReach ( mid ) and
3706+ n .getASuccessor ( ) = mid and
3707+ not subpaths ( _, mid , _, _)
3708+ )
3709+ }
3710+ }
3711+
36253712/**
36263713 * Holds if data can flow (inter-procedurally) from `source` to `sink`.
36273714 *
0 commit comments