Pointer arithmetic

[tom-kacvinsky]

In btornode.h, I see code like this:

static inline BtorNode btor_node_real_addr (const BtorNode node) { return (BtorNode *) (~3ul & (uintptr_t) node); }

This is worrisome for 64-bit Windows, as 3UL is only four bytes wide (sizeof(long) = 4 on 64-bit Windows, but sizeof(uinitptr_t) = 8). Thus I am not sure if the arithmetic being done on the input pointer and the subsequent cast back to a return pointer results in a valid pointer. I don't exactly understand what this code is supposed to do, but I do know I get crashes when importing pyboolector.pyd in python, and (after some sleuthing) came down to this inlined function being called. The stack trace doesn't show this function, though, because it is inlined.

Thoughts?

[tom-kacvinsky]

Should note that I tried changing 3UL to 3ULL (to get a 8 byte wide constant), but then crashed elsewhere.

[arminbiere]

Well I think there is no problem here.

Actually, the 'ul' (any part of it) does not seem to be necessary.

It might break if 'unsigned long' as well as 'BtorNode*' are wider than 'uintptr_t' and the latter is signed. Both conditions are not satisfied (on any system I think).

To make it easier to understand we could replace it with

static inline BtorNode btor_node_real_addr (const BtorNode node) { assert (sizeof (BtorNode) == sizeof (sizeof (uintptr_t)); return (BtorNode ) (~ (uintptr_t) 3 & (uintptr_t) node); }

Armin

On Tue, Oct 1, 2019 at 7:41 PM tom-kacvinsky notifications@github.com wrote:

Should note that I tried changing 3UL to 3ULL (to get a 8 byte wide constant), but then crashed elsewhere.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/Boolector/boolector/issues/69?email_source=notifications&email_token=AFA2SAMSD25DP2GZD6O5V4DQMODWHA5CNFSM4I4MVA3KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEACDWUY#issuecomment-537148243, or mute the thread https://github.com/notifications/unsubscribe-auth/AFA2SAKYFNDUA4HW7RPZJPDQMODWHANCNFSM4I4MVA3A .

[arminbiere]

There is one 'sizeof' too much as you might have noticed....

On Wed, Oct 2, 2019 at 6:31 AM Armin Biere biere@jku.at wrote:

Well I think there is no problem here.

Actually, the 'ul' (any part of it) does not seem to be necessary.

It might break if 'unsigned long' as well as 'BtorNode*' are wider than 'uintptr_t' and the latter is signed. Both conditions are not satisfied (on any system I think).

To make it easier to understand we could replace it with

static inline BtorNode btor_node_real_addr (const BtorNode node) { assert (sizeof (BtorNode) == sizeof (sizeof (uintptr_t)); return (BtorNode ) (~ (uintptr_t) 3 & (uintptr_t) node); }

Armin

On Tue, Oct 1, 2019 at 7:41 PM tom-kacvinsky notifications@github.com wrote:

Should note that I tried changing 3UL to 3ULL (to get a 8 byte wide constant), but then crashed elsewhere.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/Boolector/boolector/issues/69?email_source=notifications&email_token=AFA2SAMSD25DP2GZD6O5V4DQMODWHA5CNFSM4I4MVA3KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEACDWUY#issuecomment-537148243, or mute the thread https://github.com/notifications/unsubscribe-auth/AFA2SAKYFNDUA4HW7RPZJPDQMODWHANCNFSM4I4MVA3A .

[tom-kacvinsky]

OK< the proposal for how to handle this makes sense. To clarify, I was just pointing out the issue and what I did to work around it for the moment. I know what I did was not really a clean patch,

There is one other similar issues, again related to sizeof(long) and sizeof(void*):

define leaf(l) ((void *) (1lu | (unsigned long) (l)))

I propose

define leaf(l) ((void*)((uintptr_t)1 | (unitptr_t)(l)))

[aniemetz]

Well I think there is no problem here. Actually, the 'ul' (any part of it) does not seem to be necessary. It might break if 'unsigned long' as well as 'BtorNode' are wider than 'uintptr_t' and the latter is signed. Both conditions are not satisfied (on any system I think). To make it easier to understand we could replace it with static inline BtorNode btor_node_real_addr (const BtorNode node) { assert (sizeof (BtorNode) == sizeof (sizeof (uintptr_t)); return (BtorNode *) (~ (uintptr_t) 3 & (uintptr_t) node); }

@mpreiner and I will have a look at this and let @tom-kacvinsky know when we have a solution. @tom-kacvinsky can we ping you to test it for us?

[mpreiner]

@tom-kacvinsky can you try the branch https://github.com/Boolector/boolector/tree/cleanup-pointer-arith and see if this fixes your problems?

[tom-kacvinsky]

Will try this out today. I would have tried it this weekend but for some bizarre reason I did not get notification of the issue update until a co-worker pointed out the issue has been updated. Thanks for looking into this,

[tom-kacvinsky]

This worked, thank you very much.

[mpreiner]

This is now merged to master 66d0f7b.