Example for a correctness witness contains forbidden data key control

[MartinSpiessl]

The example multivar_true-unreach-call1.graphml for a correctness witness in this repository contains control annotations like the following:

<edge source="N22" target="N16">
<data key="sourcecode">[!(x &lt; 1024)]</data>
<data key="startline">12</data>
<data key="startoffset">305</data>
<data key="control">condition-false</data> <!-- this line is problematic-->
</edge>

According to the README.md, the data key control may only be used in violation witnesses, not in correctness witnesses. Here it is of course the case that the other branch is also present in the witness, so the automaton is still an observer automaton.

This probably means that the README.md needs to be updated/fixed in a way that does not break current implementations.
Enforcing the current rules might also be possible, we would need to do a quick survey on how widespread people are using the control data key in correctness witnesses.

[sim642]

This worries me now in general because when I implemented correctness witness generation in Goblint I also chose to ignore this rule and add controls to correctness witnesses because both the examples and correctness witnesses from other verifiers I looked at seemed to do that generously.

If de facto this is common in existing verifiers, then it seems to me like the README rules should be updated to also allow that. This change wouldn't punish any existing verifiers so there should be no harm.

---

And besides the README example, the new testing example also has this:

sv-witnesses/lint/test/program/simple/simple_correct.graphml

Lines 57 to 63 in e9bfcb8

	<edge source="N6" target="N8">
	<data key="startline">4</data>
	<data key="endline">4</data>
	<data key="startoffset">56</data>
	<data key="endoffset">59</data>
	<data key="control">condition-true</data>
	</edge>

[MartinSpiessl]

A opinion survey in the SV-COMP meeting showed that people would mostly welcome if this were more actively enforced, i.e., the examples in this repository should be fixed (instead of changing the witness format specification).

And besides the README example, the new testing example also has this:

Yeah, I just added that to get some way of testing the linter. That witness was produces with CPAchecker, which up until now (I am working on the fix currently) outputs control into correctness witnesses. This simle_correct.graphml needs of course to also be fixed then.

Basically we will just omit the control keys for the witnesses of CPAchecker, this should also be easy for you to do.

[danieldietsch]

Ultimate also adds control to the correctness witness.

Is there a reason to remove it? It seems easier to change the README.

Actually, reading the README again, it seems that changing the README is the best fix, because it is less likely to affect existing implementations.

[MartinSpiessl]

One argument for not allowing it is because its semantics are that parts of the state space are removed, so this can potentially be harmful if a validator then removes a branch for which there is no control edge end then errors in that part of the state space are ignored.

Another argument regarding fairness was made: it would be unfair to tools who stick to the format spec if this has disadvantages regarding validation (maybe a validator might have trouble validating a witness in case there are no control keys).

I am also not really sure whether removing it from the correcntess witnesses is really the best solution, I wouldn't have done it, but the opinion poll was quite clear ( 7 to 2, not counting myself). I would have welcomed to address this next year and ignore it for now.

Do you have a proposal for how the README would be changed to clarify things? Would the control key get a different semantics depending on the witness type (i.e., something like "these need to be ignored by the validators in case of correctness witnesses").

[danieldietsch]

I can only say: allowing the key is not the same as requiring it. It seems to me that the README was just a typo, seeing that both Ultimate and CPAChecker generate this key.

My proposal for a correction is: Change the table in section Edge Data for Automata Transitions by changing the row for control. Just switch Allowed in Correctness Witnesses from No to Yes.

control actually does not add much in terms of semantics. It is supposed to make it easier for validators or visualizers.
The only semantic difference can arise if I mislabel things, i.e., if I label the else transition with condition-true.

[MartinSpiessl]

I think in CPAchecker we actually use it to slice the state space when analyzing violation witnesses. If Ultimate doesn't do this for violation witnesses, how else is the state space then restricted?

[sim642]

Another argument regarding fairness was made: it would be unfair to tools who stick to the format spec if this has disadvantages regarding validation (maybe a validator might have trouble validating a witness in case there are no control keys).

Regarding fairness, a related point I tried to make during the meeting was that verifiers can use custom data keys in witnesses to guide validators that happen to understand that custom data key. The response was negative as if that's not allowed and only the specified data keys in README should be used.

Later reading the README again, I found it to contain this sentence which allows that:

Tools may introduce their own data nodes with custom keys and values. Other tools should ignore data nodes they do not know or are unable to handle.

Moreover, the SV-COMP FAQ seems to even encourage that:

Q: My verifier wants to use a particular hint for guiding the witness validator. Can I use it?

A: Sure. Just make sure that one of the witness validators can consume it.

It would be far more unfair to help some validator using a custom data key than using control which has precedent of being in correctness witnesses. For example, if we now agreed to generate and consume ourControl data key (which others might not even be aware of) instead in correctness witnesses to get around the rule about control specifically.

Sorry if this remark is going too off-topic.

[danieldietsch]

For violation:
Roughly, we project our control flow graph to the edges mentioned in the witness (with some relaxation for missing lines that are connected in a straight line), and add assume statements at the right places for assumptions.
So, if you leave out the else-transition, then we wont consider the else branch.

For correctness:
We add assertions for assumptions of the witness. If branches are missing we add assert false at the branching point(s). Then we check that no assertion is violated.

[danieldietsch]

@sim642 this is a very good point. We always encouraged adding custom keys -- obviously we assume a friendly verifier/validator scenario.

[sim642]

Actually, this might not just affect a verifier's score on correct tasks (by having all correctness witnesses rejected by the linter) but the verifier's qualification at all. The rules for qualification state:

Verifier. A verification tool is qualified to participate as competition candidate if the tool [...] (e) produces witness files (for violation and correctness) that adhere to the witness exchange format (syntactically correct).

If a verifier cannot produce a single syntactically correct (i.e. accepted by the linter) correctness witness, because it uses control, then one could even argue that it doesn't fulfill the qualification requirements. If I had noticed this earlier and not said a word (in an evil world), I might have argued to, for example, disqualify all CPAchecker and Ultimate derivatives by a similar argument that the rules have been known to everyone and the fact that they weren't enforced so strongly before doesn't mean that we shouldn't do it now and actually it has been unfair to others that they weren't enforced.

[danieldietsch]

@MartinSpiessl : We need to agree on some resolution. I say we change the README and are done with it. Do you agree?

[MartinSpiessl]

I carefully checked all publications as well as how witnesses were implemented by various tools in the past and now agree that this is most likely a typo/ is actually implemented this way in all tools I looked at.

I just created a PR for this: #25, @danieldietsch could you have a look?

[dbeyer]

My opinion last week was to stick with the rules and definitions. And the definition was very clear on this. Thus, I confirmed when the issue was brought up to me last week that we should follow the (strict) definition and reject witnesses with control edges. This was the general result also of a quick opinion poll in the community meeting.

However, @danieldietsch in comment #14 (comment)
and @MartinSpiessl in comment #14 (comment) came to the conclusion that the definition is actually wrong, being simply a typo.

According to the definition of correctness witnesses https://doi.org/10.1145/2950290.2950351
they are observer automata and must not restrict the state space of the program.
Therefore, if a state has an outgoing transition with a condition-true key, then this state must also have another outgoing transition that can be taken otherwise. This is granted by the semantics using stutter transitions. Witness automata are auto-completed to observer automata by adding implicit stutter transitions.
Basically, if the condition-true edge cannot be taken, the observer automaton stays in the state (it stutters)
and the program control flow can go ahead. The analysis must not restrict the state-space exploration (but can slice it into partitions).

Thus, the No in the table seems to be a typo.