@@ -30,16 +30,16 @@ predicate hasTupleCount(
30
30
float tupleCount
31
31
) {
32
32
inLayer = firstPredicate ( recursive ) and
33
- exists ( PipeLineRun run | run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) |
34
- ordering = run .getRAReference ( ) and
33
+ exists ( PipeLineRun run |
34
+ run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) and ordering = run .getRAReference ( )
35
+ |
35
36
tupleCount = run .getCount ( i )
36
- )
37
- or
38
- exists ( SummaryEvent inLayer0 , float tupleCount0 , PipeLineRun run |
39
- run = inLayer .getPipelineRuns ( ) .getRun ( pragma [ only_bind_into ] ( iteration ) ) and
40
- successor ( recursive , inLayer0 , inLayer ) and
41
- hasTupleCount ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i , tupleCount0 ) and
42
- tupleCount = run .getCount ( i ) + tupleCount0
37
+ or
38
+ exists ( SummaryEvent inLayer0 , float tupleCount0 |
39
+ successor ( recursive , inLayer0 , inLayer ) and
40
+ hasTupleCount ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i , tupleCount0 ) and
41
+ tupleCount = run .getCount ( i ) + tupleCount0
42
+ )
43
43
)
44
44
}
45
45
@@ -58,57 +58,51 @@ predicate hasDuplication(
58
58
ComputeRecursive recursive , string ordering , SummaryEvent inLayer , int iteration , int i ,
59
59
float duplication
60
60
) {
61
- inLayer = firstPredicate ( recursive ) and
62
- exists ( PipeLineRun run | run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) |
63
- ordering = run .getRAReference ( ) and
61
+ exists ( PipeLineRun run |
62
+ run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) and
63
+ ordering = run .getRAReference ( )
64
+ |
65
+ inLayer = firstPredicate ( recursive ) and
64
66
duplication = run .getDuplicationPercentage ( i )
65
- )
66
- or
67
- exists ( SummaryEvent inLayer0 , float duplication0 , PipeLineRun run |
68
- run = inLayer . getPipelineRuns ( ) . getRun ( pragma [ only_bind_into ] ( iteration ) ) and
69
- successor ( recursive , inLayer0 , inLayer ) and
70
- hasDuplication ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i , duplication0 ) and
71
- duplication = run . getDuplicationPercentage ( i ) . maximum ( duplication0 )
67
+ or
68
+ exists ( SummaryEvent inLayer0 , float duplication0 |
69
+ successor ( recursive , inLayer0 , inLayer ) and
70
+ hasDuplication ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i ,
71
+ duplication0 ) and
72
+ duplication = run . getDuplicationPercentage ( i ) . maximum ( duplication0 )
73
+ )
72
74
)
73
75
}
74
76
75
77
predicate hasDuplication ( ComputeRecursive recursive , string ordering , int i , float duplication ) {
76
78
duplication =
77
- max ( SummaryEvent inLayer , int iteration , int dup |
78
- inLayer = getInLayerOrRecursive ( recursive ) and
79
- hasDuplication ( recursive , ordering , inLayer , iteration , i , dup )
80
- |
81
- dup
82
- )
79
+ max ( int iteration , int dup | hasDuplication ( recursive , ordering , _, iteration , i , dup ) | dup )
83
80
}
84
81
85
82
/**
86
83
* Holds if the ordering `ordering` has `resultSize` resultSize in the `iteration`'th iteration.
87
- *
88
- * For example, the "base" ordering in iteration 0 has size 42.
89
84
*/
90
85
private predicate hasResultSize (
91
86
ComputeRecursive recursive , string ordering , SummaryEvent inLayer , int iteration , float resultSize
92
87
) {
93
- inLayer = firstPredicate ( recursive ) and
94
- ordering = inLayer .getPipelineRuns ( ) .getRun ( iteration ) .getRAReference ( ) and
95
- resultSize = inLayer .getDeltaSize ( iteration )
96
- or
97
- exists ( SummaryEvent inLayer0 , int resultSize0 |
98
- successor ( recursive , inLayer0 , inLayer ) and
99
- hasResultSize ( recursive , ordering , inLayer0 , iteration , resultSize0 ) and
100
- resultSize = inLayer .getDeltaSize ( iteration ) + resultSize0
88
+ exists ( PipeLineRun run |
89
+ run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) and
90
+ ordering = run .getRAReference ( )
91
+ |
92
+ inLayer = firstPredicate ( recursive ) and
93
+ resultSize = inLayer .getDeltaSize ( iteration )
94
+ or
95
+ exists ( SummaryEvent inLayer0 , int resultSize0 |
96
+ successor ( recursive , inLayer0 , inLayer ) and
97
+ hasResultSize ( recursive , ordering , inLayer0 , iteration , resultSize0 ) and
98
+ resultSize = inLayer .getDeltaSize ( iteration ) + resultSize0
99
+ )
101
100
)
102
101
}
103
102
104
103
predicate hasResultSize ( ComputeRecursive recursive , string ordering , float resultSize ) {
105
104
resultSize =
106
- strictsum ( InLayer inLayer , int iteration , float r |
107
- inLayer .getComputeRecursiveEvent ( ) = recursive and
108
- hasResultSize ( recursive , ordering , inLayer , iteration , r )
109
- |
110
- r
111
- )
105
+ strictsum ( int iteration , float r | hasResultSize ( recursive , ordering , _, iteration , r ) | r )
112
106
}
113
107
114
108
RAParser< PipeLine > :: RAExpr getAnRaOperation ( SummaryEvent inLayer , string ordering ) {
@@ -122,17 +116,20 @@ SummaryEvent getInLayerEventWithName(ComputeRecursive recursive, string predicat
122
116
123
117
bindingset [ predicateName, iteration]
124
118
int getSize ( ComputeRecursive recursive , string predicateName , int iteration , TDeltaKind kind ) {
125
- exists ( int i |
119
+ exists ( int i , SummaryEvent event |
126
120
kind = TPrevious ( ) and
127
121
i = iteration - 1
128
122
or
129
123
kind = TCurrent ( ) and
130
124
i = iteration
131
125
|
132
- result = getInLayerEventWithName ( recursive , predicateName ) .getDeltaSize ( i )
133
- or
134
- not exists ( getInLayerEventWithName ( recursive , predicateName ) .getDeltaSize ( i ) ) and
135
- result = 0
126
+ event = getInLayerEventWithName ( recursive , predicateName ) and
127
+ (
128
+ result = event .getDeltaSize ( i )
129
+ or
130
+ not exists ( event .getDeltaSize ( i ) ) and
131
+ result = 0
132
+ )
136
133
)
137
134
}
138
135
@@ -154,36 +151,53 @@ private predicate isDelta(string predicateName, TDeltaKind kind, string withoutS
154
151
withoutSuffix = predicateName .regexpCapture ( "(.+)#cur_delta" , 1 )
155
152
}
156
153
154
+ bindingset [ iteration]
155
+ float getRecursiveDependencySize (
156
+ ComputeRecursive recursive , string predicateName , int iteration , SummaryEvent inLayer ,
157
+ string ordering , TDeltaKind kind
158
+ ) {
159
+ result = getSize ( recursive , predicateName , iteration , kind ) and
160
+ isDelta ( getAnRaOperation ( inLayer , ordering ) .getARhsPredicate ( ) , kind , predicateName )
161
+ }
162
+
163
+ bindingset [ ordering, iteration]
164
+ predicate hasDependentPredicateSizeImpl (
165
+ ComputeRecursive recursive , string ordering , float size , string predicateName , int iteration ,
166
+ SummaryEvent inLayer
167
+ ) {
168
+ // We treat the base case as a non-recursive case
169
+ if ordering = "base"
170
+ then
171
+ size =
172
+ [
173
+ getDependencyWithName ( recursive .getDependencies ( ) , predicateName ) .getResultSize ( ) ,
174
+ getRecursiveDependencySize ( recursive , predicateName , iteration , inLayer , ordering ,
175
+ TCurrent ( ) )
176
+ ]
177
+ else
178
+ size =
179
+ getRecursiveDependencySize ( recursive , predicateName , iteration , inLayer , ordering , TPrevious ( ) )
180
+ }
181
+
182
+ pragma [ nomagic]
157
183
predicate hasDependentPredicateSize (
158
184
ComputeRecursive recursive , string ordering , SummaryEvent inLayer , int iteration ,
159
185
string predicateName , float size
160
186
) {
161
- exists ( |
162
- inLayer = firstPredicate ( recursive ) and
163
- ordering = inLayer .getPipelineRuns ( ) .getRun ( iteration ) .getRAReference ( )
164
- |
165
- // We treat iteration 0 as a non-recursive case
166
- if ordering = "base"
167
- then size = getDependencyWithName ( recursive .getDependencies ( ) , predicateName ) .getResultSize ( )
168
- else
169
- exists ( TDeltaKind kind |
170
- size = getSize ( recursive , predicateName , iteration , kind ) and
171
- isDelta ( getAnRaOperation ( inLayer , ordering ) .getARhsPredicate ( ) , kind , predicateName )
172
- )
173
- )
174
- or
175
- exists ( SummaryEvent inLayer0 , float size0 |
176
- successor ( recursive , inLayer0 , inLayer ) and
177
- hasDependentPredicateSize ( recursive , ordering , inLayer0 , iteration , predicateName , size0 )
187
+ exists ( PipeLineRun run |
188
+ run = inLayer .getPipelineRuns ( ) .getRun ( pragma [ only_bind_into ] ( iteration ) ) and
189
+ ordering = run .getRAReference ( )
178
190
|
179
- // We treat iteration 0 as a non-recursive case
180
- if ordering = "base"
181
- then size = getDependencyWithName ( recursive .getDependencies ( ) , predicateName ) .getResultSize ( )
182
- else
183
- exists ( TDeltaKind kind |
184
- size = getSize ( recursive , predicateName , iteration , kind ) + size0 and
185
- isDelta ( getAnRaOperation ( inLayer , ordering ) .getARhsPredicate ( ) , kind , predicateName )
186
- )
191
+ inLayer = firstPredicate ( recursive ) and
192
+ hasDependentPredicateSizeImpl ( recursive , ordering , size , predicateName , iteration , inLayer )
193
+ or
194
+ exists ( SummaryEvent inLayer0 , float size0 , float size1 |
195
+ successor ( recursive , inLayer0 , inLayer ) and
196
+ hasDependentPredicateSize ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) ,
197
+ predicateName , size0 ) and
198
+ hasDependentPredicateSizeImpl ( recursive , ordering , size1 , predicateName , iteration , inLayer ) and
199
+ size = size0 + size1
200
+ )
187
201
)
188
202
}
189
203
@@ -195,9 +209,8 @@ predicate hasDependentPredicateSize(
195
209
ComputeRecursive recursive , string ordering , string predicateName , float size
196
210
) {
197
211
size =
198
- strictsum ( SummaryEvent inLayer , int iteration , int s |
199
- inLayer = getInLayerOrRecursive ( recursive ) and
200
- hasDependentPredicateSize ( recursive , ordering , inLayer , iteration , predicateName , s )
212
+ strictsum ( int iteration , float s |
213
+ hasDependentPredicateSize ( recursive , ordering , _, iteration , predicateName , s )
201
214
|
202
215
s
203
216
)
0 commit comments