Guards: Support disjunctive implications.

[aschackmull]

This PR adds the following pattern to the set of implications in the Guards library.

b = x == v1 || g;
if (b) {
  if (x == v2) {
    // if v1 and v2 are disjoint then g must hold here
  }
}

This pattern was observed in several nullness false positives for C#, which now ought to be fixed by this change.

[Copilot]

Pull Request Overview

This PR extends the Guards library to support disjunctive implications, enabling analysis of patterns where a disjunction constrains one alternative, allowing the other alternative to be inferred. The key pattern is: if b = x == v1 || g and b is true, then within a nested condition where x == v2 (with v1 and v2 disjoint), g must hold.

• Adds a new DisjunctiveGuard module to compute disjunctive guard implications
• Integrates the new disjunctive analysis into the existing guard implication transitive closure
• Adds test case demonstrating the fix for nullness false positives in Java

Reviewed Changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File	Description
shared/controlflow/codeql/controlflow/Guards.qll	Implements the disjunctive guard implication logic and integrates it into the guard control flow analysis
java/ql/test/query-tests/Nullness/C.java	Adds test case ex19 demonstrating the disjunctive nullness pattern that should now be handled correctly

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[aschackmull]

Dca:

• C++: uneventful
• Java: A clean improvement. 2 new TPs for java/useless-null-check, 2 FPs removed for java/dereferenced-value-may-be-null
• C#: Looks like a clean improvement as well.
  • cs/constant-condition, many new results, spot-checking indicates that they're all TPs.
  • cs/inefficient-containskey, one new TP.
  • cs/dereferenced-value-may-be-null, 23 FPs removed.

[aschackmull]

There's a C# qltest that's weird - I strongly suspect that it's splitting which confuses things. Luckily that doesn't seem to affect actual query results, so I guess we can just accept the qltest weirdness for now.

[hvitved]

QL changes LGTM.

[aschackmull]

I've added a commit accepting the qltest.

[aschackmull]

I've also added a change note for C#, but not for the other languages as the possible changes there seemed too minor.