@@ -188,13 +188,12 @@ signature module InputSig<LocationSig Location> {
188
188
Expr getEqualChildExpr ( ) ;
189
189
}
190
190
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 ) ;
198
197
199
198
class ConditionalExpr extends Expr {
200
199
/** Gets the condition of this expression. */
@@ -351,12 +350,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
351
350
c .nonMatchEdge ( bb1 , bb2 )
352
351
}
353
352
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 )
360
357
}
361
358
362
359
private predicate constcaseEquality ( PreGuard g , Expr e1 , ConstantExpr e2 ) {
@@ -424,7 +421,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
424
421
* to `eqval`.
425
422
*/
426
423
predicate isEquality ( Expr e1 , Expr e2 , boolean eqval ) {
427
- eqtestHasOperands ( this , e1 , e2 , eqval )
424
+ equalityTestSymmetric ( this , e1 , e2 , eqval )
428
425
or
429
426
constcaseEquality ( this , e1 , e2 ) and eqval = true
430
427
or
@@ -466,7 +463,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
466
463
)
467
464
or
468
465
exists ( NonNullExpr nonnull |
469
- eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
466
+ equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
470
467
v2 .isNonNullValue ( )
471
468
)
472
469
or
@@ -589,7 +586,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
589
586
private predicate guardChecksEqualVars (
590
587
Guard guard , SsaDefinition v1 , SsaDefinition v2 , boolean branch
591
588
) {
592
- eqtestHasOperands ( guard , v1 .getARead ( ) , v2 .getARead ( ) , branch )
589
+ equalityTestSymmetric ( guard , v1 .getARead ( ) , v2 .getARead ( ) , branch )
593
590
}
594
591
595
592
private predicate guardReadsSsaVar ( Guard guard , SsaDefinition def ) {
@@ -773,7 +770,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
773
770
or
774
771
exists ( Expr nonnull |
775
772
exprHasValue ( nonnull , v2 ) and
776
- eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
773
+ equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
777
774
v2 .isNonNullValue ( )
778
775
)
779
776
}
0 commit comments