@@ -55,11 +55,21 @@ class StepSummary extends TStepSummary {
55
55
56
56
/** Provides predicates for updating step summaries (`StepSummary`s). */
57
57
module StepSummary {
58
+ /**
59
+ * Gets the summary that corresponds to having taken a forwards
60
+ * heap and/or intra-procedural step from `nodeFrom` to `nodeTo`.
61
+ *
62
+ * Steps contained in this predicate should _not_ depend on the call graph.
63
+ */
58
64
cached
59
65
private predicate stepNoCall ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
60
66
exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstepNoCall ( mid , nodeTo , summary ) )
61
67
}
62
68
69
+ /**
70
+ * Gets the summary that corresponds to having taken a forwards
71
+ * inter-procedural step from `nodeFrom` to `nodeTo`.
72
+ */
63
73
cached
64
74
private predicate stepCall ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
65
75
exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstepCall ( mid , nodeTo , summary ) )
@@ -68,6 +78,12 @@ module StepSummary {
68
78
/**
69
79
* Gets the summary that corresponds to having taken a forwards
70
80
* heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
81
+ *
82
+ * This predicate is inlined, which enables better join-orders when
83
+ * the call graph construction and type tracking are mutually recursive.
84
+ * In such cases, non-linear recursion involving `step` will be limited
85
+ * to non-linear recursion for the parts of `step` that involve the
86
+ * call graph.
71
87
*/
72
88
pragma [ inline]
73
89
predicate step ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
0 commit comments