Skip to content

Commit f004fcf

Browse files
authored
Merge pull request github#13388 from hvitved/type-back-tracking-inline-late
Type tracking: Use `noopt`+`inline_late` in `TypeBackTracker::[small]step`
2 parents dcd254a + 322b254 commit f004fcf

File tree

1 file changed

+40
-15
lines changed

1 file changed

+40
-15
lines changed

shared/typetracking/codeql/typetracking/TypeTracking.qll

Lines changed: 40 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -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

Comments
 (0)