@@ -57,29 +57,46 @@ class StepSummary extends TStepSummary {
5757module StepSummary {
5858 /**
5959 * Gets the summary that corresponds to having taken a forwards
60- * heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
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.
6163 */
6264 cached
63- predicate step ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
64- exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstep ( mid , nodeTo , summary ) )
65+ private predicate stepNoCall ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
66+ exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstepNoCall ( mid , nodeTo , summary ) )
6567 }
6668
6769 /**
6870 * Gets the summary that corresponds to having taken a forwards
69- * local, heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
71+ * inter-procedural step from `nodeFrom` to `nodeTo`.
72+ */
73+ cached
74+ private predicate stepCall ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
75+ exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstepCall ( mid , nodeTo , summary ) )
76+ }
77+
78+ /**
79+ * Gets the summary that corresponds to having taken a forwards
80+ * heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
7081 *
71- * Unlike `StepSummary::step`, this predicate does not compress
72- * type-preserving steps.
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.
7387 */
74- predicate smallstep ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
88+ pragma [ inline]
89+ predicate step ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
90+ stepNoCall ( nodeFrom , nodeTo , summary )
91+ or
92+ stepCall ( nodeFrom , nodeTo , summary )
93+ }
94+
95+ pragma [ noinline]
96+ private predicate smallstepNoCall ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
7597 jumpStep ( nodeFrom , nodeTo ) and
7698 summary = LevelStep ( )
7799 or
78- callStep ( nodeFrom , nodeTo ) and summary = CallStep ( )
79- or
80- returnStep ( nodeFrom , nodeTo ) and
81- summary = ReturnStep ( )
82- or
83100 exists ( string content |
84101 localSourceStoreStep ( nodeFrom , nodeTo , content ) and
85102 summary = StoreStep ( content )
@@ -88,6 +105,28 @@ module StepSummary {
88105 )
89106 }
90107
108+ pragma [ noinline]
109+ private predicate smallstepCall ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
110+ callStep ( nodeFrom , nodeTo ) and summary = CallStep ( )
111+ or
112+ returnStep ( nodeFrom , nodeTo ) and
113+ summary = ReturnStep ( )
114+ }
115+
116+ /**
117+ * Gets the summary that corresponds to having taken a forwards
118+ * local, heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
119+ *
120+ * Unlike `StepSummary::step`, this predicate does not compress
121+ * type-preserving steps.
122+ */
123+ pragma [ inline]
124+ predicate smallstep ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
125+ smallstepNoCall ( nodeFrom , nodeTo , summary )
126+ or
127+ smallstepCall ( nodeFrom , nodeTo , summary )
128+ }
129+
91130 /**
92131 * Holds if `nodeFrom` is being written to the `content` content of the object in `nodeTo`.
93132 *
0 commit comments