Specifying that an array has static storage class

Apr 9, 2011 at 8:51 PM

It is somewhat common for C functions to return pointers to arrays that are statically-allocated, or to fill in members of a struct with pointers to arrays that are statically allocated. How do I annotate this in VCC?

For example:

#include <stddef.h>
#include <vcc.h>

struct test {
	const char *str; _(ghost size_t str_length;)
	_(invariant \thread_local_array(str, str_length + 1)) // doesn't work

void fill_test(struct test *t)
	_(writes \extent(t))
	_(ensures \wrapped(t))
	static const char s_str[] = { 'a', 'b', 'c', '\0' };
	t->str = s_str;
	_(ghost t->str_length = 3;)
	_(wrap t)

With VCC 2.1.40403.0 I get:

Verification of test#adm failed.
test2.c(7,28) : error VC8018: invariant(\thread_local_array(str, str_length + 1)) of test forbids unwrapping.
test2.c(7,28) : error VC8012: invariant(\thread_local_array(str, str_length + 1)) of test is not admissible.
Verification of fill_test succeeded.
Exiting with 3 (1 error(s).)


Apr 10, 2011 at 9:07 AM
Edited Apr 10, 2011 at 9:10 AM

Hi Daniel, one thing is missing from the structure's invariant to make it admissible, and the same program would fail to verify (or at least should) if the array was heap-allocated.

Whenever an object's invariants refers to another, separate and distinct, object in memory, you need to tell VCC how exactly this dependence arises. In most cases you will just want to say that e.g. your structure statically owns the array its invariant refers to, which you can express as "_(invariant keeps(as_array(str, str_length + 1)))".

Once you've added an object to your structure's ownership set, you will need to make sure it is wrapped before wrapping the structure itself. Which means that you will also need to make sure, in your example, that you unwrap the structure and array before leaving the function, for the memory-safety end-of-function checks (that stack-allocated objects can be safely freed) to succeed.

I think the ownership section of the Documentation is fairly up-to-date for VCC2, so you can also read up on this there. EDIT: It isn't. I think there is a short example in the tutorial, though.


Apr 11, 2011 at 2:48 AM

Hi Francois,

Is there such a thing as shared ownership in VCC? I think that this is what I want, but I am not sure.


Apr 11, 2011 at 7:35 AM

There are ways of expressing "shared ownership", but it immediately gets much more complicated. What kind of sharing did you have in mind? (As in, a quick sample of code that uses the function above but maintains external ownership of the array).

If you really think you need shared ownership, though, I'd rather let someone else---someone who does not need to rely on the documentation---help you, as I'm not fully sure of the current state of things.

Apr 11, 2011 at 3:21 PM
fdupress wrote:

What kind of sharing did you have in mind? (As in, a quick sample of code that uses the function above but maintains external ownership of the array).

I wanted to allow multiple threads to call the fill_test function which overwrites the str field with a pointer to the static const string. Every thread that obtains a pointer to the statically-allocated string "abc" is able to read the string, but not write to it. In a sense, multiple test objects can share ownership of the string with the "main thread".


Apr 11, 2011 at 3:59 PM

If I understand what you mean, each thread has its own test structure, but there is only one copy of the static string. Claims would seem appropriate here, as this is exactly what they are designed for: a main thread creates an object, and "locks" it using a claim before sharing it with other threads.

However, I am not completely sure how claims and raw byte arrays interact (an object type being claimable entails a lot of things, including the fact that it contains a reference counter, which may be harder to implement for objects that do not have fields). Can someone else confirm, infirm, or give alternative solutions?

Apr 13, 2011 at 9:12 PM

Hi Daniel,

  to handle this example nicely, VCC would need extended support for const and static locals (the latter are not supported at all) - then the fill_test() function could indeed just pass out "s_str" and the caller would see the string (and not being able to modify it). Right now, s_str could be modelled as a global (i.e., changing the code for now), a global owner could be set up a that owns the embedding of s_str and has an invariant on its value, and fill_test() could pass out claims to the global owner. See the last example on http://vcc.codeplex.com/wikipage?title=Globals&referringTitle=Documentation for a similar construction. Still, quite complicated; support of read-only / const memory in VCC would be preferable in the long run.

  HTH, Mark