@@ -461,6 +461,40 @@ module TypeTracking<TypeTrackingInput I> {
461461 stepSplit ( nodeFrom , nodeTo , summary )
462462 }
463463
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+
464498 /**
465499 * A summary of the steps needed to track a value to a given dataflow node.
466500 *
@@ -493,9 +527,6 @@ module TypeTracking<TypeTrackingInput I> {
493527
494528 TypeTracker ( ) { this = MkTypeTracker ( hasCall , content ) }
495529
496- /** Gets the summary resulting from appending `step` to this type-tracking summary. */
497- private TypeTracker append ( StepSummary step ) { result = append ( this , step ) }
498-
499530 /** Gets a textual representation of this summary. */
500531 string toString ( ) {
501532 exists ( string withCall , string withContent |
@@ -553,13 +584,9 @@ module TypeTracking<TypeTrackingInput I> {
553584 * Gets the summary that corresponds to having taken a forwards
554585 * heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
555586 */
556- bindingset [ nodeFrom , this ]
587+ pragma [ inline ]
557588 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 )
563590 }
564591
565592 /**
@@ -586,13 +613,9 @@ module TypeTracking<TypeTrackingInput I> {
586613 * }
587614 * ```
588615 */
589- bindingset [ nodeFrom , this ]
616+ pragma [ inline ]
590617 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 )
596619 or
597620 simpleLocalSmallStep ( nodeFrom , nodeTo ) and
598621 result = this
0 commit comments