Newbie questions

Nov 11, 2010 at 4:10 PM

// Hi.  Sorry for some very elementary questions. I think mostly my confusion comes from not understanding \span. In the tutorial (July 2010 draft), sometimes "writes \span(s)" is used and sometimes "writes s" is used. It seems to make a difference, but not one that I understand.

// Here we go:

#include <vcc.h>

typedef struct NUM{
    int x;
    int y;
    _(invariant x==y)
}NUM;

void foo(NUM *num)
  _(requires \wrapped(num))
  _(writes \span(num))
  _(ensures \wrapped(num))
  _(ensures num->x == num->y)
{
  num->x = num->y+1 ;
  _(assert num->x == num->y) ;
}

// Verification of foo succeeds.
// Why does the assert pass? Why ensures?
// Why does the addition not trigger an overflow warning?
// Why am I allowed to write to x while *num is wrapped?

void bar(NUM *num)
  _(requires \wrapped(num))
  _(writes \span(num))
  _(ensures \wrapped(num))
{
  _(assert \thread_local(num))
  _(unwrap num) num->x = num->y+1 ; _(wrap num)
  _(assert num->x == num->y) ;
}

// Verification of bar succeeds.
// Why does the assert pass?
// Why is the invariant violation not caught at the wrap?

void baz(NUM *num)
  _(requires num->y < 100)
  _(writes \span(num) )
{
  num->x = num->y+1 ;
}

// Verification of baz succeeds
// Why is the invariant violation not caught?

// Cheers,
// Theo

Coordinator
Nov 11, 2010 at 7:24 PM

Hi Theo,

  the problem here is that "writes \span(num)" means that you can write to the fields of "num", which, by the invariants of VCC's typestate means, that "num" must be mutable. Your additional requirement on "foo()" and "bar()" however states that "num" is wrapped. Hence, your requirements (implicit and explicit) are inconsistent (anything can be derived), which makes the verification of the functions run seemingly fine, but you would not be able to prove these requirements trying to call "foo()" or "bar()"in your program later. If you suspect an inconsistency, you can run VCC with the "/smoke" option. In your example, VCC reports "found unreachable code, possible soundness violation, please check the axioms or add an explicit assert(false)" for both functions, indicating that there might be a problem.

  As opposed to that, the clause "writes num" means that you can write to the pointer "num" itself, but not necessarily the struct fields. "writes num" and the requirement "\wrapped(num)" will give you the right to unwrap "num", and thereafter write to its fields. If you change the writes clause for "bar()" like that, VCC will indeed complain about possible overflows, and the broken invariants just before trying to wrap "num" again.

  In the last function, again, "writes \span(num)" implies "\mutable(num)" (or "!num->\consistent"), which means, that the invariant of "num" does not need to hold. Indeed, for function "baz()" VCC would not implicitly check for the invariant to hold; it checks invariants implicitly only for "wrap" operations (and, in the concurrent case, for "atomic" statements).

  Hope that helps,

  Mark

Nov 12, 2010 at 2:06 PM

Thanks Mark.  I'm a bit puzzled by your statement that '"writes num" means you can write to the pointer "num" itself"; In my examples num is never written.

It seems the "write" thing to do for a mutator function is


void mut(struct T *p)
  _(requires \wrapped(p))
  _(writes p)
  _(ensures \wrapped(p))
{
  _(unwrap p)
  change the fields of *p
  _(wrap p)
}

But it's not clear to me why.  In particular, what implicit preconditions (or postconditions) are implied by "writes p" and what implicit preconditions are implied by "writes &p->x"?

Some related questions:

  Can I take "writes \span(p)" to be synonymous with "writes &p->x, &p->y" (where x and y are the declared fields of *p)?

  Why can I not "assert \writable(p)"? (I get that \writable is not in the current context.)

Coordinator
Nov 15, 2010 at 7:17 PM

Hi Theo,

  you are right, the implementation itself does not "write to num". However, a write right to "num" is required by the "_(unwrap ...)" operation (remove the writes clause and the unwrap operation will fail).

  For primitive pointers (pointer to primitive types like int), VCC assumes as an implicit precondition that the pointer is mutable. This condition is also checked a call site. Now, primitive pointers cannot be mutable on their, but only their enclosing objects (a.k.a. embedding in VCC) can be. Thus, "_(writes &p-x)" states that "\mutable(&p->x)" which states that "\mutable(p)", which would contradict "\wrappep(p)". For "_(writes p)", where "p" is an object pointer, a preoncition is implied that "p" is thread-owned, meaning that it is typed and in the ownership of the current thread ("\mutable(p) || \wrapped(p)").

  No implicit postconditions are generated through writes clauses.

  As you have written, the span of an object are the addresses of its fields; this also includes ghost fields like the owns set of an object (p->\owns).

  Regarding your last question: "\writable" is unfortunately not yet built into VCC, but it probably should (see also "http://vcc.codeplex.com/Thread/View.aspx?ThreadId=232588").

  Hope that helps,

  Mark