@@ -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
- unary_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
- unary_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
- unary_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`. */
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
+ */
741
775
private predicate unary_compares_eq (
742
- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
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 | unary_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
- unary_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
- unary_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,37 +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. */
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
+ */
785
846
private predicate unary_simple_comparison_eq (
786
- Instruction test , Operand op , int k , AbstractValue value
847
+ Instruction test , Operand op , int k , boolean inNonZeroCase , AbstractValue value
787
848
) {
788
849
exists ( SwitchInstruction switch , CaseEdge case |
789
850
test = switch .getExpression ( ) and
790
851
op .getDef ( ) = test and
791
852
case = value .( MatchValue ) .getCase ( ) and
792
853
exists ( switch .getSuccessor ( case ) ) and
793
- case .getValue ( ) .toInt ( ) = k
854
+ case .getValue ( ) .toInt ( ) = k and
855
+ inNonZeroCase = false
794
856
)
795
857
or
796
858
// There's no implicit CompareInstruction in files compiled as C since C
797
859
// doesn't have implicit boolean conversions. So instead we check whether
798
860
// there's a branch on a value of pointer or integer type.
799
- exists ( ConditionalBranchInstruction branch , IRType type |
800
- not test instanceof CompareInstruction and
801
- type = test .getResultIRType ( ) and
802
- ( type instanceof IRAddressType or type instanceof IRIntegerType ) and
803
- test = branch .getCondition ( ) and
804
- op .getDef ( ) = test
805
- |
806
- // We'd like to also include a case such as:
807
- // ```
808
- // k = 1 and
809
- // value.(BooleanValue).getValue() = true
810
- // ```
811
- // but all we know is that the value is non-zero in the true branch.
812
- // 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
813
868
k = 0 and
814
- value .( BooleanValue ) .getValue ( ) = false
869
+ value .( BooleanValue ) .getValue ( ) = false and
870
+ inNonZeroCase = false
815
871
)
816
872
}
817
873
@@ -824,11 +880,11 @@ private predicate complex_eq(
824
880
}
825
881
826
882
private predicate unary_complex_eq (
827
- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
883
+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
828
884
) {
829
- unary_sub_eq ( test , op , k , areEqual , value )
885
+ unary_sub_eq ( test , op , k , areEqual , inNonZeroCase , value )
830
886
or
831
- unary_add_eq ( test , op , k , areEqual , value )
887
+ unary_add_eq ( test , op , k , areEqual , inNonZeroCase , value )
832
888
}
833
889
834
890
/*
@@ -1093,17 +1149,19 @@ private predicate sub_eq(
1093
1149
1094
1150
// op - x == c => op == (c+x)
1095
1151
private predicate unary_sub_eq (
1096
- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
1152
+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
1097
1153
) {
1154
+ inNonZeroCase = false and
1098
1155
exists ( SubInstruction sub , int c , int x |
1099
- unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1156
+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1100
1157
op = sub .getLeftOperand ( ) and
1101
1158
x = int_value ( sub .getRight ( ) ) and
1102
1159
k = c + x
1103
1160
)
1104
1161
or
1162
+ inNonZeroCase = false and
1105
1163
exists ( PointerSubInstruction sub , int c , int x |
1106
- unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1164
+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1107
1165
op = sub .getLeftOperand ( ) and
1108
1166
x = int_value ( sub .getRight ( ) ) and
1109
1167
k = c + x
@@ -1158,11 +1216,12 @@ private predicate add_eq(
1158
1216
1159
1217
// left + x == right + c => left == right + (c-x)
1160
1218
private predicate unary_add_eq (
1161
- Instruction test , Operand left , int k , boolean areEqual ,
1219
+ Instruction test , Operand left , int k , boolean areEqual , boolean inNonZeroCase ,
1162
1220
AbstractValue value
1163
1221
) {
1222
+ inNonZeroCase = false and
1164
1223
exists ( AddInstruction lhs , int c , int x |
1165
- unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1224
+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1166
1225
(
1167
1226
left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
1168
1227
or
@@ -1171,9 +1230,9 @@ private predicate unary_add_eq(
1171
1230
k = c - x
1172
1231
)
1173
1232
or
1233
+ inNonZeroCase = false and
1174
1234
exists ( PointerAddInstruction lhs , int c , int x |
1175
-
1176
- unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1235
+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
1177
1236
(
1178
1237
left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
1179
1238
or
0 commit comments