@@ -55,31 +55,32 @@ class StepSummary extends TStepSummary {
5555
5656/** Provides predicates for updating step summaries (`StepSummary`s). */
5757module StepSummary {
58+ cached
59+ private predicate stepNoCall ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
60+ exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstepNoCall ( mid , nodeTo , summary ) )
61+ }
62+
63+ cached
64+ private predicate stepCall ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
65+ exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstepCall ( mid , nodeTo , summary ) )
66+ }
67+
5868 /**
5969 * Gets the summary that corresponds to having taken a forwards
6070 * heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
6171 */
62- cached
72+ pragma [ inline ]
6373 predicate step ( LocalSourceNode nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
64- exists ( Node mid | nodeFrom .flowsTo ( mid ) and smallstep ( mid , nodeTo , summary ) )
74+ stepNoCall ( nodeFrom , nodeTo , summary )
75+ or
76+ stepCall ( nodeFrom , nodeTo , summary )
6577 }
6678
67- /**
68- * Gets the summary that corresponds to having taken a forwards
69- * local, heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
70- *
71- * Unlike `StepSummary::step`, this predicate does not compress
72- * type-preserving steps.
73- */
74- predicate smallstep ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
79+ pragma [ noinline]
80+ private predicate smallstepNoCall ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
7581 jumpStep ( nodeFrom , nodeTo ) and
7682 summary = LevelStep ( )
7783 or
78- callStep ( nodeFrom , nodeTo ) and summary = CallStep ( )
79- or
80- returnStep ( nodeFrom , nodeTo ) and
81- summary = ReturnStep ( )
82- or
8384 exists ( string content |
8485 localSourceStoreStep ( nodeFrom , nodeTo , content ) and
8586 summary = StoreStep ( content )
@@ -88,6 +89,28 @@ module StepSummary {
8889 )
8990 }
9091
92+ pragma [ noinline]
93+ private predicate smallstepCall ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
94+ callStep ( nodeFrom , nodeTo ) and summary = CallStep ( )
95+ or
96+ returnStep ( nodeFrom , nodeTo ) and
97+ summary = ReturnStep ( )
98+ }
99+
100+ /**
101+ * Gets the summary that corresponds to having taken a forwards
102+ * local, heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
103+ *
104+ * Unlike `StepSummary::step`, this predicate does not compress
105+ * type-preserving steps.
106+ */
107+ pragma [ inline]
108+ predicate smallstep ( Node nodeFrom , LocalSourceNode nodeTo , StepSummary summary ) {
109+ smallstepNoCall ( nodeFrom , nodeTo , summary )
110+ or
111+ smallstepCall ( nodeFrom , nodeTo , summary )
112+ }
113+
91114 /**
92115 * Holds if `nodeFrom` is being written to the `content` content of the object in `nodeTo`.
93116 *
0 commit comments