Defining Predicates

Suppose we want to write a function that takes two pointers to integers and increments the contents of both of them.

First, let's deal with the "normal" case where the two arguments do not alias...

exercises/slf_incr2_noalias.c

void incr2a (unsigned int *p, unsigned int *q)
/*@ requires take P = Owned<unsigned int>(p);
             take Q = Owned<unsigned int>(q);
    ensures take P_post = Owned<unsigned int>(p);
            take Q_post = Owned<unsigned int>(q);
            P_post == P + 1u32;
            Q_post == Q + 1u32;
@*/
{
  unsigned int n = *p;
  unsigned int m = n+1;
  *p = m;
  n = *q;
  m = n+1;
  *q = m;
}

But what if they do alias? The clunky solution is to write a whole different version of incr2 with a different embedded specification...

exercises/slf_incr2_alias.c

// Increment two different pointers (same as above)
void incr2a (unsigned int *p, unsigned int *q)
/*@ requires take P = Owned<unsigned int>(p);
             take Q = Owned<unsigned int>(q);
    ensures take P_post = Owned<unsigned int>(p);
            take Q_post = Owned<unsigned int>(q);
            P_post == P + 1u32;
            Q_post == Q + 1u32;
@*/
{
  unsigned int n = *p;
  unsigned int m = n+1;
  *p = m;
  n = *q;
  m = n+1;
  *q = m;
}

// Increment the same pointer twice
void incr2b (unsigned int *p, unsigned int *q)
/*@ requires take P = Owned<unsigned int>(p);
             ptr_eq(q,p);
    ensures take P_post = Owned<unsigned int>(p);
            ptr_eq(q,p);
            P_post == P + 2u32;
@*/
{
  unsigned int n = *p;
  unsigned int m = n+1;
  *p = m;
  n = *q;
  m = n+1;
  *q = m;
}

void call_both (unsigned int *p, unsigned int *q)
/*@ requires take pv = Owned<unsigned int>(p);
             take qv = Owned<unsigned int>(q);
    ensures take pv_ = Owned<unsigned int>(p);
            take qv_ = Owned<unsigned int>(q);
            pv_ == pv + 3u32;
            qv_ == qv + 1u32;
@*/
{
  incr2a(p, q);   // increment two different pointers
  incr2b(p, p);   // increment the same pointer twice
}

This version does correctly state that the final values of p and q are,m respectively, 3 and 1 more than their original values. But the way we got there -- by duplicating the whole function incr2, is horrible.

A better way is to define a predicate that captures both the aliased and the non-aliased cases together and use it in the pre- and postconditions:

exercises/slf_incr2.c

/*@
predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q)
{
  if (ptr_eq(p,q)) {
    take PX = Owned<unsigned int>(p);
    return {P: PX, Q: PX};
  }
  else {
    take PX = Owned<unsigned int>(p);
    take QX = Owned<unsigned int>(q);
    return {P: PX, Q: QX};
  }
}
@*/

void incr2(unsigned int *p, unsigned int *q)
/*@ requires take PQ = BothOwned(p,q);
    ensures take PQ_post = BothOwned(p,q);
            PQ_post.P == (!ptr_eq(p,q) ? (PQ.P + 1u32) : (PQ.P + 2u32));
            PQ_post.Q == (!ptr_eq(p,q) ? (PQ.Q + 1u32) : PQ_post.P);
@*/
{
  /*@ split_case ptr_eq(p,q); @*/
  unsigned int n = *p;
  unsigned int m = n + 1;
  *p = m;
  n = *q;
  m = n + 1;
  *q = m;
}

void call_both_better(unsigned int *p, unsigned int *q)
/*@ requires take P = Owned<unsigned int>(p);
             take Q = Owned<unsigned int>(q);
             !ptr_eq(p,q);
    ensures take P_post = Owned<unsigned int>(p);
            take Q_post = Owned<unsigned int>(q);
            P_post == P + 3u32;
            Q_post == Q + 1u32;
@*/
{
  incr2(p, q);
  incr2(p, p);
}