Support witnesses with ghost variables #653

schuessf · 2023-10-25T12:04:36Z

This PR adds support for the validation of witnesses that contain ghost variables. Namely the entry-types (that are not official yet) in YAML-witnesses ghost_variable and ghost_update can now be handled in the validation. The validation of those entry-types works in a similar fashion to the existing entry-type invariant: We translate them to ACSL, s.t. the entries instrumented are in our Boogie-Code. This instrumentation uses ghost code in ACSL that is now supported (see #649).

bahnwaerter

Thanks @schuessf for your great work. Your changes look good to me. However, make sure that new files always contain a license header.

...k/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedCorrectnessWitness.java

...formatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostUpdate.java

...rmatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostVariable.java

.../ultimate/plugins/generator/cacsl2boogietranslator/witness/IExtractedWitnessDeclaration.java

...ce/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/GhostUpdate.java

.../WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/GhostVariable.java

...nessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/ILocationProvider.java

schuessf · 2023-11-08T13:35:55Z

Needs to be revised (after SV-COMP), because the format for YAML witnesses has changed and we also use a different parser.

maul-esel

Thanks for adding this support. I've looked through the changes and marked some points that could be improved or clarified.

trunk/examples/witness-checking/regression/AutomizerC.xml

trunk/examples/witness-checking/regression/correctness/case_distinction.c-witness.yml

trunk/examples/witness-checking/regression/correctness/mutex.c-witness.yml

...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java

.../de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainDispatcher.java

maul-esel · 2024-08-13T08:04:33Z

...e/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/YamlWitnessParser.java

@@ -92,6 +108,19 @@ private static Stream<WitnessEntry> parseWitnessEntry(final Map<String, Object>
 		}
 	}

+	private static GhostVariable parseGhostVariable(final Map<String, Object> entry) {
+		return new GhostVariable((String) entry.get("name"), (String) entry.get("initial"), (String) entry.get("scope"),
+				(String) entry.get("type"));


This seems similar but slightly different from the case GhostVariable.NAME code above. What is the reason to have both? Does it have to do with different versions of the format?

Yes, exactly, this function is used for the format version 2.1 (therefore this function is called in the case "ghost_instrumentation"), while the one above is used for version 0.1. The slight difference is variable vs. name as field name for the name of the ghost variable.

See above: It seems like a lot of effort just to keep supporting a draft format version proposed in a workshop talk. If we update our artifact repo for the workshop to point to the ULTIMATE version where this format is supported, I think we can safely abandon the old format going forward.

Since the format was now adapted and Goblint also supports the new format, I removed ghost variables in version 0.1.

...e/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/YamlWitnessParser.java

...ce/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/GhostUpdate.java

...Printer/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriterV2.java

...formatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostUpdate.java

...Printer/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriterV2.java

bahnwaerter · 2024-08-30T09:16:51Z

An important note: The current implementation does not follow the intended witness schema for ghost variables. The following things are different and should be changed in my opinion (in order to remain backwards compatible with the original style of the schema):

ghost_variables and ghost_updates are not put under content (like the invariant_set entry type does).
Expressions of ghost_variables and ghost_updates are not represented correctly. They are composed of a value and format field instead of directly assigning the value to the expression field.

bahnwaerter

Looks great! Now the implementation follows our final correctness witness schema with ghosts.

maul-esel

Looks good! I only left some minor comments.

trunk/examples/witness-checking/regression/concurrent/AutomizerC.xml

trunk/examples/witness-checking/regression/sequential/AutomizerC.epf

maul-esel · 2024-09-02T21:01:26Z

.../de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainTranslator.java

+				final ExpressionResult res = ghost.getInitializationResult(mainDispatcher);
+				staticObjectsHandler.addStatementsForUltimateInit(res.getStatements());
+				for (final var d : res.getDeclarations()) {
+					staticObjectsHandler.addGlobalVarDeclarationWithoutCDeclaration((VariableDeclaration) d);


question: what are these declarations? how are they related to the declaration added after the loop? should all of them be global?

Previously res itself contained the declarations. This was however changed, this loop can be removed.

Can the initialization require declarations of other variables? e.g. auxvars? (though they should probably not be global)

Currently this is not possible, since we (luckily) restricted the ghost updates, s.t. they can only have a primitive type and their initial value can only be a constant expression. If we wanted to be less restrictive, we probably need to adapt this anway (as it seems, we cannot add aux-vars or local declarations to the init-procedure here).

I think we said in the schema that the expression may be any expression over global variables, right @bahnwaerter?

(side-effect-free and without undefined behaviour, of course)

The only variables allowed in this expression are the global variables of the program.
The expression is evaluated after global variables declared in the program are initialized.

Okay, I see, then there might be aux-vars involved, e.g. if a ghost variable is initialized by a read of a global array.
But in that case the second sentence is problematic. Currently we initialize the ghost variables (in ULTIMATE.init) before the program. To match the specification, we would need to initialize the ghost variables at the very end, i.e., between dispatching the actual program, but before calling PostProcessor (where the ULTIMATE.init procedure is actually build).
I tried to implement this in f6123d9, but I am not sure, if this is a nice solution...

maul-esel · 2024-09-02T21:04:50Z

...formatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostUpdate.java

+			// Make the ghost update itself atomic and insert it just before the fork.
+			// TODO: Maybe we should do this atomically, but the CFG builder crashes for that case
+			// We are not sure, if this does have any different semantics.
+			return new ExpressionResultBuilder(expressionResult).addAllExceptLrValueAndStatements(witness)


We should look into this and see if CfgBuilder can be modified to support this; perhaps next week.

It's not a blocker for the merge though.

schuessf · 2024-09-04T11:53:56Z

This PR has canged the behaiour for location invariants, they are now added inside an atomic-block. Therefore some witness-tests (e.g. this) fail now with an AssertionError: Atomic section must begin with ICFG location.

@maul-esel Since you worked recently on atomic blocks, why is this the case?

maul-esel · 2024-09-07T11:35:47Z

The problem seems to be an atomic block in dead code, due to a wrong instrumentation of invariants pointing to labels. The instrumented Boogie program contains the following code:

    ...
    #res := 0;
    return;
    atomic {
        assert false;
    }
  ERROR:
    assert { :reach "ERROR_FUNCTION","reach_error" } false;
    ...

The witness specifies the invariant false at the location for the label. I don't know if we have definitively fixed the semantics for location invariants at labels, but I would expect them to hold whenever one jumps to the label. I've committed a fix for these cases, have a look if you agree.

maul-esel · 2024-09-07T11:37:52Z

Incidentally, to add regression tests for these kinds of bugs (the instrumentation was wrong, even if the atomic wouldn't have caused it to crash) we would need to support tests where we expect a witness to be rejected. We should add that in the future (maybe we can base it on our planned experiments comparing with other validators).

The atomicity of the ghost update depends on the C-statement at the given location. For now we only support locations where calls to these functions occur (we can extend this in the future): * __VERIFIER_atomic_begin: The ghost update is inserted just after the call to add it to the atomic block * __VERIFIER_atomic_end: The ghost update is inserted just before the call to add it to the atomic block * pthread_create: The ghost update is inserted atomically just before the call * pthread_mutex_lock / pthread_rwlock_rdlock / pthread_rwlock_wrlock: The ghost update is made atomically with the call to the locking function * pthread_mutex_unlock / pthread_cond_wait / pthread_rwlock_unlock: The ghost update is made atomically with the call to the unlocking function

The format has changed since and the tests were slightly modified, since in the current version we only allow specific locations for ghost updates.

schuessf requested review from maul-esel, bahnwaerter and danieldietsch October 25, 2023 12:04

danieldietsch approved these changes Oct 26, 2023

View reviewed changes

bahnwaerter requested changes Oct 26, 2023

View reviewed changes

bahnwaerter approved these changes Oct 26, 2023

View reviewed changes

schuessf marked this pull request as draft November 7, 2023 14:36

schuessf force-pushed the wip/fs/witness-ghost branch from 5734683 to 3a3bcc2 Compare January 24, 2024 16:13

schuessf marked this pull request as ready for review January 24, 2024 16:48

schuessf force-pushed the wip/fs/witness-ghost branch 4 times, most recently from 8394148 to 6fc2df3 Compare February 8, 2024 09:43

schuessf force-pushed the wip/fs/witness-ghost branch from e40b1f5 to 8d13ce8 Compare February 20, 2024 09:38

schuessf force-pushed the wip/fs/witness-ghost branch from 8d13ce8 to b44c828 Compare April 24, 2024 11:38

schuessf mentioned this pull request May 27, 2024

Simplify implementation of YAML witnesses #668

Merged

schuessf marked this pull request as draft May 28, 2024 16:10

schuessf force-pushed the wip/fs/witness-ghost branch from b44c828 to 7624e83 Compare July 2, 2024 16:02

schuessf force-pushed the wip/fs/witness-ghost branch from 7624e83 to 6fce7ec Compare August 8, 2024 10:20

schuessf marked this pull request as ready for review August 8, 2024 10:20

maul-esel requested changes Aug 13, 2024

View reviewed changes

maul-esel reviewed Aug 13, 2024

View reviewed changes

...Printer/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriterV2.java Outdated Show resolved Hide resolved

bahnwaerter approved these changes Aug 13, 2024

View reviewed changes

bahnwaerter approved these changes Aug 14, 2024

View reviewed changes

bahnwaerter approved these changes Sep 2, 2024

View reviewed changes

maul-esel approved these changes Sep 2, 2024

View reviewed changes

schuessf force-pushed the wip/fs/witness-ghost branch from 6445b06 to a60ea41 Compare September 3, 2024 08:31

schuessf and others added 6 commits September 9, 2024 16:57

Allow parsing witnesses with ghost variables

6a3f776

Allow writing ghost witnesses to YAML

bf0d8c1

Add examples from VEWIT to regression tests

0cff8b8

The format has changed since and the tests were slightly modified, since in the current version we only allow specific locations for ghost updates.

Split witness tests, use inlining for concurrent tests

0e8c7e6

fix instrumentation of location invariants at labels

d55e39c

schuessf force-pushed the wip/fs/witness-ghost branch from 4a4c57e to d55e39c Compare September 9, 2024 15:06

schuessf merged commit d55e39c into dev Sep 9, 2024
1 check was pending

schuessf deleted the wip/fs/witness-ghost branch September 9, 2024 15:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support witnesses with ghost variables #653

Support witnesses with ghost variables #653

schuessf commented Oct 25, 2023

bahnwaerter left a comment

schuessf commented Nov 8, 2023

maul-esel left a comment

maul-esel Aug 13, 2024

schuessf Aug 13, 2024

maul-esel Aug 13, 2024

schuessf Sep 2, 2024

bahnwaerter commented Aug 30, 2024 •

edited

Loading

bahnwaerter left a comment

maul-esel left a comment

maul-esel Sep 2, 2024

schuessf Sep 3, 2024

maul-esel Sep 3, 2024

schuessf Sep 3, 2024

maul-esel Sep 3, 2024

maul-esel Sep 3, 2024

schuessf Sep 3, 2024

maul-esel Sep 2, 2024

schuessf commented Sep 4, 2024

maul-esel commented Sep 7, 2024

maul-esel commented Sep 7, 2024

Support witnesses with ghost variables #653

Support witnesses with ghost variables #653

Conversation

schuessf commented Oct 25, 2023

bahnwaerter left a comment

Choose a reason for hiding this comment

schuessf commented Nov 8, 2023

maul-esel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bahnwaerter commented Aug 30, 2024 • edited Loading

bahnwaerter left a comment

Choose a reason for hiding this comment

maul-esel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

schuessf commented Sep 4, 2024

maul-esel commented Sep 7, 2024

maul-esel commented Sep 7, 2024

bahnwaerter commented Aug 30, 2024 •

edited

Loading