Verifying a function to shift bytes left by 1

Mar 26, 2011 at 2:40 AM
Edited Mar 26, 2011 at 4:53 PM

I am working on verifying an implementation of memmove with VCC, but have encountered a problem with VCC not being able to verify an assertion.

One case of memmove is that the source and destination strings overlap and the source string is "in" the destination string. In this case, memmove needs to copy forward, or shift the source string to the left onto the destination string.

For simplification, assume that I want to write a function that takes a string of n + 1 bytes and shifts the last n bytes to the left by 1:

char * shift_bytes_left1(char *d, size_t n)
{
	size_t i;
	
	for (i = 0; i < n; ++i)
	{
		d[i] = d[i + 1];
	}

	return d;
}

Here is how I annotated this function:

char * shift_bytes_left1(char *d, size_t n)
    _(requires \mutable((char[n]) d))
    _(requires \thread_local_array(d + 1, n))
    _(writes \extent((char[n]) d))
    _(ensures \mutable((char[n]) d))
    _(ensures \result == d)
    _(ensures \forall size_t j; j < n ==> d[j] == \old(d[j + 1]))
{
    size_t i;
   
    for (i = 0; i < n; ++i)
        _(invariant \forall size_t j; j <= i ==> d + j != d + 1 + i)
        _(invariant \forall size_t j; j < i ==> d[j] == \old(d[1 + j]))
    {
        _(assert 0 <= i && i < n)
        _(assert d + 1 <= d + 1 + i && d + 1 + i < d + 1 + n)
        _(assert \thread_local(d + 1 + i))
        d[i] = d[i + 1];
        _(assert d + i != d + 1 + i && d[1 + i] == \old(d[1 + i]) && d[i] == \old(d[1 + i])) // error VC9500
    }

    return d;
}

VCC 2.1.40311.0 can verify everything except that d[1 + i] == \old(d[1 + i]).

Is there a way that I can induce VCC to make the connection between none of [d, d + 1, ..., d + i] equaling d + 1 + i implying that d[1 + i] == \old(d[1 + i]) at that point?

Daniel

Mar 26, 2011 at 5:14 PM
Edited Mar 26, 2011 at 5:15 PM

Aha! After playing around a bit, I discovered that adding the loop invariant _(invariant \forall size_t j; i <= j && j < n ==> d[1 + j] == \old(d[1 + j])) was key.

Here is the completed implementation:

#include <vcc.h>

char * shift_bytes_left1(char *d, size_t n)
	_(requires \mutable((char[n]) d))
	_(requires \thread_local_array(d + 1, n))
	_(writes \extent((char[n]) d))
	_(ensures \mutable((char[n]) d))
	_(ensures \result == d)
	_(ensures \forall size_t j; j < n ==> d[j] == \old(d[1 + j]))
{
	size_t i;
	
	for (i = 0; i < n; ++i)
		_(invariant \forall size_t j; j < i ==> d[j] == \old(d[1 + j]))
		_(invariant \forall size_t j; i <= j && j < n ==> d[1 + j] == \old(d[1 + j]))
	{
		_(assert \thread_local(d + 1 + i))
		d[i] = d[i + 1];
	}

	return d;
}

Daniel