Make function pointer removal deterministic

[tautschnig]

Sort function pointer candidates by identifier name before generating the dispatch code. This ensures the order of IF/GOTO branches in the resulting GOTO program is independent of internal hash table ordering, which can vary when irep IDs are added or removed.

Without this fix, unrelated changes to irep_ids.def can cause different function pointer dispatch orderings, leading to different symbolic execution paths and dramatically different SAT solver performance.

• 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).
• n/a 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.

This PR makes function-pointer dispatch generation deterministic by sorting candidate targets by identifier before emitting IF/GOTO branches, preventing nondeterministic ordering from unordered_set iteration and avoiding downstream symbolic-execution / solver-performance variance.

Changes:

• Convert the function-candidate container from unordered_set iteration order to a sorted vector for deterministic dispatch emission.
• Update the assertion-comment helper to accept an ordered candidate list.
• Add a regression test ensuring deterministic sorted emission independent of CLI target ordering.

Reviewed changes

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

File	Description
src/goto-programs/remove_function_pointers.cpp	Sort function-pointer targets by identifier before generating dispatch; adjust helper signature accordingly.
regression/goto-instrument/restrict-function-pointer-deterministic-order/test.desc	Adds regression expectations asserting stable, sorted IF-branch order and assertion text.
regression/goto-instrument/restrict-function-pointer-deterministic-order/test.c	New minimal C test exercising function-pointer call-site restriction/dispatch.

---

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

[Copilot]

After changing function_pointer_assertion_comment to take a std::vector, its output determinism now depends on callers providing a pre-sorted vector. To make this helper robust (and prevent future call sites from accidentally reintroducing nondeterministic output), either (a) sort a local copy inside function_pointer_assertion_comment, or (b) clearly encode the precondition in the API (e.g., rename the parameter to sorted_candidates and add a short comment that the vector must be sorted by identifier).

[Copilot]

The comparator converts both identifiers via id2string(...) on every comparison, which increases work during sorting (O(n log n) conversions/allocations). Prefer comparing identifiers without repeated string materialization (e.g., compare irep_idt directly if it has a strict ordering, or precompute the string keys once and sort by those).

Suggested change

	{ return id2string(a.get_identifier()) < id2string(b.get_identifier()); });
	{ return a.get_identifier() < b.get_identifier(); });

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.47%. Comparing base (803f904) to head (4a285a7).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8952   +/-   ##
========================================
  Coverage    80.47%   80.47%           
========================================
  Files         1704     1704           
  Lines       188694   188699    +5     
  Branches        73       73           
========================================
+ Hits        151843   151854   +11     
+ Misses       36851    36845    -6     

☔ View full report in Codecov by Sentry.
📢 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.