Semantics of __VERIFIER_assume
In https://github.com/sosy-lab/sv-benchmarks/pull/539#issuecomment-346562287 it was mentioned that we should talk about the semantics of __VERIFIER_assume
. There is a long discussion about it in #504, which I will try to summarize here, but I recommend to reread that discussion, too.
The current rules are pretty clear:
A verification tool can assume that a function call __VERIFIER_assume(expression) has the following meaning: If 'expression' is evaluated to '0', then the function loops forever, otherwise the function returns (no side effects).
This means that most tasks with __VERIFIER_assume
are nonterminating.
However, there have been tasks added in the past where the submitter assumed different semantics of __VERIFIER_assume
(https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-344962928), namely that any execution that violates such an assumption should not be considered by the verifier at all, and thus violating an assumption would not lead to nontermination (source: https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-344938369).
There is also the following argument (https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-344932099):
Do submitters of verification tasks who use "__VERIFIER_assume" to restrict variable values actually really say "yes, I want to add nontermination to my task!"? I cannot imagine it.
Because I think we agree that we do not want to encourage adding trivial nontermination, this leads to the question about what the value of __VERIFIER_assume
is at all (https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-344903721).
Currently the guideline seems to be to never use __VERIFIER_assume
and call abort
instead, but then why define __VERIFIER_assume
at all in the rules (or at least declare it as deprecated)?
But of course there is also the argument that replacing __VERIFIER_assume
with abort
is good, because this means less SV-COMP-specific stuff in the tasks (https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-344910796).
Another question to consider when thinking about __VERIFIER_assume
is
Is
void *p = malloc(1); __VERIFIER_assume(false)
a violation ofmemcleanup
?
If the answer is "no" (which it would be according to both the definition with the infinite loop as well as the definition that the verifier should not consider any such execution at all, but contradicts with an abort-based definition), then __VERIFIER_assume
gets valuable again, because this is something that would be more difficult to express otherwise.
So the definition of __VERIFIER_assume
that is based on "a verifier should not consider such executions at all" would have the advantage that it neither adds unwanted nontermination nor unwanted missing memcleanups, which is something that the other definitions do not succeed. But this definition leads to the fact that the program void main( __VERIFIER_assume(0);)
would have no executions at all from the point of view from the verifier, which violates some people's intuition (https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-344996581).
So in summary, we should decide whether the definition of __VERIFIER_assume
is based on
- entering an infinite loop,
- calling
abort()
, or - not considering violation executions as part of the state space of the program (which cannot be expressed in C).
A quick summary of the existing arguments could be that 1. and 2. make little sense, because then we can just use real C code, whereas 3. allows to add assumptions easily without accidentally introducing trivial violations of properties like termination or memcleanup (https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-345165766, https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-345178879), whereas the counterargument is that this is also possible by writing a carefully crafted harness without relying on SV-COMP-specific stuff (https://github.com/sosy-lab/sv-benchmarks/issues/504#issuecomment-345177073).