Skip to content

Skip rename_symbolt::rename when maps are empty#8974

Open
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:skip-rename
Open

Skip rename_symbolt::rename when maps are empty#8974
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:skip-rename

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

rename_symbolt::rename(exprt) creates a depth_iterator and walks the entire expression tree even when both expr_map and type_map are empty. This happens during library linking when no symbols need renaming. Add an early return to avoid the wasted traversal.

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

@tautschnig tautschnig self-assigned this Apr 27, 2026
Copilot AI review requested due to automatic review settings April 27, 2026 10:27

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

Note

Copilot was unable to run its full agentic suite in this review.

Avoids an unnecessary full expression-tree traversal in rename_symbolt::rename(exprt&) when there are no renaming rules, improving library-link-time performance in no-op cases.

Changes:

  • Add an early return in rename_symbolt::rename(exprt&) when both expr_map and type_map are empty.

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

@codecov

codecov Bot commented Apr 27, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.68%. Comparing base (7750282) to head (f09d362).

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8974   +/-   ##
========================================
  Coverage    80.68%   80.68%           
========================================
  Files         1713     1714    +1     
  Lines       189462   189479   +17     
  Branches        73       73           
========================================
+ Hits        152860   152890   +30     
+ Misses       36602    36589   -13     

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

rename_symbolt::rename(exprt) creates a depth_iterator and walks
the entire expression tree even when both expr_map and type_map
are empty. This happens during library linking when no symbols
need renaming. Add an early return to avoid the wasted traversal,
mirroring the existing short-circuits in have_to_rename().

Factor the repeated `expr_map.empty() && type_map.empty()` check
(now in rename(exprt&) and both have_to_rename overloads) into a
public rename_symbolt::empty() helper, so the predicate has a
single definition and a future third map cannot be missed.

Add a unit test (unit/util/rename_symbol.cpp; there were none for
rename_symbolt) pinning the documented contract: empty maps leave
the expression unchanged and return true, while a populated map
renames the matching symbol and returns false.

Performance: the change removes a full expression-tree traversal
on every empty-map rename call. Measured with goto-cc/cbmc built
with and without the early return (in-source -O2, medians):
- goto-cc linking a large object (8000 functions, ~8 MB goto
  binary) with empty rename maps: 1.97s -> 1.94s (~ -1.6%) -- the
  library-linking scenario this targets;
- goto-cc compile+link and cbmc --program-only of CSmith programs:
  within measurement noise (<= 1%, both signs), i.e. no regression
  on workloads that do not stress empty-map renaming.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.

3 participants