@@ -120,14 +120,6 @@ module ExposedForTestingOnly {
120
120
predicate phiHasInputFromBlockExt = Impl:: phiHasInputFromBlockExt / 3 ;
121
121
}
122
122
123
- pragma [ noinline]
124
- private predicate adjacentDefRead (
125
- Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SsaInput:: SourceVariable v
126
- ) {
127
- Impl:: adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
128
- v = def .getSourceVariable ( )
129
- }
130
-
131
123
/** Holds if `v` is read at index `i` in basic block `bb`. */
132
124
private predicate variableReadActual ( BasicBlock bb , int i , Variable v ) {
133
125
exists ( VariableAccess read |
@@ -167,31 +159,6 @@ private predicate hasVariableReadWithCapturedWrite(
167
159
variableReadActualInOuterScope ( bb , i , v , scope )
168
160
}
169
161
170
- private predicate adjacentDefReachesRead (
171
- Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
172
- ) {
173
- exists ( SsaInput:: SourceVariable v | adjacentDefRead ( def , bb1 , i1 , bb2 , i2 , v ) |
174
- def .definesAt ( v , bb1 , i1 )
175
- or
176
- SsaInput:: variableRead ( bb1 , i1 , v , true )
177
- )
178
- or
179
- exists ( BasicBlock bb3 , int i3 |
180
- adjacentDefReachesRead ( def , bb1 , i1 , bb3 , i3 ) and
181
- SsaInput:: variableRead ( bb3 , i3 , _, false ) and
182
- Impl:: adjacentDefRead ( def , bb3 , i3 , bb2 , i2 )
183
- )
184
- }
185
-
186
- /** Same as `adjacentDefRead`, but skips uncertain reads. */
187
- pragma [ nomagic]
188
- private predicate adjacentDefSkipUncertainReads (
189
- Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
190
- ) {
191
- adjacentDefReachesRead ( def , bb1 , i1 , bb2 , i2 ) and
192
- SsaInput:: variableRead ( bb2 , i2 , _, true )
193
- }
194
-
195
162
private VariableAccess getACapturedVariableAccess ( BasicBlock bb , Variable v ) {
196
163
result = bb .getANode ( ) .getAstNode ( ) and
197
164
result .isCapture ( ) and
@@ -314,11 +281,7 @@ private module Cached {
314
281
*/
315
282
cached
316
283
predicate firstRead ( Definition def , CfgNode read ) {
317
- exists ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
318
- def .definesAt ( _, bb1 , i1 ) and
319
- adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
320
- read = bb2 .getNode ( i2 )
321
- )
284
+ exists ( BasicBlock bb , int i | Impl:: firstUse ( def , bb , i , true ) and read = bb .getNode ( i ) )
322
285
}
323
286
324
287
/**
@@ -328,10 +291,10 @@ private module Cached {
328
291
*/
329
292
cached
330
293
predicate adjacentReadPair ( Definition def , CfgNode read1 , CfgNode read2 ) {
331
- exists ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
294
+ exists ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , Variable v |
295
+ Impl:: ssaDefReachesRead ( v , def , bb1 , i1 ) and
296
+ Impl:: adjacentUseUse ( bb1 , i1 , bb2 , i2 , v , true ) and
332
297
read1 = bb1 .getNode ( i1 ) and
333
- variableReadActual ( bb1 , i1 , def .getSourceVariable ( ) ) and
334
- adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
335
298
read2 = bb2 .getNode ( i2 )
336
299
)
337
300
}
0 commit comments