[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Bug-glpk] minisat: copying 32 bit integer to 64 bit pointer
From: |
Andrew Makhorin |
Subject: |
Re: [Bug-glpk] minisat: copying 32 bit integer to 64 bit pointer |
Date: |
Thu, 19 Nov 2015 12:26:13 +0300 |
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