Add support for YAML-witnesses

[schuessf]

The main goal of this PR is to add support for the new YAML-witness format. This includes the following:

• Parsing witnesses (YamlWitnessParser) mostly done by @bahnwaerter. There are several classes for the datastructures of the yaml witnesses entries (LoopInvariant, Metadata, ...). They all implement the interface IYamlProvider that translates them back to an EO-YAML-Object (useful for the witness generation).
• Generate witnesses (YamlCorrectnessWitnessGenerator): The ICFG is traversed to extract invariants. This works similar to the GraphML format. There is a setting, if you want to produce YAML or GraphML witnesses (or both).
• Validate (YamlCorrectnessWitnessExtractor) witnesses: The witnesses are first parsed and then translated to ExtractedWitnessInvariant (same as for GraphML). The validation works based on the file ending, so we are able to validate GraphML- and YAML-witnesses now.

Additionally I made some other changes/refactorings:

• The witness instrumentation does not happen anymore in MainDispatcher, but there is now an interface IExtractedWitnessEntry that allows to transform an ExpressionResult (e.g. can add statements,...). This should simplify the instrumentation and allows also more witness entries in the future more easily (ghost variables, procedure contracts,...). Currently there are two implementation of this interface: ExtractedLocationInvariant (instruments an assert) and ExtractedLoopInvariant (instruments a loop invariant).
• The witness extraction now returns a HashRelation instead of Map, since a location can correspond to multiple witness entries. This holds for now (and eliminates merging of witness-invariants; still used in the old format though), but especially if we have more entries like ghost variables.
• Add WitnessRegressionTestSuite to check the validation of pre-generated YAML/GraphML-witnesses (to check that we do not break the witness validation). For now I added mostly some random SV-COMP witnesses that could be validated on dev (so looks like nothing was broken 😉)

There are still some limitations/open issues:

• The YAML-format allows column numbers, we should also use them, otherwise we might produce faulty witnesses. The problem is that IASTNode does not contain them, but an offset we could use to extract the columns. I made a first attempt here: 8b45bde21bed1e175683b99fccd1003b0c207ed9.
• The YAML-format distincts loop_invariant and location_invariant. Is there any mechanism to distinct this when generating witnesses?
• YAML-violation-witnesses are not supported, but there is also no official format yet.

[schuessf]

You can check if eo-yaml provides support for annotations which we could use to annotate fields of a YAML witness element class to automatically build YAML serializers. This would reduce further maintenance if YAML generation must be extended for new/changed entry types. Is such a feature also available for parsing?

I am not fully aware how to do this. I however just found out that objects can be dumped to YAML at the very least: https://github.com/decorators-squad/eo-yaml/wiki/Java-Bean-To-YAML

How should platform-specific elements (e.g., file paths) encoded in a YAML witness files?

I guess platform-specific file paths are fine and I don't think anything else in the witnesses are platform-specific. Also it is more an info for the user, we don't use this for validation.

Should YAML multi-document witness files also supported?

Why should we generate multiple YAML files? We just want to have one witness and if (in the very future) multi-files projects are supported, the format already has the option to provide multiple source files.

[schuessf]

You can check if eo-yaml provides support for annotations which we could use to annotate fields of a YAML witness element class to automatically build YAML serializers. This would reduce further maintenance if YAML generation must be extended for new/changed entry types. Is such a feature also available for parsing?

I am not fully aware how to do this. I however just found out that objects can be dumped to YAML at the very least: https://github.com/decorators-squad/eo-yaml/wiki/Java-Bean-To-YAML

While this works, it is not quite suitable for us. It extracts all methods using reflections and adds them as keys to YAML, therefore we also have e.g. hashCode and toString keys. Therefore I decided to implement this on my own in 5eb799a. This extracts all getters using reflections and builds a map with them (slightly renamed) as keys.