How to verify complex return value

Apr 19, 2010 at 11:27 AM
Edited Apr 19, 2010 at 11:38 AM
Hello all,

I am new to this project and have some low level questions about verification and its usage. I am really confused and would like to know:
(1) how to verify a returning value from function which returns a local variable or a result from another function and (2) how do I declare local variables as mutable. The same with pointers.
(3) Is there a way to verify an incremented pointer like p+=32?

Another one lies somewhere between theory and practice. (4) What does the error 'is typed' in vcc exactly mean?

I provided below an example with all my current issues in it. First functionA() is ok.
static void functionA( unsigned int out[32], const unsigned int a[32], const unsigned int b[32])
	writes(array_range(out, 32))
        reads(array_range(a, 32))
	reads(array_range(b, 32))

        requires(is_mutable_array(out, 32))
 
	requires(is_thread_local_array(out, 32))
        requires(is_thread_local_array(a, 32))
	requires(is_thread_local_array(b, 32))

	requires(set_disjoint(array_range(a,32), array_range(b,32)))
	requires(set_disjoint(array_range(out,32), array_range(a,32)))
	requires(set_disjoint(array_range(out,32), array_range(b,32)))
{
	unsigned int i;

	for(i=0; i<31; i++)
		invariant(0<=i && i<=31)
		invariant(forall (unsigned int k; 0<=k && k<i ==> out[k] == (a[k] ^ b[k])))
	{
		out[i] = a[i] ^ b[i];
		assert(out[i] == (a[i] ^ b[i]));
	}

	out[31] = 0;
	assert(out[31] == 0);
}
/*
	vcc : Verification of functionA succeeded. [0,67]
	Time: 1,09s total, 0,42s compiler, 0,00s Boogie, 0,67s method verification.
*/


static unsigned int FunctionB( unsigned int *c, unsigned long long clen, const unsigned int *a, const unsigned long long alen)
	writes(array_range(c, clen))
        reads(array_range(a, alen))
	reads(alen)

        requires(is_mutable_array(c, clen))
 
	requires(is_thread_local_array(c, clen))
        requires(is_thread_local_array(a, alen))

	requires(clen >= 64)
	requires(alen >= 64)

	// Is there a way to verify return value which is a local variable or another function (return functionA(...))?

returns((clen%64)?0:u) { unsigned int fBa[64]; unsigned int fBb[64]; unsigned int i; unsigned int u; unsigned long long j; for(i=0; i<64; i++) invariant(0<=i && i<=64) invariant(forall (unsigned int k; 0<=k && k<i ==> ((fBa[k] == a[k]) && (fBb[k] == 0)))) { fBa[i] = a[i]; assert(fBa[i] == a[i]); fBb[i] = 0; assert(fBb[i] == 0); } while (clen >= 64) invariant(0 <= clen) { /* Any suggestions how do I declare fBb as mutable? error VC8510: Assertion '_vcc_array_range(out, 32) is writable in call to functionA(fBb, fBa, a)' did not verify. error VC9502: Call 'functionA(fBb, fBa, a)' did not verify. error VC9599: (related information) Precondition: '_vcc_is_mutable_array(out, 32)'. */ functionA(fBb, fBa, a); functionA(fBb+32, fBa+32, a+32); u = 1; assert(u == 1); for (i = 0;i < 64;++i) invariant(0<=i && i<=64) { /* What does 'is typed' in this context mean? error VC8506: Assertion 'c[i] is typed' did not verify. error VC8507: Assertion 'c[i] is writable' did not verify. */ c[i] = fBb[i]; assert(c[i] == fBb[i]); } /* error VC8511: Assertion 'a[i] is typed' did not verify. error VC8512: Assertion 'a[i] is thread local' did not verify. */ u = a[i]; assert(u == a[i]); spec(unsigned long long _spec = clen); clen -= 64; assert(clen == _spec-64); // How do I verify incremented pointer? c += 64; } if (clen) { functionA(fBb, fBa, a); /* error VC9502: Call 'functionA(fBb+32, fBa+32, a+32)' did not verify. error VC9599: (related information) Precondition: '_vcc_is_thread_local_array(b, 32)'. */ functionA(fBb+32, fBa+32, a+32); for (j = 0;j < clen;++j) invariant((0 <= j) && (j <= clen)) { /* error VC8506: Assertion 'c[i] is typed' did not verify. error VC8507: Assertion 'c[i] is writable' did not verify. */ c[j] = fBb[j]; assert(c[j] == fBb[j]); } return 0; } else return u; }
I would be grateful for any help..


<!-- @page { margin: 0.79in } P { margin-bottom: 0.08in } -->
I would be grateful for any help..