goto-instrument --generate-function-body: bound dynamic-object allocation

[tautschnig]

The object factory's max_nondet_tree_depth cap only fires when a struct tag repeats on the pointer chain, so wide-but-non-recursive struct hierarchies still expand exponentially, making --generate-function-body emit an unboundedly large body (and, on large inputs, fail to terminate).

Add object_factory_parameterst::max_dynamic_object_instances (default 1000, exposed as --max-dynamic-object-instances): once the per-root allocation count reaches it, pointers are initialised to NULL instead of recursively expanded. The count is reset at the top-level gen_nondet_init entry, so the cap is enforced per nondet-init root.

Performance: on a goto binary built from Linux 5.10's crypto/algif_aead.c, goto-instrument --generate-function-body af_alg_alloc_areq --generate-function-body-options havoc previously did not terminate (still running after 4 hours of wall-clock time); with this cap it completes in about 2 seconds, emitting a ~10 MB goto binary.

Add a regression test with a deep non-recursive struct hierarchy capped below its natural allocation count; it fails if the cap is reverted.

• 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.
• 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 was unable to run its full agentic suite in this review.

Improves performance and termination guarantees for goto-instrument --generate-function-body by eliminating an O(N²) symbol suffix scan and adding a hard cap on dynamic object allocations during nondet initialisation.

Changes:

• Add a per-prefix suffix “search start” cache to symbol_table_baset::next_unused_suffix(prefix) to amortise repeated allocations under one prefix.
• Add max_dynamic_object_instances parameter and enforce it in symbol_factoryt::gen_nondet_init to prevent runaway nondet-init expansion.
• Add a new regression test to ensure deep/wide non-recursive struct hierarchies don’t hang/OOM during havoc body generation.

Reviewed changes

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

Show a summary per file

File	Description
src/util/symbol_table_base.h	Adds per-prefix suffix hint cache to avoid O(N²) repeated scans.
src/util/object_factory_parameters.h	Introduces max_dynamic_object_instances parameter with detailed rationale.
src/util/object_factory_parameters.cpp	Parses/propagates the new CLI option into object factory params.
src/ansi-c/c_nondet_symbol_factory.h	Adds allocation counter to enforce the new hard cap.
src/ansi-c/c_nondet_symbol_factory.cpp	Enforces allocation cap by nulling pointers once limit is reached.
src/ansi-c/ansi_c_language.h	Exposes --max-dynamic-object-instances via frontend option/help text.
regression/goto-instrument/generate-function-body-deep-struct-cap/test.desc	Adds regression harness invoking the new cap option.
regression/goto-instrument/generate-function-body-deep-struct-cap/main.c	Defines a deep/wide non-recursive struct hierarchy reproducer.

---

💡 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.68%. Comparing base (7483d0d) to head (9e695b9).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9058      +/-   ##
===========================================
- Coverage    80.68%   80.68%   -0.01%     
===========================================
  Files         1714     1714              
  Lines       189593   189606      +13     
  Branches        73       73              
===========================================
+ Hits        152979   152989      +10     
- Misses       36614    36617       +3     

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