Version 1.4 of ai12s/ai12-0287-1.txt

Unformatted version of ai12s/ai12-0287-1.txt version 1.4
Other versions for file ai12s/ai12-0287-1.txt

!standard 8.5.1(4.4/2)          18-11-20 AI12-0287-1/03
!standard 8.5.1(4.5/2)
!standard 8.5.1(4.6/2)
!standard 8.5.4(4.2/2)
!standard 12.4(8.3/2)
!standard 12.4(8.4/2)
!standard 12.4(8.5/2)
!standard 12.4(8.2/5)
!standard 12.6(8.2/5)
!class binding interpretation 18-07-27
!status Amendment 1-2012 18-11-15
!status ARG Approved 5-0-1 18-10-21
!status work item 18-07-27
!status received 18-07-23
!priority Low
!difficulty Easy
!qualifier Clarification
!subject Legality Rules for null exclusions in renaming are too fierce
!summary
The null exclusion Legality Rules for generic formal object matching should only apply to generic formal objects with mode in out.
The null exclusion Legality Rules for object renaming and for generic formal object matching have special cases that should only apply to generic formal objects with mode in out.
The null exclusion rule for object renaming needs a similar rule for the result of a generic formal function.
!question
In 8.5.1, we have paragraphs 4.4-4.6, described as a "no lying" rule for null exclusions:
For an object_renaming_declaration with a null_exclusion or an access_definition that has a null_exclusion:
* if the object_name denotes a generic formal object of a generic unit G, and
the object_renaming_declaration occurs within the body of G or within the body of a generic unit declared within the declarative region of G, then the declaration of the formal object of G shall have a null_exclusion;
* otherwise, the subtype of the object_name shall exclude null. In addition to
the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
The first bullet supposedly is to handle "one obscure case" as the AARM says (I won't put that example here, see it in the AARM at http://www.ada-auth.org/standards/2xaarm/html/AA-8-5-1.html#p4.a).
The reason we need this rule is so that a object declared with a null exclusion never has the value \null\. Recall that the subtype of a formal in out object is ignored for matching purposes, so using the name of a subtype that excludes null does not imply anything about whether the actual object excludes null. Requiring the syntactic "not null" ensures that the actual object will in fact exclude null. This sort of thing is necessary as a renamed object is not necessarily read or written at any particular point (unlike the initialization of a constant), so there is no natural place to put a dynamic check (and distributing that over any operations on the object would defeat the main purpose of the exclusion, which is to avoid such checks on uses of the object).
This example uses \in out\ formal objects. But the rule as written also applies to \in\ formal objects. But the problem does not exist for \in\ formal objects; the subtype of such an object is respected and is checked when the generic is instantiated.
Should this rule only apply to \in out\ generic formal objects? (Yes.)
!recommendation
(See Summary.)
!wording
Replace 8.5.1(4.4-6/2) with:
For an object_renaming_declaration with a null_exclusion or an access_definition that has a null_exclusion, the subtype of the object_name shall exclude null. In addition, if the object_renaming_declaration occurs within the body of a generic unit G or within the body of a generic unit declared within the declarative region of generic unit G, then:
* if the object_name statically denotes a generic formal object of mode \in out\ of G, then the declaration of that object shall have a null_exclusion;
* if the object_name statically denotes a call of a generic formal function of G, then the declaration of the result of that function shall have a null_exclusion.
In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
Modify 8.5.4(4.2/2):
* if the callable_entity_name {statically} denotes a generic formal subprogram
of a generic unit G, and the subprogram_renaming_declaration occurs within the body of a generic unit G or within the body of a generic unit declared within the declarative region of the generic unit G, then the corresponding parameter or result subtype of the formal subprogram of G shall have a null_exclusion;
[Note: This fix and the 12.6 one could have been in a presentation AI, but I put them here since they're related to the others. See the !discussion for why the change. - Editor.]
Replace 12.4(8.3-8.5/2) with:
For a formal_object_declaration of mode \in out\ with a null_exclusion or an access_definition that has a null_exclusion, the subtype of the actual matching the formal_object_declaration shall exclude null. In addition, if the actual matching the formal_object_declaration statically denotes the generic formal object of mode \in out\ of another generic unit G, and the instantiation containing the actual occurs within the body of G or within the body of a generic unit declared within the declarative region of G, then the declaration of the formal object of G shall have a null_exclusion. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
Modify 12.4(8.4/2):
* if the actual matching the formal_object_declaration {statically} denotes
the generic formal object {of mode \in out\} of another generic unit G, and the instantiation containing the actual occurs within the body of G or within the body of a generic unit declared within the declarative region of G, then the declaration of the formal object of G shall have a null_exclusion;
Modify 12.6(8.2/5) (as modified by AI12-0183-1):
* if the actual matching the formal_subprogram_declaration {statically}
denotes a generic formal subprogram of another generic unit G, and the instantiation containing the actual occurs within the body of a generic unit G or within the body of a generic unit declared within the declarative region of the generic unit G, then the corresponding parameter or result type of the formal subprogram of G shall have a null_exclusion;
!discussion
The original discussion of this issue never considered the distinction between in and in out generic formal objects. All of the examples were of generic formal objects with mode in out. Therefore, it's likely an oversight that mode in formal objects are included in these rules.
In the case of formal objects, when the actual is a formal of another generic, both the object being matched and the actual object need to be generic formal objects of mode in out. (An actual of mode in is a constant.)
Note that the rule is dubious for generic formal object with mode in anyway, since the actual is an expression, and might therefore be something that doesn't denote anything.
---
The wording used "denotes", but that is a dynamic concept inappropriate for a Legality Rule. We don't expect compilers to reject code where the name is a dereference that happens to denote the formal object! Therefore the wording was changed to "statically denotes".
---
During the discussion of this issue, Steve Baird (who else?) noticed that formal functions have a similar issue - the subtype is ignored, and since a function result is an object that can be renamed, we need a similar assume-the-worst rule for that case. Note that we need that rule only for renaming; the actual for a generic formal in out object has be a variable, while a function result is always a constant. Thus a function result can never be the actual for a generic formal in out object.
!corrigendum 8.5.1(4.4/2)
Replace the paragraph:
For an object_renaming_declaration with a null_exclusion or an access_definition that has a null_exclusion:
by:
For an object_renaming_declaration with a null_exclusion or an access_definition that has a null_exclusion, the subtype of the object_name shall exclude null. In addition, if the object_renaming_declaration occurs within the body of a generic unit G or within the body of a generic unit declared within the declarative region of generic unit G, then:
!corrigendum 8.5.1(4.5/2)
Replace the paragraph:
by:
!corrigendum 8.5.1(4.6/2)
Replace the paragraph:
by:
In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
!corrigendum 8.5.4(4.2/2)
Replace the paragraph:
by:
!corrigendum 12.4(8.3/2)
Replace the paragraph:
For a formal_object_declaration with a null_exclusion or an access_definition that has a null_exclusion:
by:
For a formal_object_declaration of mode in out with a null_exclusion or an access_definition that has a null_exclusion, the subtype of the actual matching the formal_object_declaration shall exclude null. In addition, if the actual matching the formal_object_declaration statically denotes the generic formal object of mode in out of another generic unit G, and the instantiation containing the actual occurs within the body of G or within the body of a generic unit declared within the declarative region of G, then the declaration of the formal object of G shall have a null_exclusion. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
!corrigendum 12.4(8.4/2)
Delete the paragraph:
!corrigendum 12.4(8.5/2)
Delete the paragraph:
!corrigendum 12.6(8.2/2)
Replace the paragraph:
by:
!ASIS
No ASIS effect.
!ACATS test
The existing ACATS tests for these rules (B851002 and BC40003) have been modified to reflect the possibility of this change, and should be modified again to require these changes for Ada 2020.
!appendix

From: Randy Brukardt
Sent: Monday, July 23, 2018  7:11 PM

In 8.5.1, we have paragraphs 4.4-4.6, described as a "no lying" rule for null 
exclusions.

For an object_renaming_declaration with a null_exclusion or an 
access_definition that has a null_exclusion:

* if the object_name denotes a generic formal object of a generic unit G, and 
  the object_renaming_declaration occurs within the body of G or within the 
  body of a generic unit declared within the declarative region of G, then the 
  declaration of the formal object of G shall have a null_exclusion;

* otherwise, the subtype of the object_name shall exclude null. In addition to 
  the places where Legality Rules normally apply (see 12.3), this rule applies 
  also in the private part of an instance of a generic unit.

The first bullet supposedly is to handle "one obscure case" as the AARM says
(I won't put that example here, see it in the AARM at 
http://www.ada-auth.org/standards/2xaarm/html/AA-8-5-1.html#p4.a).

This example and all of the examples in the ACATS tests use "in out" formal 
parameters. However, the rule as written above applies to "in" formal 
parameters as well. But "in" formal parameters don't ignore their subtype 
information. So a similar example to the one in the AARM using "in"
parameters (without the "assume-the-worst" rule) raises Constraint_Error:

type Acc_I is access Integer;
subtype Acc_NN_I is not null Acc_I;
Obj : Acc_I := null;

generic
   B : in Acc_NN_I;
package Gen is
   ...
end Gen;

package body Gen is
   D : not null Acc_I renames B;
end Gen;

package Inst is new Gen (B => Obj); -- Raise Constraint_Error here.

Which means that there is no lying going on in this case. And by making the 
body illegal, we're rejecting a generic which works perfectly fine if the 
parameter is not null (just like the contract says!).

So I believe that the rule above should say "...denotes an in out generic 
formal object...".

There is a similar rule in the generic object matching case. That one is even 
more confusing, as it ought to apply to all generic formal objects, but just 
apply when the actual is an in out formal object. (This rule only applies to 
instances found in bodies, so we need to check if an actual to the instance is
a formal in out object itself, in which case the subtype info is not reliable;
there's no such problem for formal in objects.) [We recently fixed a typo in 
that rule, which is part of what started this train of thought. Working on the
minutes for the generic formal default AI reminded me of it, as the proposal 
is to use different syntax for a default in out object -- a similar case to 
this one.]

Does this make sense? Should we fix this wording (both places)?

P.S. Aside: The latter question meets Bob's test, in that implementing this 
Legality Rule is complex, and changing the wording (and thus the rule) will 
change the behavior of at least one implementer (me!).

****************************************************************

From: Bob Duff
Sent: Monday, July 23, 2018  7:35 PM

> Does this make sense? Should we fix this wording (both places)?

Yes.  Yes.

> P.S. Aside: The latter question meets Bob's test, in that implementing 
> this Legality Rule is complex, and changing the wording (and thus the 
> rule) will change the behavior of at least one implementer (me!).

Fair enough.  ;-)

****************************************************************

From: Tucker Taft
Sent: Tuesday, July 24, 2018  11:08 AM

Agreed.

****************************************************************

From: Steve Baird
Sent: Tuesday, July 24, 2018  11:39 AM

There appears to be a similar situation in the case of a renaming of call 
to a formal function. The renaming declaration in the following example is
currently legal; should it be illegal?

   procedure Bad_Call_Rename is
    type T is access Integer;

    subtype S is not null T;

    function F return T is (null);

    generic
       with function Ff return S;
    package G is
    end G;

    package body G is
       X : not null T renames Ff;
    begin
       X.all := 123;
    end G;

    package I is new G (Ff => F);
   begin
    null;
   end Bad_Call_Rename;

***************************************************************

From: Randy Brukardt
Sent: Tuesday, July 24, 2018  11:57 PM

...
> There appears to be a similar situation in the case of a renaming of 
> call to a formal function.

See? I warned you guys... :-) :-) :-)

[This was sent the day after Steve officially took the reins of the ARG, and I
had yanked his chain by noting that we'll have more "more scintillating 
discussions about minutia, like renaming of formal function results in a 
generic body" in that announcement. (Of course, he'd privately asked me about
this issue the previous day, so I knew it was coming.) - Editor.]

...
> The renaming
> declaration in the following example is currently legal; should it be 
> illegal?
> 
>    procedure Bad_Call_Rename is
>     type T is access Integer;
> 
>     subtype S is not null T;
> 
>     function F return T is (null);
> 
>     generic
>        with function Ff return S;
>     package G is
>     end G;
> 
>     package body G is
>        X : not null T renames Ff;
>     begin
>        X.all := 123;
>     end G;
> 
>     package I is new G (Ff => F);
>    begin
>     null;
>    end Bad_Call_Rename;

It certainly seems like it should be illegal. We have fairly complex rules to 
make similar renames of (stand-alone) objects and functions illegal, so it 
would be bizarre to allow the combination of the two to be legal.

It seems that the fix would be to add a call to a formal function with an 
appropriate result type to the object renames and generic matching rules
(which we're changing anyway).

***************************************************************

From: Randy Brukardt
Sent: Friday, November 16, 2018  4:52 PM

At our recent meeting, we adopted the wording for a Legality Rule in object 
renames. In context, the adopted wording (8.5.1(4.4-4.6/2)) is:

For an object_renaming_declaration with a null_exclusion or an 
access_definition that has a null_exclusion:
* if the object_renaming_declaration occurs within the body of a generic unit
  G or within the body of a generic unit declared within the declarative
  region of generic unit G, then
  * if the object_name statically denotes a generic formal object of mode 
    \in out\ of G, then the declaration of that object shall have a 
    null_exclusion;
  * if the object_name statically denotes a call of a generic formal 
    function of G, then the declaration of the result of that function shall 
    have a null_exclusion;
* otherwise, the subtype of the object_name shall exclude null. In addition
  to the places where Legality Rules normally apply (see 12.3), this rule
  applies also in the private part of an instance of a generic unit.

However, this doesn't quite work. The intent is that if the neither of the two 
subbullets of the first bullet are true, then the otherwise bullet applies. 
But the association of the bullets doesn't really work that way; at least it
is arguable that the otherwise only applies if the first primary bullet does
not apply (regardless of whether the subbullets are true or not).

The fully correct fix would be to duplicate the "otherwise" bullet. But that 
would defeat the original purpose of this restructuring, which was to avoid
redundancy.

My second thought was to add a To Be Honest note and forget it:

  AARM To Be Honest: If neither of these subbullets applies to the
  object_renaming_declaration, then the otherwise bullet below applies.

But it occurred to me that a trivial fix would be to add "and" before the 
then:

* if the object_renaming_declaration occurs within the body of a generic unit
  G or within the body of a generic unit declared within the declarative
  region of generic unit G, {and} then

which makes it clearer that these have to be completely satisfied; but I'd 
still want the AARM note (now a Ramification) to make this clearer. (This is
what I'm using for the moment, so I don't stay stuck on this AI.)

However, it strikes me that starting over would be better still. In 
particular, in this case, the object_name always has to exclude null. In 
some cases, the original declaration has to do that syntactically, which is
an additional (as opposed to separate) requirement. So we can eliminate the
otherwise by putting it into the header (this also makes it clearer that 
the generic contract boilerplate applies to the entire thing, not just the 
otherwise).

That leaves us with:

For an object_renaming_declaration with a null_exclusion or an 
access_definition that has a null_exclusion, the subtype of the object_name 
shall exclude null. In addition, if the object_renaming_declaration occurs 
within the body of a generic unit G or within the body of a generic unit 
declared within the declarative region of generic unit G, then
  * if the object_name statically denotes a generic formal object of mode 
    \in out\ of G, then the declaration of that object shall have a 
    null_exclusion;
  * if the object_name statically denotes a call of a generic formal 
    function of G, then the declaration of the result of that function shall 
    have a null_exclusion.
In addition to the places where Legality Rules normally apply (see 12.3), 
this rule applies also in the private part of an instance of a generic unit.

Is this better? 

This brings up the question whether the other similar wordings should be 
redone similarly (they're all modified by this AI). For instance, we're 
changing 12.4(8.3-8.4/2), giving us:

For a formal_object_declaration of mode \in out\ with a null_exclusion or 
an access_definition that has a null_exclusion:
* if the actual matching the formal_object_declaration statically denotes
  the generic formal object of mode \in out\ of another generic unit G, and
  the instantiation containing the actual occurs within the body of G or within
  the body of a generic unit declared within the declarative region of G,
  then the declaration of the formal object of G shall have a null_exclusion;
* otherwise, the subtype of the actual matching the formal_object_declaration
  shall exclude null. In addition to the places where Legality Rules normally
  apply (see 12.3), this rule applies also in the private part of an instance
  of a generic unit.

We could do the same reorganization here:

For a formal_object_declaration of mode \in out\ with a null_exclusion or an 
access_definition that has a null_exclusion, the subtype of the actual 
matching the formal_object_declaration shall exclude null. In addition, if 
the actual matching the formal_object_declaration statically denotes the 
generic formal object of mode \in out\ of another generic unit G, and the
instantiation containing the actual occurs within the body of G or within
the body of a generic unit declared within the declarative region of G, 
then the declaration of the formal object of G shall have a null_exclusion.
In addition to the places where Legality Rules normally apply (see 12.3), 
this rule applies also in the private part of an instance of a generic unit.

(Or possibly as three paragraphs, which would be a bit more readable.)

If we do any of these, I think is enough change that we ought to revote the 
AI, which means either having a Letter Ballot on it or putting it on the 
agenda for re-approval on the December 10 call (the latter would be faster
in this case).

Thoughts??

***************************************************************

From: Randy Brukardt
Sent: Friday, November 16, 2018  5:15 PM

...
> However, this doesn't quite work. The intent is that if the neither of 
> the two subbullets of the first bullet are true, then the otherwise 
> bullet applies. But the association of the bullets doesn't really work 
> that way; at least it is arguable that the otherwise only applies if 
> the first primary bullet does not apply.

I mean here that it is arguable that whether or not the truth of the 
subbullets is considered in determining whether the otherwise applies.
Ignoring them for that purpose is not the intent here.

...
> This brings up the question whether the other similar wordings should 
> be redone similarly (they're all modified by this AI). For instance, 
> we're changing 12.4(8.3-8.4/2), giving us:

I might note that as an implementer and as an ACATS test writer, I found 
the original wording inscrutable. It took me a long time to hit on the 
insight that the lengthy bullet(s) is really an *additional* condition on
a renames (or an instance) given in a generic body. (And I had to 
understand the problem case that this is trying to fix to understand 
that.) This reorganization would say that outright, which might be easier 
to understand.

I also could note that I'm not sure that spending the effort on 
reorganizing the subprogram renames and subprogram actual cases are
worth it, simply because we aren't otherwise changing those (other than 
to add the word "statically"). The two we're changing significantly are 
easier to justify spending additional work on (and especially the one 
that is confusing).

***************************************************************

From: Tucker Taft
Sent: Friday, November 16, 2018  9:27 PM

I agree it makes sense to fix the ones that are significantly changed 
anyway, but not convinced it is worth making further changes.

***************************************************************

From: Randy Brukardt
Sent: Saturday, November 17, 2018  1:27 AM

But you didn't tell us which of the rewrites you preferred. Don't want to 
write/edit an AI with three choices for wording!

***************************************************************

From: Tucker Taft
Sent: Saturday, November 17, 2018  7:15 AM

I presumed you recommended the third one, which does seem the cleanest:


"For an object_renaming_declaration with a null_exclusion or an 
access_definition that has a null_exclusion, the subtype of the object_name 
shall exclude null. In addition, if the object_renaming_declaration occurs 
within the body of a generic unit G or within the body of a generic unit 
declared within the declarative region of generic unit G, then
 * if the object_name statically denotes a generic formal object of mode 
   \in out\ of G, then the declaration of that object shall have a 
   null_exclusion;
 * if the object_name statically denotes a call of a generic formal 
   function of G, then the declaration of the result of that function shall
   have a null_exclusion.
In addition to the places where Legality Rules normally apply (see 12.3),
this rule applies also in the private part of an instance of a generic unit."

***************************************************************

Questions? Ask the ACAA Technical Agent