@@ -55,31 +55,32 @@ class StepSummary extends TStepSummary {
55
55
56
56
/** Provides predicates for updating step summaries (`StepSummary`s). */
57
57
module 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
+
58
68
/**
59
69
* Gets the summary that corresponds to having taken a forwards
60
70
* heap and/or inter-procedural step from `nodeFrom` to `nodeTo`.
61
71
*/
62
- cached
72
+ pragma [ inline ]
63
73
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 )
65
77
}
66
78
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 ) {
75
81
jumpStep ( nodeFrom , nodeTo ) and
76
82
summary = LevelStep ( )
77
83
or
78
- callStep ( nodeFrom , nodeTo ) and summary = CallStep ( )
79
- or
80
- returnStep ( nodeFrom , nodeTo ) and
81
- summary = ReturnStep ( )
82
- or
83
84
exists ( string content |
84
85
localSourceStoreStep ( nodeFrom , nodeTo , content ) and
85
86
summary = StoreStep ( content )
@@ -88,6 +89,28 @@ module StepSummary {
88
89
)
89
90
}
90
91
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
+
91
114
/**
92
115
* Holds if `nodeFrom` is being written to the `content` content of the object in `nodeTo`.
93
116
*
0 commit comments