@@ -463,6 +463,21 @@ private predicate interestingCond(SsaSourceVariable npecand, ConditionBlock cond
463463 not cond .getCondition ( ) .( Expr ) .getAChildExpr * ( ) = npecand .getAnAccess ( )
464464}
465465
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+
466481/** A pair of correlated conditions for a given NPE candidate. */
467482private predicate correlatedConditions (
468483 SsaSourceVariable npecand , ConditionBlock cond1 , ConditionBlock cond2 , boolean inverted
@@ -485,25 +500,23 @@ private predicate correlatedConditions(
485500 inverted = branch1 .booleanXor ( branch2 )
486501 )
487502 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
495508 inverted = branch1 .booleanXor ( branch2 )
496509 )
497510 or
498511 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
501514 inverted = branch1 .booleanXor ( branch2 )
502515 )
503516 or
504517 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
507520 inverted = pol1 .booleanXor ( pol2 )
508521 )
509522 or
0 commit comments