This project is read-only.

Loops et al (purity, constant loop expressions, invariants, reads clause ... )

Oct 17, 2012 at 7:00 PM
Edited Oct 17, 2012 at 7:08 PM

Hello,

I am puzzled by the need of loop invariants regarding data that remains constant in a loop, and its relation with "pure" functions and the "reads" clause. To illustrate the issue consider the following example (the simplest one I could come up with to illustrate my questions below):

 

#include <vcc.h>

typedef struct {
  int someField;
  _(invariant someField >= 0)
  _(invariant someField < 100)
} Data;

Data* freshData(void)
 _(ensures \fresh(\result))
 _(ensures \wrapped(\result))
 _(ensures \result->someField >= 0 && \result->someField < 100)
;

void getFieldValue(Data* d, int* v)
  _(reads d)
  _(writes v)
  _(maintains \wrapped(d))
  _(maintains \thread_local(v))
  _(ensures *v == d->someField)
;

void _(pure) doSomething(Data* data, int v, int i);

void main(int argc, char** argv)
{
  int v;

  Data* data = freshData(); // data->someField in [0, 100[ 
  getFieldValue(data, &v); // v = data->someField

  // v and d are not changed by the loop
  // and since doSomething is pure I do not need to
  // state loop invariants to assert A1, A2, A3 after the loop
  for (int i=0; i < 10; i++) {
    doSomething(data, v, i);
  }
  _(assert v == data->someField) // A1
  _(assert v >= 0 && v < 100)    // A2
  _(assert \wrapped(data))       // A3
}

 

 

Basically I have a simple data structure with an int field with values between 0 and 100.  In main(), I allocate it, get the int field through the getFieldValue() operation. Then there is a loop in which data and v are not modified. The assertions A1 to A3 hold without problem. A key aspect to note is that I declare doSomething() as pure. 

Now if I remove the pure annotation in the prototype of doSomething()  and add a "reads" clause in place of that, I am forced to use loop invariants to assert A1 to A3 at the end. That is, I get the following code (remaining code is the same as above): 

void doSomething(Data* data, int v, int i)
   _(reads data) 
;

void main(int argc, char** argv)
{
  int v;

  Data* data = freshData(); // data->someField in [0, 100[
  getFieldValue(data, &v);   // v = data->someField

  // v and d are not changed or unwrapped by the loop
  // Why do I need the invariants ? 
  for (int i=0; i < 10; i++)
    _(invariant \wrapped(data))
    _(invariant data->someField >= 0 && data->someField < 100)
    _(invariant v == data->someField)
  {
    doSomething(data, v, i);
  }
  _(assert v == data->someField) // A1
  _(assert v >= 0 && v < 100)    // A2
  _(assert \wrapped(data))       // A3
}

I expected that since doSomething() in this case is just declared to read "data", data would remain constant in the loop.  I do need doSomething() not to be declared pure in the problem I am working on, and would like also to omit "unnecessary" invariants for data that remains constant in the loop for "sure". 

What am I doing wrong (or perhap VCC)?

A side question is if I can declare a specific function  argument to be "pure" (i.e free of side effects), as opposed to having to declare an entire function as "pure" ? tThanks, 

Eduardo

 

 

Oct 19, 2012 at 2:34 AM

Hi Eduardo,

This is partly your fault and partly a bug.

The easy way to solve the problem is to give your loop an explicit empty writes clause _(writes {}). This will let you remove the invariants.

According to the manual and the tutorial, VCC should actually be deducing an empty writes clause anyway. The rule is that if the body possibly writes to the heap, then the default writes clause is the one from the function in which the body appears (we should probably deprecate this), and is otherwise the empty writes clause. However, it considers an impure function to possibly write to the heap, even if that function has an empty writes clause (which I think is a bug.) So it should still deduce the empty writes clause from the spec of main() (which doesn't have a writes clause), but it doesn't.

Hope this helps,

ernie

Oct 22, 2012 at 8:40 PM
Edited Nov 13, 2012 at 11:16 AM

Thanks.

The empty writes clause won't solve my problem in principled terms, nevertheless it will provide  me with a temporary workaround.

You see, I actually simplified the example, the case I have at hand (within the loop) is more like:

 

void doSomething(Data* data, int v, int i, int* output)
   _(reads data) 
   _(writes output)
;

 

This makes the empty writes clause inadequate in the loop, but for now I can drop the writes clause in doSomething() as a workaround.

Oct 23, 2012 at 1:49 AM

Hi Eduardo,

The writes clause inherited from the function should still be able to do the job for you. If you still have trouble, contact me out of band (ernie.cohen@microsoft.com).

 

cheers,

ernie

Oct 23, 2012 at 10:21 AM

Thanks a lot. 

Cheers,

Eduardo