Move goto_convert files

[kroening]

The goto_convertt class and associated helpers convert a C parse tree into a set of GOTO functions. They are specific to C, and hence, should be in the ansi-c/ directory.

• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 66.04361% with 327 lines in your changes are missing coverage. Please review.

Project coverage is 78.02%. Comparing base (4f5b402) to head (2b3d12c).

Files	Patch %	Lines
src/ansi-c/goto-conversion/builtin_functions.cpp	49.46%	94 Missing ⚠️
.../ansi-c/goto-conversion/string_instrumentation.cpp	28.70%	77 Missing ⚠️
src/ansi-c/goto-conversion/format_strings.cpp	36.97%	75 Missing ⚠️
src/ansi-c/printf_formatter.cpp	68.00%	56 Missing ⚠️
src/ansi-c/goto-conversion/goto_convert.cpp	91.61%	13 Missing ⚠️
src/ansi-c/goto-conversion/goto_convert_class.h	90.24%	4 Missing ⚠️
...ansi-c/goto-conversion/goto_convert_exceptions.cpp	66.66%	3 Missing ⚠️
...nsi-c/goto-conversion/goto_convert_side_effect.cpp	96.66%	3 Missing ⚠️
...ecode/java_virtual_functions/virtual_functions.cpp	0.00%	1 Missing ⚠️
...i-c/goto-conversion/goto_convert_function_call.cpp	88.88%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8253      +/-   ##
===========================================
+ Coverage    78.00%   78.02%   +0.01%     
===========================================
  Files         1721     1721              
  Lines       188940   188868      -72     
  Branches     18415    18447      +32     
===========================================
- Hits        147388   147369      -19     
+ Misses       41552    41499      -53     

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

[tautschnig]

Is this one really C specific? It appears to be used by JBMC, and perhaps more so than anywhere else?

[kroening]

I'd say it tries to do too much. Object construction is clearly language specific, and this should get split up.

[tautschnig]

I have a couple of concerns:

• The ansi-c folder is starting to become unmanageable. At bare minimum I'd suggest that we have a new subfolder ansi-c/goto-conversion/ (or some similar name) to hold those files.
• As indicated by my comment, but perhaps applicable in more cases: are all those files really all about goto conversion?
• Is it really correct to assert that only C parse trees can be converted? Isn't it rather the case that we actually have a further intermediate language of codet statements?
• Do we perhaps need to become a lot more clinical on where we use goto_convert? As this PR documents, we make use of it in a number of places well outside the C front-end. To that effect, I'd like to put up for debate whether we do such cleanup before moving files.

[kroening]

• The ansi-c folder is starting to become unmanageable. At bare minimum I'd suggest that we have a new subfolder ansi-c/goto-conversion/ (or some similar name) to hold those files.

Ok, will do.

• As indicated by my comment, but perhaps applicable in more cases: are all those files really all about goto conversion?

No, there's also object construction, but that appears to be intertwined with the conversion. As said in the comment about it, it's also language specific, and hence should move out of the goto-programs folder.

• Is it really correct to assert that only C parse trees can be converted? Isn't it rather the case that we actually have a further intermediate language of codet statements?

This is getting reduced, and I'd like to get rid of it altogether.

• Do we perhaps need to become a lot more clinical on where we use goto_convert? As this PR documents, we make use of it in a number of places well outside the C front-end. To that effect, I'd like to put up for debate whether we do such cleanup before moving files.

We realistically won't do the cleanup. For symtab2gb, this lives outside of the codebase. For jbmc, we don't have the person to do it.

[tautschnig]

• The ansi-c folder is starting to become unmanageable. At bare minimum I'd suggest that we have a new subfolder ansi-c/goto-conversion/ (or some similar name) to hold those files.

Ok, will do.
[...]

Happy to approve once this is done: I think this goes a long way towards making all of my other concerns easy to track (and, if resources ever permit: fix).

[kroening]

Now with ansi-c/goto-conversion subdirectory.

[peterschrammel]

❓ Isn't linking a pure GOTO thing? Why is there a dependency on ansi-c now? This seems to indicate that either some functionality has been moved that should not be moved or that some functionality is used in other modules that shouldn't be used there.

[kroening]

The culprit for this is recreate_initialize_function. I'd like to kill it, and one benefit would be to remove this coupling.

[tautschnig]

Being the one who introduced this function in the first place: can you share some ideas on how to replace it?

[kroening]

As mentioned out-of-band, simply create the goto instructions directly. This should be done separately.