This project is read-only.

Annotating an array allocation

Aug 4, 2009 at 9:25 AM

Hi all,

  currently, annotating an allocation of an array is more cumbersome than annotating the allocation of a regular struct (I'm using here regular compilable code based on stdlib.h):

#include <stdlib.h>
#include "vcc.h"

void foo()
{
    struct T { int dummy; } *a;

    a = (struct T *) malloc(sizeof(*a));
    free(a);
}

void bar()
{
    int *a;

    a = (int*) malloc(sizeof(*a) * 42);

#ifndef VERIFY
    free(a);
#else
    free((void*) as_array(a,42));
#endif
    // free(speccast(array_type(int,42),a));
}
I'm wondering whether we can improve the situation for array allocation by (i) making the (void*) cast implicit, as for regular allocation, and (ii) introducing a pseudo-type for array (only available for such speccasts?). 
What do you think?
Thanks, Mark
Aug 4, 2009 at 9:41 AM
Edited Aug 4, 2009 at 9:43 AM

Hi Mark,

I totally agree that the cast to void* should not be required. Secondly, the as_array is our current way of expressing this array type. I have been experimenting with turning this from an expression-based approach into something that uses types directly, but this does not work so well. Problems start when we would use arrays of a size that is not compile-time constant. Currently, we cannot represent such types in our syntax tree and to do things properly, we would probably have to extend our mechanism for generic types to allow int parameters (as they do in C++).

An a related note, I am currently in the process of re-thinking allocation, e.g., to distinguish between ghost malloc, which will always succeed, and the 'real' malloc, which can potentially return null, which the caller needs to guard against.

Let's first consider the aspect of the ghost (or safe) alloc. As this function will only be used in ghost code, we are free to use the extended syntax that VCC supports and make safe_alloc a generic function like this:

template<typename T> T* vcc_safe_alloc();

To use this function, you call

struct  S *p = vcc_safe_alloc<struct S>();

which certainly beats

struct S *p = (struct S *)vcc_safe_alloc(sizeof(struct S));

For arrays, we could use a similar approach and define

template<typename T> T* vcc_safe_alloc_array(unsigned int n);

This would turn your call from above into

a = vcc_safe_alloc_array<int>(42);

Does this make sense?

Stephan

Aug 4, 2009 at 10:12 AM

Hi Stephan,

  the ghost allocation syntax looks nice to me.

  My initial example was for implementation code, though (see vcc\Test\testsuite\examples\ArrayList.c). Getting rid of the (void*) cast and introducing #define speccast_array(a,n) would probably be nice enough for now.

  Let me know if I should turn any of these into an issue.

  Thanks,

  Mark

Aug 4, 2009 at 10:18 AM

Instead of introducing a speccast_array, should we not simply define as_array(p,sz) as a macro that expands to (p) in the non-verify case? That would solve the second issue.

Getting rid of the (void *) seems to be rather simple: we can declare

void free(obj_t);

in vccp.h; by including vcc.h before stdlib.h, this will become the definition of free that we use for type checking and voila, no extra cast required.

The downside of this solution is that free would be defined even if stdlib was not included, although only in the case VERIFY=1 case, which should not hurt.

Aug 4, 2009 at 10:29 AM

As it turns out, the as_array macro is already in place.

Aug 4, 2009 at 10:34 AM

I like your suggestion for changing #define as_array().

With regards to declaring "void free(obj_t)" to get rid of the (void*) cast, I wonder though, why the cast wasn't required for freeing a struct pointer. My guess was that there is some magic behind the scene which doesn't (yet?) apply to as_array()-type pointers...

Best, Mark

P.S.: I only noticed now that this discussion should have been titled "Annotating an array deallocation" :)

Aug 4, 2009 at 11:04 AM

That was a good hint - turns out that we were missing a case in our type checking code when converting implicitly from obj_t to void *. I have checked in a fix for this also.

Aug 4, 2009 at 11:23 AM

Cool, thanks!

Sep 8, 2009 at 10:32 AM

Hi all,

From the looks of this thread, I understood that the following code should verify without problems.

#include <stdlib.h>
#include <vcc.h>

void bar()
{
    int *a;

    a = (int*) malloc(sizeof(*a) * 42);
    free((void*) as_array(a,42));
}

However, when running the verification, VCC comes back with the following error:

Verification of bar failed.
test.c(10,5) : error VC8510: Assertion '_vcc_as_array(a, 42) is writable in call to free((void*) _vcc_as_array(a, 42))' did not verify.
Exiting with 2 (1 errors)

I have had other problems lately with VCC not being able to prove writability, even in this kind of trivial case. I could not tell you when they started (I am working on other things and use VCC a bit too irregularly to be of any real use to you).

Cheers,
Francois

 

Sep 8, 2009 at 10:39 AM

Hi Francois,

the problem is that malloc may return NULL (this has changed a few weeks ago from the previous contract of malloc, which would always succeed). Although the C standard allows free(NULL), we require the pointer to be non-null. If you guard the free with 'if (a != NULL)', then the code verifies fine.

Stephan

Sep 8, 2009 at 11:13 AM

Thanks, Stephan. It does indeed solve the problem. And forces me to write robust code :)

Francois.