This project is read-only.
The following is an example usage of skinny_expose() and domain_updated_at().

#include <vcc.h>

struct B {
  int x;
  int y;
};
struct A {
  int z;
  struct B *b;
  invariant(keeps(b))
};

void foo(struct A *a)
  maintains(wrapped(a))
  writes(a)
  ensures(domain_updated_at(a, SET(&a->b->x)))
{
  skinny_expose(a, a->b)
    writes(&a->b->x)
  {
    a->b->x = 12;
  }
}


In particular, the statement:

  skinny_expose(a, a->b)
    writes(&a->b->x)
  {
    a->b->x = 12;
  }


Desugars into the following:

  state_t pre, post_unwrap;
  pre = current_state();
  unwrap(in_state(pre, a));
  unwrap(in_state(pre, a->b));
  post_unwrap = current_state();
  a->b->x = 12;
  assert(updated_only_values(post_unwrap, current_state(), SET(in_state(pre, &a->b->x))));
  assert(updated_only_domains(post_unwrap, current_state(), SET(in_state(pre, &a->b->x))));
  assert(in_state(pre, owns(a->b)) == owns(a->b));
  wrap(in_state(pre, a->b));
  assert(in_state(pre, owns(a)) == owns(a));
  wrap(in_state(pre, a));
  assume(domain_updated_at(in_state(pre, a), SET(in_state(pre, &a->b->x))));


Note the extensive use of in_state(pre, ...). Note that the meaning of old(...) in user code in skinny_expose(...) is currently unaffected (to be revised later), i.e. refers to the beginning of the function.

The predicate updated_only_values(S1, S2, W) states that all memory locations directly owned by the current thread in S1 are either unchanged between S1 and S2 or are listed in the set W. For example the following will not verify, because &a->b->y is mutable just after unwraps introduced by the skinny_expose(...) and is modified:

  skinny_expose(a, a->b)
    writes(&a->b->x)
  {
    a->b->y = 12;
  }


The predicate updated_only_domains(S1, S2, W) states that for every non-primitive pointer p in W, we know domain_updated_at(S1, S2, p, W2) where W2 is a subset of W. This allows for function calls in skinny_expose(...), as long as they use skinny_expose(...) themselves and state that in their contracts. See below for details.

The predicate domain_updated_at(S1, S2, p, W) says that the values of primitive pointers in the ownership domain of p stayed unchanged, except for locations in W. It also states that the ownership domain of p was unchanged across S1 and S2.

This really talks about version of p as read in S1 and S2, thus if you know that the version of p is the same in version(S0, p) == version(S1, p) and version(S2, p) == version(S3, p) and domain_updated_at(S1, S2, p, W) then we can derive domain_updated_at(S0, S3, p, W). We can thus verify the following:

void baz(struct A *a, struct B *b)
  maintains(wrapped(a))
  maintains(wrapped(b))
  writes(a,b)
  ensures(domain_updated_at(a, SET(&a->b->x)))
{
  skinny_expose(a, a->b)
    writes(&a->b->x)
  {
    a->b->x = 12;
  }

  expose(b) {
    b->y = 12;
  }
}


but not the following:

void bazFail(struct A *a, struct B *b)
  maintains(wrapped(a))
  maintains(wrapped(b))
  writes(a,b)
  ensures(domain_updated_at(a, SET(&a->b->x)))
{
  skinny_expose(a, a->b)
    writes(&a->b->x)
  {
    a->b->x = 12;
  }

  expose(a) {
    a->z = 12;
  }
}

Function calls in skinny_expose(...)

If inside of a skinny expose you want to call a function that writes a, you need to list a in writes(...) of the skinny expose and the function called needs to have a postcondition domain_updated_at(a, W), for some W contained within your writes(...). The domain_updated_at(...) that you expose to the outside may omit the non-primitive pointers. For example:

#include <vcc.h>

struct A {
  int x;
  int y;
};

struct B {
  struct A a;
  invariant(keeps(&a))
};

struct C {
  struct B b;
  int z;
  invariant(keeps(&b))
};

void up1(int sw, struct B *b)
  writes(b)
  maintains(wrapped(b))
  ensures(sw ==> domain_updated_at(b, SET(&b->a.x)))
  ensures(!sw ==> domain_updated_at(b, SET(&b->a.y)))
{
  if (sw) {
    skinny_expose(b, &b->a)
      writes(&b->a.x)
    {
      b->a.x = 1;
    }
  } else {
    skinny_expose(b, &b->a)
      writes(&b->a.y)
    {
      b->a.y = 1;
    }
  }
}

void up3(struct C *c)
  writes(c)
  requires(wrapped(c))
  // note that &c->b is hidden from the set, as it is non-primitive
  ensures(domain_updated_at(c, SET(&c->b.a.x, &c->z)))
{
  skinny_expose(c)
    writes(&c->b.a.x, &c->z, &c->b)
  {
    up1(1, &c->b);
    c->z = 12;
  }
}

void up6(struct C *c)
  writes(c)
  requires(wrapped(c))
  ensures(domain_updated_at(c, SET(&c->b.a.x, &c->b.a.y)))
{
  skinny_expose(c)
    writes(&c->b.a.x, &c->b.a.y, &c->b)
  {
    up1(1, &c->b);
    up1(0, &c->b);
  }
}

Last edited Nov 13, 2009 at 1:05 PM by stobies, version 5

Comments

No comments yet.