GOTO conversion: create temporaries with minimal scope

[tautschnig]

GOTO conversion introduces temporaries when cleaning expression, e.g., removing side effects. We previously considered them to have block scope as they only were marked dead when the block containing them was left. This, however, can be a much larger range of instructions than for what instructions they actually need to be live for. As a consequence, GOTO conversion frequently deemed it necessary to introduce declaration hops for we had goto instructions that would jump over the declaration of the temporary, but still within the block that contained that temporary (and well after the last actual use of that temporary).

This PR now largely (with the exception of compound literals, which yield temporaries that must have block scope) removes the side effect that creating temporaries had on scope tracking. Instead, methods explicitly return the list of temporaries in need of cleanup.

This avoids performance penalties seen when trying to upgrade Kani to CBMC version 6. Kani makes extensive use of statement expressions, which are one case of instructions that yield a temporary that needs to be cleaned up as soon as possible.

The second commit is code cleanup that touches almost the same lines as the first commit, so this PR is best reviewed all-commits-at-once.

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

[codecov]

Codecov Report

Attention: Patch coverage is 86.58892% with 46 lines in your changes missing coverage. Please review.

Project coverage is 78.11%. Comparing base (c7d7704) to head (cb2e20c).

Files	Patch %	Lines
src/ansi-c/goto-conversion/goto_convert.cpp	80.95%	20 Missing ⚠️
...nsi-c/goto-conversion/goto_convert_side_effect.cpp	89.71%	11 Missing ⚠️
src/ansi-c/goto-conversion/goto_clean_expr.cpp	86.84%	10 Missing ⚠️
...s/dynamic-frames/dfcc_contract_clauses_codegen.cpp	50.00%	3 Missing ⚠️
src/ansi-c/goto-conversion/destructor.cpp	91.66%	1 Missing ⚠️
...i-c/goto-conversion/goto_convert_function_call.cpp	85.71%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8363      +/-   ##
===========================================
- Coverage    78.32%   78.11%   -0.22%     
===========================================
  Files         1726     1726              
  Lines       188506   189207     +701     
  Branches     18249    18258       +9     
===========================================
+ Hits        147646   147790     +144     
- Misses       40860    41417     +557     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[remi-delmas-3000]

Just asking for documentation on the clean_expr_resultt so that users of clean_expr know what to do with it.

[kroening]

Probably low priority, but I am wondering whether it makes sense to return a compound that includes both the objects that need to be destroyed and the generated goto program.

[tautschnig]

Probably low priority, but I am wondering whether it makes sense to return a compound that includes both the objects that need to be destroyed and the generated goto program.

Could you please be more specific on how this should be different from what's being done now? Arguably, right now it's just the names plus goto program, would you want symbol_exprt instead?