This project is read-only.

Annotating memcpy

Mar 25, 2011 at 8:56 PM
Edited Mar 26, 2011 at 5:59 PM

Hello,

I am working on a project to annotate C standard library functions with VCC annotations (https://github.com/dtrebbien/verlibc). I am just starting out, so there isn't much there right now, but I did manage to annotate and implement strlen, and I am currently working on memcpy.

When I declare memcpy like this:

char * memcpy(char *d, const char *s, size_t n)
	_(requires \thread_local_array(s, n))
	_(writes (char[n]) d)
	_(ensures \result == d)
	_(ensures \forall size_t i; i < n ==> d[i] == s[i])
	;

And attempt to implement with this:

char * memcpy(char *d, const char *s, size_t n)
{
	return d;
}

VCC 2.1.40311.0 correctly complains:

Verification of memcpy failed.
C:\Users\Daniel\Documents\projects\verlibc\src\string\memcpy.c(22,2) : error VC9501: Post condition '\forall size_t i; i < n ==> d[i] == s[i])' did not verify.

My problem is that memcpy uses void pointers, so when I instead declare memcpy like this:

void * memcpy(void *d, const void *s, size_t n)
	_(requires \thread_local_array((const char *) s, n))
	_(writes (char[n]) d)
	_(ensures \result == d)
	_(ensures \forall size_t i; i < n ==> ((const char*) d)[i] == ((const char *) s)[i])
	;

VCC now succeeds in verifying:

void * memcpy(void *d, const void *s, size_t n)
{
	return d;
}

 

Is this a bug or should I be doing something different?

Daniel

Mar 25, 2011 at 9:26 PM

Hi,

  good to hear :)

  When I check your two variants, I'm getting errors for both, using version 2.1.40311.0 also. Can you double-check / provide a full file?

  Thanks, Mark

Mar 25, 2011 at 9:48 PM
Edited Mar 26, 2011 at 6:00 PM

Ah, okay. So I actually had another _(requires ...) line because I was attempting to specify that the regions can not overlap. I didn't include it originally because I am not sure that I like it, and I did not think that its presence would affect the verification.

Here is a complete test case:

#include <vcc.h>

void * memcpy(void *d, const void *s, size_t n)
	_(requires \thread_local_array((const char *) s, n))
	_(requires ! (((const char*) d) + n > s || ((const char *) s) + n > d))
	_(writes (char[n]) d)
	_(ensures \result == d)
	_(ensures \forall size_t i; i < n ==> ((const char*) d)[i] == ((const char *) s)[i])
	;

void * memcpy(void *d, const void *s, size_t n)
{
	return d;
}

When I run this through VCC with vcc /2 memcpy.c, I get:

Verification of memcpy succeeded.

Without _(requires ! (((const char*) d) + n > s || ((const char *) s) + n > d)), I get:

Verification of memcpy failed.
C:\Users\Daniel\Documents\projects\verlibc\memcpy.c(12,2) : error VC9501: Post condition '\forall size_t i; i < n ==> ((const char*) d)[i] == ((const char *) s)[i])' did not verify.
C:\Users\Daniel\Documents\projects\verlibc\memcpy.c(7,26) : error VC9599: (related information) Location of post condition.
Exiting with 3 (1 error(s).)
Mar 25, 2011 at 10:25 PM

I guess you meant to be dropping the ! from your extra requirements, otherwise "_(assert n == 0 && s == d)" holds... To prove the failing post condition, some extra work needs to be done :)

Hope that helps, Mark

Mar 26, 2011 at 1:19 AM

Here is what I ended up with:

void * memcpy(void *dv, const void *sv, size_t n)
	_(requires \mutable((char[n]) ((char *) dv)))
	_(requires \thread_local_array((const char *) sv, n))
	_(requires \forall size_t i; i < n ==> (\forall size_t j; j < n ==> ((const char *) sv) + i != ((char *) dv) + j))
	_(writes \extent((char[n]) ((char *) dv)))
	_(ensures \mutable((char[n]) ((char *) dv)))
	_(ensures \result == dv)
	_(ensures \forall size_t j; j < n ==> ((char *) dv)[j] == ((const char *) sv)[j])
	;

void * memcpy(void *dv, const void *sv, size_t n)
{
	size_t i = 0;
	char *d = (char *) dv;
	const char *s = (const char *) sv;
	
	for (; i < n; ++i)
		_(invariant \forall size_t j; j < i ==> d[j] == s[j])
	{
		d[i] = s[i];
	}

	return dv;
}

When I didn't have _(requires \forall size_t i; i < n ==> (\forall size_t j; j < n ==> ((const char *) sv) + i != ((char *) dv) + j)), I was confused why I kept getting the error message "error VC9500: Loop body invariant '\forall size_t j; j < i ==> d[j] == s[j])' did not verify". I then realized that VCC was smart enough to know that the ranges could overlap, so the loop invariant might not be true, exactly as it should be! So, yeah, VCC is awesome.

Mar 31, 2011 at 8:52 PM

Just a few notes:

  In VCC there's a difference between a set of adjacent pointer to characters (denoted \array_range(c,n)) and a character array object (denoted ((char[n])a)). Character array objects don't come with a user-defined invariant or fields, but otherwise are real objects, which embed an array range. For example, two such objects cannot overlap if their element type, base pointer, or sizes are different. Also, you can't arbitrarily chop array objects into parts, unless you know that they are not embedded into other objects (using the \object_root() notation) and nobody needs them to stay (i.e., their extent is writable). Long story short, by requiring an array object for "dv", as above, you cannot call memcpy() passing in a sub-range of an array. It's probably better to use \array_range() and \mutable_array(). On another note, the disjointness requirement from one your earlier posts should also be sufficient. Likewise, requiring the disjointness of the two input array range is sufficient. Below, I've integrated those two changes.

Best, Mark

#include <vcc.h>

void *memcpy(void *dv, const void *sv, size_t n)
  _(requires \mutable_array((char *) dv, n))
  _(requires \thread_local_array((char *) sv, n))
  _(requires \disjoint(\array_range((char *) sv, n), \array_range((char *) dv, 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] == ((char *) sv)[j])
  ;

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

  for (; i < n; ++i)
    _(invariant \forall size_t j; j < i ==> d[j] == s[j])
  {
    d[i] = s[i];
  }

  return dv;
}

 

Mar 31, 2011 at 9:48 PM

Hi Mark,

Thank you for the suggestions! I had already discovered that I was not able to pass sub-ranges into memcpy, but I thought that maybe this was a temporary limitation of VCC. Using \array_range instead of \extent fixed the problem.

https://github.com/dtrebbien/verlibc/commit/e2d032539b85019029ebcf18dffe06215b4df64c

Daniel