Preelaboration

Preelaboration

[Simon Wright]

I (think I) need to eliminate elaboration calls in parts of my Cortex
GNAT Runtime Systems project[1], and I'm left with one that I can't
understand.

(1) what does pragma Preelaborate actually mean? I hoped it would mean
"you don't need to elaborate this package".

(2) If you give Preelaborate, is it a compiler error to generate
elaboration code? (the generated elaboration procedure does nothing).

(3) I find ARM 10.2.1(10)[2] unclear (I got here because the problematic
package body instantiates a generic). Does it mean that the
instantiation won't be preelaborable unless all of 10.1 .. 10.4 are
false? Or does it mean that the compiler will make these assumptions
regardless of actuals?

And, looking at (10.1), would you expect

   generic
      type Item is private with Preelaborable_Initialization;
   package Generic_Queues is

to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" not
allowed for formal type declaration'.

[1] https://sourceforge.net/projects/cortex-gnat-rts/
[2] http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-10-2-1.html#p10

Re: Preelaboration

[Jeffrey R. Carter]

On 05/16/2016 09:26 AM, Simon Wright wrote:
>
> And, looking at (10.1), would you expect
>
>    generic
>       type Item is private with Preelaborable_Initialization;
>    package Generic_Queues is
>
> to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" not
> allowed for formal type declaration'.

Preelaborable_Initialization is not listed as a language-defined aspect in ARM 
K.1. ARM 10.2.1 (11.8/2) says that pragma Preelaborable_Initialization may 
appear in a generic formal part, so if you replace the aspect with the pragma it 
should be legal.

-- 
Jeff Carter
"I'm a vicious jungle beast!"
Play It Again, Sam
131

Re: Preelaboration

[Simon Wright]

"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes:

> On 05/16/2016 09:26 AM, Simon Wright wrote:
>>
>> And, looking at (10.1), would you expect
>>
>>    generic
>>       type Item is private with Preelaborable_Initialization;
>>    package Generic_Queues is
>>
>> to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization"
>> not allowed for formal type declaration'.
>
> Preelaborable_Initialization is not listed as a language-defined
> aspect in ARM K.1. ARM 10.2.1 (11.8/2) says that pragma
> Preelaborable_Initialization may appear in a generic formal part, so
> if you replace the aspect with the pragma it should be legal.

Thanks! Solved the compilation issue, but that wasn't the cause of the
original problem.

I guess the fact that Preelaborable_Initialization isn't listed in K.1
was an oversight.

Re: Preelaboration

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lymvnqnf3h.fsf@pushface.org...
>I (think I) need to eliminate elaboration calls in parts of my Cortex
> GNAT Runtime Systems project[1], and I'm left with one that I can't
> understand.
>
> (1) what does pragma Preelaborate actually mean? I hoped it would mean
> "you don't need to elaborate this package".

What it says in 10.2.1, no more and no less. There is no required effect on 
code generation (unless Annex C is supported, and even then it is limited).

> (2) If you give Preelaborate, is it a compiler error to generate
> elaboration code? (the generated elaboration procedure does nothing).

No, the only errors are those defined by 10.2.1.

C.4 says that a subset of preelaborable packages should not generate any 
code. Which only applies if Annex C is implemented, and in any case is not a 
testable requirement (the ACATS cannot require code inspection, which is the 
only way to determine if C.4 is followed).

C.4(12) supposedly requires documentation of cases where code is generated, 
but that sort of requirement is widely ignored. (And would be useless, I'd 
just write something like "Elaboration of a preelaborable package may 
execute code in all cases other than those required by C.4 to not execute 
any code." It's way too hard for an implementer to figure out what will and 
will not do something.

(And this whole set of requirements is silly anyway. What implementer 
executes code if they don't have to?? So anything that can be done without 
code is done that way, and everything else executes some code, regardless of 
any categorization pragma.)

> (3) I find ARM 10.2.1(10)[2] unclear (I got here because the problematic
> package body instantiates a generic). Does it mean that the
> instantiation won't be preelaborable unless all of 10.1 .. 10.4 are
> false? Or does it mean that the compiler will make these assumptions
> regardless of actuals?

This means that the generic body would be illegal if preelaborated, unless 
it means the preelaboration requirements using those assumptions. The 
instance can't be preelaborable unless the body is.

> And, looking at (10.1), would you expect
>
>   generic
>      type Item is private with Preelaborable_Initialization;
>   package Generic_Queues is
>
> to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" not
> allowed for formal type declaration'.

Preelaborable_Initialization is not an aspect, as it is not the same for all 
views of a type. We tried to come up with a model to make it an aspect and 
failed to come up with something that makes sense.

In addition, formal types aren't allowed to have language-defined aspects, 
as that would add implicit contracts to the specification (and notably, 
would need rules for those contracts). pragma P_I isn't allowed in a formal 
part, either.

To get a formal type that has P_I, you'd need to use a generic derived type 
where the ancestor has P_I. Probably not what you want.

I would guess in this case that the instance in a preelaborable package 
should make the package illegal; the generic would need to be Preelaborable, 
but then it most likely would be illegal.

But this area is complicated (I might be getting it all wrong) and it 
probably doesn't do what you want anyway (Pure/Preelaborable categorizations 
in general were a failure, as they can't be applied to the majority of 
packages). I don't really have any advice, other than if you really care, 
look up the old AIs on the topic.

                           Randy.

Re: Preelaboration

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> In addition, formal types aren't allowed to have language-defined aspects,
> as that would add implicit contracts to the specification (and notably,
> would need rules for those contracts). pragma P_I isn't allowed in a formal
> part, either.

But 10.2.1(10.1), (11.2) explicitly mention P_I in a formal part?

> But this area is complicated (I might be getting it all wrong) and it
> probably doesn't do what you want anyway (Pure/Preelaborable categorizations
> in general were a failure, as they can't be applied to the majority of
> packages). I don't really have any advice, other than if you really care,
> look up the old AIs on the topic.

Thanks for the advice. Things are clearer now, I think; anyway, it turns
out it was indeed the generic that caused the package it was
instantiated in to require elaboration. I expanded the generic (of which
this was the only instance, huh) by hand in the caller, no more
elaboration.

GNAT has a program-unit restriction No_Elaboration_Code[1] which is a
lot closer to what I want. I can't remember now how I got into the state
where the compiler told me I couldn't use it ...

[1] https://gcc.gnu.org/onlinedocs/gnat_rm/No_005fElaboration_005fCode.html

Re: Preelaboration

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lya8jpoguk.fsf@pushface.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> In addition, formal types aren't allowed to have language-defined 
>> aspects,
>> as that would add implicit contracts to the specification (and notably,
>> would need rules for those contracts). pragma P_I isn't allowed in a 
>> formal
>> part, either.
>
> But 10.2.1(10.1), (11.2) explicitly mention P_I in a formal part?

These are bug, IMHO, because there are no matching rules for P_I. One could 
not be allowed to instantiate a generic whose formal has P_I with a type 
that does not have P_I. Else the assumptions of the body are violated.

Besides, 10.2.1(11.6/2) says that the pragma has to appear in the visible 
part of a package or generic package; the formal part of a generic package 
is not part of the visible part.

I suspect that there was an intent that this would work, but there is a lot 
missing that would make it work.

>> But this area is complicated (I might be getting it all wrong) and it
>> probably doesn't do what you want anyway (Pure/Preelaborable 
>> categorizations
>> in general were a failure, as they can't be applied to the majority of
>> packages). I don't really have any advice, other than if you really care,
>> look up the old AIs on the topic.
>
> Thanks for the advice. Things are clearer now, I think; anyway, it turns
> out it was indeed the generic that caused the package it was
> instantiated in to require elaboration. I expanded the generic (of which
> this was the only instance, huh) by hand in the caller, no more
> elaboration.
>
> GNAT has a program-unit restriction No_Elaboration_Code[1] which is a
> lot closer to what I want. I can't remember now how I got into the state
> where the compiler told me I couldn't use it ...
>
> [1] 
> https://gcc.gnu.org/onlinedocs/gnat_rm/No_005fElaboration_005fCode.html

                            Randy.

Re: Preelaboration

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> Besides, 10.2.1(11.6/2) says that the pragma has to appear in the visible 
> part of a package or generic package; the formal part of a generic package 
> is not part of the visible part.

But 8.2(8) says otherwise.  How else could it be?  The generic formals
have to be visible at the instantiation, so they can be referred to in
named-notation assocs.

I'm not sure how this affects the P_I pragma, but for sure generic
formals are visible at the instantiation.

- Bob