Version 1.4 of 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 WG9 Approved 22-06-22
!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