Add capability to export goto-program in symex-ready-goto form to CBMC.

[NlightNFotis]

This allows CBMC to dump the goto-program when it is in symex-ready-goto form in a file on disk (when it is just before SYMEX, and all transformations have been applied).

• 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.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Patch coverage: 88.23% and project coverage change: -0.02 ⚠️

Comparison is base (ce4c504) 78.56% compared to head (1e26b7f) 78.55%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7697      +/-   ##
===========================================
- Coverage    78.56%   78.55%   -0.02%     
===========================================
  Files         1685     1685              
  Lines       192927   192979      +52     
===========================================
+ Hits        151579   151596      +17     
- Misses       41348    41383      +35     

Impacted Files	Coverage Δ
src/cbmc/cbmc_parse_options.cpp	80.13% <88.23%> (+0.33%)	⬆️

... and 17 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.

[esteffin]

Looks good to me

[thomasspriggs]

⛏️ I think that ideally the contents of cmdline should be validated and written to options in the cbmc_parse_optionst::get_command_line_options function, before the options are acted on at this point in the control flow. This helps separate the validation of the command line arguments supplied by the user from the code which acts on the options that are specified by those arguments. Think of cmdline as being the parse tree and options as being the setting being acted upon.

[NlightNFotis]

Done.

[thomasspriggs]

❔ What happens if the user specifies --export-core-goto without specifying an output filename?

[NlightNFotis]

I have added extra checks for a missing filename.

[thomasspriggs]

I think this check belongs back where the option is set. That way we can halt processing before going to the effort of building the goto-model in memory.

[thomasspriggs]

⛏️ bool please?

[thomasspriggs]

⛏️ I'd put these 2 lines in an else block. Just so that the two blocks of code of equivalent control flow significance are at the same level of indentation.

[kroening]

Please reconsider the name "core goto". This word carries no meaning for users. How about "pre-symex-goto".

Is there a particular reason to have this facility in CBMC, as opposed to goto-instrument?

[NlightNFotis]

Hi @kroening,

The name core-goto comes from the concept added in the documentation #7505, in January. This is defined as the input program after necessary instrumentation and all the simplification steps, and that name will carry meaning for both developers and users going forward.

Since core-goto is already in the documentation/repository, we would prefer to keep the terminology for this PR. If you have suggestions for a better name, we'd happily consider this in a later PR that renames globally rather than conflating renaming other in parts of the codebase with the functionality here.

---

With regards to the flag being added to cbmc and not to goto-instrument, this location we added it to is the spot at which we maintain the highest confidence that the goto-model is in core-goto form - but we keep an open mind as to alternatives that would have the same effect.

The primary challenge with experimenting with altenative locations for the implementation is that we can't remain confident about the state of the goto-program in those alternative locations, and given the lack of a programatic check for the model being in core-goto form, we decided to be conservative in an effort to be correct in terms of program semantics.

Note that once your PR #7695 is merged we can check that a goto model is in core-goto form, and so safely output core goto from other binaries such as goto-instrument.

[kroening]

The name core-goto comes from the concept added in the documentation #7505, in January. This is defined as the input program after necessary instrumentation and all the simplification steps, and that name will carry meaning for both developers and users going forward.

I would strongly urge to revisit this terminology. We have a multi-backend strategy, and every backend will have a different set of requirements on the language features it handles well. Hence, there is no "core". I do not see how you can establish a particular goto program form as a "core" given that both consumers and producers have very different needs.

[thomasspriggs]

👍

[kroening]

I am adding a block on this PR because I'd like to settle the discussion on the idea of a "core goto program".

[TGWDB]

I am adding a block on this PR because I'd like to settle the discussion on the idea of a "core goto program".

As described in previous PR #7505 the "core goto" is choosing a place where all required instrumentation/simplification transforms have been done for the goto program to be consumable by symex/checking. So I see there being two potential areas of discussion and resolution.

1. There is sufficient interest in such a form of goto program to warrant the ability to: check it is in this form, output it to file, or read it in and send it to symex/checking. I believe there is such interest, which leaves your concern being about the naming. Thus, I'd propose that here we progress down finding the right name for this form and then merge this PR (with that new name, or doing it in an immediate follow-up that also renames documentation introduced in Added concept of core goto language form #7505 ).
2. There is a broader discussion about which points/forms of a goto program are interesting should be handled in some special ways (and have names?). Ideally we'd like to be able to check all the potential goto program forms, and other things such as output/input of any form could have some utility (maybe this is more the domain of tools like goto-instrument that can carefully transform between forms). However, I'd argue that this is beyond the scope of this PR.

With the above in mind, let's progress down path 1 here. I believe there is desire to decouple the form from the concept of symex and consider it to be a form suitable for many kinds of checkers. I'd like to hear opinions on "checkable-goto" or other potential names (in addition to "core goto" and "pre symex goto") to see if we can agree on something that is expressive and helpful. (I'm not sure my name suggestion is great, but wanted to get the discussion started ASAP.)

[kroening]

It's really essential here to think beyond symex.

We want to be able to deliver a portfolio of backend engines/solvers for the same verification task. In particular, we want to phase out BMC in favour of methods that can do unbounded proof.

These backends will have vastly different requirements about the goto features that they support or handle well. It therefore doesn't make sense to identify one single set of features as "core".

Furthermore, it is important not to do the modelling equivalent of "premature optimisation". You want to stay high-level as long as possible, as it is difficult to undo any lowering once it has happened.

[kroening]

Some squashing would be nice.