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

Hi,
I have been struggling with outofmemory 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 postcondition 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

