[PPL-devel] Regression test failures on OpenBSD

[Roberto Bagnara]

On 07/17/12 19:04, Roberto Bagnara wrote:
> On 07/16/12 17:48, Abramo Bagnara wrote:
>> Il 14/07/2012 20:40, Edd Barrett ha scritto:
>>> On Sat, Jul 14, 2012 at 11:25:53AM +0200, Abramo Bagnara wrote:
>>>> Il 04/07/2012 12:27, Edd Barrett ha scritto:
>>>>> On Tue, Jul 03, 2012 at 03:23:33PM +0200, Roberto Bagnara wrote:
>>>>>> thanks to you for the report.  Could you please send to
>>>>>> ppl-devel at cs.unipr.it the config.log file generated at
>>>>>> configure time, along with the output of `make check' in
>>>>>> `/usr/ports/pobj/ppl-1.0/ppl-1.0/tests/Concrete_Expression'
>>>>>> once you have added `PPL_NOISY_TESTS=yes' to the environment?
>>>>>
>>>>> See attached the gzipped config.log and regression test failures in
>>>>> verbose mode.
>>>>
>>>> We have changed the test to produce more output to help to diagnose what
>>>> you're observing.
>>>>
>>>> Can you retry the above with current git head?
>>>
>>> I applied the patch you just comitted and re-ran the tests with noisy output.
>>
>> I've just tried with a VirtualBox image where I've installed a pristine
>> OpenBSD 5.1 amd64, gmp-5.0.5 and I'm unable to reproduce what you're
>> observing: both polyhedron1 and polyhedron2 succeeds.
>>
>> Might you have something installed that cause the miscompilation or a
>> bogus library?
>
> It is indeed a bogus version of libstdc++ to cause the problem.
> Here is what happens (experiments repeated with identical results
> with OpenBSD 5.1 both on x86_64 and sparc64):
>
> -bash-4.2$ cat bug.cc
> #include <cmath>
> #include <cstdlib>
> #include <cstdio>
>
> int main(int argc, char **argv) {
>    long double x = strtold(argv[1], 0);
>    long double y = std::floor(x);
>    printf("%.1000Lg\n%.1000Lg\n", x, y);
> }
> -bash-4.2$ g++ bug.cc
> -bash-4.2$ ./a.out  13311002825915415087
> 13311002825915415087
> 13311002825915414528
> -bash-4.2$
>
> As you can see, std::floor(x) returns a wrong result.
> An equivalent C program does the right thing:
>
> -bash-4.2$ cat bug.c
> #include <math.h>
> #include <stdlib.h>
> #include <stdio.h>
>
> int main(int argc, char **argv) {
>    long double x = strtold(argv[1], 0);
>    long double y = floorl(x);
>    printf("%.1000Lg\n%.1000Lg\n", x, y);
> }
> -bash-4.2$ gcc bug.c -lm
> -bash-4.2$ ./a.out  13311002825915415087
> 13311002825915415087
> 13311002825915415087
> -bash-4.2$
>
> But not if it is linked with -lstdc++ instead of -lm:
>
> -bash-4.2$ gcc bug.c -lstdc++
> -bash-4.2$ ./a.out  13311002825915415087
> 13311002825915415087
> 13311002825915414528
> -bash-4.2$
>
> The reason why libstdc++ on OpenBSD exports a
> bogus version of floorl() probably lies with the
> following piece of code:
>
> #ifndef HAVE_FLOORL
> long double
> floorl(long double x)
> {
>    return floor((double) x);
> }
> #endif
>
> We have no idea why on OpenBSD libstdc++ is compiled
> with HAVE_FLOORL not defined.

Dear Edd,

I am not sure if fixed versions of OpenBSD are already
available and if you are using them.  We have just uploaded
a new snapshot of PPL 1.1 (to be released soon) that works
around the problem you reported.  If you are still running
a version of OpenBSD where the problem manifests itself,
can you please test the snapshot available at

   http://bugseng.com/products/ppl/download/ftp/snapshots/

Many thanks for your kind cooperation.
All the best,

    Roberto



-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com