@@ -375,6 +375,33 @@ cached
375
375
class IRGuardCondition extends Instruction {
376
376
Instruction branch ;
377
377
378
+ /*
379
+ * An `IRGuardCondition` supports reasoning about four different kinds of
380
+ * relations:
381
+ * 1. A unary equality relation of the form `e == k`
382
+ * 2. A binary equality relation of the form `e1 == e2 + k`
383
+ * 3. A unary inequality relation of the form `e < k`
384
+ * 4. A binary inequality relation of the form `e1 < e2 + k`
385
+ *
386
+ * where `k` is a constant.
387
+ *
388
+ * Furthermore, the unary relations (i.e., case 1 and case 3) are also
389
+ * inferred from `switch` statement guards: equality relations are inferred
390
+ * from the unique `case` statement, if any, and inequality relations are
391
+ * inferred from the [case range](https://gcc.gnu.org/onlinedocs/gcc/Case-Ranges.html)
392
+ * gcc extension.
393
+ *
394
+ * The implementation of all four follows the same structure: Each relation
395
+ * has a cached user-facing predicate that. For example,
396
+ * `GuardCondition::comparesEq` calls `compares_eq`. This predicate has
397
+ * several cases that recursively decompose the relation to bring it to a
398
+ * canonical form (i.e., a relation of the form `e1 == e2 + k`). The base
399
+ * case for this relation (i.e., `simple_comparison_eq`) handles
400
+ * `CompareEQInstruction`s and `CompareNEInstruction`, and recursive
401
+ * predicates (e.g., `complex_eq`) rewrites larger expressions such as
402
+ * `e1 + k1 == e2 + k2` into canonical the form `e1 == e2 + (k2 - k1)`.
403
+ */
404
+
378
405
cached
379
406
IRGuardCondition ( ) { branch = getBranchForCondition ( this ) }
380
407
@@ -776,7 +803,9 @@ private predicate unary_compares_eq(
776
803
Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
777
804
) {
778
805
/* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
779
- exists ( AbstractValue v | unary_simple_comparison_eq ( test , op , k , inNonZeroCase , v ) |
806
+ exists ( AbstractValue v |
807
+ unary_simple_comparison_eq ( test , k , inNonZeroCase , v ) and op .getDef ( ) = test
808
+ |
780
809
areEqual = true and value = v
781
810
or
782
811
areEqual = false and value = v .getDualValue ( )
@@ -821,45 +850,55 @@ private predicate simple_comparison_eq(
821
850
value .( BooleanValue ) .getValue ( ) = false
822
851
}
823
852
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
853
/**
844
854
* Rearrange various simple comparisons into `op == k` form.
845
855
*/
846
856
private predicate unary_simple_comparison_eq (
847
- Instruction test , Operand op , int k , boolean inNonZeroCase , AbstractValue value
857
+ Instruction test , int k , boolean inNonZeroCase , AbstractValue value
848
858
) {
849
859
exists ( SwitchInstruction switch , CaseEdge case |
850
860
test = switch .getExpression ( ) and
851
- op .getDef ( ) = test and
852
861
case = value .( MatchValue ) .getCase ( ) and
853
862
exists ( switch .getSuccessor ( case ) ) and
854
863
case .getValue ( ) .toInt ( ) = k and
855
864
inNonZeroCase = false
856
865
)
857
866
or
858
- // There's no implicit CompareInstruction in files compiled as C since C
859
- // doesn't have implicit boolean conversions. So instead we check whether
860
- // there's a branch on a value of pointer or integer type.
861
- relevantUnaryComparison ( test ) and
862
- op .getDef ( ) = test and
867
+ // Any instruction with an integral type could potentially be part of a
868
+ // check for nullness when used in a guard. So we include all integral
869
+ // typed instructions here. However, since some of these instructions are
870
+ // already included as guards in other cases, we exclude those here.
871
+ // These are instructions that compute a binary equality or inequality
872
+ // relation. For example, the following:
873
+ // ```cpp
874
+ // if(a == b + 42) { ... }
875
+ // ```
876
+ // generates the following IR:
877
+ // ```
878
+ // r1(glval<int>) = VariableAddress[a] :
879
+ // r2(int) = Load[a] : &:r1, m1
880
+ // r3(glval<int>) = VariableAddress[b] :
881
+ // r4(int) = Load[b] : &:r3, m2
882
+ // r5(int) = Constant[42] :
883
+ // r6(int) = Add : r4, r5
884
+ // r7(bool) = CompareEQ : r2, r6
885
+ // v1(void) = ConditionalBranch : r7
886
+ // ```
887
+ // and since `r7` is an integral typed instruction this predicate could
888
+ // include a case for when `r7` evaluates to true (in which case we would
889
+ // infer that `r6` was non-zero, and a case for when `r7` evaluates to false
890
+ // (in which case we would infer that `r6` was zero).
891
+ // However, since `a == b + 42` is already supported when reasoning about
892
+ // binary equalities we exclude those cases here.
893
+ not test .isGLValue ( ) and
894
+ not simple_comparison_eq ( test , _, _, _, _) and
895
+ not simple_comparison_lt ( test , _, _, _) and
896
+ not test = any ( SwitchInstruction switch ) .getExpression ( ) and
897
+ (
898
+ test .getResultIRType ( ) instanceof IRAddressType or
899
+ test .getResultIRType ( ) instanceof IRIntegerType or
900
+ test .getResultIRType ( ) instanceof IRBooleanType
901
+ ) and
863
902
(
864
903
k = 1 and
865
904
value .( BooleanValue ) .getValue ( ) = true and
@@ -913,7 +952,8 @@ private predicate compares_lt(
913
952
914
953
/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
915
954
private predicate compares_lt ( Instruction test , Operand op , int k , boolean isLt , AbstractValue value ) {
916
- simple_comparison_lt ( test , op , k , isLt , value )
955
+ unary_simple_comparison_lt ( test , k , isLt , value ) and
956
+ op .getDef ( ) = test
917
957
or
918
958
complex_lt ( test , op , k , isLt , value )
919
959
or
@@ -960,12 +1000,11 @@ private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Ope
960
1000
}
961
1001
962
1002
/** Rearrange various simple comparisons into `op < k` form. */
963
- private predicate simple_comparison_lt (
964
- Instruction test , Operand op , int k , boolean isLt , AbstractValue value
1003
+ private predicate unary_simple_comparison_lt (
1004
+ Instruction test , int k , boolean isLt , AbstractValue value
965
1005
) {
966
1006
exists ( SwitchInstruction switch , CaseEdge case |
967
1007
test = switch .getExpression ( ) and
968
- op .getDef ( ) = test and
969
1008
case = value .( MatchValue ) .getCase ( ) and
970
1009
exists ( switch .getSuccessor ( case ) ) and
971
1010
case .getMaxValue ( ) > case .getMinValue ( )
0 commit comments