Version 1.4 of 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:
- if the object_name denotes the 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;
by:
- 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;
!corrigendum 8.5.1(4.6/2)
Replace the paragraph:
- 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.
by:
- 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.
!corrigendum 8.5.4(4.2/2)
Replace the paragraph:
- if the callable_entity_name 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;
by:
- 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;
!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:
- if the actual matching the formal_object_declaration denotes the
generic formal object 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;
!corrigendum 12.4(8.5/2)
Delete the paragraph:
- 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.
!corrigendum 12.6(8.2/2)
Replace the paragraph:
- if the actual matching the formal_subprogram_declaration
denotes a generic formal object of another generic unit G, and the
instantiation containing the actual that 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;
by:
- 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;
!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