This project is read-only.

How to pass an array?

Jan 11, 2011 at 12:45 PM
Edited Jan 11, 2011 at 1:39 PM

Hello,

Consider the following program:

int lsearch(int val, int a[], int a_length) 
maintains(wrapped(as_array(a, (unsigned int)a_length)))
ensures(result >=  0 <==>  exists(int k; 0 <= k && k < a_length && a[k]
== val))
ensures(result == -1 <==> !exists(int k; 0 <= k && k < a_length && a[k]
== val))
{
int k;

for(k = 0; k < a_length; k++)
invariant(forall(int l; 0 <= l && l < k ==> a[l] != val))
{
if(a[k] == val) return k;
}
return -1;
}


int main() {
int a[5] = {1,2,3,4,5};
int k;

wrap(as_array(a,5));
k = lsearch(3, a, 5);
return 0;
}

I've seen wrapped(as_array(a, (unsigned int)a_length)) in some other code which I believe verified. In the light of Mark's post however I assume we need thread_local here. What's the correct syntax and what is needed at the call site?

Also, what does (unsigned int)a_length mean for a_length < 0?

Boris

Jan 12, 2011 at 10:45 AM

Hi Boris,

first of all, this example should work the thread_local, as you have suggested. At the call site, no syntax is necessary, you can just pass the array and do not need to do anything with it first.

Secondly, I think it is a bug that VCC complains about the wrap in your example. It should be possible to wrap a stack allocated array in exactly the way that you do there.

Thirdly, the meaning of (unsigned int)a_length for a_length<0 depends on the context. In a statement context, i.e., when writing 'unsigned int ua = (unsigned int)a_length;' you would need to be able to prove that a_length falls within the range of unsigned. In a pure context (like in your example, or when having the cast inside of an assert), if it is unknown that a_lenght is indeed positive, the exact value of (unsigned int)a_length is unknown and it is only known that it is in range of the target type. Adding a requirement for a_length >= 0 would be a good thing, though.

There seems to be another problem in VCC that currently eliminates the cast from generated Boogie - I will look into these problems.

Generally, it is a good idea to use 'unsigned' for index values, and thus eliminate this whole range of problems.

Stephan

 

 

Jan 12, 2011 at 12:21 PM

Hello Stefan,

with the VCC version of today, VCC complains "Call 'lsearch(3, a, 5)' did not verify" for the code below.

int lsearch(int val, int a[], int a_length) 
maintains(thread_local(as_array(a, (unsigned int)a_length)))
ensures(result >=  0 <==>  exists(int k; 0 <= k && k < a_length && a[k] == val))
ensures(result == -1 <==> !exists(int k; 0 <= k && k < a_length && a[k] == val))
{
	int k;

	for(k = 0; k < a_length; k++)
	invariant(forall(int l; 0 <= l && l < k ==> a[l] != val))
	{
		if(a[k] == val) return k;
	}
	return -1;
}


int main() {
	int a[5] = {1,2,3,4,5};
	int k;
	
	k = lsearch(3, a, 5);
	return 0;
}

If I change thread_local to wrapped in the precondition of lsearch and add assert(0); at the top of the body of lsearch, this assertion doesn't verify. This shows that the precondition

wrapped(as_array(a, (unsigned int)a_length))

is not false. In the examples in one of my other threads, wrapped is false for primitive data types. Aren't arrays considered as primitive data types in VCC?

Regarding int and unsigned int, the problem here is that lsearch is of type int as it may return -1.  Therefore k, which, may be returned, and also a_length must be of type int. Otherwise, an overflow may occur. As lsearch is also correct for a_length < 0, this doesn't create a problem.

Boris

Jan 12, 2011 at 12:35 PM

Hi,

  by default, an array with elements of primitives types is not an object, the elements are rather embedded (regarded as fields) of an enclosing object. In the case of local arrays, the embedding can be though of as "the stack frame" of the function. Using the vcc(as_array) declaration, this default interpretation can be changed, the elements are then part of an artificial as-array-object, denoted "as_array(a,n)". This as-array-object can be wrapped and unwrapped as a regular object but does not have user-defined type invariants. So, in theory the example can be fixed by declaring a[5] as "vcc(as_array)" and wrapping before the lsearch() and unwrapping afterswards. However, issue 5977 currently forbids the combination of "vcc(as_array)" and initializers.

  Here is the example in two version (currently working, and what should be working after 5977 is fixed):

 

#include <vcc.h>

int lsearch(int val, int a[], int a_length) 
maintains(thread_local(as_array(a, (unsigned int)a_length)))
ensures(result >=  0 <==>  exists(int k; 0 <= k && k < a_length && a[k] == val))
ensures(result == -1 <==> !exists(int k; 0 <= k && k < a_length && a[k] == val))
{
  int k;

  for(k = 0; k < a_length; k++)
  invariant(forall(int l; 0 <= l && l < k ==> a[l] != val))
  {
    if(a[k] == val) return k;
  }
  return -1;
}


int main() {
#ifdef ISSUE_5977_FIXED
  vcc(as_array) int a[5] = { 1, 2, 3, 4, 5 };
#else
  vcc(as_array) int a[5];
  a[0] = 1;
  a[1] = 2;
  a[2] = 3;
  a[3] = 4;
  a[4] = 5;
#endif
  int k;
  
  wrap(as_array(a,5));
  k = lsearch(3, a, 5);
  unwrap(as_array(a,5));
  return 0;
}

  Hope that helps, Mark

Jan 12, 2011 at 1:27 PM

Hi,

so, if as_array converts an array into an object which can be wrapped as in the call of lsearch above, should't the appropriate precondition be wrapped instead of thread_local?

Above, Stefan wrote that you can just pass the array and do not need to do anything with it first if you use thread_local. What't the needed syntax in the precondition of lsearch?

And what does thread_local_array denote?

Boris

Jan 12, 2011 at 3:06 PM

Ah yes, I had forgotten about this stack frame business. Also, I have committed a fix for 5977, so it should now also work for arrays with initializers.

In the old syntax, requires(is_thread_local_array(a, a_length)) is what you want, in the new syntax _(requires \thread_local_array(a, a_length))

Stephan