Out-of-memory error / write specifications / simple example

Dec 18, 2012 at 1:18 AM
Edited Dec 18, 2012 at 12:02 PM

Hi,

I have been struggling with out-of-memory issues in vcc. The following simple example illustrates it: beyond a certain number of calls to test() vcc runs out of memory when verifying foo() [increase the number of calls at will; in my machine the instances shown suffice]. 

That is not however the case for foo2(), in which vcc flows through easily. Something goes the wrong way due to the call to assign() in foo(), the only difference between foo() and foo2(). Note that the variables written by assign() are not even used in subsequent calls to test.

Can anyone please give me a hint of what's  at stake?  I guess the problem lies with the contract of assign(). I tried adding \requires \thread_local(pv) or \maintains \thread_local(pv) with no result ... how it should it be done differently? According to the vcc manual, it's perfectly ok. If I remove the writes clause, the problem goes away, but I'm not sure what would be the consequences of that (is the assign post-condition enough ? in simple cases it seems to be)

Thank you.

 

#include <vcc.h>

void
assign(int v, int* pv)
  _(writes pv)
  _(ensures *pv == v);

void test(int v, int max)
  _(requires v >= 0 && v < max);

void foo(int a, int max)
  _(requires max > 0 && max <= 8)
  _(requires a >= 0 && a < max)
{

  int local_a, local_max;

  assign(a, &local_a);
  assign(max, &local_max);
  
  if (a > 0)
  {
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
  }

  if (a < max - 1)
  {
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
  }
}
void foo2(int a, int max)
  _(requires max > 0 && max <= 8)
  _(requires a >= 0 && a < max)
{


  if (a > 0)
  {
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
    test(a - 1, max); 
  }

  if (a < max - 1)
  {
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
    test(a + 1, max); 
  }
}

Developer
Dec 20, 2012 at 6:14 PM

Hi Eduardo,

There's nothing wrong with what you wrote; this is definitely a perf bug. As a workaround, you can put all of foo after the two calls to assign() in a block, and preced the block with the following contract:

_(writes {})
_(requires max > 0 && max <= 8)
_(requires a >= 0 && a < max)
{
    if (...) {
      ...
    }
    if (...) {
      ...
    }
}
  

hope this helps, ernie