Simplify implementation of YAML witnesses #668
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
bahnwaerter
reviewed
May 28, 2024
...ate/plugins/generator/cacsl2boogietranslator/witness/GraphMLExtractedCorrectnessWitness.java
Outdated
Show resolved
Hide resolved
...timate/plugins/generator/cacsl2boogietranslator/witness/YamlExtractedCorrectnessWitness.java
Outdated
Show resolved
Hide resolved
| location: | ||
| file_name: contract.c | ||
| file_hash: UNUSED |
trunk/examples/witness-checking/regression/correctness/contract.c-witness.yml
Show resolved
Hide resolved
...ate/plugins/generator/cacsl2boogietranslator/witness/GraphMLCorrectnessWitnessExtractor.java
Show resolved
Hide resolved
...e/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/YamlWitnessParser.java
Show resolved
Hide resolved
...rc/de/uni_freiburg/informatik/ultimate/witnessprinter/preferences/PreferenceInitializer.java
Show resolved
Hide resolved
...de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlCorrectnessWitnessGenerator.java
Show resolved
Hide resolved
...ssPrinter/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriter.java
Show resolved
Hide resolved
...Printer/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriterV0.java
Show resolved
Hide resolved
bahnwaerter
approved these changes
May 29, 2024
schuessf
force-pushed
the
wip/fs/yaml-witnnes-refactoring
branch
from
71b46da
to
a136772
Compare
schuessf
force-pushed
the
wip/fs/yaml-witnnes-refactoring
branch
from
a136772
to
ce97273
Compare
maul-esel
approved these changes
Aug 7, 2024
...tik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedFunctionContract.java
Outdated
Show resolved
Hide resolved
...ate/plugins/generator/cacsl2boogietranslator/witness/GraphMLCorrectnessWitnessExtractor.java
Outdated
Show resolved
Hide resolved
...timate/plugins/generator/cacsl2boogietranslator/witness/YamlCorrectnessWitnessExtractor.java
Outdated
Show resolved
Hide resolved
schuessf
force-pushed
the
wip/fs/yaml-witnnes-refactoring
branch
from
ce97273
to
1a6cfd7
Compare
- function_contracts are contained in the invariant_set - the format for location_invariant and loop_invariant remains unchanged - since the format is now downwards compatible, the version number changes from 3.0 to 2.1 - see https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/-/tree/2.1-function-contracts-dev for the format for function contracts
We always generate the same witness independent from the format version. Therefore WitnessSetEntry was removed and we have different writers instead. The toMap method was removed from WitnessEntry, since it was specific to format version 0.1. Only some common classes for the different format versions still provide a toMap method.
- only parse the entries from the YAML witness that are necessary for the validation - produce the other entries only in YamlWitnessWriter without storing them in the witness object itself - remove Invariant, Metadata, Producer, Task and produce nested maps directly in MetadataProvider and YamlWitnessWriter
This label is only required for GraphML. Instead there is now an interface IExtractedCorrectnessWitness with two implementations, one for GraphML and one for YAML, and only the GraphML implementation uses the label internally (using the internal class LabeledInvariant). Therefore it is no more required to parse the UUID from the YAML witness.
This should be done by witness linter in SV-COMP
schuessf
force-pushed
the
wip/fs/yaml-witnnes-refactoring
branch
from
1a6cfd7
to
dd23793
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR attempts to simplify the implementation for YAML witnesses. The format has completely changed just before SV-COMP 2024 and thus the previous implementation for YAML witnesses was just an ad-hoc adaptation to the changed format.
invariant_set(as in version 2.0), therefore the format for function contracts is downwards compatible and thus the format version was changed from 3.0 to 2.1WitnessEntryhad the methodstoMapandtoSetEntryfor the string-conversion to format version 0.1 and 2.0 respectively. Instead of these methods, we have now two different writer-classes that decide which entries should be considered (function contracts should only be exported in version >= 2.1) and how the entries should be formatted in YAML.YamlWitnessParser. Metadata are only needed for witness export, which are now produced using the introduced classMetadataProviderMainDispatcherthat each entry is only instrumented once. This is however only specific to GraphML-witnesses. Therefore I added an interfaceIExtractedCorrectnessWitnessas an abstraction for the extracted witness entries from GraphML and YAML witnesses and only the GraphML-implementation uses these labels internally. For YAML witnesses we can already ensure that each entry is only instrumented once during extraction.After this PR is merged, #653 needs to be reworked.