New Execution Model

[CapZTr]

In this PR a new implementation of execution model called ExecutionModelNext is added. With the new model more Events (Locals and Asserts) and Relations (theoretically all the Relations defined in the .cat files) can be shown in the witness graph.

Similar as the old one, the new model serves as the representation of an execution in Dartagnan. The two models hold similar information which is organized in similar names and formats. But they two differ in the following:

1. The new model acts as a data structure only. Behaviors of extracting Events, Relations and MemoryObjects out of the model are separated and implemented in three corresponding Managers: EventModelManager, RelationModelManager and ExecutionModelManager. Besides ExecutionModelNext, we have RelationModels and EventModels representing Relations and Events, respectively.
2. All the methods which invoke generateGraphvizFile() of ExecutionGraphVisualizer use the new model. In other words, the new model is utilized for witness generation only, while the CAATSolver still uses the old model.

As explained above, the new model does NOT replace the old one so far. They have to coexist, which can be seen as a repetition of some data structures and functionalities and needs further refinements.

[hernanponcedeleon]

I ran the CI 3 times and each time there is a different set of benchmarks failing. Both ms and dglm are always there, but I suspect they will stop failing once we merge #784. This only means that the bug (whatever it is) is not uncovered when using C11 rather than IMM as a compilation target. The benchmarks failing non-deterministically are mutex or musl_mutex (some of the variants with /without relaxation).

Based on a quick check to the changes in this PR, I suspect the issue in not in this code. The non-determinism of the problem makes me believe this is yet another issue with the alias analysis.

[ThomasHaas]

I don't see why the alias analysis should be the culprit. This PR should not introduce any semantic changes and not affect solving at all, thus it should not be able to uncover any new bugs.
The issue is more likely due to the fact that ExecutionModel was changed to now include local events, which will throw off the CAAT solver. I assume this change is unintended.
More generally, changes to the RefinementSolver class were made (and some underlying solver classes) which are also likely to break something.

[ThomasHaas]

What are the goals of the new execution model?
Is it a goal to have a general-purpose execution model/witness format that is independent from SMT solving?
Is it a goal to have an exchangable execution format, i.e., it should be dumpable/parsable (at least in principle)?
Any other possible goals?

[hernanponcedeleon]

I still need to review the RelationModelManager. Will try to do that one tomorrow

[hernanponcedeleon]

It is not clear to me where is the code there is the distinction between what we want to display in a graph (the "visualizer") and the model per se (which should be used to compute derived relations). We discussed the bug due to co not having the whole transitive closure, but the same would probably happen for po

[hernanponcedeleon]

LGTM

[ThomasHaas]

I think the code is good enough to merge now :)