Dominator sets: use sharing map to avoid quadratic memory

[tautschnig]

cfg_dominators_templatet stored the full dominator set of every program point in a per-node std::set. Dominator sets of adjacent program points are nearly identical, so this representation needs memory quadratic in the function size: for a mostly straight-line function of N instructions the sets hold N^2/2 elements in total. Machine-generated functions make this prohibitive: goto-instrument --ensure-one-backedge-per-target (which Kani runs on every harness) peaked at 22.1 GB resident memory on a 3.6 MB goto binary from the Rust sha2 crate, whose macro-unrolled compression function has ~80k instructions.

Back the dominator sets by sharing_mapt, CBMC's copy-on-write hash trie: copying a predecessor's set is now O(1), inserting a single element into a copy is O(log N), and the fixed point's intersection uses get_delta_view, which only visits elements in subtrees not physically shared between the two sets and hence is cheap precisely when the sets are similar.

On the sha2 goto binary above, --ensure-one-backedge-per-target improves from 22.1 GB / 67 s to 1.9 GB / 12.6 s, with bit-identical output; the crate becomes verifiable on ordinary hardware. Consumers that iterated the sorted std::set now sort explicitly where order matters for tie-breaking (full_slicer, sese_regions) and for stable output (output()), since the sharing map iterates in hash order.

Alternative approaches to the same problem were proposed before and remain complementary:

• Dominator nodes only store immediate dominator #5137 stores only the immediate dominator per node (Cooper et al.'s dominator tree). That is asymptotically stronger still (linear memory even for join-heavy CFGs where structural sharing degrades), but changes the interface of every dominator-set consumer, which must walk idom chains instead of querying sets; the PR has been inactive since 2019. The change here keeps the existing set-based API and its consumers intact, at the cost of remaining an iterative set-based fixed point.
• Dominator analysis: analyse on basic block granularity #5042 computes dominators on basic-block rather than instruction granularity. That reduces N by a constant factor but keeps the quadratic set representation; it would compose with this change, further reducing both memory and the delta-view work.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR reduces memory usage of dominator/post-dominator analysis by backing per-program-point dominator sets with CBMC’s copy-on-write sharing_mapt, avoiding the previous quadratic blow-up from storing full std::set copies per node. This keeps the existing set-based API while making copying and intersection cheap when sets are similar (the common case for adjacent CFG nodes).

Changes:

• Replace per-node std::set dominator sets with a structurally-sharing sharing_mapt-backed set and update the fixed-point intersection accordingly.
• Update dominator-set consumers to use the new set API (count, for_each) and add explicit sorting where deterministic order matters.
• Ensure stable output/behavior where previous ordered-set iteration implied determinism (e.g., output and tie-breaking logic).

Reviewed changes

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

Show a summary per file

File	Description
src/analyses/cfg_dominators.h	Reworks dominator-set representation to use sharing_mapt, updates intersection and output ordering.
src/goto-instrument/full_slicer.cpp	Adjusts dominator iteration to remain deterministic by explicitly sorting dominators before tie-breaking.
src/analyses/sese_regions.cpp	Ensures deterministic selection by sorting post-dominator candidates explicitly.
src/analyses/dependence_graph.cpp	Migrates dominator membership checks from find to count.
src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp	Migrates dominator membership checks from find to count.
jbmc/src/java_bytecode/java_local_variable_table.cpp	Updates dominator iteration to use for_each and retains deterministic behavior via explicit sorting.

---

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

[codecov]

Codecov Report

❌ Patch coverage is 95.91837% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.83%. Comparing base (7483d0d) to head (2ad63df).
⚠️ Report is 42 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/analyses/sese_regions.cpp	83.33%	1 Missing ⚠️
src/goto-instrument/full_slicer.cpp	88.88%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9141      +/-   ##
===========================================
+ Coverage    80.68%   80.83%   +0.14%     
===========================================
  Files         1714     1715       +1     
  Lines       189593   190004     +411     
  Branches        73       73              
===========================================
+ Hits        152979   153590     +611     
+ Misses       36614    36414     -200     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.