Daily verification ease 2: assert(false) for inconsistency checks?

Nov 12, 2009 at 7:32 AM

Hi all,

it can happen to generate an inconsistent specification by a "foolish" verification engineer, e.g. below I assert ownership of "inner" (I) to the current thread (T) twice, once directly (T->I) "maintains(wrapped(&outer->inner))" (line  10) and once indirectly via an intermediate structure outer (O) "maintains(wrapped(outer))" (line 9, T->O, in combination with "invariant(keeps(inner))", O->I, line 5). My interpretation is that then inner (I) has two owners (T) and (O), and that is inconsistent.

Anyway (regardless of any underlying theory in this particular case), because the specification is inconsistent now, we can "assert(false)" (line 11). Or, alternatively (not shown), "ensures(false)" in the function contract.

Question: Is there a switch to vcc, boogie or z3 that would detect the inconsistency without manually inserting "assert(false)" in line 11? One can live with the manual insertion, but it would (slightly) ease verification flow, if one could do without ...

 

$ cat assert-false.c
#include "vcc.h" //line 1
//example for inconsistent specification

typedef struct inner_str { //line 2
        int i; } inner_t; //line 3

typedef struct outer_str { //line 4

        inner_t *inner; //line 5 (I)

        invariant(keeps(inner)) } outer_t; //line 6

outer_t *outer; //line 7 (O)

void test()  //line 8
maintains(wrapped(outer)) //line 9
maintains(wrapped(&outer->inner)) //line 10
{  assert(false);  } //line 11

$ vcc /b:smoke /v assert-false.c
Verification of outer_str#adm succeeded.
Verification of test succeeded.

 

Cheers, Holger

 

BTW, "daily verification ease 1" was Monday's: Can I make a not-always-satisfied assert fail immediately? :-)

Coordinator
Nov 12, 2009 at 8:38 AM

Hi Holger, please try /b:/smoke, i.e., the Boogie smoke-check switch. Best, Mark

Nov 12, 2009 at 10:30 AM

Hi Mark,

thanks - however at least in my setup this is not covered by "/b:/smoke" ...

$ vcc /version
Microsoft Research Vcc Version 2.1.21112.0
Microsoft Research Boogie Version 2.0.11102
Microsoft Research Z3 Version 2.0.30923.2
$ vcc /v /b:smoke assert-false.c
Verification of outer_str#adm succeeded.
Verification of test succeeded.
$ vcc /b:smoke /v assert-false.c
Verification of outer_str#adm succeeded.
Verification of test succeeded.

(Don't know whether the order of arguments passed to vcc matters.) --- Rgds, Holger

Coordinator
Nov 12, 2009 at 12:23 PM

Hi Holger,

  please add a slash before smoke, i.e., /b:/smoke. The order does not matter. We should investigate why VCC / Boogie doesn't complain about the unknown option.

  Best, Mark

Nov 12, 2009 at 2:03 PM

Hi Mark,

good point. However, adding the "/" does not really change anything on my system (and it does not change anything one other system too).

 

$ vcc /v /b:/smoke assert-false.c
Verification of outer_str#adm succeeded.
Verification of test succeeded.

 

Can anyone else reproduce that?

Coordinator
Nov 12, 2009 at 3:13 PM

Hi Holger,

  sorry for being too terse earlier. With /smoke Boogie will systematically implicitly insert assert(0) at control flow locations and report on "unreachable code" if it can prove one of these. Sometimes, a code portion may be unreachable for good reason. In this case an explicit assert(0) is used to defuse Boogie smoke check. This is what happened in your example. If you remove the explicit assert(0) you will get the following output instead:

Verification of outer_str#adm succeeded.
Verification of test succeeded.
Z:\assert_false.c(18): found unreachable code, possible soundness violation, please check the axioms or add an explicit assert(false)
Found unreachable code, but cannot figure out where it is.

With VCC there are some more subtleties concerning defusing smoke checks in (i) expression with lazy operators with known outcome, (ii) if & while conditionals, and (iii) non-present, unreachable default cases for switch statements. For (i) and (ii) VCC since recently provides the known(E,x) annotation which can be used to mark the value of a Boolean expression E as x; see issue http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=3101, http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2259 for the only documentation. For (iii) you have to specify an "default: assert(0)" case in ghost code, see also http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2278.

Hope that clarifies things :)

Mark

Nov 12, 2009 at 4:54 PM

Hi Mark,

now *that* indeed is much more detail :-) First, the replacing "assert(0)" by ";" fix as posted today 5:13 PM in combination with the "/b:/smoke" fix as posted today 2:23 PM gave desired same result (VCC rejecting) --- the joys of fixing simultaneous errors! Concerning the work items you mention, if my understanding is right, all of them are about dealing with false positives (and a useful reference for that). Now, as currently I am more concerned with false negatives, for the moment I'll see how far the corrected "/b:/smoke" notation carries and be very careful about "assert(0)" or its equivalent "assert(false)" (in case you are aware of other constructs with the side-effect of defusing smoke it is may be prudent to let me and the list know). (Maybe we should start a thread on regression testing one day.)

Good night, Holger

Coordinator
Nov 13, 2009 at 10:35 AM

I have added some documentation on this feature at http://vcc.codeplex.com/wikipage?title=Smoke%20Tests .

Coordinator
Dec 7, 2009 at 5:54 PM

Let me add to my list from Nov 12 at 5:13 PM that there's another situation where defusing the smoke check is currently in general not possible, namely in case of inlined functions (cf. http://vcc.codeplex.com/wikipage?title=Atomic%20inline) that have conditionals / lazy expressions where code may become unreachable depending on the actual arguments that the function is inlined for.