CodePlexProject Hosting for Open Source Software

- use vcc(...) block for most of the spec constructs (i.e.,
vcc(int foo() { ... }) instead of
spec(int foo() { ... }), and vcc(p->f = true;) instead of
spec(p->f = true;))
- we might go as far as vcc(assert x >= 0;) and possibly even vcc(requires x >= 0;)

- use field/methods notation wherever possible (i.e., p->closed instead of closed(p), and p->wrap() (or p->close()) instead of wrap(p))
- simplify set syntax

assert assume requires ensures writes reads invariant

Alternatively, we could make the parser recognize those only in vcc(...) blocks. This would make the parenthesis optional, i.e.:

int foo(int x) vcc( requires x >= 0; requires x <= 10; ensures result == x + 7 ) { int tmp = x; x++; vcc( assert x > 0; assert x < 100; ) // this semicolon is optional return x + 6; }

These become context-dependent keywords:

forall exists lambda old unchecked speccast speccast_uc nospeccast this obj_t state_t typeid_t claim_t ptrset // ? bool true false me() program_entry_point() spec_malloc spec_malloc_array reads_havoc havoc_others atomic_op atomic_read

Blocks:

vcc(block) requires(x >= 0) { ... } vcc(atomic(a, b, c)) { ... } vcc(expose(a, b, c)) { } vcc(skinny_expose(a, b, c) writes &c->x; ) { } // or: vcc(skinny_expose(a, b, c)) writes(&c->x) { }

We might (also?) have a vcc_block, vcc_atomic, etc.

Axioms:

vcc(axiom forall(int x; ...); axiom exists(...); ) // last semicolon optional

Spec-functions, spec-types:

vcc(pure int foo() { ... } void bar() { ... } struct G { ... }; )

Context-dependent special fields/methods:

p->array_range(20) p->array_member(20) p->array(20) // was: as_array(p, 20); not sure about this one p->in_array(q, 20) p->is_array(20) p->is_mutable_array(20) p->is_thread_local_array(20) p->is_array_emb(20, e) p->closed ?? containing_struct p->depends_on(this) p->domain p->emb p->extent p->full_extent p in q->domain p in q->vdomain // these two might be largely replaced with the following p->controls(a, b); // expanding to: assert(p in p->domain); assert(a in p->domain); assert(b in p->domain); ?? use(...) p->inv p->inv2 p->is<T> // ? p->claimable p->fresh p->is_malloc_root p->is_object_root p->is_ptr_to_composite p->is_thread p->mutable p->nested // remove? p->owner p->owns p->span p->thread_local p->typed p->wrapped // ? p->not_shared p->union_active(f) p->gemb this->keeps(a, b, c) p->is_non_primitive_ptr p->extent_is_mutable p->extent_is_fresh p->extent_is_zero someone->approves(field) p->domain_updated_at(S) p->ref_cnt c->claims(P) c->claims_obj(o) c->claims_claim(c) p in c->domain // in_claim_domain c->eval(expr) // by_claim c->always_eval(o) // always_by_claim

Common stuff:

x->owner = me(); // giveup_closed_owner x->owner = p; // set_closed_owner x->owns += set(a); // set_owner x->owns = s; // set_owns x->closed_owns = s; // set_closed_owns (maybe can also use x->owns) u->union_reinterpret(f) p->open() // unwrap(p) p->close() // wrap(p) p->bump_volatile_version() // This one needs some work anyhow, but maybe now this time. begin_update() c = claim(o1, o2, P); c->unclaim(o1, o2);

Memory reinterpretation:

join_arrays(a1, a2) split_array(a, sz) to_bytes(p) from_bytes(p)

frame_axiom admissibility_check pure no_reads_check postcondition_sanity // to be removed reads_check(f) skip_verification use_vcc_options(o) backing_member member_name(n) no_admissibility force_splits(n) keep_splitting(n) volatile_owns claimable inline no_inline dynamic_owns atomic_inline thread_local_storage record verified specified

in_group(g) def_group(g) inv_group(n, i)

public_writes(s) // remove? shallow_eq(s1, s2) deep_eq(s1, s2) boogie(...) bv_lemma(...) assume(start_here())

Shortcut macros (stay as they are?):

out_param weak_out_param always claimp maintains returns unchanged wrapped0 wrapped_dom on_unwrap

State manipulation (not sure about these):

in_state(state, expr) current_state() when_claimed(e)

Triggering hacks:

ex_act(x) // from existential activation, was: sk_hack(x); alternative use_lemma(...) dont_instantiate(...) dont_instantiate_int(...) dont_instantiate_size_t(...)

set(a, b, c) // or {a,b,c}, but not clear a - b // set_difference a + b // set_union a * b // set_intersection x in a // set_in, not sure about set_in0 a == b // set_eq a * b == set() // set_disjoint a <= b // set_subset universe() cardinality(s)

Last edited Feb 11, 2011 at 8:01 PM by MarkHillebrand, version 4

Something that would be nice is to have a syntax for a proof state that is not flushed after a function call, e.g. something like permanent_add(assert(in_domain(A,A)) because the verification engineer knows that it is needed again and is willing to pay the overhead for not flushing it. Maybe also have permanent_remove(assert(in_domain(A,A)) for removing the an assertion from the proof state.

We have too many operators that can apparently be defined as quantifications, e.g. p->extent_is_fresh. Does perf actualy suffer if these become macros?

Re: Regarding set theory: there's a request for that, http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2264

make disjointness !some(a&&b)

Regarding set theory, why aren't we using boolean maps? This would be much, much, much nicer.

To do the set operators, we should use therule that if you apply an operator on a map or maps for which it is not explicitly overloaded already (I don't know if there are any of these), it just applies pointwise (the maps have to have compatible types). On top of this, you would define reduction operators, like all(). So

intersection: a && b

union: a || b

difference: a && !b

membership: a[x]

equality: a==b

disjointness: some(a&&b)

subset: all(!a || b)

universe: lambda(T t; true)

cardinality has to be a primitive, but if you want cardinality of a set of ints to return an int, you need a precondition that some int is not in the set

To do the set operators, we should use therule that if you apply an operator on a map or maps for which it is not explicitly overloaded already (I don't know if there are any of these), it just applies pointwise (the maps have to have compatible types). On top of this, you would define reduction operators, like all(). So

intersection: a && b

union: a || b

difference: a && !b

membership: a[x]

equality: a==b

disjointness: some(a&&b)

subset: all(!a || b)

universe: lambda(T t; true)

cardinality has to be a primitive, but if you want cardinality of a set of ints to return an int, you need a precondition that some int is not in the set