-
Notifications
You must be signed in to change notification settings - Fork 41
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support witnesses with ghost variables #653
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
Outdated
Show resolved
Hide resolved
...formatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostUpdate.java
Show resolved
Hide resolved
...rmatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostVariable.java
Show resolved
Hide resolved
.../ultimate/plugins/generator/cacsl2boogietranslator/witness/IExtractedWitnessDeclaration.java
Show resolved
Hide resolved
...ce/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/GhostUpdate.java
Show resolved
Hide resolved
.../WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/GhostVariable.java
Show resolved
Hide resolved
...nessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/ILocationProvider.java
Outdated
Show resolved
Hide resolved
Needs to be revised (after SV-COMP), because the format for YAML witnesses has changed and we also use a different parser. |
5734683
to
3a3bcc2
Compare
8394148
to
6fc2df3
Compare
e40b1f5
to
8d13ce8
Compare
8d13ce8
to
b44c828
Compare
b44c828
to
7624e83
Compare
7624e83
to
6fce7ec
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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/correctness/case_distinction.c-witness.yml
Outdated
Show resolved
Hide resolved
trunk/examples/witness-checking/regression/correctness/mutex.c-witness.yml
Outdated
Show resolved
Hide resolved
...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java
Outdated
Show resolved
Hide resolved
.../de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainDispatcher.java
Outdated
Show resolved
Hide resolved
@@ -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")); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
Outdated
Show resolved
Hide resolved
...ce/WitnessParser/src/de/uni_freiburg/informatik/ultimate/witnessparser/yaml/GhostUpdate.java
Show resolved
Hide resolved
...Printer/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriterV2.java
Outdated
Show resolved
Hide resolved
...formatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedGhostUpdate.java
Show resolved
Hide resolved
...Printer/src/de/uni_freiburg/informatik/ultimate/witnessprinter/yaml/YamlWitnessWriterV2.java
Outdated
Show resolved
Hide resolved
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):
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great! Now the implementation follows our final correctness witness schema with ghosts.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good! I only left some minor comments.
trunk/examples/witness-checking/regression/concurrent/AutomizerC.xml
Outdated
Show resolved
Hide resolved
final ExpressionResult res = ghost.getInitializationResult(mainDispatcher); | ||
staticObjectsHandler.addStatementsForUltimateInit(res.getStatements()); | ||
for (final var d : res.getDeclarations()) { | ||
staticObjectsHandler.addGlobalVarDeclarationWithoutCDeclaration((VariableDeclaration) d); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
question: what are these declarations? how are they related to the declaration added after the loop? should all of them be global?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Previously res
itself contained the declarations. This was however changed, this loop can be removed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can the initialization require declarations of other variables? e.g. auxvars? (though they should probably not be global)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we said in the schema that the expression may be any expression over global variables, right @bahnwaerter?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(side-effect-free and without undefined behaviour, of course)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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...
// 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) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
6445b06
to
a60ea41
Compare
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? |
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 |
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.
4a4c57e
to
d55e39c
Compare
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
andghost_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).