New binary for inspection of properties of goto-programs: goto-inspect

[NlightNFotis]

Hello,

In #7377, Michael identified an issue with goto-instrument and the dumping of goto-binaries: namely, that we get to do some instrumentation before we show the goto-functions if a user has asked for them.

In investigating how to add support for this in goto-instrument, I discovered that the way we inspect properties of goto-binaries (either properties/assertions, goto-functions, etc) is not consistent between different tools.

It then striked me as a potential streamlining of our tools to offload the inspection of binaries to a single tool, which does no instrumentation, and start sunsetting these options (or hint that they are deprecated when a user activates the command line options, and direct them to this tool over time) would be of benefit:

1. It makes binary inspection consistent across tools (in that it no longer suffers from instrumentation sequencing issues),
2. It stops saturating different tools with more options on manipulating goto-programs,
3. It allows narrower focus of some tools (say, offloading some work from CBMC in preparation for core-BMC.

In this spirit, I have authored PR #7673, which is now a draft, but I would like to get some thoughts from the community before I go forward and merge the PR.

Some questions:

1. Is the streamlining opportunity as evident to others as it is for me?
2. Am I missing something in the usage of the tools we already have that this move is disturbing?
3. Could there be a better way to approach this issue? Or do we think that this is a good solution to the greater problem?

[martin-cs]

Some fragments of answers:

• These are old options and widely used, I am a little concerned about removing them.
• We should aim to remove unnecessary variation in instrumentation and processing. I have committed patches to try to normalise this a bit. There is more that can be done.
• Then there is a question about what is necessary variation in instrumentation. This touches on the normal form discussion ( RFC: Documenting and checking "normal form" properties of goto_models #6495 ).
• It used to be that --show-goto-functions was after the instrumentation passes and before the actual analysis. This meant that you could see the effect of each instrumentation by diffing the output of --show-goto-functions and --show-goto-functions --cool-instrumentation. I am not sure how having a separate tool allows this without many calls to goto-instrument.
• goto-instrument used to have the most minimal processing so that it could be used for the same role as the proposed tool.

[tautschnig]

I'm generally in favour of (well, I'd say in Version 6) removing options from goto-instrument, and possibly also other tools, very much in the spirit of a narrower focus of tools. (I like the Unix philosophy "Make each program do one thing well.") So what we could perhaps do:

1. Introduce the new tool now.
2. Remove the options from other tools as part of the Version 6 release.

[NlightNFotis]

I am also in favour of the approach suggested by @tautschnig (and the tool was designed with this philosophy in mind).

I think we can proceed with the current tool being added for now (it doesn't seem to cause any harm), and over time experiment to see we can get closer to what Martin (cleaning up the other tools to make them consistent).

If that is harder than anticipated, then we can proceed with removing the inconsistent functionality of the other tools and focusing our implementation on just one tool.