Annotation language simplifications

The objective is to revisit the annotation language, make it more coherent and easier to use. Most of the changes proposed can be easily automated, so the overhead on the existing annotations should be minimal. The benefits is clearer syntax (think: publications) and more obvious separation between spec and physical code.

Major ideas

  • 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

Specific syntax

No changes to:

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


Operations

All to be enclosed in vcc(...)

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)

Function/type attributes

Also all enclosed in vcc(...):

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)

Misc

Stays unchanged:

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 theory

  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

Comments

holgerblasum May 30, 2010 at 7:38 PM 
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.

erniecohen Oct 10, 2009 at 3:46 PM 
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?

MarkHillebrand Oct 10, 2009 at 3:09 PM 
Re: Regarding set theory: there's a request for that, http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2264

erniecohen Oct 10, 2009 at 2:43 PM 
make disjointness !some(a&&b)

erniecohen Oct 10, 2009 at 2:42 PM 
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