This project is read-only.

Memory reinterpretation for non-root objects

Apr 27, 2010 at 10:06 AM

(posted on behalf of Thorsten)

Hi all,

in the method "test" below (which is a test case for a custom memory allocator we want to verify), I want to be able to pass one chunk of memory starting at a->b back to the caller (although with a different type).

For this, ownership of the array starting at a->b is removed from "a" and the array is split into two parts -- however, I have to assume that is_object_root(as_array(a->b,2)) holds to be able to do that. Is there any consistent way to reinterpret embedded objects?

Secondly, the call to split_array makes VCC forget about the fact that "a" is mutable -- how do I assert this property over the function call (or does split_array indeed change ownership/closedness-properties of "a")?

Thanks, Thorsten

#include "vcc.h"

typedef struct vcc(dynamic_owns) A {

   int dummy;

   vcc(as_array) unsigned char *b;

} A_t;

void test (A_t *a)



requires(set_eq(owns(a), SET(as_array(a->b,2)) ))


  unsigned char *c;


  giveup_owner(as_array(a->b,2), a);

  assert(set_eq(SET(), owns(a)));

  c = a->b;

  unwrap(as_array(c, 2));




  split_array(as_array(c, 2), 1);

  //[...] return one half of the array to "a"

  //doesn't verify




Apr 27, 2010 at 2:13 PM

Hi Thorsten / Holger,

  the second issue looks like a bug, which needs further investigation. Maybe it's realted to You can possibly work-around by reordering your ghost operations (i.e., wrap before split_array).

  With regard to your first question: reinterpretation can only be done for objects roots, i.e., objects not embedded anywhere else. For example, reinterpreting "&s->t in struct { struct { int a; } t; int b } t;" would break VCC's type invariants.

  I've added a small memory allocator example derived from the baby hypervisor below, which hopefully illustrates how that could work out in a simple allocator scenario (no freeing of memory here).

  Best, Mark

P.S.: Note that the vcc(as_array) annotation you have has / should have no effect - vcc(as_array) makes sense for arrays embedded in a struct only.


#include "vcc.h"

typedef unsigned __int8 uint8_t;
typedef unsigned __int64 uint64_t;

typedef struct alloc_t {
    uint64_t addr;
    uint64_t size;
} alloc_t;

void alloc_init(alloc_t *allocator, uint64_t addr, uint64_t size)
    allocator->addr = addr;
    allocator->size = size;
    wrap(as_array((uint8_t*)addr, size));

uint8_t *alloc(alloc_t *allocator, uint64_t size)
    maintains(wrapped_dom(allocator)) // wrapped_dom is for caller convenience
    requires(size) // non-empty allocation
    requires(allocator->size > size) // > avoids a corner case...
    ensures(allocator->size >= old(allocator->size) - size)
    ensures(is_object_root(as_array(result,size)) &&
        mutable(as_array(result,size)) &&
    uint8_t *result = (uint8_t*) allocator->addr;
    expose (allocator) {
		expose (as_array((uint8_t*) allocator->addr, allocator->size)) {
			split_array(as_array(result, allocator->size), size);
			allocator->addr += size;
			allocator->size -= size;
    return result;


Apr 27, 2010 at 3:36 PM

Hi Mark,

thank you for the explanations and the example -  I think based on this we can specify a version that suits our implementation.

Regarding the second issue, I already noticed that the example verifies if the order of wrap and split_array is changed. Unfortunately, this workaround is not applicable in our example: after splitting the array, some updates to "a" are performed that involve the second part of the array a->b to get a consistent state of  "a".  I guess work item 3229 gets my vote, then. :)

As for the constraint on memory reinterpretation, I simply misinterpreted the meaning of the is_object_root predicate. In our example I'll simply replace the assumption with a requirement which is a safe assumption that this will be guaranteed by the caller -- in the real implementation this would be replaced by an invariant of the allocator as in your example.



Apr 28, 2010 at 1:41 PM

Hi Thorsten,

  I had another look a the example and the issue I linked to. The problem is that VCC wouldn't know that the embedding of the structure is not the reinterpreted array, which then destroys its mutability. This particular case can be fixed by adding additional annotation on the embedding, as Michal noted earlier. (Alternatively, VCC might be extended to derive this automatically; the embedding of an object may not be an as_array() object with elements of primitive types). Consider the example below, where I've starred the critical requirement:

#include "vcc.h"

struct S { char a; };

void bar(struct S *s, char *a)
	requires(emb(s)!=as_array(a,5)) // (*)

void test_bar() {
	struct S s;
	char a[5];
	assume(0); // deliberate, stack_free won't prove

Hope this helps, Mark


May 5, 2010 at 1:51 PM

Hi Mark,

just as a late follow-up on this: seems that I misinterpreted the bugreport you mentioned earlier -- using your second example everything works as expected in our case.

Thanks again for your help!