@@ -565,7 +565,7 @@ class IRGuardCondition extends Instruction {
565
565
/** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
566
566
cached
567
567
predicate comparesEq ( Operand op , int k , boolean areEqual , AbstractValue value ) {
568
- compares_eq ( this , op , k , areEqual , value )
568
+ unary_compares_eq ( this , op , k , areEqual , value )
569
569
}
570
570
571
571
/**
@@ -586,7 +586,7 @@ class IRGuardCondition extends Instruction {
586
586
cached
587
587
predicate ensuresEq ( Operand op , int k , IRBlock block , boolean areEqual ) {
588
588
exists ( AbstractValue value |
589
- compares_eq ( this , op , k , areEqual , value ) and this .valueControls ( block , value )
589
+ unary_compares_eq ( this , op , k , areEqual , value ) and this .valueControls ( block , value )
590
590
)
591
591
}
592
592
@@ -611,7 +611,7 @@ class IRGuardCondition extends Instruction {
611
611
cached
612
612
predicate ensuresEqEdge ( Operand op , int k , IRBlock pred , IRBlock succ , boolean areEqual ) {
613
613
exists ( AbstractValue value |
614
- compares_eq ( this , op , k , areEqual , value ) and
614
+ unary_compares_eq ( this , op , k , areEqual , value ) and
615
615
this .valueControlsEdge ( pred , succ , value )
616
616
)
617
617
}
@@ -738,21 +738,21 @@ private predicate compares_eq(
738
738
}
739
739
740
740
/** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
741
- private predicate compares_eq (
741
+ private predicate unary_compares_eq (
742
742
Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
743
743
) {
744
744
/* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
745
- exists ( AbstractValue v | simple_comparison_eq ( test , op , k , v ) |
745
+ exists ( AbstractValue v | unary_simple_comparison_eq ( test , op , k , v ) |
746
746
areEqual = true and value = v
747
747
or
748
748
areEqual = false and value = v .getDualValue ( )
749
749
)
750
750
or
751
- complex_eq ( test , op , k , areEqual , value )
751
+ unary_complex_eq ( test , op , k , areEqual , value )
752
752
or
753
753
/* (x is true => (op == k)) => (!x is false => (op == k)) */
754
754
exists ( AbstractValue dual | value = dual .getDualValue ( ) |
755
- compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , areEqual , dual )
755
+ unary_compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , areEqual , dual )
756
756
)
757
757
or
758
758
// ((test is `areEqual` => op == const + k2) and const == `k1`) =>
@@ -782,7 +782,9 @@ private predicate simple_comparison_eq(
782
782
}
783
783
784
784
/** Rearrange various simple comparisons into `op == k` form. */
785
- private predicate simple_comparison_eq ( Instruction test , Operand op , int k , AbstractValue value ) {
785
+ private predicate unary_simple_comparison_eq (
786
+ Instruction test , Operand op , int k , AbstractValue value
787
+ ) {
786
788
exists ( SwitchInstruction switch , CaseEdge case |
787
789
test = switch .getExpression ( ) and
788
790
op .getDef ( ) = test and
@@ -821,12 +823,12 @@ private predicate complex_eq(
821
823
add_eq ( cmp , left , right , k , areEqual , value )
822
824
}
823
825
824
- private predicate complex_eq (
826
+ private predicate unary_complex_eq (
825
827
Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
826
828
) {
827
- sub_eq ( test , op , k , areEqual , value )
829
+ unary_sub_eq ( test , op , k , areEqual , value )
828
830
or
829
- add_eq ( test , op , k , areEqual , value )
831
+ unary_add_eq ( test , op , k , areEqual , value )
830
832
}
831
833
832
834
/*
@@ -1090,16 +1092,18 @@ private predicate sub_eq(
1090
1092
}
1091
1093
1092
1094
// op - x == c => op == (c+x)
1093
- private predicate sub_eq ( Instruction test , Operand op , int k , boolean areEqual , AbstractValue value ) {
1095
+ private predicate unary_sub_eq (
1096
+ Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
1097
+ ) {
1094
1098
exists ( SubInstruction sub , int c , int x |
1095
- compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1099
+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1096
1100
op = sub .getLeftOperand ( ) and
1097
1101
x = int_value ( sub .getRight ( ) ) and
1098
1102
k = c + x
1099
1103
)
1100
1104
or
1101
1105
exists ( PointerSubInstruction sub , int c , int x |
1102
- compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1106
+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1103
1107
op = sub .getLeftOperand ( ) and
1104
1108
x = int_value ( sub .getRight ( ) ) and
1105
1109
k = c + x
@@ -1153,11 +1157,12 @@ private predicate add_eq(
1153
1157
}
1154
1158
1155
1159
// left + x == right + c => left == right + (c-x)
1156
- private predicate add_eq (
1157
- Instruction test , Operand left , int k , boolean areEqual , AbstractValue value
1160
+ private predicate unary_add_eq (
1161
+ Instruction test , Operand left , int k , boolean areEqual ,
1162
+ AbstractValue value
1158
1163
) {
1159
1164
exists ( AddInstruction lhs , int c , int x |
1160
- compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1165
+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1161
1166
(
1162
1167
left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
1163
1168
or
@@ -1167,7 +1172,8 @@ private predicate add_eq(
1167
1172
)
1168
1173
or
1169
1174
exists ( PointerAddInstruction lhs , int c , int x |
1170
- compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1175
+
1176
+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1171
1177
(
1172
1178
left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
1173
1179
or
0 commit comments