@@ -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
@@ -837,6 +864,32 @@ private predicate unary_simple_comparison_eq(
837864 inNonZeroCase = false
838865 )
839866 or
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.
840893 not test .isGLValue ( ) and
841894 not simple_comparison_eq ( test , _, _, _, _) and
842895 not simple_comparison_lt ( test , _, _, _) and
0 commit comments