@@ -4308,8 +4308,7 @@ module MakeImpl<InputSig Lang> {
4308
4308
pragma [ only_bind_into ] ( apout ) ) and
4309
4309
pathIntoCallable ( arg , par , _, _, innercc , sc , _) and
4310
4310
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 ) , _)
4313
4312
}
4314
4313
4315
4314
/**
@@ -4340,42 +4339,98 @@ module MakeImpl<InputSig Lang> {
4340
4339
)
4341
4340
}
4342
4341
4343
- private PathNodeImpl localStepToHidden ( PathNodeImpl n ) {
4342
+ private PathNodeImpl localStep ( PathNodeImpl n ) {
4344
4343
n .getASuccessorImpl ( ) = result and
4345
- result .isHidden ( ) and
4346
4344
exists ( NodeEx n1 , NodeEx n2 | n1 = n .getNodeEx ( ) and n2 = result .getNodeEx ( ) |
4347
4345
localFlowBigStep ( n1 , _, n2 , _, _, _, _) or
4348
4346
storeEx ( n1 , _, n2 , _, _) or
4349
4347
readSetEx ( n1 , _, n2 )
4350
4348
)
4351
4349
}
4352
4350
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
+
4353
4369
pragma [ nomagic]
4354
4370
private predicate hasSuccessor ( PathNodeImpl pred , PathNodeMid succ , NodeEx succNode ) {
4355
- succ = pred .getANonHiddenSuccessor ( ) and
4371
+ succ = pred .getASuccessorImpl ( ) and
4356
4372
succNode = succ .getNodeEx ( )
4357
4373
}
4358
4374
4359
4375
/**
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 .
4363
4379
*/
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
+ ) {
4365
4384
exists (
4366
4385
ParamNodeEx p , NodeEx o , FlowState sout , DataFlowType t , AccessPath apout ,
4367
4386
PathNodeMid out0
4368
4387
|
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
4371
4390
hasSuccessor ( pragma [ only_bind_into ] ( arg ) , par , p ) and
4372
- not ret .isHidden ( ) and
4373
4391
pathNode ( out0 , o , sout , _, _, t , apout , _)
4374
4392
|
4375
4393
out = out0 or out = out0 .projectToSink ( )
4376
4394
)
4377
4395
}
4378
4396
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
+
4379
4434
/**
4380
4435
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
4381
4436
*/
0 commit comments