@@ -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 , false , 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 , false , 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 , false , value ) and
615
615
this .valueControlsEdge ( pred , succ , value )
616
616
)
617
617
}
@@ -737,26 +737,66 @@ private predicate compares_eq(
737
737
)
738
738
}
739
739
740
- /** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
741
- private predicate compares_eq (
742
- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
740
+ /**
741
+ * Holds if `op == k` is `areEqual` given that `test` is equal to `value`.
742
+ *
743
+ * Many internal predicates in this file have a `inNonZeroCase` column.
744
+ * Ideally, the `k` column would be a type such as `Option<int>::Option`, to
745
+ * represent whether we have a concrete value `k` such that `op == k`, or whether
746
+ * we only know that `op != 0`.
747
+ * However, cannot instantiate `Option` with an infinite type. Thus the boolean
748
+ * `inNonZeroCase` is used to distinquish the `Some` (where we have a concrete
749
+ * value `k`) and `None` cases (where we only know that `op != 0`).
750
+ *
751
+ * Thus, if `inNonZeroCase = true` then `op != 0` and the value of `k` is
752
+ * meaningless.
753
+ *
754
+ * To see why `inNonZeroCase` is needed consider the following C program:
755
+ * ```c
756
+ * char* p = ...;
757
+ * if(p) {
758
+ * use(p);
759
+ * }
760
+ * ```
761
+ * in C++ there would be an int-to-bool conversion on `p`. However, since C
762
+ * does not have booleans there is no conversion. We want to be able to
763
+ * conclude that `p` is non-zero in the true branch, so we need to give `k`
764
+ * some value. However, simply setting `k = 1` would make the rest of the
765
+ * analysis think that `k == 1` holds inside the branch. So we distinquish
766
+ * between the above case and
767
+ * ```c
768
+ * if(p == 1) {
769
+ * use(p)
770
+ * }
771
+ * ```
772
+ * by setting `inNonZeroCase` to `true` in the former case, but not in the
773
+ * latter.
774
+ */
775
+ private predicate unary_compares_eq (
776
+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
743
777
) {
744
778
/* 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 ) |
779
+ exists ( AbstractValue v | unary_simple_comparison_eq ( test , op , k , inNonZeroCase , v ) |
746
780
areEqual = true and value = v
747
781
or
748
782
areEqual = false and value = v .getDualValue ( )
749
783
)
750
784
or
751
- complex_eq ( test , op , k , areEqual , value )
785
+ unary_complex_eq ( test , op , k , areEqual , inNonZeroCase , value )
752
786
or
753
787
/* (x is true => (op == k)) => (!x is false => (op == k)) */
754
- exists ( AbstractValue dual | value = dual .getDualValue ( ) |
755
- compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , areEqual , dual )
788
+ exists ( AbstractValue dual , boolean inNonZeroCase0 |
789
+ value = dual .getDualValue ( ) and
790
+ unary_compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , inNonZeroCase0 , areEqual , dual )
791
+ |
792
+ k = 0 and inNonZeroCase = inNonZeroCase0
793
+ or
794
+ k != 0 and inNonZeroCase = true
756
795
)
757
796
or
758
797
// ((test is `areEqual` => op == const + k2) and const == `k1`) =>
759
798
// test is `areEqual` => op == k1 + k2
799
+ inNonZeroCase = false and
760
800
exists ( int k1 , int k2 , ConstantInstruction const |
761
801
compares_eq ( test , op , const .getAUse ( ) , k2 , areEqual , value ) and
762
802
int_value ( const ) = k1 and
@@ -781,35 +821,53 @@ private predicate simple_comparison_eq(
781
821
value .( BooleanValue ) .getValue ( ) = false
782
822
}
783
823
784
- /** Rearrange various simple comparisons into `op == k` form. */
785
- private predicate simple_comparison_eq ( Instruction test , Operand op , int k , AbstractValue value ) {
824
+ /**
825
+ * Holds if `test` is an instruction that is part of test that eventually is
826
+ * used in a conditional branch.
827
+ */
828
+ private predicate relevantUnaryComparison ( Instruction test ) {
829
+ not test instanceof CompareInstruction and
830
+ exists ( IRType type , ConditionalBranchInstruction branch |
831
+ type instanceof IRAddressType or type instanceof IRIntegerType
832
+ |
833
+ type = test .getResultIRType ( ) and
834
+ branch .getCondition ( ) = test
835
+ )
836
+ or
837
+ exists ( LogicalNotInstruction logicalNot |
838
+ relevantUnaryComparison ( logicalNot ) and
839
+ test = logicalNot .getUnary ( )
840
+ )
841
+ }
842
+
843
+ /**
844
+ * Rearrange various simple comparisons into `op == k` form.
845
+ */
846
+ private predicate unary_simple_comparison_eq (
847
+ Instruction test , Operand op , int k , boolean inNonZeroCase , AbstractValue value
848
+ ) {
786
849
exists ( SwitchInstruction switch , CaseEdge case |
787
850
test = switch .getExpression ( ) and
788
851
op .getDef ( ) = test and
789
852
case = value .( MatchValue ) .getCase ( ) and
790
853
exists ( switch .getSuccessor ( case ) ) and
791
- case .getValue ( ) .toInt ( ) = k
854
+ case .getValue ( ) .toInt ( ) = k and
855
+ inNonZeroCase = false
792
856
)
793
857
or
794
858
// There's no implicit CompareInstruction in files compiled as C since C
795
859
// doesn't have implicit boolean conversions. So instead we check whether
796
860
// there's a branch on a value of pointer or integer type.
797
- exists ( ConditionalBranchInstruction branch , IRType type |
798
- not test instanceof CompareInstruction and
799
- type = test .getResultIRType ( ) and
800
- ( type instanceof IRAddressType or type instanceof IRIntegerType ) and
801
- test = branch .getCondition ( ) and
802
- op .getDef ( ) = test
803
- |
804
- // We'd like to also include a case such as:
805
- // ```
806
- // k = 1 and
807
- // value.(BooleanValue).getValue() = true
808
- // ```
809
- // but all we know is that the value is non-zero in the true branch.
810
- // So we can only conclude something in the false branch.
861
+ relevantUnaryComparison ( test ) and
862
+ op .getDef ( ) = test and
863
+ (
864
+ k = 1 and
865
+ value .( BooleanValue ) .getValue ( ) = true and
866
+ inNonZeroCase = true
867
+ or
811
868
k = 0 and
812
- value .( BooleanValue ) .getValue ( ) = false
869
+ value .( BooleanValue ) .getValue ( ) = false and
870
+ inNonZeroCase = false
813
871
)
814
872
}
815
873
@@ -821,12 +879,12 @@ private predicate complex_eq(
821
879
add_eq ( cmp , left , right , k , areEqual , value )
822
880
}
823
881
824
- private predicate complex_eq (
825
- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
882
+ private predicate unary_complex_eq (
883
+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
826
884
) {
827
- sub_eq ( test , op , k , areEqual , value )
885
+ unary_sub_eq ( test , op , k , areEqual , inNonZeroCase , value )
828
886
or
829
- add_eq ( test , op , k , areEqual , value )
887
+ unary_add_eq ( test , op , k , areEqual , inNonZeroCase , value )
830
888
}
831
889
832
890
/*
@@ -1090,16 +1148,20 @@ private predicate sub_eq(
1090
1148
}
1091
1149
1092
1150
// op - x == c => op == (c+x)
1093
- private predicate sub_eq ( Instruction test , Operand op , int k , boolean areEqual , AbstractValue value ) {
1151
+ private predicate unary_sub_eq (
1152
+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
1153
+ ) {
1154
+ inNonZeroCase = false and
1094
1155
exists ( SubInstruction sub , int c , int x |
1095
- compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1156
+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1096
1157
op = sub .getLeftOperand ( ) and
1097
1158
x = int_value ( sub .getRight ( ) ) and
1098
1159
k = c + x
1099
1160
)
1100
1161
or
1162
+ inNonZeroCase = false and
1101
1163
exists ( PointerSubInstruction sub , int c , int x |
1102
- compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1164
+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1103
1165
op = sub .getLeftOperand ( ) and
1104
1166
x = int_value ( sub .getRight ( ) ) and
1105
1167
k = c + x
@@ -1153,11 +1215,13 @@ private predicate add_eq(
1153
1215
}
1154
1216
1155
1217
// left + x == right + c => left == right + (c-x)
1156
- private predicate add_eq (
1157
- Instruction test , Operand left , int k , boolean areEqual , AbstractValue value
1218
+ private predicate unary_add_eq (
1219
+ Instruction test , Operand left , int k , boolean areEqual , boolean inNonZeroCase ,
1220
+ AbstractValue value
1158
1221
) {
1222
+ inNonZeroCase = false and
1159
1223
exists ( AddInstruction lhs , int c , int x |
1160
- compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1224
+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1161
1225
(
1162
1226
left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
1163
1227
or
@@ -1166,8 +1230,9 @@ private predicate add_eq(
1166
1230
k = c - x
1167
1231
)
1168
1232
or
1233
+ inNonZeroCase = false and
1169
1234
exists ( PointerAddInstruction lhs , int c , int x |
1170
- compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1235
+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1171
1236
(
1172
1237
left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
1173
1238
or
0 commit comments