Version 1.3 of ai12s/ai12-0338-1.txt

Unformatted version of ai12s/ai12-0338-1.txt version 1.3
Other versions for file ai12s/ai12-0338-1.txt

!standard 7.3.2(20/5)          19-07-02 AI12-0338-1/03
!class binding interpretation 19-06-15
!status Amendment 1-2012 19-07-02
!status ARG Approved 10-0-0 19-06-16
!status work item 19-06-15
!status received 19-06-14
!priority Low
!difficulty Easy
!qualifier Omission
!subject type invariant checking and incomplete types
!summary
Type invariants for type T are not checked for incomplete types whose completion is not available, even if that completion has components of type T.
!question
In the rules about when type invariants are checked, one case is:
an access-to-object parameter or result whose designated nominal type has a part of type T;
What does this mean when the designated nominal type is incomplete? (There is no check.)
For example:
limited with P2; package P1 is type T1 is private with Type_Invariant => Is_Ok (T1); function Is_Ok (X : T1) return Boolean; procedure Op (T2_Ref : access P2.T2); private type T1 is new Integer; function Is_Ok (X : T1) return Boolean is (X mod 123 /= 45); end P1;
with P1.Child; package body P1 is procedure Op (T2_Ref : access P2.T2) is begin P1.Child.Child_Op (T2_Ref); end Op; end P1;
private package P1.Child is procedure Child_Op (T2_Ref : access P2.T2); end P1.Child;
with P2; package body P1.Child is procedure Child_Op (T2_Ref : access P2.T2) is begin T2_Ref.all := (123, 45); end Child_Op; end P1.Child;
with P1; package P2 is type T2 is array (Boolean) of P1.T1; end P2;
with P1, P2; procedure Main is Ptr : access P2.T2 := new P2.T2; begin P1.Op (Ptr); end Main;
!recommendation
(See Summary.)
!wording
Replace the deleted 7.3.2(20/5) with:
If the nominal type of a formal parameter (or the designated nominal type of an access-to-object parameter or result) is incomplete at the point of the declaration of the callable entity, and if the completion of that incomplete type does not occur in the same declaration list as the incomplete declaration, then for purposes of the preceding rules the nominal type is considered to have no parts of type T.
Add after AARM 7.3.2(23.f/5):
Invariant checks are not performed for parts of incomplete types when the completion is not available. For this leak to occur for a type T that has a type invariant and is declared in a package P, one has to use a limited with on a package that has P in its semantic closure, and then use a type from that package as a parameter or result of a boundary subprogram for T (or as the designated type of a parameter or result of such a subprogram).
!discussion
To the extent that this obscure corner case has any importance at all, a check failure would be preferable from the user's perspective because it prevents a "bad" value from leaking out.
This interpretation is also consistent with the AI12-0191 rule:
For example, a reference to the components of an object in a rule that is interpreted at compile-time would not apply to components that are not visible. On the other hand, a reference to the components of an object in a dynamic semantics rule would apply to all components of the object, visible or not, including (for tagged objects) components which are not components of the nominal type of the object (see 3.9.1). Other terms, such as "subcomponent" and "part", are interpreted analogously.
But this could be burdensome for implementations because it could require checking the values of subcomponents whose existence is unknown at the point where invariant checking code is being generated.
If, for example, the implementation chooses to generate invariant checking code as part of code generation for the body of the callee (which is a reasonable choice that we don't want to preclude), then the completion of the designated type is unavailable and heroic measures would be required to generate a type invariant check.
Therefore, we define this as a leak similar to the class-wide leak.
!corrigendum 7.3.2(20/3)
Replace the paragraph:
The check is performed on each such part of type T.
by:
If the nominal type of a formal parameter (or the designated nominal type of an access-to-object parameter or result) is incomplete at the point of the declaration of the callable entity, and if the completion of that incomplete type does not occur in the same declaration list as the incomplete declaration, then for purposes of the preceding rules the nominal type is considered to have no parts of type T.
!ASIS
No ASIS effect.
!ACATS test
An ACATS C-Test should be constructed for a case like this.
!appendix

From: Steve Baird
Sent: Saturday, June 15, 2019  3:58 PM

Opening a new AI, spun off from AI12-0191. [This is version /01 of the 
AI - Editor.]

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

From: Randy Brukardt
Sent: Saturday, June 15, 2019  5:04 PM

Couple of comments:

(1) You need some wording to add to the "leak" AARM note, since this clearly 
causes another leak. That is, a short explanation of the leak and how to avoid 
it (see AI12-0210-1 for the form).

(2) I think you need to explain somewhere (probably !discussion) why there 
isn't a similar problem for parameters of an incomplete type (rather than 
just access types of incomplete types). I know you guys claimed it isn't a 
problem, and perhaps that's true, but we need to make it clear that we 
considered that (obviously similar) case and ruled out problems. (It's 
uncomfortable to have different rules for designated types and directly used 
types, but one can argue making a hole as small as possible is best.)

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

From: Randy Brukardt
Sent: Saturday, June 15, 2019  5:14 PM

BTW, I continue to believe you guys (Steve and Tucker) are wrong about the 
direct parameter case.

If, in your example, you replace type T2 by:


    type T2 is tagged record C : T1 end record;


and then consistently replace "access" with "in out" in your example, you 
get a program that is legal and has the same problem as you are fixing for
access cases. (Remember, that you can pass a tagged incomplete parameter to 
another tagged incomplete parameter without seeing the completion, because 
those have to be by-reference types, and presumably the compiler always knows 
how to do that regardless of the actual type. That rule was left over from the
failed Ada 2005 incomplete rules, but it still exists because we didn't want 
an incompatibility).

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

From: Tucker Taft
Sent: Saturday, June 15, 2019  5:53 PM

Good point.  I had forgotten about this "left over" capability.  So as long 
as the type is tagged incomplete, then the caller might not have visibility 
of the full type, so they shouldn't be expected to do the type-invariant 
check.

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

From: Steve Baird
Sent: Sunday, June 16, 2019  2:04 AM

Ditto.

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

From: Steve Baird
Sent: Sunday, June 16, 2019  2:58 AM

In response to Randy's good point, I withdraw the previously suggested wording 
change for this AI and suggest the following version instead.
[This is version /02 of the AI - Editor.]

====

!wording

Add before 7.3.2(21/4):

If the nominal type of a formal parameter (or the designated nominal type of 
an access-to-object parameter) is incomplete at the point of the declaration 
of the callable entity, and if the completion of that incomplete type does 
not occur in the same declaration list as the incomplete declaration, then 
for purposes of the preceding rules the nominal type is considered to have 
no parts of type T.

modify 7.3.2(23.a/5)
     ...  is not itself externally visible. { Incomplete types or
     class-wide types may be used to produce cases where subcomponents
     are not checked. } These cases represent holes ...

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

From: Randy Brukardt
Sent: Tuesday, July 2, 2019  11:06 PM

[A for-the-record note.]

[In relation to what is now AI12-0338-1.]

> !wording
> 
> Add before 7.3.2(21/4):
> 
> If the nominal type of a formal parameter (or the designated 
> nominal type of an access-to-object parameter) is incomplete 
> at the point of the declaration of the callable entity, and 
> if the completion of that incomplete type does not occur in 
> the same declaration list as the incomplete declaration, then 
> for purposes of the preceding rules the nominal type is 
> considered to have no parts of type T.

This placement would have this after the unrelated rule of 7.3.2(20.1/4). I
believe Steve meant to put it before that rule, or really to use the currently
deleted paragraph of 7.3.2(20/3) to hold this rule.

Also, not sure why this rule doesn't mention the designated nominal type of 
an access-to-object result, it's certainly legal to define such an access type.
So I added "or result" immediately before the closing paren.

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

Questions? Ask the ACAA Technical Agent