values of union pointer components & casting issues

Oct 1, 2009 at 4:47 PM
Edited Oct 1, 2009 at 4:48 PM

Hi there, currently i have been dealing with abstract data types containing pointers. As I understand a common way to implement such things are unions. Now it appears VCC has some problems mapping the pointer values to other components of the union. please consider the following example:

 

#include "vcc.h"

union bla_t {
	int a;	
backing_member int* b;
} bla;

void f(int* c )
writes(span(&bla))
{
bla.b = c;

assert(bla.a == (int)c); // FAIL assert((int *)bla.a == (int *)(int)c); // FAIL assert((int *)(int)bla.b == (int *)bla.a); // FAIL assert(bla.a == (int)bla.b); // FAIL assert((int *)bla.a == c); //FAIL assert(bla.b == (int *)bla.a); //FAIL }

 

As you can see all the assertions fail. On the contrary there are less problems in a scenario without unions:

#include "vcc.h"

void g(int* c)
{
int * d = c;
int e = (int)d;

assert(e == (int)c);
assert((int *)e == (int *)(int)c);
assert((int *)(int)d == (int *)e);
assert(e == (int)d);
assert((int *)e == c); //FAIL
assert(d == (int *)e); //FAIL
}

However also here not everything can be shown... i guess it boils down to the following assertion which cannot be shown:

assert(d == (int *)(int)d);

First i thought this might have to do with the internal representation/size of the pointers but i guess it's a general issue with pointer casting to non-pointer-types


assert(forall(int * x;x == (int *)(int)x)); //FAIL
assert(forall(int * x;(unsigned int)x <= (unsigned int)~0 ==> x == (int *)(int)x)); //FAIL
assert(forall(int * x;x == (int *)(long long)x)); //FAIL

iirc, this issue was discussed already some time ago, however it would be interresting to have an update on this. Also there seems to be a novel problem in combination with unions

Christoph


union bla_t {
    int a;    
    backing_member int* b;
} bla;

void f(int* c/*, int* x, int ** y*/)
    //requires((unsigned long long)c <= (unsigned int)~0)
    //requires(c == (int *)3)
    //requires(((unsigned int)c & 1) == 0)
    //requires((unsigned long long)y <= (unsigned int)~0)
    //requires(x == (int *)y)
    //requires(*x == (int *)y)
    writes(/*x,y,*/span(&bla))
{
    
    //int d = 3;
    //int * e = (int *)d;
    //
    
    int * d = c;
    int e = (int)d;
    //int * e = (int *)3;
    
    //assert(forall(int y; y == (int)(int *)y));

    //assert(d == (int *)(int)d); // FAIL
    assert(e == (int)(int *)e); // FAIL

    

    assert(e == (int)c);
    assert((int *)e == (int *)(int)c);
    assert((int *)(int)d == (int *)e);
    assert(e == (int)d);
    assert((int *)e == c); //FAIL
    assert(d == (int *)e); //FAIL

    //assert(d == (int *)(int)c);
    //assert(e == (int)(int *)e);
    //assert(e == (int *)(int)e);

    
    bla.b = c;
    
    /*assert(x == y);
    assert(x == (int *)y);
    assert(*x == *(int *)y);
    assert((int *)*x == *y);*/

    //*y = c;

    //assert(*x == *(int *)y);
    //assert((int *)*x == *y);

    //assert((int *)bla.a == (int *)3);
    
    //assert(((unsigned long long)c <= (unsigned int)~0));
    //assert(forall(unsigned long long x; x <= (unsigned int)~0 ==> (unsigned int)x == x));
    //assert((unsigned int)(unsigned long long)c == (unsigned long long)c);
    //assert((unsigned int)(unsigned long long)bla.b == (unsigned long long)c);
    
    //assert((unsigned int)(unsigned long long)bla.b == bla.a);
    
    //assert((bla.a & 1) == 0);
    //assert(bla.a == (unsigned int)(unsigned long long)c);
    //assert((int)e == 3);
    //assert(e == (int)c);
    //assert(e == (int)d);

    assert(bla.a == (int)c); // FAIL
    assert((int *)bla.a == (int *)(int)c); // FAIL
    assert((int *)(int)bla.b == (int *)e); // FAIL
    assert(bla.a == (int)bla.b); // FAIL
    assert((int *)bla.a == c); //FAIL
    assert(bla.b == (int *)bla.a); //FAIL

    assert(forall(int * x;x == (int *)(int)x));
    assert(forall(int * x;(unsigned int)x <= (unsigned int)~0 ==> x == (int *)(int)x));
    assert(forall(int * x;x == (int *)(long long)x));


    //assert(false);
}
Oct 7, 2009 at 9:00 AM

does noone have an opinion on this?

Coordinator
Oct 7, 2009 at 6:21 PM

Christoph, I can't reproduce your failures.

The only failing assertions I've seen from functions f() and g() are

assert(bla.a == (int)c); // FAIL
assert((int *)bla.a == c); //FAIL
assert((int *)e == c); //FAIL

I would explain these by the loss of precision between integers (32-bit) and pointers (64-bit).

Which version of VCC are you using?

Coordinator
Oct 8, 2009 at 9:30 AM
Edited Oct 8, 2009 at 11:31 AM

Okay, I can reproduce it now; only assertions should be enabled one at a time, that's why copy-and-paste of the code above doesn't give the claimed result. I'm gonna have another look...

Oct 8, 2009 at 12:11 PM
Edited Oct 8, 2009 at 12:12 PM

you are right i should have made this explicit...

i also tried casting to 64 bit integers but with no avail, so i would doubt the issue is caused (exclusively) by lack of precision

 

#include "vcc.h"

void f(int* c)
{
int * d = c;
unsigned __int64 f = (unsigned __int64)d;

assert((int *)f == c); //FAIL, also assert(d == (int *)f);
}

 


After all, some assertions that work for the ordinary assignment to local variables fail for union components.

But thanks for looking into this!

Coordinator
Oct 8, 2009 at 2:33 PM

Hi Christoph,

  (a) your assertions in f() and g() are not similar, because in the union case you assign to the pointer and not the integer. To get an apples-to-apples comparison, you should assign to the integer field of the union. In contrast to a regular assignment to an integer, this kind of assignment has to be in range of the variable and we need an extra requirement (I don't know why the range check is not enforced for regular integers). Moreover, VCC seems happier about an integer variable as a backing member as opposed to an integer pointer.  See here for an example getting your first assertion to work in this scenario (I've switch from unsigned to int, but this shouldn't matter):

#include "vcc.h"

void f() {
    int *c;
    unsigned e = (unsigned)c;
    assert(e == (unsigned)c);
}

union x {
    unsigned a;    
    int *b;

    backing_member
    unsigned __int64 x;
};

void g(int *c)
    requires(0 <= (unsigned)c && (unsigned)c < 1UI64<<32)
{
    union x bla;
    bla.a = (unsigned)c;
    assert(bla.a == (unsigned)c);
}

  (b) With regards to the assertion in your latest post, VCC needs to know that the pointer is a valid range for 'unsigned __int64'. For physical pointers, this would be the case, but it may not be so for ghost pointers. AFAIU, Stephan want's to provide the required axioms for physical pointers, once ghost-vs-physical pointers are completely implemented in VCC (feel free to make an issue for that). For now you can assume, that your pointers is in range to make this work. Unfortunately, it's a little bit awkward to formulate such an assumption. The idea is to provide / require the existence of a witness of an integer, that, when converted, gives you the pointer. The type constraint on the witness is the missing information which VCC needs to prove the assertion. Here's an example:

#include "vcc.h"

void h()
{
    int *c;
#ifdef EXPLICIT
    unsigned __int64 helper;
    assume((int*)helper==c);
#else
    assume(exists(unsigned __int64 helper; (int*)helper==c));
#endif
    assert((int *) (unsigned __int64) c == c); // no failure anymore
}

  Hope that helps.

  Mark

Oct 9, 2009 at 1:33 PM
Edited Oct 9, 2009 at 1:34 PM

Hi Mark!

thanks for your efforts. I see a bit clearer now. Unfortunately your first example does not match what i want to prove and what doesnt prove at the moment (I admit my examples may have been too extensive and thus obfuscating the core problem).

if you replace your line "bla.a = (unsigned)c;" with "bla.b = c;" you get the original issue.

However there seems to be a general problem with type conversion between union components.

#include "vcc.h"

union y {
    backing_member unsigned a;    
    int b;
};

void h(int c)
{
union y bla;

bla.b = c;

assert(bla.a == (unsigned)c);
}

Nevertheless with your "witness trick" i could now verify the examples, e.g. with

assume(exists(unsigned helper; 0 <= (unsigned)c && (unsigned)c < 1UI64<<32 ==> (int *)helper==c));

or

assume(exists(unsigned int helper; (int)helper==c));

respectively. Yet i'm not very happy with this "assume hacketry". concerning soundness i would feel way more comfortable with asserts instead of assumes (which do not work atm, that is)

Coordinator
Oct 9, 2009 at 3:34 PM

Hi Christoph,

I tried to show the type conversions with an appropriate BV lemma but got stuck (see Issue 2968). With regards to your earlier examples, BV lemmas currently won't help because they do not support pointers. I don't know whether this can be relaxed.

With regards to the "hacketry": I understand your concerns. As I said above already, it is planned to support the above out of the box for physical 64-bit pointers; physical / spec pointers are not yet completely implemented. Please ask Stephan and / or file an issue.

Restricting the pointer size to 2^32 (which you have done above) you won't get for free even after this change, though. Finally, you need to know that from context (for example, your memory allocator might guarantee to give out only pointers in a specific range).

Hope that helps, Mark

Oct 12, 2009 at 11:02 AM
Edited Oct 12, 2009 at 11:03 AM

yes, thanks for the clarification!

for the moment i will go with the "witness trick" as a workaround

 

Coordinator
Oct 13, 2009 at 7:52 PM

Hi Christoph, Issue 2968 is fixed in the next drop; so int <-> unsigned type conversion thing should at least work now (see the example attached to that issue).