groups, assert(in_domain) and wrapping

Feb 24, 2011 at 10:22 AM

Hello all,

with the current VCC, looking at groups (below an example with one group) it looks that unwrapping followed by wrapping has side-effects on assertable in_domain-ness:

 

~/sandbox/elementary/group$ vcc /version 
Microsoft Research Vcc Version 2.1.40224.0
Microsoft Research Boogie Version 2.1.21217.0
Microsoft Research Z3 Version 2.0.41203.1
~/sandbox/elementary/group$ cat wrapping.c 
#include "vcc.h"

struct vcc(dynamic_owns) S {

  def_group(G);
  invariant(set_in(this::G, owns(this)));
  in_group(G) int a;

};

void test(struct S *s)
maintains(wrapped(s))
writes(s)
{
 assert(in_domain(s::G, s));
 //assert(in_domain(s::G, s::G)); //fails
 unwrap(s);
 assert(in_domain(s::G, s::G));
 wrap(s);
 //assert(in_domain(s::G, s)); //fails
 assert(in_domain(s::G, s::G));
}

~/sandbox/elementary/group$ vcc wrapping.c 
Verification of S#adm succeeded.
Verification of test succeeded.

 

Note: an alternative is

 

#include "vcc.h"

struct vcc(dynamic_owns) S {

  def_group(G);
  invariant(set_in(this::G, owns(this)));
  in_group(G) int a;

};

void test(struct S *s)
maintains(wrapped(s))
writes(s)
{
 assert(in_domain(s::G, s));
 unwrap(s);
 assert(in_domain(s::G, s::G));
 wrap(s);
 assert(in_domain(s,s));
 assert(in_domain(s::G, s));
 assert(in_domain(s::G, s::G));
}

But also this would mean that the rhs of in_domain of s::G is no longer unique (is the graph that represents the in_domain relation supposed to be acyclic or not?). Is this desired behavior? If so, is the behavior documented somewhere? E.g. in http://vcc.codeplex.com/wikipage?title=Sequential Domains

Best, Holger

 

Mar 1, 2011 at 1:26 PM

To follow-up,

* the above remark is orthogonal to groups, the effect that the rhs of in_domain depends on the proof state also can be shown with structs (see below)

* thinking about it, it simply illustrates how the assertion obtained while the struct was open is still available to the proof state after wrapping the struct

~/sandbox/elementary/group$ vcc struct.c
Verification of S#adm succeeded.
Verification of test succeeded.
~/sandbox/elementary/group$ cat struct.c 
#include "vcc.h"

typedef struct A_str {
    unsigned int a;
} A_t;


struct vcc(dynamic_owns) S 
  A_t *a;
  invariant(set_in(a, owns(this)));
};

void test(struct S *s)
maintains(wrapped(s))
writes(s)
{
 assert(in_domain(s->a, s));
 //assert(in_domain(s->a, s->a)); //not yet verifying here
 unwrap(s);
 assert(in_domain(s->a, s->a)); //move info about subdomain into proof state
 wrap(s); assert(in_domain(s,s)); assert(in_domain(s->a, s->a)); //now verifying assert(in_domain(s->a, s)); } ~/sandbox/elementary/group$ vcc /version Microsoft Research Vcc Version 2.1.40226.0 Microsoft Research Boogie Version 2.1.21217.0 Microsoft Research Z3 Version 2.0.41203.1

(I agree that this enrichment of the proof state - assuming that the in_domain relation is not a function - is not a problem. Correct me if I'm wrong :-) )

Holger

Coordinator
Mar 1, 2011 at 6:45 PM

This is indeed by design, even though it might look a bit odd :)

in_domain(p,q) is written as p \in \domain(q) in the new syntax, which is also more intuitive way of thinking about it (there is still some special triggering involved, which I guess I need to fix one day...)

We just do not provide a way to reason about \domain(x) when x is not wrapped, because you would anyhow lose any information about it after any function call or atomic block. There is no soundness reason for that, just utility.

Michal