Merge pull request #20438 from MathiasVP/remove-antijoin-in-shared-guards

Shared: Remove antijoin from `Guards.qll`
This commit is contained in:
Mathias Vorreiter Pedersen
2025-09-16 10:40:45 +01:00
committed by GitHub

View File

@@ -731,13 +731,14 @@ module Make<
private predicate impliesStep1(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
baseImpliesStep(g1, v1, g2, v2)
or
exists(SsaDefinition def, Expr e |
exists(SsaDefinition def, Expr e, BasicBlock bb1 |
// If `def = g2 ? v1 : ...` and all other assignments to `def` are different from
// `v1` then a guard proving `def == v1` ensures that `g2` evaluates to `v2`.
uniqueValue(def, e, v1) and
guardReadsSsaVar(g1, def) and
g2.directlyValueControls(e.getBasicBlock(), v2) and
not g2.directlyValueControls(g1.getBasicBlock(), v2)
bb1 = g1.getBasicBlock() and
not g2.directlyValueControls(bb1, v2)
)
or
exists(int k, boolean upper |