[Solved&Explained] While loop (or calling swap) produces a lot of errors

Jul 28, 2012 at 11:06 PM
Edited Jul 28, 2012 at 11:11 PM

Hello.

I am learning VCC and I get stuck. I would like to verify the following code:

#include <vcc.h>

void swap( unsigned * a, unsigned * b )
	_(writes a, b)
	_(ensures \old(*a) == *b && \old(*b) == *a)
{
	unsigned c = *a;
	*a = *b;
	*b = c;
}

unsigned gcd( unsigned a, unsigned b)
{
	while( a != 0 )
	{
		b %= a;
		swap(&a,&b);
	}
	
	return b;
}

This produces a lot of errors:

Error	2	Assertion 'a is thread local' did not verify.	14	1	
Error	3	Assertion 'b is writable' did not verify.	16	1	
Error	4	Assertion '&a is writable in call to swap(&a,&b)' did not verify.	17	1	
Error	5	Assertion 'b is thread local' did not verify.	20	1	
Error	6	Call 'stack_free(&b)' did not verify.	12	1	
Error	7	(related information) Precondition: 'the extent of the object being reclaimed is mutable'.	1520	1	
Error	8	Call 'stack_free(&a)' did not verify.	12	1	

But if I do one of these changes, verification completes successfully:

1) Replacing "while" loop in function gdb with "if" statement. (Of course the algorithm do not work then.)
2) Not calling "swap" function but makes swap directly.

I am lost, I don't know where could be a problem. Probably some loop invariants or some swap ensures are missing?

Thank you for any kind of help, I am quite sure I just overlooked something during reading of a tutorial.

Aug 9, 2012 at 2:06 AM

When you call function "swap", the parameters are points. And in you swap(int *, int *) these two parameters are modified. In this case, you need to let VCC knows this. If you add _(writes a, b) for you while block, just like the specification for function contract, you can solve these errors.

Aug 9, 2012 at 11:51 AM

Oh yes, you are right! Thank you!

Well, one must add "_(writes &a, &b)", I am sure I tried it without the ampersands before and that produced an error that confused me.

But I still think VCC can deduce, that "a" and "b" are modified - from the writes annotation of "swap".

Nevertheless, this is working code:

#include <vcc.h>

void swap( unsigned * a, unsigned * b )
	_(writes a, b)
	_(ensures \old(*a) == *b && \old(*b) == *a)
{
	unsigned c = *a;
	*a = *b;
	*b = c;
}

unsigned gcd( unsigned a, unsigned b)
{
	while( a != 0 )
		_(writes &a, &b)
	{
		b %= a;
		swap(&a,&b);
	}
	
	return b;
}

Aug 9, 2012 at 4:58 PM

Well, it seems that the writes clause for function swap is some kind of requirement, i.e. precondition. When you call the function swap in unsigned gcd(unsigned a, unsigned b), the requirements for function calls would be transfer to _(assert ...). But it can't be proved. Therefore, you need something to let VCC know that. I also tried following code. It is also working.

#include<vcc.h>

void swap( unsigned * a, unsigned * b )
    _(writes a, b)
    _(ensures \old(*a) == *b && \old(*b) == *a)
{
    unsigned c = *a;
    *a = *b;
    *b = c;
}

unsigned gcd( unsigned a, unsigned b)
{
    while( a != 0 )
        _(invariant \writable(&a) && \writable(&b))
    {
        b %= a;
        swap(&a,&b);
    }
	
    return b;
}

Aug 9, 2012 at 7:12 PM
Edited Aug 9, 2012 at 7:17 PM

 

Thank you for your interesting points and code!

> it seems that the writes clause for function swap is some kind of requirement, i.e. precondition

Just a small note, I looked into the official tutorial (v0.2) and it says:

"(...) writability is a property of a
particular instance of an executing function. (That is, just because something
is writable for you doesn't mean it will be writable for a function you call.)
Therefore, you can't express that a function needs \permission" to write p
by _(requires \writable(p)), because preconditions are evaluated in the
context of the caller."

I made a test:

unsigned gcd2( unsigned a, unsigned b)
{
	_(assert \writable(&a)) // OK
	_(assert \writable(&b)) // OK

    while( a != 0 )
    {
		_(assert \writable(&a)) // FAIL
		_(assert \writable(&b)) // FAIL
        b %= a;
        swap(&a,&b);
    }
	
    return b;
}

unsigned gcd3( unsigned a, unsigned b)
{
	_(assert \writable(&a)) // OK
	_(assert \writable(&b)) // OK

    while( a != 0 )
        _(invariant \writable(&a) && \writable(&b))
    {
		_(assert \writable(&a)) // OK
		_(assert \writable(&b)) // OK
        b %= a;
        swap(&a,&b);
    }
	
    return b;
}

It looks like VCC wants an explicit order how to handle writablity (if yes, than - surprisingly - invariant is also "an order"). But it behaves a little bit strange I think:

void test( unsigned a )
{
	_(assert \writable(&a)) // OK

	while( a < 5 )
	{
		_(assert \writable(&a)) // OK
		a++;
	}

	{
		_(assert \writable(&a)) // OK
		a = 0;
	}

	while( a < 5 )
	{
		_(assert \writable(&a)) // FAIL
		swap(&a,&a);
	}

	{
		_(assert \writable(&a)) // FAIL
		swap(&a,&a);
	}
}

 

Developer
Aug 23, 2012 at 10:31 PM

Your last example verifies if you add to the second loop the invariant _(invariant \writable(&a)).

Regarding writability, you might find it helpful to think of it in terms of permissions. When you call a function, you might not want to give it all the permissions you have, because you'd like to make sure that it doesn't misuse permissions it doesn't need to do its job. Instead, you give it only the permissions it needs. The advantage of this is that you know that things it doesn't have permission to change won't change.

So you shouldn't think of a thread as having permission to write to a location, you should think of a function activation (i.e., an instance of a function call) as having that permission. On a function call, only those permissions specified in the contract of the called activation are actually passed to the called activation, and the caller must have these permissions to make the call. Of course the called activations might also get permissions in other ways, such as allocating memory (on the stack or on the heap) or acquiring ownership of something in another way (e.g., unwrapping an object to get something it owns); in these cases, these permissions pass to the caller if they are not given up by the called activation.

So asserting writability is really just asserting that you have a permission to write something, whereas a writes clause specifies which permissions are passed to a called function.

The whole reason for going through this song and dance for writing permissions is to allow the caller to deduce that other things don't change. No such "framing" is needed for reading, which is why there are no reads clauses (well, there are, but you don't need to worry about them).

Hope this helps,

ernie

Aug 30, 2012 at 8:23 PM
Edited Aug 31, 2012 at 11:16 AM

Thank you very much for your detailed explanation, Ernie.

In my last post (on Aug 9) I moved slightly to another "problem" that is related with writability. I will try to explain it again with comments in the following code:

#include <vcc.h>

void setZero( int * i )
	_(writes i)
{
	*i = 0;
}

// Without calling setZero.
void f_1() {
	int i = 10;

	while( 1 ) i = 0;
}

// Same function as f_1, but setZero is used.
void f_2() {
	int i = 10;

	while( 1 )
		// The same semantic as f_1, but invariant is needed!
		_(invariant \writable(&i)) 
	{
		setZero( &i );
	}
}

void f_3() {
	int i = 10;

	setZero( &i );
	// Vcc can deduce that i is writable.
	setZero( &i ); 
}

At first glance, it looks like calling setZero() in f_2() requires adding the invariant. But f_3() shows that the problem is not in calling the function setZero() but in the loop. So, in f_1() Vcc can somehow directly deduce that \writable(&i) is true, but in f_2() it can't. In other words: It is not like we can add the invariant in f_2(), but, contrary, we can omit the invariant in f_1().

Is this true?

Thanks

Martin Jiricka

Developer
Sep 7, 2012 at 10:59 AM

Essentially you are right. The difference between the two is that in f_1, the write is to a purely local variable (i.e., a local variable whose address is never taken). Such variables can never alias, and so are treated in a different way (see the manual for details); in particular, they are not subject to the rules of writes clauses. (Instead, VCC knows that they are unmodified if they are not explicitly assigned to.)

Conversely, in f_2, the address of i is taken, which means it is considered part of the heap. Without an invariant (or a writes clause) on the loop, VCC treats writing to any part of the heap as writing the whole heap, which includes ownership information, so VCC doesn't know that the loop doesn't give up ownership of i at some point. This is something we plan to remedy in the future (i.e. if, as here, you only write to ordinary object fields, VCC should be able to deduce that ownership didn't change).

Hope this helps,

ernie

Sep 10, 2012 at 9:08 PM

Thank you very much, Ernie!

I am going to mark this topic as solved :)