@@ -179,6 +179,59 @@ private predicate hasVariableReadWithCapturedWrite(
179179 variableReadActualInOuterScope ( bb , v , scope )
180180}
181181
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+
182235cached
183236private module Cached {
184237 /**
@@ -341,7 +394,7 @@ private module Cached {
341394 predicate firstRead ( Definition def , VariableReadAccessCfgNode read ) {
342395 exists ( Cfg:: BasicBlock bb1 , int i1 , Cfg:: BasicBlock bb2 , int i2 |
343396 def .definesAt ( _, bb1 , i1 ) and
344- adjacentDefNoUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
397+ adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
345398 read = bb2 .getNode ( i2 )
346399 )
347400 }
@@ -358,7 +411,7 @@ private module Cached {
358411 exists ( Cfg:: BasicBlock bb1 , int i1 , Cfg:: BasicBlock bb2 , int i2 |
359412 read1 = bb1 .getNode ( i1 ) and
360413 variableReadActual ( bb1 , i1 , _) and
361- adjacentDefNoUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
414+ adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
362415 read2 = bb2 .getNode ( i2 )
363416 )
364417 }
@@ -371,7 +424,7 @@ private module Cached {
371424 cached
372425 predicate lastRead ( Definition def , VariableReadAccessCfgNode read ) {
373426 exists ( Cfg:: BasicBlock bb , int i |
374- lastRefNoUncertainReads ( def , bb , i ) and
427+ lastRefSkipUncertainReads ( def , bb , i ) and
375428 variableReadActual ( bb , i , _) and
376429 read = bb .getNode ( i )
377430 )
@@ -386,7 +439,13 @@ private module Cached {
386439 */
387440 cached
388441 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+ )
390449 }
391450
392451 cached
0 commit comments