This project is read-only.

Memory reinterpretation and primitive types

Mar 30, 2010 at 4:05 PM

Hi all,

I am in a situation where I would like to be able to copy an integer value into a byte array of type unsigned char*. I am not able to  use reinterpretation on the integer, since it may, in the general case, be a structure field, on top of which the structure may actually be wrapped (so no writing privileges there). However, the byte array is freshly allocated. Parts of it will be copied from an integer (the problematic bit), and the rest is copied from existing byte arrays of the same type (using memcpy() or a similar function).

My question is: do you know how I could achieve this? The following sample fails, and I tried various combinations of the memory reinterpretation primitives, and various ways of performing the copy (using memcpy(), doing an integer assignment after a type cast...).

 

typedef struct {unsigned char *ptr;
                      unsigned long len;
                      invariant(keeps(as_array(ptr,len)))} bytes;

void *memcpy(void * _Dst, const void * _Src, size_t _Size)
requires(is_array((unsigned char*)_Dst,_Size))
requires(is_array((unsigned char*)_Src,_Size))
writes(extent(as_array((unsigned char*)_Dst,_Size)))
ensures(mutable(as_array((unsigned char*)_Dst,_Size)))
ensures(unchanged(emb(as_array((unsigned char*)_Dst,_Size))));

bytes *toto(bytes *b)
requires(b->len != 0 && b->len <= INT_MAX + sizeof(b->len))
requires(wrapped(b))
{
  bytes *res;

  res = malloc(sizeof(*res)); assume(res != NULL);
  res->ptr = malloc(sizeof(b->len) + b->len); assume(res->ptr != NULL);

  res->len = b->len + sizeof(b->len);

  assert(in_domain(as_array(b->ptr,b->len),b));
  split_array(as_array(res->ptr,res->len),sizeof(b->len));

  memcpy(res->ptr,&(b->len),sizeof(b->len));  // This is the problematic point
  memcpy(res->ptr + sizeof(b->len),b->ptr,b->len);

  join_arrays(as_array(res->ptr,sizeof(b->len)),as_array(res->ptr + sizeof(b->len),b->len));

  return res;
}

Cheers,
Francois

 

 

Apr 1, 2010 at 10:40 PM

Hi Francois,

At first I thought that maybe we could have some sort of read-only reinterpretation, but then I realized that memcpy() and memzero() seem to be special, and should be defined polymorphicaly. Reinterpretation should be used when you want to use a chunk of memory as type T now, and as a different type S later, but memcpy() and memzero() do not really use the memory as byte[] type, they just don’t care about types.

Moreover, I think that there are no more such operations (without knowing the type you can only copy or zero stuff).

Unfortunately, we currently do not have a way of specifying it.

Cheers,

Michal (who’s hoping to cause a modest flame war about special-casing stuff)

Apr 3, 2010 at 9:58 AM

Hi Michal,

Thanks for your answer. I do believe a read-only reinterpretation would be a nice thing to have, although I am fuzzy on the specifics. Did anyone else report wanting to reinterpret an unwritable object?
In the meantime, I've been looking into other solutions for this: since this is purely verification-specific code (I'm simply writing semi-symbolic wrappers around concrete functions), I figured I could change whatever I want, and I simply copy out the contents of the wrapped structure into local variables that I can then reinterpret. One of the drawbacks of this is the loss of precision (although the reinterpretation itself completely forgets the contents of memory, so I believe I'm not accentuating it in any way through the intermediate copy...). The other is that it still doesn't work, but I'm confident I can make it go through eventually...

As for your flame war, I'm sorry I cannot join in. However, I don't think it's that much of a special case. I may want to write myself another function that doesn't care about type, possible using combinations of memcpy() and memzero(), and specify it "polymorphically" as well.

Thanks again,
Francois