@@ -4308,8 +4308,7 @@ module MakeImpl<InputSig Lang> {
43084308 pragma [ only_bind_into ] ( apout ) ) and
43094309 pathIntoCallable ( arg , par , _, _, innercc , sc , _) and
43104310 paramFlowsThrough ( kind , pragma [ only_bind_into ] ( sout ) , innercc , sc ,
4311- pragma [ only_bind_into ] ( t ) , pragma [ only_bind_into ] ( apout ) , _) and
4312- not arg .isHidden ( )
4311+ pragma [ only_bind_into ] ( t ) , pragma [ only_bind_into ] ( apout ) , _)
43134312 }
43144313
43154314 /**
@@ -4340,42 +4339,98 @@ module MakeImpl<InputSig Lang> {
43404339 )
43414340 }
43424341
4343- private PathNodeImpl localStepToHidden ( PathNodeImpl n ) {
4342+ private PathNodeImpl localStep ( PathNodeImpl n ) {
43444343 n .getASuccessorImpl ( ) = result and
4345- result .isHidden ( ) and
43464344 exists ( NodeEx n1 , NodeEx n2 | n1 = n .getNodeEx ( ) and n2 = result .getNodeEx ( ) |
43474345 localFlowBigStep ( n1 , _, n2 , _, _, _, _) or
43484346 storeEx ( n1 , _, n2 , _, _) or
43494347 readSetEx ( n1 , _, n2 )
43504348 )
43514349 }
43524350
4351+ private PathNodeImpl summaryCtxStep ( PathNodeImpl n ) {
4352+ n .getASuccessorImpl ( ) = result and
4353+ exists ( SummaryCtxSome sc |
4354+ pathNode ( n , _, _, _, pragma [ only_bind_into ] ( sc ) , _, _, _) and
4355+ pathNode ( result , _, _, _, pragma [ only_bind_into ] ( sc ) , _, _, _)
4356+ )
4357+ }
4358+
4359+ private PathNodeImpl localStepToHidden ( PathNodeImpl n ) {
4360+ result = localStep ( n ) and
4361+ result .isHidden ( )
4362+ }
4363+
4364+ private PathNodeImpl localStepFromHidden ( PathNodeImpl n ) {
4365+ n = localStep ( result ) and
4366+ result .isHidden ( )
4367+ }
4368+
43534369 pragma [ nomagic]
43544370 private predicate hasSuccessor ( PathNodeImpl pred , PathNodeMid succ , NodeEx succNode ) {
4355- succ = pred .getANonHiddenSuccessor ( ) and
4371+ succ = pred .getASuccessorImpl ( ) and
43564372 succNode = succ .getNodeEx ( )
43574373 }
43584374
43594375 /**
4360- * Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
4361- * a subpath between `par` and `ret` with the connecting edges `arg -> par` and
4362- * `ret -> out` is summarized as the edge `arg -> out` .
4376+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple.
4377+ *
4378+ * All of the nodes may be hidden .
43634379 */
4364- predicate subpaths ( PathNodeImpl arg , PathNodeImpl par , PathNodeImpl ret , PathNodeImpl out ) {
4380+ pragma [ nomagic]
4381+ private predicate subpaths04 (
4382+ PathNodeImpl arg , PathNodeImpl par , PathNodeImpl ret , PathNodeImpl out
4383+ ) {
43654384 exists (
43664385 ParamNodeEx p , NodeEx o , FlowState sout , DataFlowType t , AccessPath apout ,
43674386 PathNodeMid out0
43684387 |
4369- pragma [ only_bind_into ] ( arg ) .getANonHiddenSuccessor ( ) = pragma [ only_bind_into ] ( out0 ) and
4370- subpaths03 ( pragma [ only_bind_into ] ( arg ) , p , localStepToHidden * ( ret ) , o , sout , t , apout ) and
4388+ pragma [ only_bind_into ] ( arg ) .getASuccessorImpl ( ) = pragma [ only_bind_into ] ( out0 ) and
4389+ subpaths03 ( pragma [ only_bind_into ] ( arg ) , p , ret , o , sout , t , apout ) and
43714390 hasSuccessor ( pragma [ only_bind_into ] ( arg ) , par , p ) and
4372- not ret .isHidden ( ) and
43734391 pathNode ( out0 , o , sout , _, _, t , apout , _)
43744392 |
43754393 out = out0 or out = out0 .projectToSink ( )
43764394 )
43774395 }
43784396
4397+ /**
4398+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple.
4399+ *
4400+ * `par` and `ret` are not hidden.
4401+ */
4402+ pragma [ nomagic]
4403+ private predicate subpaths05 (
4404+ PathNodeImpl arg , PathNodeImpl par , PathNodeImpl ret , PathNodeImpl out
4405+ ) {
4406+ // direct subpath
4407+ subpaths04 ( arg , localStepFromHidden * ( par ) , localStepToHidden * ( ret ) , out ) and
4408+ not par .isHidden ( ) and
4409+ not ret .isHidden ( ) and
4410+ ret = summaryCtxStep * ( par )
4411+ or
4412+ // wrapped subpath using hidden nodes, e.g. flow through a callback inside
4413+ // a summarized callable
4414+ exists ( PathNodeImpl par0 , PathNodeImpl ret0 |
4415+ subpaths05 ( localStepToHidden * ( par0 ) , par , ret , localStepFromHidden * ( ret0 ) ) and
4416+ subpaths04 ( arg , par0 , ret0 , out )
4417+ )
4418+ }
4419+
4420+ /**
4421+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
4422+ * a subpath between `par` and `ret` with the connecting edges `arg -> par` and
4423+ * `ret -> out` is summarized as the edge `arg -> out`.
4424+ *
4425+ * None of the nodes are hidden.
4426+ */
4427+ pragma [ nomagic]
4428+ predicate subpaths ( PathNodeImpl arg , PathNodeImpl par , PathNodeImpl ret , PathNodeImpl out ) {
4429+ subpaths05 ( localStepToHidden * ( arg ) , par , ret , localStepFromHidden * ( out ) ) and
4430+ not arg .isHidden ( ) and
4431+ not out .isHidden ( )
4432+ }
4433+
43794434 /**
43804435 * Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
43814436 */
0 commit comments