@@ -57,29 +57,46 @@ class StepSummary extends TStepSummary {
57
57
module StepSummary {
58
58
/**
59
59
* 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.
61
63
*/
62
64
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 ) )
65
67
}
66
68
67
69
/**
68
70
* 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`.
70
81
*
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.
73
87
*/
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 ) {
75
97
jumpStep ( nodeFrom , nodeTo ) and
76
98
summary = LevelStep ( )
77
99
or
78
- callStep ( nodeFrom , nodeTo ) and summary = CallStep ( )
79
- or
80
- returnStep ( nodeFrom , nodeTo ) and
81
- summary = ReturnStep ( )
82
- or
83
100
exists ( string content |
84
101
localSourceStoreStep ( nodeFrom , nodeTo , content ) and
85
102
summary = StoreStep ( content )
@@ -88,6 +105,28 @@ module StepSummary {
88
105
)
89
106
}
90
107
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
+
91
130
/**
92
131
* Holds if `nodeFrom` is being written to the `content` content of the object in `nodeTo`.
93
132
*
0 commit comments