Memory reinterpretation: soundness problem

May 5, 2010 at 12:58 PM

Hi all,

in the example below I'd like to reinterpret a global object (in method clientUnsound()). Both methods verify just fine but the last line in clientUnsound() makes VCC produce a soundness violation warning when using the smoke check.

In contrast, passing a pointer to a struct of the same type (as in method clientOK()) or changing the type of pointer "d" in clientUnsound to type A_t doesn't lead to any warning.

Is there any implicit property of the global object "a" that conflicts with the specification of clientUnsound?

Best regards,

Thorsten

 

#include "vcc.h"

typedef struct A_str {
    int dummy ;
} A_t;

A_t a;

typedef struct D_str {
    int dummy; 
} D_t;

void clientOK(A_t *z) 
writes(extent(z))
requires(is_object_root(z))
{
    D_t *d;
    to_bytes(z);    
    d = (D_t *)z;
    from_bytes(d, false);
    d->dummy = 0;
}


void clientUnsound() 
writes(extent(&a))
{
    D_t *d;
    to_bytes(&a);
    d = (D_t *)&a;
    from_bytes(d, false);
    //the next line produces the soundness violation warning
    d->dummy = 0;
}

May 7, 2010 at 2:13 PM
Let me add that one way to "fix" this (make the unsoundness warning disappear) is to specify "unsigned int dummy" instead of "int dummy" in definition of "A_str". (Maybe that helps pin-pointing the issue.)
May 12, 2010 at 1:30 PM
hmm this looks to me rather like a VCC bug with the weird cornercase (reinterpreting global variable to same type) that is exhibited in the example, than a general problem with the reinterpretation. Maybe someone of the experts can state his opinion about this? It would be helpful to get feedback in order to determine whether our way to use reinterpretation is OK in general...
Coordinator
May 12, 2010 at 6:48 PM

This is indeed a soundness bug. We generate an axiom saying that globals are always typed as their declared type, which just isn't true after reinterpretation.

I would guess that a "fix" that would prohibit reinterpretation of globals would not be satisfactory to you, right?

Alternative solution would be to get rid of the axiom. Maybe that wouldn’t be all that harmful, because to actually read the global you need to pass “thread_local(&g)” as a precondition anyhow.

May 17, 2010 at 3:10 PM

Thank you for clarifying this issue. Actually, this example was the result of simplifying a larger one and we can work around this problem in our case, so no need to change the axiomatization for now :)

The information that this is a bug, however, is helpful in order to know that our way to use memory reinterpretation is consistent wrt. our larger example.

Coordinator
May 17, 2010 at 5:38 PM

So you would be fine with disallowing reinterpretation of globals?

May 21, 2010 at 1:19 PM

We briefly discussed this issue and at the moment we don't see any point were we'd need to reinterpret globals. In the long run, this feature might be nice to have,  if only for compliance with the C standard.