@@ -179,6 +179,59 @@ private predicate hasVariableReadWithCapturedWrite(
179
179
variableReadActualInOuterScope ( bb , v , scope )
180
180
}
181
181
182
+ pragma [ noinline]
183
+ private predicate adjacentDefRead (
184
+ Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2 ,
185
+ SsaInput:: SourceVariable v
186
+ ) {
187
+ adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
188
+ v = def .getSourceVariable ( )
189
+ }
190
+
191
+ private predicate adjacentDefReachesRead (
192
+ Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
193
+ ) {
194
+ exists ( SsaInput:: SourceVariable v | adjacentDefRead ( def , bb1 , i1 , bb2 , i2 , v ) |
195
+ def .definesAt ( v , bb1 , i1 )
196
+ or
197
+ SsaInput:: variableRead ( bb1 , i1 , v , true )
198
+ )
199
+ or
200
+ exists ( SsaInput:: BasicBlock bb3 , int i3 |
201
+ adjacentDefReachesRead ( def , bb1 , i1 , bb3 , i3 ) and
202
+ SsaInput:: variableRead ( bb3 , i3 , _, false ) and
203
+ adjacentDefRead ( def , bb3 , i3 , bb2 , i2 )
204
+ )
205
+ }
206
+
207
+ /** Same as `adjacentDefRead`, but skips uncertain reads. */
208
+ pragma [ nomagic]
209
+ private predicate adjacentDefSkipUncertainReads (
210
+ Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
211
+ ) {
212
+ adjacentDefReachesRead ( def , bb1 , i1 , bb2 , i2 ) and
213
+ SsaInput:: variableRead ( bb2 , i2 , _, true )
214
+ }
215
+
216
+ private predicate adjacentDefReachesUncertainRead (
217
+ Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
218
+ ) {
219
+ adjacentDefReachesRead ( def , bb1 , i1 , bb2 , i2 ) and
220
+ SsaInput:: variableRead ( bb2 , i2 , _, false )
221
+ }
222
+
223
+ /** Same as `lastRefRedef`, but skips uncertain reads. */
224
+ pragma [ nomagic]
225
+ private predicate lastRefSkipUncertainReads ( Definition def , SsaInput:: BasicBlock bb , int i ) {
226
+ lastRef ( def , bb , i ) and
227
+ not SsaInput:: variableRead ( bb , i , def .getSourceVariable ( ) , false )
228
+ or
229
+ exists ( SsaInput:: BasicBlock bb0 , int i0 |
230
+ lastRef ( def , bb0 , i0 ) and
231
+ adjacentDefReachesUncertainRead ( def , bb , i , bb0 , i0 )
232
+ )
233
+ }
234
+
182
235
cached
183
236
private module Cached {
184
237
/**
@@ -341,7 +394,7 @@ private module Cached {
341
394
predicate firstRead ( Definition def , VariableReadAccessCfgNode read ) {
342
395
exists ( Cfg:: BasicBlock bb1 , int i1 , Cfg:: BasicBlock bb2 , int i2 |
343
396
def .definesAt ( _, bb1 , i1 ) and
344
- adjacentDefNoUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
397
+ adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
345
398
read = bb2 .getNode ( i2 )
346
399
)
347
400
}
@@ -358,7 +411,7 @@ private module Cached {
358
411
exists ( Cfg:: BasicBlock bb1 , int i1 , Cfg:: BasicBlock bb2 , int i2 |
359
412
read1 = bb1 .getNode ( i1 ) and
360
413
variableReadActual ( bb1 , i1 , _) and
361
- adjacentDefNoUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
414
+ adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
362
415
read2 = bb2 .getNode ( i2 )
363
416
)
364
417
}
@@ -371,7 +424,7 @@ private module Cached {
371
424
cached
372
425
predicate lastRead ( Definition def , VariableReadAccessCfgNode read ) {
373
426
exists ( Cfg:: BasicBlock bb , int i |
374
- lastRefNoUncertainReads ( def , bb , i ) and
427
+ lastRefSkipUncertainReads ( def , bb , i ) and
375
428
variableReadActual ( bb , i , _) and
376
429
read = bb .getNode ( i )
377
430
)
@@ -386,7 +439,13 @@ private module Cached {
386
439
*/
387
440
cached
388
441
predicate lastRefBeforeRedef ( Definition def , Cfg:: BasicBlock bb , int i , Definition next ) {
389
- lastRefRedefNoUncertainReads ( def , bb , i , next )
442
+ lastRefRedef ( def , bb , i , next ) and
443
+ not SsaInput:: variableRead ( bb , i , def .getSourceVariable ( ) , false )
444
+ or
445
+ exists ( SsaInput:: BasicBlock bb0 , int i0 |
446
+ lastRefRedef ( def , bb0 , i0 , next ) and
447
+ adjacentDefReachesUncertainRead ( def , bb , i , bb0 , i0 )
448
+ )
390
449
}
391
450
392
451
cached
0 commit comments