Including functionality from goto-instrument in another tool

[martin-cs]

A "how do you want it done" type question @kroening @tautschnig @peterschrammel

I want to use the reachability slicer (in goto-instrument/reachability-slicer*) in goto-analyze after (domain specific) simplification to remove unconditional gotos and unreachable code. This would break the rule of "folders for tools contain their code and solely their code". So it seems the right thing to do is to move it into goto-programs.

Any objections / better ideas?

[peterschrammel]

Ideally, reusable classes should not be in tool folders. Practically, this rule is currently broken in many places, eg. Also by goto-instrument/cover.h used by cbmc.

[tautschnig]

I do agree with @peterschrammel that the rule is already broken a number of times; code should get moved, but doing so has a whole lot of implications (in particular: breaking too many pull requests) so maybe it's better to make sure newly added code is put in the right place (analyses/).

With regards to your specific implementation bit, doesn't the dominator analysis provide what you really need, i.e., you don't actually need the slicer? But I could be wrong/lacking sufficient context.

[martin-cs]

On Tue, 2016-11-15 at 03:03 -0800, Michael Tautschnig wrote:

I do agree with @peterschrammel that the rule is already broken a number of times; code should get moved, but doing so has a whole lot of implications (in particular: breaking too many pull requests) so maybe it's better to make sure newly added code is put in the right place (analyses/).

Fair. Perhaps around / after the next release we should have a "stop
and tidy up" period for changes that will break stuff. It would give
people an incentive to get their patches merged :-)

With regards to your specific implementation bit, doesn't the dominator analysis provide what you really need, i.e., you don't actually need the slicer? But I could be wrong/lacking sufficient context.

The simplifier mode of goto-analyze can replace some branch conditions
with true or false (especially for unwound loops!) and I'd like to do
the appropriate removal of instructions / linearisation of branches. If
I can do this with something less than the reachability slicer I'm very
open to suggestions (esp. as the reachability slicer seems broken on the
code I'm generating).

Cheers,

• Martin

[thomasspriggs]

I think the original question of "How should it be done?" and "How is it done?" have already been answered. Therefore I am going to close this issue out.

[martin-cs]

Thanks; I should have closed this at the time.