Make all methods of dfcc_utilst static

[tautschnig]

This class has no state, there is no need to instantiate it.

Depends on #7680, among others.

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

[remi-delmas-3000]

This PR seems to contain changes outside of contracs/dynamic-frames

[remi-delmas-3000]

We're in for a lot of refactoring if we go that way: all dfcc_* classes are actually singletons that keep references to context arguments that are present for the whole model transformation and would otherwise have to be passed explicitly to each and every function/method call: the goto model, the symbol table, the message handler, the language mode, other singletons that provide utility functions, etc.

It is usually a pain to realize you need a logger or a irep for the language mode and to have to modify a whole trail of function signatures just to propagate a context argument.

Is there a better solution ?

[tautschnig]

This PR seems to contain changes outside of contracs/dynamic-frames

Yes, that's #7680, which moves what was introduced as a DFCC utility to wider scope (and use).

[tautschnig]

We're in for a lot of refactoring if we go that way: all dfcc_* classes are actually singletons that keep references to context arguments that are present for the whole model transformation and would otherwise have to be passed explicitly to each and every function/method call: the goto model, the symbol table, the message handler, the language mode, other singletons that provide utility functions, etc.

While it was a good way to get us started, I am not sure this is an appropriate application of the Singleton pattern. We end up with many methods that have access to objects that they don't need to be able to access. This makes it very hard to see what a method does/does not change. Also, it's often not clear in what state a method expects a particular object to be in.

It is usually a pain to realize you need a logger or a irep for the language mode and to have to modify a whole trail of function signatures just to propagate a context argument.

Is there a better solution ?

Not that I know of. Take #6915 as an example, where I had to thread through a message handler. Wasn't fun, but ultimately the change wasn't all that big. At the moment, we have a lot of maybe-we-need-this-later code, and I'm afraid I haven't yet seen that this would result in small changes/pull requests when new features are added.

[codecov]

Codecov Report

Patch coverage: 97.56% and project coverage change: -0.08 ⚠️

Comparison is base (339505b) 78.55% compared to head (a79682b) 78.48%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7683      +/-   ##
===========================================
- Coverage    78.55%   78.48%   -0.08%     
===========================================
  Files         1686     1685       -1     
  Lines       192905   192905              
===========================================
- Hits        151536   151393     -143     
- Misses       41369    41512     +143     

Impacted Files	Coverage Δ
...nstrument/contracts/dynamic-frames/dfcc_cfg_info.h	100.00% <ø> (ø)
...cts/dynamic-frames/dfcc_contract_clauses_codegen.h	100.00% <ø> (ø)
...contracts/dynamic-frames/dfcc_contract_functions.h	100.00% <ø> (ø)
...t/contracts/dynamic-frames/dfcc_contract_handler.h	100.00% <ø> (ø)
...nt/contracts/dynamic-frames/dfcc_instrument_loop.h	66.66% <ø> (ø)
...racts/dynamic-frames/dfcc_lift_memory_predicates.h	100.00% <ø> (ø)
...ent/contracts/dynamic-frames/dfcc_spec_functions.h	100.00% <ø> (ø)
...ment/contracts/dynamic-frames/dfcc_swap_and_wrap.h	100.00% <ø> (ø)
...ument/contracts/dynamic-frames/dfcc_instrument.cpp	83.43% <87.50%> (-0.01%)	⬇️
...instrument/contracts/dynamic-frames/dfcc_utils.cpp	98.68% <98.43%> (+9.10%)	⬆️
... and 11 more

... and 12 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

[qinheping]

LGTM

[feliperodri]

Suggested change

	/// \param goto_model: target goto_model holding the symbol table
	/// \param goto_model target goto_model holding the symbol table

[tautschnig]

CODING_STANDARD.md suggests to have the colon here, so I'll keep it as-is.