Memory reinterpretation is a mean of changing type assignment, i.e. the meaning of typed(...) predicate. It falls into three categories: one can split or join adjacent arrays, interpret an array of bytes as an object of some different type and interpret a object of arbitrary type as an array of bytes. The splitting/joining arrays does not influence what we know about the contents of the memory, however other kinds of reinterpretation currently cause the prover to forget the contents of memory.

Splitting and Joining Arrays

is_object_root(p) means that p is not embedded inside another struct, which is necessary in order to perform reinterpretation.

#include <vcc.h>

void split(int *arr)
  requires(is_object_root(as_array(arr, 100)))
  writes(extent(as_array(arr, 100)))
{
  split_array(as_array(arr, 100), 50);
  split_array(as_array(arr+50, 50), 25);
  split_array(as_array(arr, 50), 25);
  split_array(as_array(arr+25, 25), 10);
}

void splitAndJoin(int *arr)
  requires(is_object_root(as_array(arr, 100)))
  writes(extent(as_array(arr, 100)))
{
  split_array(as_array(arr, 100), 50);
  join_arrays(as_array(arr, 50), as_array(arr+50, 50));
}

void join(int *arr1, int *arr2)
  requires(arr1 + 100 == arr2)
  requires(is_object_root(as_array(arr1, 100)))
  requires(is_object_root(as_array(arr2, 32)))
  writes(extent(as_array(arr1, 100)), extent(as_array(arr2, 32)))
{
  join_arrays(as_array(arr1, 100), as_array(arr2, 32));
}

Interpreting Byte Arrays as Objects

#include <vcc.h>

typedef unsigned char byte;

void *alloc(unsigned __int64  sz)
  ensures(is_object_root(as_array((byte*)result, sz)))
  ensures(mutable(as_array((byte*)result, sz)))
  ensures(is_fresh(as_array((byte*)result, sz)))
  ;

struct A {
  int x, y;
};

void f1()
{
  struct A * a = alloc(sizeof(struct A));
  from_bytes(a, false);
  a->x = 10;
  a->y = 20;
}

Interpreting Objects as Byte Arrays

#include <vcc.h>

typedef unsigned char byte;

struct A { int a; };

void flatten(struct A *a)
  writes(extent(a))
  requires(is_object_root(a))
{
  byte*p = (byte*) a;

  to_bytes(a);
  p[2] = 10; // assuming sizeof(A) > 2
}


The two operations can be combined:

void mfree(void *p spec(unsigned __int64 sz))
  writes(extent(as_array((byte*)p, sz)));

void f2()
{
  struct A * a = alloc(sizeof(struct A));
  from_bytes(a, false);
  // operate on a
  to_bytes(a);
  mfree(a spec(sizeof(struct A)));
}

Last edited Nov 13, 2009 at 4:38 PM by MarkHillebrand, version 6

Comments

holgerblasum Apr 14, 2010 at 10:01 AM 
The second argument of from_bytes ("false" in the examples above) means preserve-zero, for examples
see http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2495 .