@@ -630,6 +630,42 @@ module TypeTracking<TypeTrackingInput I> {
630630 TypeTracker end ( ) { result .end ( ) }
631631 }
632632
633+ pragma [ nomagic]
634+ private predicate backStepProj ( LocalSourceNode nodeTo , StepSummary summary ) {
635+ step ( _, nodeTo , summary )
636+ }
637+
638+ bindingset [ t, nodeTo]
639+ pragma [ inline_late]
640+ pragma [ noopt]
641+ private TypeBackTracker backStepInlineLate (
642+ TypeBackTracker t , LocalSourceNode nodeFrom , LocalSourceNode nodeTo
643+ ) {
644+ exists ( StepSummary summary |
645+ backStepProj ( nodeTo , summary ) and
646+ result = prepend ( t , summary ) and
647+ step ( nodeFrom , nodeTo , summary )
648+ )
649+ }
650+
651+ pragma [ nomagic]
652+ private predicate backSmallStepProj ( LocalSourceNode nodeTo , StepSummary summary ) {
653+ smallStep ( _, nodeTo , summary )
654+ }
655+
656+ bindingset [ t, nodeTo]
657+ pragma [ inline_late]
658+ pragma [ noopt]
659+ private TypeBackTracker backSmallStepInlineLate (
660+ TypeBackTracker t , LocalSourceNode nodeFrom , LocalSourceNode nodeTo
661+ ) {
662+ exists ( StepSummary summary |
663+ backSmallStepProj ( nodeTo , summary ) and
664+ result = prepend ( t , summary ) and
665+ smallStep ( nodeFrom , nodeTo , summary )
666+ )
667+ }
668+
633669 /**
634670 * A summary of the steps needed to back-track a use of a value to a given dataflow node.
635671 *
@@ -665,9 +701,6 @@ module TypeTracking<TypeTrackingInput I> {
665701
666702 TypeBackTracker ( ) { this = MkTypeBackTracker ( hasReturn , content ) }
667703
668- /** Gets the summary resulting from prepending `step` to this type-tracking summary. */
669- private TypeBackTracker prepend ( StepSummary step ) { result = prepend ( this , step ) }
670-
671704 /** Gets a textual representation of this summary. */
672705 string toString ( ) {
673706 exists ( string withReturn , string withContent |
@@ -704,13 +737,9 @@ module TypeTracking<TypeTrackingInput I> {
704737 * Gets the summary that corresponds to having taken a backwards
705738 * heap and/or inter-procedural step from `nodeTo` to `nodeFrom`.
706739 */
707- bindingset [ nodeTo , this ]
740+ pragma [ inline ]
708741 TypeBackTracker step ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo ) {
709- exists ( StepSummary summary |
710- step ( _, pragma [ only_bind_out ] ( nodeTo ) , pragma [ only_bind_into ] ( summary ) ) and
711- result = pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( this ) ) .prepend ( summary ) and
712- step ( nodeFrom , pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( nodeTo ) ) , summary )
713- )
742+ result = backStepInlineLate ( this , nodeFrom , nodeTo )
714743 }
715744
716745 /**
@@ -737,13 +766,9 @@ module TypeTracking<TypeTrackingInput I> {
737766 * }
738767 * ```
739768 */
740- bindingset [ nodeTo , this ]
769+ pragma [ inline ]
741770 TypeBackTracker smallstep ( Node nodeFrom , Node nodeTo ) {
742- exists ( StepSummary summary |
743- smallStep ( _, pragma [ only_bind_out ] ( nodeTo ) , pragma [ only_bind_into ] ( summary ) ) and
744- result = pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( this ) ) .prepend ( summary ) and
745- smallStep ( nodeFrom , pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( nodeTo ) ) , summary )
746- )
771+ result = backSmallStepInlineLate ( this , nodeFrom , nodeTo )
747772 or
748773 simpleLocalSmallStep ( nodeFrom , nodeTo ) and
749774 result = this
0 commit comments