Re: [Bug-glpk] minisat: copying 32 bit integer to 64 bit pointer

[Heinrich Schuchardt]

Hello Chris,

> integer shifted by one bit. Even in 64bit Windows, the bits are
> correctly aligned since the byte order is little-endian.
And the code will fail on a big endian machine if size_t(int) <
size_t(void *).

> The attached patch tries to improve the situation by using size_t
The integer type that is long enough to hold a pointer is intptr_t.

> #if 1 /* by mao; meaningless non-portable check */
If the check is necessary, the comment should be removed.

And of cause Andrew was right. The code (probably based on MiniSat-C
v1.14.1) is non-portable.

The easiest way to fix the code would be to use

struct storage {
  char is_pointer;
  union {
    void *pointer;
    int  lit;
  };
};

Best regards

Heinrich Schuchardt

On 19.11.2015 02:40, Chris Matrakidis wrote:
> 
> On 29 September 2015 at 23:42, Heinrich Schuchardt <address@hidden
> <mailto:address@hidden>> wrote:
> 
>     Hello Andrew,
> 
>     on 64bit Windows unsigned long has 32 bits and a pointer has 64 bits.
> 
>     The coding in minisat.c is definitely flawed.
> 
> 
> ...
>  
> 
>     clause_from_lit returns a pointer to memory Nirwana.
> 
>     Furthermore the unjustified assumption is made that struct clause is
>     two byte aligned.
>     This may be true for most architectures and compilers but at least
>     on amd64 you could also
>     enforce a one byte alignment by compiling with Visual C and setting
>     /Zp1.
> 
> 
> This version of minisat makes two assumptions:
> 1. long has the same size with a pointer, and
> 2. pointers are at least two byte aligned.
> 
> As Heinrich pointed out, the first one does not hold for 64bit Windows
> and the second is not always true. 
> 
> However, in practise the code works: The assumptions are made
> (presumably for memory efficiency) in order to store an integer using
> the same memory location with the pointer, and the least significant bit
> is used as a flag - if zero, we have a pointer and if one we have an
> integer shifted by one bit. Even in 64bit Windows, the bits are
> correctly aligned since the byte order is little-endian. 
> 
> The attached patch tries to improve the situation by using size_t
> instead of unsigned long in the problematic macros, which should have
> the correct size in all architectures, and the check in glp_minisat1()
> is modified to ensure this. Moreover, the assert that checked the
> pointer alignment is reinstated (again modified to use size_t).
> Unfortunately, I don't have access to a 64bit Windows system to check
> whether this actually helps.
> 
> Best Regards,
> 
> Chris Matrakidis