This project is read-only.

# groups, assert(in_domain) and wrapping

 holgerblasum Feb 24, 2011 at 11: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 holgerblasum Mar 1, 2011 at 2: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 MichalMoskal Mar 1, 2011 at 7: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