Version 1.5 of ai12s/ai12-0191-1.txt

Unformatted version of ai12s/ai12-0191-1.txt version 1.5
Other versions for file ai12s/ai12-0191-1.txt

!standard 3.9.1(4.1/2)          19-02-06 AI12-0191-1/02
!standard 7.3.2(10.1/4)
!standard 7.3.2(15/5)
!class binding interpretation 16-06-06
!status work item 16-06-06
!status received 16-05-31
!priority Low
!difficulty Medium
!qualifier Omission
!subject Clarify "part" for type invariants
!summary
Screened components are not checked even if a type invariant check would apply to them.
!question
The term "part" is used several times in the section on Type Invariants. Does this usage of "part" include the "parent part"? (No.)
!recommendation
(See Summary.)
!wording
Add after AARM 3.1(7.d/3): [continuing the AARM note]
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 screened components (see 3.9.1). Other terms, such as "subcomponent" and "part", are interpreted analogously.
Add after 3.9.1(4.1/2):
In the case where the (compile time) view of an object X is of a tagged type T1 or T1'Class and the (runtime) tag of X is T2'Tag, the components (if any) of X which are not components of T1 (and which are not discriminants which correspond to a discriminant of T1) are said to be "screened". For example, if T2 is an undiscriminated extension of T1 which declares a component named Comp, then X.Comp would be an screened component of X. A part of an object is said to be either a screened part or an unscreened part depending on whether it is a part of a screened component of the object.
AARM note: For example, there is a dynamic semantics rule that finalization of an object includes finalization of its components (see 7.6.1). In the following case
type T1 is tagged null record; type T2 is new T1 with record Comp : Some_Controlled_Type; end record; function Func return T1'Class is (T2'(others => <>)); X : T1'Class := Func;
the rule that "every component of the object is finalized" (as opposed to something like "every unscreened component of the object is finalized") means that the finalization of X will include finalization of X.Comp. For another example, see the rule about accessibility checking of access discriminants of parts of function results in 6.5. In contrast, the rules in 7.3.2 explicitly state that type invariant checks are only performed for unscreened parts which are of the type-invariant bearing type (as opposed to for all parts, screened or not, which are of that type).
Modify 7.3.2(10.1/4):
After successful explicit initialization of the completion of a deferred constant with a part of type T, if the completion is inside the immediate scope of the full view of T, and the deferred constant is visible outside the immediate scope of T, the check is performed on the {unscreened} part(s) of type T;
Modify 7.3.2(15/5):
Upon a successful return from a call on any subprogram or entry which is type-invariant preserving for T, an invariant check is performed on each {unscreened} part of type T which is subject to an invariant check for T. In the case of a call to a protected operation, the check is performed before the end of the protected action. In the case of a call to a task
entry, the check is performed before the end of the rendezvous;
Replace AARM 7.3.2(20.a.1/5):
To be honest: {AI12-0167-1} In all of the above, for a class-wide object, we are only referring to the parts of the specific root type of the class. We don't want the overhead of checking every class-wide object in case some future extension component might have type T (contrast this to finalization, where we do intend that overhead).
with:
Reason: The various rules requiring type invariant checks for unscreened parts of type T, as opposed to all parts of type T, are motivated by a desire to avoid overhead associated with the possibility that there might exist an extension of the tagged type in question which has a part of type T.
!discussion
If the programmer wants the invariant to be enforced on all descendants, she can use Type_Invariant'Class on the original type. Therefore, we want Type_Invariant to work differently.
Also note that it is unusual to have a type extension in the same package as its parent. If, at a later point, the type extension is given its own package, we'd prefer that the invariant enforcement change as little as possible.
The wording does not guarantee that every use of "component", "subcomponent", and "part" in the RM has the correct meaning with respect to "hidden" components of tagged types, but it fixes the problematic cases that we know about and provides a framework so that fixing any further problems that are discovered should be straightforward.
Note that we don't use the word "hidden" in the proposed wording because that seems too tied to visibility, which is not what we are talking about. We are talking about components whose existence is likely to be unknown at compile-time even if the compiler looks through all private types and expands all generic instances (specs and bodies). The implementation of any dynamic semantics rule requiring that some action needs to be performed for such components (e.g., finalization) will typically require dispatching.
Probably the hardest question here is the choice of a term to refer to these hidden-but-we-don't-want-to-use-that-word components. For a view of an object X of a tagged type T1 whose underlying tag (i.e., the result of evaluating T1'Class (X)'Tag) is not T1'Tag, we are talking about the components of X which were declared in extensions of T1.
Choices that were considered include "underlying", "screened", "sequestered", "cloaked", and "occulted". We used "screened", but that's a fairly arbitrary choice and is easily changed.
!example
with Derived; use Derived; procedure Testinv is X : D; begin Create (X); end Testinv; --- package Derived is
type T is tagged private; type D is tagged private;
procedure Create (X : out T); procedure Create (X : out D);
private
type T is tagged record C : Integer; end record with Type_Invariant => T.C /= 0;
type D is new T with null record;
end Derived; --- package body Derived is
procedure Create (X : out T) is begin X.C := 1; end Create;
procedure Create (X : out D) is begin X.C := 0; -- Parent part type-invariant failure on return? (No.) end Create;
end Derived;
!ASIS
No ASIS effect.
!ACATS test
!appendix

From: Tucker Taft
Sent: Tuesday, May 31, 2016  2:13 PM

The term "part" is used several times in the section on Type Invariants.  The 
question is whether this always is meant to apply to the "parent part" (and
for that matter, every ancestor part) of the object.  My view is that when the
RM says "any part", we usually want it to mean precisely "any subcomponent, or
the object as a whole."  The definition of "part" also talks about sets of
subcomponents, and mentions it use in terms like the "parent part" and the
"extension part."  But I think those usages only make sense when we are
talking about untyped sets of things.  For a type invariant, clearly we are
only talking about "typed" parts, and I don't believe the parent part has a
type in the normal sense.  You can create a "typed view" of the parent part
by a view conversion, but until you do that, the parent part is not an object,
but rather just a collection of components.

Below is an example that shows the issue.  The question is whether the call on
Create for type D should fail on return, because the parent part doesn't
satisfy its invariant:
----

with Derived; use Derived;
procedure Testinv is
    X : D;
begin
    Create (X);
end Testinv;
---
package Derived is

    type T is tagged private;
    type D is tagged private;

    procedure Create (X : out T);
    procedure Create (X : out D);

private

    type T is tagged record
       C : Integer;
    end record
      with Type_Invariant => T.C /= 0;

    type D is new T with null record;

end Derived;
---
package body Derived is

    procedure Create (X : out T) is
    begin
       X.C := 1;
    end Create;

    procedure Create (X : out D) is
    begin
       X.C := 0; --  Parent part type-invariant failure on return?
    end Create;

end Derived;

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

From: Randy Brukardt
Sent: Tuesday, May 31, 2016  6:48 PM

> The term "part" is used several times in the section on Type 
> Invariants.  The question is whether this always is meant to apply to 
> the "parent part" (and for that matter, every ancestor part) of the 
> object.  My view is that when the RM says "any part", we usually want 
> it to mean precisely "any subcomponent, or the object as a whole."  
> The definition of "part" also talks about sets of subcomponents, and 
> mentions it use in terms like the "parent part" and the "extension 
> part."  But I think those usages only make sense when we are talking 
> about untyped sets of things.  For a type invariant, clearly we are 
> only talking about "typed" parts, and I don't believe the parent part 
> has a type in the normal sense.  You can create a "typed view" of the 
> parent part by a view conversion, but until you do that, the parent 
> part is not an object, but rather just a collection of components.

As usual, it's probably better to figure out what we want and then decide
whether the words say that, rather than try to figure out what the words
actually say. We already know (at least those of us that have tried to write
ACATS tests and objectives) that the wording of 7.3.2 is pretty fast-and-loose
about what is and is not included. (Steve's notes about "parts" known
dynamically vs. "parts" known statically are a big deal to this check being
efficient, but the wording is interpreted 100% differently than the very
similar wording for finalization.)

And I think that it doesn't make much sense for the parent extension to get
enforced separately for a type extension. If a programmer wants to ensure
that an invariant is enforced on extensions, they can use a
Type_Invariant'Class. Otherwise, as with all derived types, nothing gets
inherited.

> Below is an example that shows the issue.  The question is whether the 
> call on Create for type D should fail on return, because the parent 
> part doesn't satisfy its invariant:
> ----
> 
> with Derived; use Derived;
> procedure Testinv is
>     X : D;
> begin
>     Create (X);
> end Testinv;
> ---
> package Derived is
> 
>     type T is tagged private;
>     type D is tagged private;
> 
>     procedure Create (X : out T);
>     procedure Create (X : out D);
> 
> private
> 
>     type T is tagged record
>        C : Integer;
>     end record
>       with Type_Invariant => T.C /= 0;
> 
>     type D is new T with null record;
> 
> end Derived;
> ---
> package body Derived is
> 
>     procedure Create (X : out T) is
>     begin
>        X.C := 1;
>     end Create;
> 
>     procedure Create (X : out D) is
>     begin
>        X.C := 0; --  Parent part type-invariant failure on return?
>     end Create;
> 
> end Derived;

It's of course unusual to put a type and its extension into the same package,
so the answer here isn't terrible critical. But it's probably best for the
behavior to change as little as possible when these two types are inevitably
split into separate packages.

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

From: Steve Baird
Sent: Friday, August 19, 2016  2:24 PM

Pisa minutes say:

   Steve volunteers to help find out what GNAT does on cases of “parts”
   that are only dynamically known for type invariant checks.

No checks for these guys. For the following example (with all assertions
enabled) compiled with the GNAT compiler,

  procedure Type_Invariant_Breaker is

   type Root is tagged null record;

    package Pkg is
       type Has_Invariant is private;

       procedure Oops (X : in out Root'Class);
       procedure Rely_On_Incoming_Invariant (Y : Has_Invariant);
    private
       type Has_Invariant is record Lo, Hi : Integer := 0; end record
	with Type_Invariant => (Has_Invariant.Lo <= Has_Invariant.Hi);
    end Pkg;

    type Ext is new Root with
      record Field : Pkg.Has_Invariant; end record;

    package body Pkg is
       procedure Break_It (Xx : out Has_Invariant) is
       begin
	 Xx := (Lo => 1, Hi => 0);
       end;

       procedure Oops (X : in out Root'Class) is
       begin
	 if X in Ext'Class then
	    Break_It (Ext (X).Field);
	 end if;
       end;

       procedure Rely_On_Incoming_Invariant (Y : Has_Invariant) is
       begin
	 pragma Assert (Y.Lo <= Y.Hi);
       end;
    end Pkg;

    Ext_Var : Ext;
  begin
    Pkg.Oops (Ext_Var);
    Pkg.Rely_On_Incoming_Invariant (Ext_Var.Field);
  end;

we fail the assertion in Rely_On_Incoming_Invariant, which means that the
preceding call to Oops didn't fail any checks. I believe this implementation
is correct and should not be changed. The problem here is that the RM wording
doesn't make this clear (which is the topic of this AI).

The other interpretation (i.e., the one where the call to Oops would be
required to fail an invariant check) would be better in some sense but I don't
know how to implement it without introducing distributed overhead and a lot
more implementation complexity than than this feature would be worth.

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

From: Jeff Cousins
Sent: Tuesday, August 23, 2016  9:34 AM

Thanks for looking into that Steve.  I think we have accepted that invariant
checking can't check everything all of the time, and is just providing a
limited number of check points.

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

From: Steve Baird
Sent: Wednesday, February  6, 2019  7:18 PM

Here is some proposed wording for this AI, although I still have not gone 
through the RM with a fine-toothed comb reviewing each use of the terms 
"component", "subcomponent", and "part" with these issues in mind.

Many thanks to Randy for much helpful review, although (as usual) don't 
blame him for anything here that you don't like.

[This is version /02 of the AI - Editor.]

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

From: Randy Brukardt
Sent: Wednesday, February  6, 2019  10:06 PM

> Here is some proposed wording for this AI, ...

>!discussion (in addition to existing !discussion section)
>
>The following wording ...

Ahem. !wording *precedes* any !discussion. I dropped the word "following".

Also:

> ... The current write-up of the AI uses "screened", ...

Ahem, the reader is currently reading the AI, so this is mostly noise. I 
replaced this with "We used "screened", ..."

>append after 3.1(7.d/3), continuing the AARM note

As I noted before (and in the formatting rules I posted to the list), this 
should read something like:

Add after AARM 3.1(7.d/3): [continuing the AARM note]

Similar comments apply to the rest of this wording section.

Otherwise, looks good.

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

Questions? Ask the ACAA Technical Agent