@@ -461,6 +461,40 @@ module TypeTracking<TypeTrackingInput I> {
461
461
stepSplit ( nodeFrom , nodeTo , summary )
462
462
}
463
463
464
+ pragma [ nomagic]
465
+ private predicate stepProj ( LocalSourceNode nodeFrom , StepSummary summary ) {
466
+ step ( nodeFrom , _, summary )
467
+ }
468
+
469
+ bindingset [ t, nodeFrom]
470
+ pragma [ inline_late]
471
+ pragma [ noopt]
472
+ private TypeTracker stepInlineLate ( TypeTracker t , LocalSourceNode nodeFrom , LocalSourceNode nodeTo ) {
473
+ exists ( StepSummary summary |
474
+ stepProj ( nodeFrom , summary ) and
475
+ result = append ( t , summary ) and
476
+ step ( nodeFrom , nodeTo , summary )
477
+ )
478
+ }
479
+
480
+ pragma [ nomagic]
481
+ private predicate smallStepProj ( LocalSourceNode nodeFrom , StepSummary summary ) {
482
+ smallStep ( nodeFrom , _, summary )
483
+ }
484
+
485
+ bindingset [ t, nodeFrom]
486
+ pragma [ inline_late]
487
+ pragma [ noopt]
488
+ private TypeTracker smallStepInlineLate (
489
+ TypeTracker t , LocalSourceNode nodeFrom , LocalSourceNode nodeTo
490
+ ) {
491
+ exists ( StepSummary summary |
492
+ smallStepProj ( nodeFrom , summary ) and
493
+ result = append ( t , summary ) and
494
+ smallStep ( nodeFrom , nodeTo , summary )
495
+ )
496
+ }
497
+
464
498
/**
465
499
* A summary of the steps needed to track a value to a given dataflow node.
466
500
*
@@ -493,9 +527,6 @@ module TypeTracking<TypeTrackingInput I> {
493
527
494
528
TypeTracker ( ) { this = MkTypeTracker ( hasCall , content ) }
495
529
496
- /** Gets the summary resulting from appending `step` to this type-tracking summary. */
497
- private TypeTracker append ( StepSummary step ) { result = append ( this , step ) }
498
-
499
530
/** Gets a textual representation of this summary. */
500
531
string toString ( ) {
501
532
exists ( string withCall , string withContent |
@@ -553,13 +584,9 @@ module TypeTracking<TypeTrackingInput I> {
553
584
* Gets the summary that corresponds to having taken a forwards
554
585
* heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
555
586
*/
556
- bindingset [ nodeFrom , this ]
587
+ pragma [ inline ]
557
588
TypeTracker step ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo ) {
558
- exists ( StepSummary summary |
559
- step ( pragma [ only_bind_out ] ( nodeFrom ) , _, pragma [ only_bind_into ] ( summary ) ) and
560
- result = pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( this ) ) .append ( summary ) and
561
- step ( pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( nodeFrom ) ) , nodeTo , summary )
562
- )
589
+ result = stepInlineLate ( this , nodeFrom , nodeTo )
563
590
}
564
591
565
592
/**
@@ -586,13 +613,9 @@ module TypeTracking<TypeTrackingInput I> {
586
613
* }
587
614
* ```
588
615
*/
589
- bindingset [ nodeFrom , this ]
616
+ pragma [ inline ]
590
617
TypeTracker smallstep ( Node nodeFrom , Node nodeTo ) {
591
- exists ( StepSummary summary |
592
- smallStep ( pragma [ only_bind_out ] ( nodeFrom ) , _, pragma [ only_bind_into ] ( summary ) ) and
593
- result = pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( this ) ) .append ( summary ) and
594
- smallStep ( pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( nodeFrom ) ) , nodeTo , summary )
595
- )
618
+ result = smallStepInlineLate ( this , nodeFrom , nodeTo )
596
619
or
597
620
simpleLocalSmallStep ( nodeFrom , nodeTo ) and
598
621
result = this
0 commit comments