Skip to content

C/C++ overlay: avoid massive cartesian product in overlay discardElement#21939

Draft
IdrissRio wants to merge 1 commit into
mainfrom
idrissrio/cpp/overlay/alerts
Draft

C/C++ overlay: avoid massive cartesian product in overlay discardElement#21939
IdrissRio wants to merge 1 commit into
mainfrom
idrissrio/cpp/overlay/alerts

Conversation

@IdrissRio
Copy link
Copy Markdown
Contributor

On mupen64/mupen64-rr-lua PR #695, overlay + diff-informed analysis takes ~660s vs ~45s standalone. The optimiser materialises a @element × @trap_or_tag × string join of 2 396 674 785 rows from a forall in Overlay.qll::discardElement.

[2026-06-04 12:13:52] (568s)  >>> Created relation _#Overlay::locallyReachableTrapOrTag/3#11241854MergeNoDiscard_#Overlay::locallyReachableTrapOrTag/3#__#antijoin_rhs/3@e74ac3nt with 2396674785 rows and digest 002245oukoao3iug59rvgipruqe.
[2026-06-04 12:13:52] (568s) Starting to evaluate predicate _#Overlay::locallyReachableTrapOrTag/3#11241854MergeNoDiscard_021#join_rhs__#Overlay::locallyInTrapO__#antijoin_rhs/1@002e89t2
[2026-06-04 12:13:52] (568s)  >>> Created relation _#Overlay::locallyReachableTrapOrTag/3#11241854MergeNoDiscard_#Overlay::locallyReachableTrapOrTag/3#__#antijoin_rhs/3@17997dcp with 2396674785 rows and digest 002245oukoao3iug59rvgipruqe.

This PR rewrites that conjunct as nested existentials.

Result

Overlay + diff-informed Wall time Peak intermediate
Before 660 s 2 396 674 785 rows
After 198 s 31 071 598 rows

@github-actions github-actions Bot added the C++ label Jun 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant