Refactor: Use appropriate control configurations in trace checks

[maul-esel]

As discussed internally, this is an attempt at fixing the detection of perfect interpolant sequences, and some other usages of the control locations (or in the case of concurrent programs, control configurations) visited along a counterexample trace.

Motivation

At various points of the code, we either used the IcfgLocation returned by IIcfgTransition::getSource (usually via TraceCheckUtils::getSequenceOfProgramPoints) or the predicate in the IRun for the counterexample.

• The IcfgLocations do not make sense in the context of concurrent programs, we want the whole control configuration, i.e., the locations of all threads.
• The run predicates are typically not what is intended either. If the run is a run of the difference automaton between program and interpolant automata, and is found by DFS or BFS, it will never contain any repeated state, and is thus useless for determining isPerfect.

Changes

1. In places where the control configurations / states of the run are not needed at all, I have replaced IRun by Word. 1.1 This includes usages in LassoChecker, where, according to @Heizmann, any emphasis on the usage of "perfect" proofs was unintentional.
2. In other places, I have replaced an IRun by a new class Counterexample<L>, which bundles the trace (a Word<L>) and an optional List<Object> controlConfigurationSequences.
   • 2.1 The type of configurations is Object, any type will do -- we only care about equality of instances (as defined by Object::equals).
   • 2.2 It is easier to pass some list rather than creating an IRun on the original program (e.g. a CEGAR loop's initial abstraction).

As a lot of these changes touch code I am unfamiliar with, I would appreciate it if someone with more knowledge could take a look, in particular for accelerated interpolation and assert order modulation. @danieldietsch?

Evaluation

The nightly tests look fine: https://jenkins.sopranium.de/job/Ultimate/job/Ultimate%20Nightly/job/wip%252Fdk%252Fperfect-tracechecks/4/testReport/

Once the current evaluations are finished, I will run a fast SV-COMP run on this branch to stress-test these changes, and also to see if the "correct" notion of perfect proofs for concurrent programs has any positive impact.

Update: SV-COMP evaluation is currently running.

[maul-esel]

The conflict is with the addition of the new Fox refinement strategy. I'll rebase after I have run the SV-COMP evaluation, because the current base is our reference point for the comparison.

[Heizmann]

I did not find the place where we really see a benefit from the removal of IRun. Can you point me to it so that I can have a closer look?

TraceChecks were made for for sequences of IActions. Perfect Interpolants and Assert Orders and an additional bonus that are sometimes desired and that require and additional sequence of control configurations.

• We must separate the sequence of IActions from the sequence of control configurations in order to maintain support for applications that provide only a sequence of IActions.
• A run is a concept from automata theory. It is misleading to utilize a object with this name for other applications. (Would you use ComplexNumber for storing temperature and humidity only because the ComplexNumber can store two reals?)

In contrast, I see many places that become more convoluted and difficult to understand, in particular because word and sequence of control locations is now separated. This leads to passing null or returning pairs, having even more parameters, and generally obfuscating the relation between things. It was a major concern for me to not let that happen.

Please introduce some wrapper class that combines both and perhaps provides helpful abstractions. In contrast to IRun, it can make its control location sequence optional, but then we should ensure that we fail early, i.e., that strategy modules that require control sequences fail if they are not provided with them.

Our TraceChecks are work in progress. We have to try to keep them as simple and as modular as possible. Let us pass null for the sequence of control configurations if there is no sequence of control configurations. Wrapper classes and additional abstractions will make our TraceChecks even more convoluted.

[danieldietsch]

I am not arguing for keeping IRun. I am arguing for adding a new type that describes a trace and optional metadata.