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

[Andrew Makhorin]

Hi Heinrich, hi Chris,

> 
> 
> 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.
> 

Chris, thank you for bug analysis and the patch provided.

> > 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.

Using size_t is okay. Glpk is written in ANSI C89 (ISO C90), so I
wouldn't like to use 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;
>   };
> };


> GNU Linear Programming Kit (GLPK) uses MiniSat-C.
> 
> On 64bit Windows unsigned long has 32 bits and a pointer has 64 bits.
> clause_from_lit returns a pointer to an invalid memory adress.
> 
> Are there any plans to update MiniSat-C? The latest release seems to
> be v1.14.1.
> 
> I could not find MiniSat-C on https://github.com/niklasso/minisat.

I downloaded the code (on 25/VII-2011) from http://minisat.se/ . The
link is still valid. The latest MiniSat version is 2.2.0, though I don't
think the core part was significamtly changed. The code (about 2000
lines) is in C++ as in all previous versions.

In principle, it would be possible to translate the code to C (by hand),
or maybe better, implement the algorithm from scratch.

In any case a CNF-SAT solver is a valuable tool that accomplished
methods to solve pure MIP, so I plan to include in glpk other similar
solvers.


Andrew Makhorin