GNAT doing macro‑expansion for generics? (Pre/Post conditions)

GNAT doing macro‑expansion for generics? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Is this GNAT doing macro‑expansion for generics, or me missing some trick  
of Ada 2012?

Small snippet first, then comments below (not Ada comments).


     -- g.ads

     package G is

        pragma Pure;

        type E
           is (E1, E2, E3);

        type I_Type
           is interface;

        function F
          (I : I_Type)
           return E
           is abstract;

        procedure P
          (I : I_Type)
           is abstract
           with Pre'Class => F (I) = E1;

     end;


     -- m.adb

     with G;

     procedure M is

        type I_Type
           is new G.I_Type
           with null record;

        overriding function F (I : I_Type) return G.E;
        overriding procedure P (I : I_Type);

        -- subtype E is G.E;
        -- E1 : constant E := G.E1;
        -- use type E;

        function F (I : I_Type) return G.E
           is (G.E1);

        procedure P (I : I_Type) is
           begin null; end;

     begin
        null;
     end;


GNAT can compile package `G`, but while compiling `M`, complains `E1`  
(from the precondition of `P` in `G`) is not visible in `M`. Un‑commenting  
the three initially commented lines solves the issue, but still leave me  
with a feeling, things are going here as if a kind of macro‑expansion was  
applying. The precondition should be compiled in the context of its  
definition, isn't it?

Other funny stuff: in the precondition of P, substitute `P (I)` to `F  
(I)`. GNAT will compile `G` without a complain, and will only figure  
something is wrong while compiling `M`. Is this GNAT's fault, or mine  
missing something?

Note: both occur using FSF GNAT 4.6


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro‑expansion? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Le Fri, 19 Oct 2012 01:44:29 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Is this GNAT doing macro‑expansion for generics, or me missing some  
> trick of Ada 2012?

Don't care about the reference to generics in the title, that's just that  
my real work case involves generics, but while trying to simplify the  
case, I noted the package need not be generic for the case to be exposed.  
What looks like macro‑expansion here, is with Pre/Post conditions, not  
generics. Sorry for the erroneous title.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro‑expansion? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Le Fri, 19 Oct 2012 01:44:29 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Is this GNAT doing macro‑expansion for generics, or me missing some  
> trick of Ada 2012?
>

Really has issue with DbC (Design by Contract). Here is another bug I  
encountered. Note: I know source snippets exposing bugs are boring things  
to read, but I will post it anyway, if ever that can be of interest for  
someone. I will post two or three other cases, around the same snippet.  
Obviously, this does not stand for the reliable, it was simplified down as  
much as possible, as the purpose is two talk about the issue.

     -- bug1.adb

     procedure Bug1 is

        package P is

           type A_Type  is mod 256;
           type I_Type  is range 0 .. 4_000;
           type S_Type is array (I_Type range <>) of A_Type;

           type T (I, J : I_Type)
              is record
                 S : S_Type (1 .. J);
                 K : I_Type := 1;
              end record
              with
                 Predicate =>
                    (T.K <= T.I) and
                    (T.I <= T.J);

        end P;

        package body P is
           -- Useless, but see below,
           -- in the second comments
           -- about a variation on the bug.
        end P;

        E : P.T (I => 2_000, J => 2_006);

     begin
        null;
     end Bug1;


## First bug

Compiled with GNAT 4.6, then executed, I get this:

     raised CONSTRAINT_ERROR : bug1.adb:16 invalid data

While `K` which is (or should) be initialized to 1, is really (or should)  
lower or equal to `I`, which is 2 000.


## Variation

Interesting variation: remove the useless package body given to `P`. Now,  
compiling fails, with this error:

     bug1.adb:16: operator for type "I_Type" defined at line 6 is not  
directly visible

So it says operators of `I_Type` are not visible from the location of the  
expression `(T.K <= T.I)`; that's obviously buggy.

The latter is similar to the one of the first post. Surprisingly, it  
depends on the presence of absence of th useless package body.

Another variation, exposing two other bugs (if my mind is right), to come  
later (just the time to me to simplify it down).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro‑expansion? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Le Wed, 24 Oct 2012 18:40:58 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> same snippet. Obviously, this does not stand for the reliable
Read “does not stand for the real thing”.

>            type A_Type  is mod 256;

Sorry, forget to say about a second variation: replace the above with  
`type A_Type is new Positive;` and there will be no more error at runtime  
(the first error, that is, with the useless package body still there).  
That one is a lot weird.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro‑expansion? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Le Wed, 24 Oct 2012 18:45:27 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Le Wed, 24 Oct 2012 18:40:58 +0200, Yannick Duchêne (Hibou57)  
> <yannick_duchene@yahoo.fr> a écrit:
>
>> same snippet. Obviously, this does not stand for the reliable
> Read “does not stand for the real thing”.
>
>>            type A_Type  is mod 256;
>
> Sorry, forget to say about a second variation: replace the above with  
> `type A_Type is new Positive;` and there will be no more error at  
> runtime (the first error, that is, with the useless package body still  
> there). That one is a lot weird.
>

More on that particular point. I you change `mod 256` into anything the  
modulo is above 256, not necessarily a power of two, as this works with  
`mod 257` two, then the bug disappears. The bug is there for any value  
below and included, 256.

I suspected the element size, and indeed, that's not really the modulo,  
but the size. Replace `type A_Type is mod 256;` with this, with an added  
representation clause:

     type A_Type  is mod 256;
     for A_Type'Size use 16;

The module is still 256, but now the size changed, and the bug is not  
exposed.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro-expansion? (Pre/Post conditions)

[Anh Vo]

On Wednesday, October 24, 2012 10:20:36 AM UTC-7, Hibou57 (Yannick Duchêne) wrote:
> Le Wed, 24 Oct 2012 18:45:27 +0200, Yannick Duchêne (Hibou57) <yannick_duchene@yahoo.fr> a écrit: > Le Wed, 24 Oct 2012 18:40:58 +0200, Yannick Duchêne (Hibou57) > <yannick_duchene@yahoo.fr> a écrit: > >> same snippet. Obviously, this does not stand for the reliable > Read “does not stand for the real thing”. > >> type A_Type is mod 256; > > Sorry, forget to say about a second variation: replace the above with > `type A_Type is new Positive;` and there will be no more error at > runtime (the first error, that is, with the useless package body still > there). That one is a lot weird. > More on that particular point. I you change `mod 256` into anything the modulo is above 256, not necessarily a power of two, as this works with `mod 257` two, then the bug disappears. The bug is there for any value below and included, 256. I suspected the element size, and indeed, that's not really the modulo, but the size. Replace `type A_Type is mod 256;` with this, with an added representation clause: type A_Type is mod 256; for A_Type'Size use 16; The module is still 256, but now the size changed, and the bug is not exposed.>>


You should file bug report for these problems. So far, I have filed two bug reports at report@gnat.com when using GNAT-GPL-2012 to compile Ada 2012 codes.

Re: GNAT doing macro-expansion? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Le Wed, 24 Oct 2012 20:16:26 +0200, Anh Vo <anhvofrcaus@gmail.com> a écrit:

> On Wednesday, October 24, 2012 10:20:36 AM UTC-7, Hibou57 (Yannick  
> Duchêne) wrote:
>> Le Wed, 24 Oct 2012 18:45:27 +0200, Yannick Duchêne (Hibou57)  
>> <yannick_duchene@yahoo.fr> a écrit: > Le Wed, 24 Oct 2012 18:40:58  
>> +0200, Yannick Duchêne (Hibou57) > <yannick_duchene@yahoo.fr> a écrit:  
>> > >> same snippet. Obviously, this does not stand for the reliable >  
>> Read “does not stand for the real thing”. > >> type A_Type is mod 256;  
>> > > Sorry, forget to say about a second variation: replace the above  
>> with > `type A_Type is new Positive;` and there will be no more error  
>> at > runtime (the first error, that is, with the useless package body  
>> still > there). That one is a lot weird. > More on that particular  
>> point. I you change `mod 256` into anything the modulo is above 256,  
>> not necessarily a power of two, as this works with `mod 257` two, then  
>> the bug disappears. The bug is there for any value below and included,  
>> 256. I suspected the element size, and indeed, that's not really the  
>> modulo, but the size. Replace `type A_Type is mod 256;` with this, with  
>> an added representation clause: type A_Type is mod 256; for A_Type'Size  
>> use 16; The module is still 256, but now the size changed, and the bug  
>> is not exposed.>>
>
>
> You should file bug report for these problems. So far, I have filed two  
> bug reports at report@gnat.com when using GNAT-GPL-2012 to compile Ada  
> 2012 codes.

But I'm not an AdaCore client, so I believe this would be useless. I use  
to send them bug reports, but they always underlined there's no warranty  
it will be taken into account, as as‑understandably, their clients comes  
first, and are already source of supported support requests.

That said, I may compile the snippets into a bug report to them, later, if  
ever that may be useful to them and their clients, but I feel to guess  
their clients are less interested in Ada 2012's predicates than I am, and  
seems to favor Ada 95 and Ada 2005 (or am I wrong?).

Also, the cases are even more tricky than I first believed, I've noticed  
some other new things (should I post these or not?).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro-expansion? (Pre/Post conditions)

[Simon Wright]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> But I'm not an AdaCore client, so I believe this would be useless.

If you don't send the bug report, and it's one that their customers
haven't come across, then it won't get fixed.

AdaCore _do_ take note of bugs filed by unsupported customers, but I'd
think this is much more likely to happen for good bug reports (that is,
with a clear statement of what you expected to happen, what actually
happened, and a reproducer).

Re: GNAT doing macro-expansion? (Pre/Post conditions)

[Yannick Duchêne (Hibou57)]

Le Wed, 24 Oct 2012 20:53:50 +0200, Simon Wright <simon@pushface.org> a  
écrit:
> AdaCore _do_ take note of bugs filed by unsupported customers, but I'd
> think this is much more likely to happen for good bug reports (that is,
> with a clear statement of what you expected to happen, what actually
> happened, and a reproducer).

I you see issues with the expected clarity of what I presented, feel free  
to tell, before I send them. I will post some other details later (or not  
here, I don't already know).

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: GNAT doing macro-expansion? (Pre/Post conditions)

[Simon Wright]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> Le Wed, 24 Oct 2012 20:53:50 +0200, Simon Wright <simon@pushface.org>
> a écrit:
>> AdaCore _do_ take note of bugs filed by unsupported customers, but
>> I'd think this is much more likely to happen for good bug reports
>> (that is, with a clear statement of what you expected to happen, what
>> actually happened, and a reproducer).
>
> I you see issues with the expected clarity of what I presented, feel
> free to tell, before I send them. I will post some other details later
> (or not here, I don't already know).

Looks clear enough to me!

When I tried this it failed on x86_64 Mac with all of GCC 4.6, 4.7 and
GNAT GPL 2012. I get CE with "erroneous memory access".

Under the debugger, it turns out it's an assertion failure (tell AdaCore
you compiled with -gnata !), probably caused by some mis-ordering of the
initializations vs the predicate checks; with 4.7, I is -7952, J is
24515 and K is -1 at the point of failure.