Guards: Improve performance of forall in guardDeterminesPhiInput.

[aschackmull]

I noticed poor performance in this predicate for Java after merging the new CFG. It's a classic case of quadratic forall blowup, but instead of fixing it via the usual ranking trick, I noticed the we can magic the forall with a strictcount restriction, which seems to work well.

Before:

[2026-03-04 09:54:18] Evaluated non-recursive predicate _Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#antijoin_rhs@2478cem4 in 1857ms (size: 356148).
Evaluated relational algebra for predicate _Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#antijoin_rhs@2478cem4 with tuple counts:
           389224      ~0%    {4} r1 = SCAN `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb` OUTPUT In.1, In.0, In.2, In.3
           389224      ~4%    {5}    | JOIN WITH `Guards::GuardValue.getDualValue/0#dispred#262050dd` ON FIRST 1 OUTPUT Lhs.2, Lhs.0, Rhs.1, Lhs.1, Lhs.3
        222420202      ~0%    {6}    | JOIN WITH `project#SSA::Ssa::Cached::phiHasInputFromBlockCached/3#0736af18` ON FIRST 1 OUTPUT Lhs.1, Lhs.2, Lhs.3, Lhs.0, Lhs.4, Rhs.1
                              {6}    | REWRITE WITH TEST InOut.4 != InOut.5
        222030978      ~0%    {6}    | SCAN OUTPUT In.2, In.1, In.3, In.5, In.0, In.4
                              {6}    | AND NOT `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb`(FIRST 4)
        219465590  ~61416%    {5}    | SCAN OUTPUT In.4, In.1, In.0, In.2, In.5
                              return r1
[2026-03-04 09:54:18] Evaluated non-recursive predicate Guards::Guards_v2::guardDeterminesPhiInput/4#17435ff9@7d4e39du in 4ms (size: 14409).
Evaluated relational algebra for predicate Guards::Guards_v2::guardDeterminesPhiInput/4#17435ff9@7d4e39du with tuple counts:
        389224   ~0%    {4} r1 = SCAN `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb` OUTPUT In.1, In.0, In.2, In.3
        389224   ~0%    {5}    | JOIN WITH `Guards::GuardValue.getDualValue/0#dispred#262050dd` ON FIRST 1 OUTPUT Lhs.0, Rhs.1, Lhs.1, Lhs.2, Lhs.3
                        {5}    | AND NOT `_Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#antijoin_rhs`(FIRST 5)
         35364   ~1%    {4}    | SCAN OUTPUT In.4, In.0, In.2, In.3
         14409   ~3%    {4}    | JOIN WITH `SSA::Ssa::SsaExplicitWrite.getValue/0#dispred#ac67f64a` ON FIRST 1 OUTPUT Lhs.2, Lhs.1, Lhs.3, Rhs.1
                        return r1

After:

[2026-03-04 10:39:43] Evaluated non-recursive predicate _Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#shared@c25a43go in 21ms (size: 43277).
Evaluated relational algebra for predicate _Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#shared@c25a43go with tuple counts:
        49186   ~0%    {4} r1 = AGGREGATE `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb`, `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb` ON  WITH COUNT OUTPUT In.0, In.1, In.2, Agg.0
        49186   ~0%    {4}    | SCAN OUTPUT In.1, In.0, In.2, In.3
        49186   ~0%    {6}    | JOIN WITH `Guards::GuardValue.getDualValue/0#dispred#262050dd` ON FIRST 1 OUTPUT Lhs.0, Rhs.1, Lhs.1, Lhs.2, Lhs.3, _
                       {5}    | REWRITE WITH Tmp.5 := 1, TEST InOut.4 = Tmp.5 KEEPING 5
        43277   ~0%    {4}    | SCAN OUTPUT In.2, In.0, In.3, In.1
                       return r1
[2026-03-04 10:39:43] Evaluated non-recursive predicate _Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb__Guards::GuardValue.getDualValue/0#dispred#262__#antijoin_rhs@088a898i in 17ms (size: 7913).
Evaluated relational algebra for predicate _Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb__Guards::GuardValue.getDualValue/0#dispred#262__#antijoin_rhs@088a898i with tuple counts:
         43277    ~1%    {5} r1 = JOIN `_Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#shared` WITH `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb` ON FIRST 3 OUTPUT Lhs.2, Lhs.1, Lhs.3, Lhs.0, Rhs.3
        202880    ~3%    {6}    | JOIN WITH `project#SSA::Ssa::Cached::phiHasInputFromBlockCached/3#0736af18` ON FIRST 1 OUTPUT Lhs.1, Lhs.2, Lhs.3, Lhs.0, Lhs.4, Rhs.1
                         {6}    | REWRITE WITH TEST InOut.4 != InOut.5
        159603    ~0%    {6}    | SCAN OUTPUT In.2, In.1, In.3, In.5, In.0, In.4
                         {6}    | AND NOT `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb`(FIRST 4)
         56124  ~591%    {5}    | SCAN OUTPUT In.4, In.1, In.0, In.2, In.5
                         return r1
[2026-03-04 10:39:43] Evaluated non-recursive predicate Guards::Guards_v2::guardDeterminesPhiInput/4#17435ff9@7e17883k in 8ms (size: 14409).
Evaluated relational algebra for predicate Guards::Guards_v2::guardDeterminesPhiInput/4#17435ff9@7e17883k with tuple counts:
        43277   ~2%    {5} r1 = JOIN `_Guards::GuardValue.getDualValue/0#dispred#262050dd_Guards::Guards_v2::guardControlsPhiBranch/4#af96__#shared` WITH `Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb` ON FIRST 3 OUTPUT Lhs.1, Lhs.3, Lhs.0, Lhs.2, Rhs.3
                       {5}    | AND NOT `_Guards::Guards_v2::guardControlsPhiBranch/4#af96bfdb__Guards::GuardValue.getDualValue/0#dispred#262__#antijoin_rhs`(FIRST 5)
        35364   ~1%    {4}    | SCAN OUTPUT In.4, In.0, In.2, In.3
        14409   ~3%    {4}    | JOIN WITH `SSA::Ssa::SsaExplicitWrite.getValue/0#dispred#ac67f64a` ON FIRST 1 OUTPUT Lhs.2, Lhs.1, Lhs.3, Rhs.1
                       return r1

[Copilot]

Pull request overview

This PR improves the performance of the guardDeterminesPhiInput predicate in Guards.qll by adding a strictcount restriction that acts as a cheap pre-filter before an expensive forall check, avoiding classic quadratic forall blowup. The PR description shows an evaluation time reduction for the main antijoin auxiliary predicate from ~1857ms to ~21ms.

Changes:

• Adds a strictcount guard to ensure there is exactly one SsaDefinition controlled by guard == v before entering the forall check, exploiting the fact that the forall itself implies this uniqueness in valid cases
• Includes an explanatory comment documenting why this pre-filter is semantically valid and why it improves performance

---

You can also share your feedback on Copilot code review. Take the survey.