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

[Chris Matrakidis]

On 29 September 2015 at 23:42, Heinrich Schuchardt <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

minisat.patch
Description: Binary data