@@ -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
@@ -837,6 +864,32 @@ private predicate unary_simple_comparison_eq(
837
864
inNonZeroCase = false
838
865
)
839
866
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.
840
893
not test .isGLValue ( ) and
841
894
not simple_comparison_eq ( test , _, _, _, _) and
842
895
not simple_comparison_lt ( test , _, _, _) and
0 commit comments