@@ -375,6 +375,33 @@ cached
375375class IRGuardCondition extends Instruction {
376376 Instruction branch ;
377377
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+
378405 cached
379406 IRGuardCondition ( ) { branch = getBranchForCondition ( this ) }
380407
@@ -776,7 +803,9 @@ private predicate unary_compares_eq(
776803 Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
777804) {
778805 /* 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+ |
780809 areEqual = true and value = v
781810 or
782811 areEqual = false and value = v .getDualValue ( )
@@ -821,45 +850,55 @@ private predicate simple_comparison_eq(
821850 value .( BooleanValue ) .getValue ( ) = false
822851}
823852
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-
843853/**
844854 * Rearrange various simple comparisons into `op == k` form.
845855 */
846856private 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
848858) {
849859 exists ( SwitchInstruction switch , CaseEdge case |
850860 test = switch .getExpression ( ) and
851- op .getDef ( ) = test and
852861 case = value .( MatchValue ) .getCase ( ) and
853862 exists ( switch .getSuccessor ( case ) ) and
854863 case .getValue ( ) .toInt ( ) = k and
855864 inNonZeroCase = false
856865 )
857866 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
863902 (
864903 k = 1 and
865904 value .( BooleanValue ) .getValue ( ) = true and
@@ -913,7 +952,8 @@ private predicate compares_lt(
913952
914953/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
915954private 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
917957 or
918958 complex_lt ( test , op , k , isLt , value )
919959 or
@@ -960,12 +1000,11 @@ private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Ope
9601000}
9611001
9621002/** 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
9651005) {
9661006 exists ( SwitchInstruction switch , CaseEdge case |
9671007 test = switch .getExpression ( ) and
968- op .getDef ( ) = test and
9691008 case = value .( MatchValue ) .getCase ( ) and
9701009 exists ( switch .getSuccessor ( case ) ) and
9711010 case .getMaxValue ( ) > case .getMinValue ( )
0 commit comments