This project is read-only.

How can I require that all arrays are disjoint?

Feb 18, 2011 at 6:06 AM

I am new to using VCC.  I was trying to write a verified version of memcpy().  However, VCC (very correctly) complains about the case where the two buffers overlap.  I can add requirements stating that the ranges should not overlap, but that gets very arduous to write for a large number of arrays.  Is there an easier way to specify this?  The code I really want to verify will be doing a lot of this kind of copying of values (or transformed values) from one collection to another; should i forgo arrays and move my collections to another representation?

Thanks.

Lewis

/* This is the version of memcpy with the buffer overlap restrictions */ 

void memcpy(unsigned char *dest, unsigned char *source, unsigned size)
	_(requires \thread_local_array(source, size))
	_(requires \thread_local_array(dest, size))
	_(requires (source < dest) || (source >= (dest + size)))
	_(requires (dest < source) || (dest >= (source + size)))
	_(writes \array_range(dest, size))
	_(ensures \forall unsigned i; i < size ==> dest[i] == source[i])
{
	unsigned int i;
	for (i = 0; i < size; i++)
		_(invariant \forall unsigned j; j < i ==> dest[j] == source[j])
	{
		dest[i] = source[i];
	}
}

 

 

Feb 18, 2011 at 10:50 AM
Edited Feb 18, 2011 at 10:51 AM

I'm no expert on this but I would assume that your requirements already imply that the arrays are disjoint. This is because of VCC's memory model where two typed objects (implied by \thread_local_array) never overlap. Someone may please correct me if I'm wrong here.

Nevertheless the typed memory model of VCC2 was actually introduced exactly because of these tiresome disjointness requirement annotations you had to insert in the first version of VCC.

What kind of error message do you get from VCC without the range assertions?

Feb 18, 2011 at 11:43 AM
Edited Feb 18, 2011 at 11:44 AM

VCC's memory model says that two typed objects never overlap unless they are equal or one is embedded in the other. In this case, the objects considered are individual bytes (as far as I understand it, arrays are not really objects unless you wrap them), so they cannot be embedded in one another, but nothing at all prevents them from being equal in general.

I noticed that there is an "\arrays_disjoint" function in the new syntax that could potentially do the trick, although I just tried it and it generates buggy Boogie (I'll take a look at it later and possibly create a ticket). You can work around this by defining a macro instead, in the style of

 

#define arrays_disjoint(unsigned char* a1, unsigned l1, unsigned char* a2, unsigned l2) (\forall \integer i,j; 0 <= i && i < l1 && 0 <= j && j < l2 ==> a1 + i != a2 + j)

 

This is still really heavy when you have multiple arrays you want to be disjoint (you have to write n! requires clauses when dealing with n arrays (instead of your 2*n!), but if your collection of arrays is well structured, you could also quantify over the array start addresses and lengths.

You may also need to give some hints, in the form of assertions, as to why the disjointness precondition holds when you call memcpy(). For example, if one of your arrays came in as an argument and was known to be typed then, and the other was freshly allocated inside the verification scope, VCC will be able to infer that they are disjoint, as long as you guide it through the proof by writing, for example:

 

ptr = (unsigned char*) malloc(len); // This would be the fresh allocation
_(assert \forall \integer i; 0 <= i && i < len ==> \fresh(ptr + i)) // Hint sometimes needed by VCC to prove the allocated array does not overlap with existing ones

 

I hope this helps, and I'll be happy to clarify any obscure statements I may have just made. Cheers,
Francois 

Feb 18, 2011 at 12:30 PM

Hi,

  right, "\thread_local_array(a,n)" does not imply the existence of any array objects; think of it merely as an abbreviation for "\forall unsigned i; i < n ==> \thread_local(&a[i])". There are array object (denoted "((type[size]) a)"), but their use has to be considered carefully, and they probably shouldn't go on the contract of a generic function like "memcpy()" (their use would forbid using "memcpy()" for sub-arrays).

  The "\arrays_disjoint" predicate has, AFAICS, been recently introduced for VCC3 (http://vcc.codeplex.com/wikipage?title=VCC3&referringTitle=Home); it is a bug that it dumps Boogie for "vcc /2". For the old syntax, VCC has a "set_disjoint()" predicate, that can be used in combination with "array_range()". Unfortunately, there does not seem to be a new-syntax version of set disjointness yet.

  Note that the requirement in the original code are perfectly fine; you could shorten them by "_(requires source + size < dest || dest + size < source)".

  For many arrays, this unfortunately does not scale. If you have more typing context, and this is what Christoph and Francois hinted it, you may not need to state disjointness requirements explicitly. For example, in "struct A { int a[20], b[20]; };" VCC knows that "a" and "b" are disjoint. Also, they would be disjoint from an embedded array in another struct, say "struct B { int c[42]; };", or a freshly allocated array.

  Hope that helps, Mark

Mar 26, 2011 at 2:21 AM

Hi Lewis,

I just discovered this post. Writing a verified implementation of memcpy was a goal of mine, too. Here is what I came up with:  https://github.com/dtrebbien/verlibc/commit/e22b5da53478a627d8c3f5431de50033435e1d17

Apr 1, 2011 at 2:24 AM

BTW, expressing pairwise disjointness for n objects of the same type requires (naively) n^2 requires conjuncts, not n!. If you do it more intelligently, you can do it with a linear amount of annotation in various ways. However, we should provide some syntactic sugar to do this.