@@ -463,6 +463,21 @@ private predicate interestingCond(SsaSourceVariable npecand, ConditionBlock cond
463
463
not cond .getCondition ( ) .( Expr ) .getAChildExpr * ( ) = npecand .getAnAccess ( )
464
464
}
465
465
466
+ pragma [ nomagic]
467
+ private ConditionBlock ssaIntegerGuard ( SsaVariable v , boolean branch , int k , boolean is_k ) {
468
+ result .getCondition ( ) = integerGuard ( v .getAUse ( ) , branch , k , is_k )
469
+ }
470
+
471
+ pragma [ nomagic]
472
+ private ConditionBlock ssaIntBoundGuard ( SsaVariable v , boolean branch_with_lower_bound_k , int k ) {
473
+ result .getCondition ( ) = intBoundGuard ( v .getAUse ( ) , branch_with_lower_bound_k , k )
474
+ }
475
+
476
+ pragma [ nomagic]
477
+ private ConditionBlock ssaEnumConstEquality ( SsaVariable v , boolean polarity , EnumConstant c ) {
478
+ result .getCondition ( ) = enumConstEquality ( v .getAUse ( ) , polarity , c )
479
+ }
480
+
466
481
/** A pair of correlated conditions for a given NPE candidate. */
467
482
private predicate correlatedConditions (
468
483
SsaSourceVariable npecand , ConditionBlock cond1 , ConditionBlock cond2 , boolean inverted
@@ -485,25 +500,23 @@ private predicate correlatedConditions(
485
500
inverted = branch1 .booleanXor ( branch2 )
486
501
)
487
502
or
488
- exists ( SsaVariable v , VarRead rv1 , VarRead rv2 , int k , boolean branch1 , boolean branch2 |
489
- rv1 = v .getAUse ( ) and
490
- rv2 = v .getAUse ( ) and
491
- cond1 .getCondition ( ) = integerGuard ( rv1 , branch1 , k , true ) and
492
- cond1 .getCondition ( ) = integerGuard ( rv1 , branch1 .booleanNot ( ) , k , false ) and
493
- cond2 .getCondition ( ) = integerGuard ( rv2 , branch2 , k , true ) and
494
- cond2 .getCondition ( ) = integerGuard ( rv2 , branch2 .booleanNot ( ) , k , false ) and
503
+ exists ( SsaVariable v , int k , boolean branch1 , boolean branch2 |
504
+ cond1 = ssaIntegerGuard ( v , branch1 , k , true ) and
505
+ cond1 = ssaIntegerGuard ( v , branch1 .booleanNot ( ) , k , false ) and
506
+ cond2 = ssaIntegerGuard ( v , branch2 , k , true ) and
507
+ cond2 = ssaIntegerGuard ( v , branch2 .booleanNot ( ) , k , false ) and
495
508
inverted = branch1 .booleanXor ( branch2 )
496
509
)
497
510
or
498
511
exists ( SsaVariable v , int k , boolean branch1 , boolean branch2 |
499
- cond1 . getCondition ( ) = intBoundGuard ( v . getAUse ( ) , branch1 , k ) and
500
- cond2 . getCondition ( ) = intBoundGuard ( v . getAUse ( ) , branch2 , k ) and
512
+ cond1 = ssaIntBoundGuard ( v , branch1 , k ) and
513
+ cond2 = ssaIntBoundGuard ( v , branch2 , k ) and
501
514
inverted = branch1 .booleanXor ( branch2 )
502
515
)
503
516
or
504
517
exists ( SsaVariable v , EnumConstant c , boolean pol1 , boolean pol2 |
505
- cond1 . getCondition ( ) = enumConstEquality ( v . getAUse ( ) , pol1 , c ) and
506
- cond2 . getCondition ( ) = enumConstEquality ( v . getAUse ( ) , pol2 , c ) and
518
+ cond1 = ssaEnumConstEquality ( v , pol1 , c ) and
519
+ cond2 = ssaEnumConstEquality ( v , pol2 , c ) and
507
520
inverted = pol1 .booleanXor ( pol2 )
508
521
)
509
522
or
0 commit comments