Witness validation with CPAChecker not working on minepump example

[Zsófia Ádám]

Hello,

I am currently working on generating violation witnesses in the given format of SVComp and I'd like to validate them with CPAChecker.

However even validating the given examples in the sv-witnesses github repository seems to fail.

I'm using CPAChecker 1.9.1 with the following command that was given in the sv-witness repository readme:

./scripts/cpa.sh -witnessValidation -witness ../../sv-witnesses/minepump_spec1_product33_false-unreach-call_false-termination.cil.graphml -spec ../../sv-witnesses/PropertyUnreachCall.prp ../../sv-witnesses/minepump_spec1_product33_false-unreach-call_false-termination.cil.c

and I'm getting a result of TRUE. (See attached complete output)

I assume that I have overlooked something, but I cannot find out what.

(I tried the cloud validation service as well, but I got a 500 internal server error, so I assumed, that it is out of service right now.)

If you have any ideas about this issue or you get different results, please share.

Thank you in advance,

Zsófia Ádám

[Martin Spießl]

Hi Zsófia Ádám,

Thanks for bringing this to the mailing list!
I just had a look at the problem and listed my findings below:

On 31.07.20 16:14, Zsófia Ádám wrote:
>
> Hello,
>
> I am currently working on generating violation witnesses in the given format of SVComp and I'd like to validate them with CPAChecker.

> However even validating the given examples in the sv-witnesses github repository <https://github.com/sosy-lab/sv-witnesses> seems to fail.

> I'm using CPAChecker 1.9.1 with the following command that was given in the sv-witness repository readme:
> |
> ./scripts/cpa.sh -witnessValidation -witness ../../sv-witnesses/minepump_spec1_product33_false-unreach-call_false-termination.cil.graphml -spec ../../sv-witnesses/PropertyUnreachCall.prp
> ../../sv-witnesses/minepump_spec1_product33_false-unreach-call_false-termination.cil.c
> |
>
> and I'm getting a result of TRUE. (See attached complete output)
>
> I assume that I have overlooked something, but I cannot find out what.

In this case, the easiest explanation is the right one: You did not overlook anything, this is a bug!

In the Report.html, we can observe (in the ARG tab) that the analysis has trouble getting past the state A9 in the witness automaton.
In the ARG state "62 @N445", we can see that the witness automaton jumped to state A9:

"AutomatonState: WitnessAutomaton: A9"

Two transitions later we would expect to have gone from A9 to A11 via the call of valid_product(), in the witness it states:

<edge source="A9" target="A11">
<data key="startline">763</data>
<data key="startoffset">15314</data>
<data key="enterFunction">valid_product</data>
</edge>

Now why did CPAchecker not match that transition? The witness lists a startoffset of 15314,
which is actually the first character of the whole statement in line 763:

tmp = valid_product();
^--offset 15134

If I generate a witness for that verification task with the current version of CPAchecker via this command:

scripts/cpa.sh -predicateAnalysis minepump_spec1_product33_false-unreach-call_false-termination.cil.c -spec PropertyUnreachCall.prp

I get the witness (in output/Counterexample.1.graphml.gz) which I attached here as newWitness.graphml.
That witness can be successfully validated by CPAchecker.

There the transition for matching the call of valid_product looks like this:

<edge source="A132" target="A134">
<data key="startline">763</data>
<data key="endline">763</data>
<data key="startoffset">15320</data>
<data key="endoffset">15334</data>
<data key="enterFunction">valid_product</data>
</edge>

So it only matches the part right of the "=" in line 763 (observe that the startoffset now is 15320!).
There seems to have been a change in CPAchecker
somewhere between version 1.6.1 (the one that created the witness in the sv-witnesses repository)
and the current version that modified/improved the offset handling.

As far as I can tell, the witness in the sv-witnesses repository is buggy (1.), but also CPAchecker could be blamed (2.):

1. The witness actually wants to enter the function, so it should just have given the startoffset for the function call, not the whole statement.
2. CPAchecker could have matched either the whole function call or entered the function instead of just getting stuck in the witness state A9

Regarding 1.: This can be fixed if we update the witness in the sv-witnesses repository, e.g. by replacing it with the witness I attached here.
Usually we would want to avoid this and keep backwards compatibility, but since the witness is imprecise, replacing it seems OK to me.

Regarding 2.: The witness is already unclear (does it want us to enter the function or match the whole statement?).
We could try to make CPAchecker decide on either matching the function call or the whole statement, but in the end this could lead to bugs that are hard to track.
We could throw an exception in such a case, but that would reduce the validators performance in case we find the violation nonetheless (e.g. on a different path).
So adding a WARNING in the log output would probably be the most reasonable chain of action in such case.
But newer versions of CPAchecker would never produce such a witness, so adding code to handle that case is probably not worth it.
Another possibilty that just came to my mind is that we could also branch nondeterministically and try to follow both possible interpretations of that transition.
Still I do not think that this is worth the effort, unless this is actually a common use case.

> (I tried the cloud validation service as well, but I got a 500 internal server error, so I assumed, that it is out of service right now.)

I did not get an error code of 500, but 308 instead. I created an issue for the general problem that the script is outdated:

https://github.com/sosy-lab/sv-witnesses/issues/15

The version of that script that is contained in the CPAchecker repository still works.
As described in the issue I think it would be best to remove it
and replace mentions of it in the README.md by a reference to CPAchecker instead.

Side note:

Since you want to generate violation witnesses it is probably best to also look at the violation witnesses
from SV-COMP 2020 and take those that were successfully validated as examples.
You can also generate witnesses yourself with the verifiers very easily, in the SV-COMP results
at the beginning of each log file there is the command line that was used to verify the corresponding task,
so you can change that command line to run the tool of your liking on your own example programs.
Tracking traversal of the witness automaton in CPAchecker's Report.html is also invaluable as we just saw.

In case you find further bugs, do not hesitate to open an issue
(for CPAchecker you can do that at: https://gitlab.com/sosy-lab/software/cpachecker)
or just write to the mailing list again.
In the end, we are always happy if things like this get reported!

Best,

Martin
--
Martin Spießl
Software and Computational Systems Lab
LMU Munich, Germany

[Zsófia Ádám]

Hi!

Thank you for your fast and thorough response.

I completely agree with your conclusions about the outdated minepump witness, however there may be more issues with the cloud service,

therefore it may be useful if I summarize, what I saw.

2020. augusztus 3., hétfő 12:51:11 UTC+2 időpontban Martin Spießl a következőt írta:

> (I tried the cloud validation service as well, but I got a 500 internal server error, so I assumed, that it is out of service right now.)

I did not get an error code of 500, but 308 instead. I created an issue for the general problem that the script is outdated: 

https://github.com/sosy-lab/sv-witnesses/issues/15

 

You are right, using that script, you get 308. But if you try the other given option in the readme (this one), then you'll get 500.

Furthermore, if you use the updated script from the cpachecker github repository or the 1.9.1 binary, then again, you'll get the same error. So that's why I assumed that it's down right now.

Side note:

Since you want to generate violation witnesses it is probably best to also look at the violation witnesses
from SV-COMP 2020 and take those that were successfully validated as examples.
You can also generate witnesses yourself with the verifiers very easily, in the SV-COMP results
at the beginning of each log file there is the command line that was used to verify the corresponding task,
so you can change that command line to run the tool of your liking on your own example programs.
Tracking traversal of the witness automaton in CPAchecker's Report.html is also invaluable as we just saw.

Thanks for the tips! I actually took a look at some of the witnesses from SVComp-2020 already, but I didn't know about the log files.

If you have a minute for one more question regarding witnesses:

I've read through the possible elements and attributes of the witness automatons, but most of these seem more like possible elements than requirements (for example: I can add offsets to my witness, but I don't have to - the validators will consider it as syntactically correct regardless).

What kind of rules or guidelines should I use (like which attributes should always be included), so most of the time I get a witness, which isn't just "validatable" but can be validated successfully? Are there any or is it just "the more the better" and at one point it will contain enough information, so it works?

Best regards,

Zsófi