Skip to content

Share object maps in value_sett::make_union when destination is empty#9125

Open
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:perf/value-set-make-union-sharing
Open

Share object maps in value_sett::make_union when destination is empty#9125
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:perf/value-set-make-union-sharing

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

The object_mapt representation is reference counted precisely so that multiple owners can share one map, yet make_union built the union element by element even when the destination was empty. Value-set queries for a single symbol (via get_value_set_rec) arrive here with an empty destination, so each such query copied the symbol's entire object map, including one std::optional offset per element. Sharing the source map instead makes this constant time and removes the dominant allocation churn from value-set queries in symbolic execution.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.

The object_mapt representation is reference counted precisely so that
multiple owners can share one map, yet make_union built the union
element by element even when the destination was empty. Value-set
queries for a single symbol (via get_value_set_rec) arrive here with an
empty destination, so each such query copied the symbol's entire
object map, including one std::optional<exprt> offset per element.
Sharing the source map instead makes this constant time and removes the
dominant allocation churn from value-set queries in symbolic execution.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig self-assigned this Jul 22, 2026
Copilot AI review requested due to automatic review settings July 22, 2026 09:10

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR improves pointer-analysis value-set performance by avoiding element-by-element copying in value_sett::make_union when the destination map is empty. It leverages the existing copy-on-write reference_counting<> representation to share the underlying object map in constant time, reducing allocation churn during frequent single-symbol value-set queries in symbolic execution.

Changes:

  • Early-return when the source object map is empty.
  • When the destination object map is empty, assign dest = src to share the reference-counted representation instead of inserting entries one-by-one.

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

@codecov

codecov Bot commented Jul 22, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.83%. Comparing base (f71fdad) to head (29eeb0d).

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #9125   +/-   ##
========================================
  Coverage    80.83%   80.83%           
========================================
  Files         1715     1715           
  Lines       189948   189951    +3     
  Branches        73       73           
========================================
+ Hits        153540   153543    +3     
  Misses       36408    36408           

☔ 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants