Shared: Cache the sourceBoundedFastTC structure instead of the resulting materialized relation.

This commit is contained in:
Mathias Vorreiter Pedersen
2025-09-08 13:37:48 +01:00
parent fd7d216fe3
commit 3aee4a88aa

View File

@@ -70,6 +70,10 @@ module TypeTracking<LocationSig Location, TypeTrackingInput<Location> I> {
private class ContentOption = ContentOption::Option;
private predicate isLocalSourceNode(LocalSourceNode n) {
not nonStandardFlowsTo(_, _) and exists(n)
}
cached
private module Cached {
cached
@@ -249,21 +253,9 @@ module TypeTracking<LocationSig Location, TypeTrackingInput<Location> I> {
returnStep(nodeFrom, nodeTo) and summary = ReturnStep()
}
private predicate isLocalSourceNode(LocalSourceNode n) {
not nonStandardFlowsTo(_, _) and exists(n)
}
private predicate simpleLocalSmallStepPlus(Node localSource, Node dst) =
sourceBoundedFastTC(simpleLocalSmallStep/2, isLocalSourceNode/1)(localSource, dst)
cached
predicate standardFlowsTo(Node localSource, Node dst) {
// explicit type check in base case to avoid repeated type tests in recursive case
isLocalSourceNode(localSource) and
dst = localSource
or
simpleLocalSmallStepPlus(localSource, dst)
}
predicate simpleLocalSmallStepPlus(Node localSource, Node dst) =
sourceBoundedFastTC(simpleLocalSmallStep/2, isLocalSourceNode/1)(localSource, dst)
cached
predicate stepNoCall(LocalSourceNode nodeFrom, LocalSourceNode nodeTo, StepSummary summary) {
@@ -276,6 +268,15 @@ module TypeTracking<LocationSig Location, TypeTrackingInput<Location> I> {
}
}
pragma[inline]
predicate standardFlowsTo(Node localSource, Node dst) {
// explicit type check in base case to avoid repeated type tests in recursive case
isLocalSourceNode(localSource) and
dst = localSource
or
simpleLocalSmallStepPlus(localSource, dst)
}
import Cached
/**