Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,10 @@ module TypeTracking<LocationSig Location, TypeTrackingInput<Location> I> {

private class ContentOption = ContentOption::Option;

private predicate isLocalSourceNode(LocalSourceNode n) {
Copy link
Contributor

@aschackmull aschackmull Sep 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a small helper for standardFlowsTo. I think it should be moved down, so it appears directly before standardFlowsTo. Also, check whether the RA is affected by manually inlining this - if not, then that simplifies things. Gah, never mind, it's of course also input to the TC.

not nonStandardFlowsTo(_, _) and exists(n)
}

cached
private module Cached {
cached
Expand Down Expand Up @@ -249,21 +253,9 @@ module TypeTracking<LocationSig Location, TypeTrackingInput<Location> I> {
returnStep(nodeFrom, nodeTo) and summary = ReturnStep()
}

pragma[inline]
private predicate isLocalSourceNode(LocalSourceNode n) { any() }

cached
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't it better to cache simpleLocalSmallStepPlus, which will persist the underlying FastTC structure instead of the materialized relation? standardFlowsTo then needs to be non-cached and pragma[inline]ed. See also

predicate epsilonStar(ApiNode pred, ApiNode succ) = fastTC(epsilonEdge/2)(pred, succ)
for another example of this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Uh, that's a good idea. I didn't actually know that caching a fastTC didn't just cache the materialized relation. I've fixed this in bd7e20d

predicate standardFlowsTo(Node localSource, Node dst) {
not nonStandardFlowsTo(_, _) and
// explicit type check in base case to avoid repeated type tests in recursive case
isLocalSourceNode(localSource) and
dst = localSource
or
exists(Node mid |
standardFlowsTo(localSource, mid) and
simpleLocalSmallStep(mid, dst)
)
}
predicate simpleLocalSmallStepPlus(Node localSource, Node dst) =
sourceBoundedFastTC(simpleLocalSmallStep/2, isLocalSourceNode/1)(localSource, dst)

cached
predicate stepNoCall(LocalSourceNode nodeFrom, LocalSourceNode nodeTo, StepSummary summary) {
Expand All @@ -276,6 +268,14 @@ module TypeTracking<LocationSig Location, TypeTrackingInput<Location> I> {
}
}

pragma[inline]
private predicate standardFlowsTo(Node localSource, Node dst) {
isLocalSourceNode(localSource) and
dst = localSource
or
simpleLocalSmallStepPlus(localSource, dst)
}

import Cached

/**
Expand Down
Loading