Avoid materializing value sets when simplifying POINTER_OBJECT equalties

[tautschnig]

Symbolic execution is O(N^2) in the number of heap deallocations: each free generates same-object checks against __CPROVER_deallocated and __CPROVER_dead_object, whose value sets accumulate one element per previously freed object, and
simplify_expr_with_value_sett::simplify_inequality_pointer_object materialized each such value set into a std::set on every query. This was 30.1% of symex instructions (callgrind) on a Kani-generated benchmark performing 128 allocate/free iterations, growing with the square of the iteration count: each query built an object_descriptor_exprt per element and inserted it into a set ordered by deep-tree irept::compare, with all the attendant irep sharing and allocation churn.

Instead, collect the root objects of value-set elements as a set of object numbers in value_sett::object_numbering. The numbering is hash-consed, so numbers are sound proxies for expression equality, and all set operations become operations over integers. The per-element classification (root object computation and failed-symbol test) is cached per object number, which is sound because the numbering is global, append-only, and maps numbers to immutable expressions. Also skip collecting the right-hand side objects entirely when the left-hand side came back empty, and test set disjointness without materializing the intersection.

This makes the object_mapt-returning value_sett::get_value_set overload public; it was previously only accessible to subclasses while the public overload materialized an expression per element.

On the benchmark family above (N allocate/free iterations, goto binaries generated by Kani, verified with --slice-formula etc.), Runtime Symex improves, together with the separately-proposed change sharing object maps in value_sett::make_union, from 7.2s to 5.3s (N=128), 19.5s to 10.9s (N=256), 62.1s to 23.3s (N=512) and 222.5s to 53.1s (N=1021), i.e. growth flattens from ~3.2x to ~2.1x per doubling of N. --show-vcc output is unchanged at N=8 and N=128, i.e. exactly the same simplifications are made. The function is down to 3.4% inclusive of symex time at N=512, which is also why a size cap on the simplification and memoization of whole value-set queries (both considered as alternatives) were not pursued: they would give up simplifications, or add cache invalidation complexity, for at most a few percent.

• 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

Note

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Improves symex performance by avoiding repeated materialization and deep comparison of expression trees when simplifying pointer-object equalities, switching to integer object-number sets with caching.

Changes:

• Exposes an object_mapt-returning value_sett::get_value_set overload publicly to avoid per-element object_descriptor_exprt materialization.
• Refactors pointer-object inequality simplification to operate on sets of object numbers, caching root-object classification and avoiding intersection materialization.

Reviewed changes

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

File	Description
src/pointer-analysis/value_set.h	Makes the object_mapt overload of get_value_set public and documents its purpose (avoid expression materialization).
src/goto-symex/simplify_expr_with_value_set.cpp	Switches simplification to integer set operations with cached root-object computation and more efficient disjointness testing.

---

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

[codecov]

Codecov Report

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

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9128      +/-   ##
===========================================
- Coverage    80.83%   80.83%   -0.01%     
===========================================
  Files         1715     1715              
  Lines       189948   189974      +26     
  Branches        73       73              
===========================================
+ Hits        153540   153559      +19     
- Misses       36408    36415       +7     

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