This project is read-only.

Verifying memmove

Mar 26, 2011 at 10:42 PM

As I mentioned in a previous thread, I am currently working on a VCC-verifiable implementation of memmove. I have chosen to base the implementation off of code from David MacKenzie in the Public Domain (https://www.google.com/codesearch/p?hl=en#p9nGS4eQGUI/gnu/gettext/gettext-0.14.6.tar.gz|jPzy56HzMrQ/gettext-0.14.6/gettext-tools/lib/memmove.c).

The C code that I started with is:

void * memmove(void *dv, const void *sv, size_t n)
{
	size_t i;
	char *d = (char *) dv;
	const char *s = (const char *) sv;

	if (s < d)
	{
		for (i = n; i > 0; --i)
			d[i - 1] = s[i - 1];
	}
	else if (s != d)
	{
		for (i = 0; i < n; ++i)
			d[i] = s[i];
	}

	return dv;
}

I have succeeded in verifying the else if (s != d) {...} part, but the if (s < d) {...} part is tricky. Here is what I have so far for this part:

		for (i = n; i > 0; --i)
			_(invariant n >= i && i >= 0)
			_(invariant \forall size_t j; n >= j && j > i ==> d[j - 1] == \old(s[j - 1]))
			_(invariant \forall size_t j; i >= j && j > 0 ==> s[j - 1] == \old(s[j - 1]))
		{
			_(assert n >= i && i > 0)
			_(assert n > (i - 1) && (i - 1) >= 0)
			d[i - 1] = s[i - 1];
		}
		
		_(assert \forall size_t j; n > (j - 1) && (j - 1) >= 0 ==> d[j - 1] == \old(s[j - 1]))
		_(assert \forall size_t k; n > k && k >= 0 ==> d[k] == \old(s[k]))

VCC 2.1.40311.0 is able to verify all of the invariants and assertions except for the last one, which results in "error VC9500: Assertion '\forall size_t k; n > k && k >= 0 ==> d[k] == \old(s[k]))' did not verify". A human can see that the difference between the last assertion and the previous one is the substitution k = j - 1. Is there a way that I can instruct VCC to make this substitution?

Daniel

Mar 31, 2011 at 9:56 PM

Hi Daniel,

  this is indeed a more tricky one, related to VCC (and the underlying prover Z3's) handling of quantifiers, which is based on so-called triggers. Triggers are associated with quantified formulas, and provide hints to the prover on how it might instantiate these quantifiers. Triggers are automatically selected or user-defined. In this case, the automatically selected triggers are unfortunately not sufficient, and VCC will not prove your postcondition by the loop invariant because of the index shift. While should be possible to make it work with user-defined triggers (see http://vcc.codeplex.com/wikipage?title=Quantifiers&referringTitle=Documentation or the function foo() below), I think the easiest thing here is to "align" the quantifiers in the loop invariants and the postconditions, such that they do not shift indices, which VCC can then prove directly (also, the annotations are a little shorter overall), cf. below.

Best, Mark

#include <vcc.h>

void *memmove(void *dv, const void *sv, size_t n)
  _(requires \mutable_array((char *) dv, n))
  _(requires \thread_local_array((char *) sv, n))
  _(writes \array_range((char *)dv, n))
  _(ensures \mutable_array((char *) dv, n))
  _(ensures \result == dv)
  _(ensures \forall size_t j; j < n ==> ((char *)dv)[j] == \old(((char *) sv)[j]))
{
  size_t i;
  char *d = (char *) dv;
  const char *s = (const char *) sv;

  if (s < d)
  {
    for (i = n; i > 0; --i)
      _(invariant n >= i && i >= 0)
      _(invariant \forall size_t j; j < i ==> \unchanged(s[j]))
      _(invariant \forall size_t j; i <= j && j < n ==> d[j] == \old(s[j]))
    {
      d[i - 1] = s[i - 1];
    }
  }
  else if (s != d)
  {
    for (i = 0; i < n; ++i)
      _(invariant \forall size_t j; j < i ==> d[j] == \old(s[j]))
      _(invariant \forall size_t j; i <= j && j < n ==> \unchanged(s[j]))
      d[i] = s[i];
  }

  return dv;
}


void foo(int *a, int *b)
  _(requires \mutable_array(a,42))
  _(requires \mutable_array(b,42))
{
  _(assume \forall unsigned i; {\match_long(i)} 0 < i && i <= 42 ==> a[i - 1] == b[i - 1])
  _(assert \forall unsigned i; {:hint \match_long(i+1)} 0 <= i && i < 42 ==> a[i] == b[i])

}
Apr 2, 2011 at 11:16 PM

Hi Mark,

Do you know of a good reference on triggers? I adapted the techniques that you demonstrated in foo (above) to the implementation of memmove, and it worked like a charm. However, I only vaguely understand what the special user-defined trigger syntax does.

Daniel

Apr 4, 2011 at 9:20 PM

Hi Daniel,

  you can find some info here (Appendix A) and here (Chapter 3). Unfortunately, this is not an easy topic; we hope that user-defined triggers will be required less and less in the long run.

  Hope that helps, Mark

P.S.: @Michal: if you have more suggestions for reading, please go ahead...