@@ -188,13 +188,12 @@ signature module InputSig<LocationSig Location> {
188188 Expr getEqualChildExpr ( ) ;
189189 }
190190
191- class EqualityTest extends Expr {
192- /** Gets an operand of this expression. */
193- Expr getAnOperand ( ) ;
194-
195- /** Gets a boolean indicating whether this test is equality (true) or inequality (false). */
196- boolean polarity ( ) ;
197- }
191+ /**
192+ * Holds if `eqtest` is an equality or inequality test between `left` and
193+ * `right`. The `polarity` indicates whether this is an equality test (true)
194+ * or inequality test (false).
195+ */
196+ predicate equalityTest ( Expr eqtest , Expr left , Expr right , boolean polarity ) ;
198197
199198 class ConditionalExpr extends Expr {
200199 /** Gets the condition of this expression. */
@@ -351,12 +350,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
351350 c .nonMatchEdge ( bb1 , bb2 )
352351 }
353352
354- pragma [ nomagic]
355- private predicate eqtestHasOperands ( EqualityTest eqtest , Expr e1 , Expr e2 , boolean polarity ) {
356- eqtest .getAnOperand ( ) = e1 and
357- eqtest .getAnOperand ( ) = e2 and
358- e1 != e2 and
359- eqtest .polarity ( ) = polarity
353+ private predicate equalityTestSymmetric ( Expr eqtest , Expr e1 , Expr e2 , boolean eqval ) {
354+ equalityTest ( eqtest , e1 , e2 , eqval )
355+ or
356+ equalityTest ( eqtest , e2 , e1 , eqval )
360357 }
361358
362359 private predicate constcaseEquality ( PreGuard g , Expr e1 , ConstantExpr e2 ) {
@@ -424,7 +421,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
424421 * to `eqval`.
425422 */
426423 predicate isEquality ( Expr e1 , Expr e2 , boolean eqval ) {
427- eqtestHasOperands ( this , e1 , e2 , eqval )
424+ equalityTestSymmetric ( this , e1 , e2 , eqval )
428425 or
429426 constcaseEquality ( this , e1 , e2 ) and eqval = true
430427 or
@@ -466,7 +463,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
466463 )
467464 or
468465 exists ( NonNullExpr nonnull |
469- eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
466+ equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
470467 v2 .isNonNullValue ( )
471468 )
472469 or
@@ -589,7 +586,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
589586 private predicate guardChecksEqualVars (
590587 Guard guard , SsaDefinition v1 , SsaDefinition v2 , boolean branch
591588 ) {
592- eqtestHasOperands ( guard , v1 .getARead ( ) , v2 .getARead ( ) , branch )
589+ equalityTestSymmetric ( guard , v1 .getARead ( ) , v2 .getARead ( ) , branch )
593590 }
594591
595592 private predicate guardReadsSsaVar ( Guard guard , SsaDefinition def ) {
@@ -773,7 +770,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
773770 or
774771 exists ( Expr nonnull |
775772 exprHasValue ( nonnull , v2 ) and
776- eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
773+ equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
777774 v2 .isNonNullValue ( )
778775 )
779776 }
0 commit comments