!standard 3.9.1(4.1/2) 19-06-03 AI12-0191-1/10 !standard 7.3.2(10.1/4) !standard 7.3.2(15/5) !class binding interpretation 16-06-06 !status Amendment 1-2012 19-05-09 !status ARG Approved 11-0-0 19-05-09 !status work item 16-06-06 !status received 16-05-31 !priority Low !difficulty Medium !qualifier Omission !subject Clarify "part" for type invariants !summary Components that are not components of the nominal type 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 (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. Modify 3.3(23/5): At the place where a view of an object is defined, a *nominal subtype* is associated with the view.{ The *nominal type* of a view is the type of the nominal subtype.} ... 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 (run-time) tag of X is T2'Tag, only the components (if any) of X that are components of T1 (or that are discriminants which correspond to a discriminant of T1) are said to be "components of the nominal type" of X. Similarly, only parts (respectively, subcomponents) of T1 are parts (respectively, subcomponents) of the nominal type of X. AARM Ramification: For example, if T2 is an undiscriminated extension of T1 which declares a component named Comp, then X.Comp is not a component of the nominal type of X. 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 component of the nominal type 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 parts which are of the type-invariant bearing type and which are parts of the nominal type of the object (as opposed to for all parts, whether part of the nominal type or not, which are of the invariant-bearing type). Similarly, the rule in 13.13.2 governing which components of a composite value are read and written by the default implementations of Read and Write for a composite type states that only the components of the object which are components of the nominal type of the object are read or written. Replace 6.8(5.8/5): [from AI12-0075-1] * for result type R, if the function is a boundary entity for type R (see 7.3.2), no type invariant applies to type R; if R has a component type C, a similar rule applies to C. Replace 7.3.2(8.3-8.12/5) with: [from AI12-0075-1] For a nonabstract type T, a callable entity is said to be a *boundary entity* for T if it is declared within the immediate scope of T (or by an instance of a generic unit, and the generic is declared within the immediate scope of type T), or is the Read or Input stream-oriented attribute of type T, and either: * T is a private type or a private extension and the callable entity is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T; or * T is a record extension, and the callable entity is a primitive operation visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T. AARM Reason: A *boundary entity* is one that might require an invariant check for T. It includes subprograms that don't (visibly) involve T; since we don't want to break privacy, we can't statically know if some private type has some part of T. We'll reduce the set when we describe the actual checks. Modify 7.3.2(10.1/4): After successful explicit initialization of the completion of a deferred constant [with]{whose nominal type has} 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 part(s) of {the nominal type of the object that have }type T; Replace 7.3.2(15/5) with: [most recent version for AI12-0075-1] Upon successful return from a call on any callable entity which is a boundary entity for T, an invariant check is performed on each object 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 the object initialized by the stream attribute. The following objects of a callable entity are subject to an invariant check for T: * a result with a nominal type that has a part of type T; * an *out* or *in out* parameter whose nominal type has a part of type T; * an access-to-object parameter or result whose designated nominal type has a part of type T; or [Author's question: is "designated nominal type" OK? Or do we have to say "whose nominal type of its designated type"?] * for a procedure or entry, an *in* parameter of whose nominal type has a part of type T. AARM Ramification: This is a Dynamic Semantics rule, so we ignore privacy when determining if a check is needed. We do, however, use the nominal type to determine if a part of type T is present; therefore, parts that aren't known at compile-time (after ignoring privacy) are never subject to invariant checks. This is preferable, as we don't want overhead associated with the possibility that there might exist an extension of a tagged type that has a part of type T. (See the "leaks" note below for avoidance advice.) [Editor's note: The "leaks" note is actually in AI12-0210-1.] AARM Discussion: We don't check in parameters for functions to avoid infinite recursion for calls to public functions appearing in invariant expressions. Such function calls are unavoidable for class-wide invariants and likely for other invariants. This is the simplest rule that avoids trouble, and functions are much more likely to be queries that don't modify their parameters than other callable entities. [Editor's note: This is an existing note that just getting moved with the associated wording.] Delete AARM 7.3.2(20.a.1/5). [This is rewritten into a Ramification above.] Modify in 13.13.2(9/3): ... the Write or Read attribute for each component (excluding those, if any, that are not components of the nominal type of the object) is called ... !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 (for instance, finalization) will typically require dispatching. AI12-0075-1 moved much of the 7.3.2 wording to Static Semantics. That, however, doesn't work, as Static Semantics rules do not break privacy, meaning that in many cases, the "parts of T" and whether or not a type invariant applies is not known at the point of the subprogram definition. Therefore, we move most of the 7.3.2 rules back to the Dynamic Semantics part, and adjust the AI12-0075-1 Legality Rules accordingly. The AI12-0075-1 Legality Rules don't have to be very general, as the other rules of static expression functions ensure that the parameters and result all have static subtypes (thus eliminating partial views, access types, and composite types other than string types) and the parameters are all of mode in (so no invariants are checked on the parameters, ever). Thus, the only case to worry about is of the result type, and only when the full type has already happened (so privacy is not an issue). !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; !corrigendum 3.3(23/3) @drepl At the place where a view of an object is defined, a @i is associated with the view. The object's @i (that is, its subtype) can be more restrictive than the nominal subtype of the view; it always is if the nominal subtype is an @i. A subtype is an indefinite subtype if it is an unconstrained array subtype, or if it has unknown discriminants or unconstrained discriminants without defaults (see 3.7); otherwise, the subtype is a @i subtype (all elementary subtypes are definite subtypes). A class-wide subtype is defined to have unknown discriminants, and is therefore an indefinite subtype. An indefinite subtype does not by itself provide enough information to create an object; an additional @fa or explicit initialization @fa is necessary (see 3.3.1). A component cannot have an indefinite nominal subtype. @dby At the place where a view of an object is defined, a @i is associated with the view. The @i of a view is the type of the nominal subtype of the view. The object's @i (that is, its subtype) can be more restrictive than the nominal subtype of the view; it always is more restrictive if the nominal subtype is an @i. A subtype is an indefinite subtype if it is an unconstrained array subtype, or if it has unknown discriminants or unconstrained discriminants without defaults (see 3.7); otherwise, the subtype is a @i subtype (all elementary subtypes are definite subtypes). A class-wide subtype is defined to have unknown discriminants, and is therefore an indefinite subtype. An indefinite subtype does not by itself provide enough information to create an object; an additional @fa or explicit initialization @fa is necessary (see 3.3.1). A component cannot have an indefinite nominal subtype. !corrigendum 3.9.1(4.1/2) @dinsa A record extension is a @i if its declaration has no @fa and its @fa includes no @fas. @dinst In the case where the (compile-time) view of an object @i is of a tagged type T1 or T1'Class and the (run-time) tag of @i is T2'Tag, only the components (if any) of @i that are components of T1 (or that are discriminants which correspond to a discriminant of T1) are said to be @i of @i. Similarly, only parts (respectively, subcomponents) of T1 are parts (respectively, subcomponents) of the nominal type of @i. !corrigendum 6.8(5/4) !AI-0075-1 !AI-0191-1 @dinsa If the result subtype has one or more unconstrained access discriminants, the accessibility level of the anonymous access type of each access discriminant, as determined by the @fa or @fa of the @fa, shall not be statically deeper than that of the master that elaborated the @fa. @dinss Aspect Static shall be specified to have the value True only if the associated @fa: @xbullet @xbullet that is a potentially static expression;> @xbullet @xbullet and is of a static subtype;> @xbullet @xbullet @xbullet, if the function is a boundary entity for type @i (see 7.3.2), no type invariant applies to type @i; if @i has a component type @i, a similar rule applies to @i.> !corrigendum 7.3.2(8/3) @drepl If the Type_Invariant'Class aspect is specified for a tagged type @i, then the invariant expression applies to all descendants of @i. @dby If the Type_Invariant'Class aspect is specified for a tagged type @i, then a @i also applies to each nonabstract descendant @i of @i (including @i itself if it is nonabstract). For a nonabstract type @i, a callable entity is said to be a @i for @i if it is declared within the immediate scope of @i (or by an instance of a generic unit, and the generic is declared within the immediate scope of type @i), or is the Read or Input stream-oriented attribute of type @i, and either: @xbullet<@i is a private type or a private extension and the callable entity is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of @i; or> @xbullet<@i is a record extension, and the callable entity is a primitive operation visible outside the immediate scope of type @i or overrides an inherited operation that is visible outside the immediate scope of @i.> !corrigendum 7.3.2(10.1/4) @drepl @xbullet, if the completion is inside the immediate scope of the full view of @i, and the deferred constant is visible outside the immediate scope of @i, the check is performed on the part(s) of type @i;> @dby @xbullet, if the completion is inside the immediate scope of the full view of @i, and the deferred constant is visible outside the immediate scope of @i, the check is performed on the part(s) of type @i;> !corrigendum 7.3.2(15/4) @drepl @xbullet, the check is performed on the object initialized by the stream attribute;> @dby @xbullet, an invariant check is performed on each object which is subject to an invariant check for @i. 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. The following objects of a callable entity are subject to an invariant check for @i: @xinbull;> !corrigendum 7.3.2(17/4) @drepl @xinbull (or by an instance of a generic unit, and the generic is declared within the immediate scope of type @i),> @dby @xinbull or @i parameter whose nominal type has a part of type @i;> @xinbull; or> !corrigendum 7.3.2(19/3) @drepl @xinbull, or one or more parameters with a part of type @i, or an access to variable parameter whose designated type has a part of type @i.> @dby @xinbull parameterwhose nominal type has a part of type @i.> !corrigendum 13.13.2(9/3) @drepl For elementary types, Read reads (and Write writes) the number of stream elements implied by the Stream_Size for the type @i; the representation of those stream elements is implementation defined. For composite types, the Write or Read attribute for each component is called in canonical order, which is last dimension varying fastest for an array (unless the convention of the array is Fortran, in which case it is first dimension varying fastest), and positional aggregate order for a record. Bounds are not included in the stream if @i is an array type. If @i is a discriminated type, discriminants are included only if they have defaults. If @i is a tagged type, the tag is not included. For type extensions, the Write or Read attribute for the parent type is called, followed by the Write or Read attribute of each component of the extension part, in canonical order. For a limited type extension, if the attribute of the parent type or any progenitor type of @i is available anywhere within the immediate scope of @i, and the attribute of the parent type or the type of any of the extension components is not available at the freezing point of @i, then the attribute of @i shall be directly specified. @dby For elementary types, Read reads (and Write writes) the number of stream elements implied by the Stream_Size for the type @i; the representation of those stream elements is implementation defined. For composite types, the Write or Read attribute for each component (excluding those, if any, that are not components of the nominal type of the object) is called in canonical order, which is last dimension varying fastest for an array (unless the convention of the array is Fortran, in which case it is first dimension varying fastest), and positional aggregate order for a record. Bounds are not included in the stream if @i is an array type. If @i is a discriminated type, discriminants are included only if they have defaults. If @i is a tagged type, the tag is not included. For type extensions, the Write or Read attribute for the parent type is called, followed by the Write or Read attribute of each component of the extension part, in canonical order. For a limited type extension, if the attribute of the parent type or any progenitor type of @i is available anywhere within the immediate scope of @i, and the attribute of the parent type or the type of any of the extension components is not available at the freezing point of @i, then the attribute of @i shall be directly specified. !ASIS No ASIS effect. !ACATS test We could write a test to check that such components aren't checked (as in the example), but that doesn't seem to be very valuable. !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. **************************************************************** From: Steve Baird Sent: Tuesday, February 12, 2019 7:32 PM Here is another version of this AI, reflecting feedback received since the previous version was distributed on Feb 6 2019, notably at the last phone meeting. Two changes: 1) The term "screened" has been replaced with "supplementary" throughout the AI as per the guidance of the group. 2) The rules about which components are streamed in and out in the default implementations of 'Read and 'Write for a a tagged type are clarified. [This is version /03 of the AI - Editor.] **************************************************************** From: Tucker Taft Sent: Tuesday, February 12, 2019 8:01 PM The term "supplementary" is growing on me. The !discussion should still come afterward. I am somewhat worried we are combining the rules for class-wide objects with the rules for "shortened" specific views of objects. By "shortened" I mean a specific view of a type extension like T2 through a T1 "lens," where T1 is an ancestor of T2. A class-wide view and a "shortened" view generally seem to behave pretty differently. For example on assignment, clearly you finalize the whole left-hand side in the case of a class-wide assignment, but for a "shortened" specific view, I would think the "supplementary" components are completely untouched as far as finalization and adjustment. Is there really *any* case where for a shortened view, we touch the supplementary components? For type invariants, we have an elaborate set of rules on type conversions, so that we start looking at the masked components (hmm -- "masked" vs. "supplementary"?) as we unwind the conversions. But when you have the shortened view, you don't do anything with those supplementary/masked components. **************************************************************** From: Tucker Taft Sent: Tuesday, February 12, 2019 9:03 PM How about "masked" vs. "unmasked" components? Not sure if it is better... **************************************************************** From: Steve Baird Sent: Tuesday, February 12, 2019 9:12 PM I prefer "masked" to "supplementary". **************************************************************** From: Randy Brukardt Sent: Tuesday, February 12, 2019 9:22 PM Of course, if the concern is about implying something about visibility, "screened" or "masked" certainly have that flavor, while "supplementary" does not. The correct flavor would be more like "unknown components", since they are completely unknown to the implementation at the interesting point. "Unknown" doesn't appear in my thesaurus, someone else will have to look for alternatives to that... **************************************************************** From: Randy Brukardt Sent: Tuesday, February 12, 2019 9:29 PM > I am somewhat worried we are combining the rules for class-wide > objects with the rules for "shortened" specific views of objects. By > "shortened" I mean a specific view of a type extension like T2 through > a T1 "lens," where T1 is an ancestor of T2. A class-wide view and a > "shortened" view generally seem to behave pretty differently. For > example on assignment, clearly you finalize the whole left-hand side > in the case of a class-wide assignment, but for a "shortened" > specific view, I would think the "supplementary" components are > completely untouched as far as finalization and adjustment. Is there > really *any* case where for a shortened view, we touch the > supplementary components? Dunno. I didn't know/remember that assignment isn't supposed to finalize such components. I doubt that there is any ACATS test like that (assignments to [entire] tagged objects are rare in real code) -- I wonder if anyone gets that right? > For type invariants, we have an elaborate set of rules on type > conversions, so that we start looking at the masked components (hmm -- > "masked" vs. "supplementary"?) as we unwind the conversions. But when > you have the shortened view, you don't do anything with those > supplementary/masked components. But specifically for type conversions, if you have a class-wide view (that is, T'Class) in the spec of an invariant-preserving , then you want to check the T components (only). That is what is different here, I think. If that's not the case, then there's an argument that there never was a bug in the first place. That is, the (dynamic) components are *always* those of the view of the object (where the runtime view ignores any privacy). When one finalizes a stand-alone object or component of such an object, you always have the original view of that object/component, so of course you can see all of the subcomponents. And if you always see all of the components of a class-wide object, then QED (since that would cover any "interesting" deallocations). **************************************************************** From: Tucker Taft Sent: Wednesday, February 13, 2019 11:02 AM > But specifically for type conversions, if you have a class-wide view > (that is, T'Class) in the spec of an invariant-preserving , then you > want to check the T components (only). That is what is different here, I > think. I am not convinced we have this right. In my understanding of the intent, any class-wide object is presumed to satisfy all of its invariants. Another way of thinking about it is when you create a class-wide object, you are effectively passing outside of the package barrier, and you must be sure the object satisfies all invariants that apply to it. > If that's not the case, then there's an argument that there never was > a bug in the first place. That is, the (dynamic) components are > *always* those of the view of the object (where the runtime view > ignores any privacy). When one finalizes a stand-alone object or > component of such an object, you always have the original view of that > object/component, so of course you can see all of the subcomponents. > And if you always see all of the components of a class-wide object, then > QED (since that would cover any "interesting" deallocations). Class-wide objects generally worry about all of their components. The weird case is an object of a specific type, that was produced by doing a view conversion on an object with more components. These are the real oddball guys, and we need to decide how these are to be handled. **************************************************************** From: Steve Baird Sent: Wednesday, February 13, 2019 12:29 PM > For example on assignment, clearly you finalize the whole left-hand > side in the case of a class-wide assignment, but for a "shortened" > specific view, I would think the "supplementary" components are completely > untouched as far as finalization and adjustment. That's certainly true, but maybe this ought to be stated more clearly (perhaps in an AARM note) in the section on assignment statements. If we want to do that, that should probably be included in this AI. > Is there really *any* case where for a shortened view, we touch the > supplementary components? I can't think of any. The two cases that came to mind are finalization and the accessibility checks for access discriminants of a function result. But if the function result type is specific then there are no supplementary components of the function result object. And the cases where we get "shortened" views of longer objects (e.g., via parameter passing or View_Conversion'Access) are not cases where exiting a scope causes finalization of that shortened object. **************************************************************** From: Tucker Taft Sent: Wednesday, February 13, 2019 1:23 PM >I am not convinced we have this right. In my understanding of the intent, >any class-wide object is presumed to satisfy all of its invariants. Another >way of thinking about it is when you create a class-wide object, you are >effectively passing outside of the package barrier, and you must be sure the >object satisfies all invariants that apply to it. See AARM 7.3.2(20.a/4) for this "intent": Reason: Class-wide objects are treated as though they exist outside the scope of every type, and may be passed across package "boundaries" freely without further invariant checks. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 13, 2019 3:50 PM >See AARM 7.3.2(20.a/4) for this "intent": > >Reason: Class-wide objects are treated as though they exist outside the >scope of every type, and may be passed across package "boundaries" freely >without further invariant checks. This note is on class-wide types that are in the tree-of-T. These are invariants that the package reasonably could know about. But Steve has pointed out this also happens in the case of extensions of otherwise unrelated types that contain objects of T. This intent is not covered by any current invariant checks, since nothing class-wide related to T is involved. In the somewhat pathological case that the body has sufficient visibility to such an extension to pass/assign it an unchecked T, preventing that requires a dispatching check. Or some other substantial change to the model. Since this case requires contortions, we don't want to require implementations to check it, but would rather would describe it as a hole. At least that has been my understanding. Steve shows the case in interest in the e-mail: 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; I was thinking a case with an interface: package Pkg2 is type Has_Invariant is private; procedure Rely_On_Incoming_Invariant (Y : Has_Invariant); type Some_Interface is interface; procedure Munge (I : in out Some_Interface; Z : Has_Invariant) is abstract; procedure Oops (X : in out Some_Interface'Class); private type Has_Invariant is record Lo, Hi : Integer := 0; end record with Type_Invariant => (Has_Invariant.Lo <= Has_Invariant.Hi); end Pkg2; package body Pkg2 is procedure Break_It (Xx : out Has_Invariant) is begin Xx := (Lo => 1, Hi => 0); end; procedure Oops (X : in out Some_Interface'Class) is Bad : Has_Invariant; begin Break_It (Bad); X.Munge (Bad); end; end Pkg2; Here, the implementation of Munge (which is not related at all to the package, and thus will not be checking any invariants) can save Bad into an extension of X. Oops in theory should be checking that part when it exits, but there is no way for that to happen short of there being a dispatching routine that knows about all of the components of each extension of Some_Interface. (Again, Some_Interface itself is not related to T in any way.) --- I also note that the original question was about "parent part", and was posed by one Tucker Taft. I'm not sure why this matters (the "parent part" is not a "part" in the technical sense of "object or its components"), but I can see why it would confuse. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 13, 2019 6:25 PM > Here, the implementation of Munge (which is not related at all to the > package, and thus will not be checking any > invariants) can save Bad into an extension of X. Oops in theory should > be checking that part when it exits, but there is no way for that to > happen short of there being a dispatching routine that knows about all > of the components of each extension of Some_Interface. (Again, > Some_Interface itself is not related to T in any > way.) You might want to claim that Munge should check the invariant (inbound) because the dispatching is to an abstract routine that is itself "invariant-preserving". I think that's arguable, but in any case, if we change Munge to a function, it becomes irrelevant (invariants of inbound "in" parameters of functions are never checked). (And even if the invariant is checked in the procedure case, the object X is modified before the failure, meaning that the "leak" has already happened.) One could also create this case by using two interfaces, I1 and I2, with I2 a descendant of I1, I2 being in a separate package C1 and containing the Munge operation (which is therefore not invariant-preserving itself). If the body of the invariant-containing package Pkg2 withs C1, it can dispatch to the Munge operation, and again we can have a leak. As with all permitted holes in invariant protection, this sort of issue requires active participation of the package containing the invariant, so there is no reason to pay the steep cost to fix it. But we also want to ensure that (A) no one thinks that they have to implement such a check; and (B) that we include it in the list of holes. Both of these require a reasonable definition of what is *not* checked. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 13, 2019 6:47 PM ... > Of course, if the concern is about implying something about > visibility, "screened" or "masked" certainly have that flavor, while > "supplementary" > does not. > > The correct flavor would be more like "unknown components", since they > are completely unknown to the implementation at the interesting point. > "Unknown" > doesn't appear in my thesaurus, someone else will have to look for > alternatives to that... I just ran across a thesaurus in LibreOffice (never thought to look there), and it is happy to give alternatives to "unknown": "unmapped" "unbeknownst" "unheard-of" "unacknowledged" "unfamiliar" "dishonorable" :-) "unidentified" "anonynous" (um, no.) "unsuspected" "obscure" "unsung" "terra incognita" :-) :-) "stranger" "alien" "variable" (um, really no.) I have some favorites here, both serious and not so serious. Not sure how the rest of us feel. **************************************************************** From: Tullio Vardanega Sent: Thursday, February 14, 2019 2:17 AM Seems like "obscure", to me. **************************************************************** From: Tucker Taft Sent: Thursday, February 14, 2019 7:39 AM Here are two other pairs: *Overt* components, and *latent* components, of the current view. Components *included* in the current view, components *excluded* from the current view. I think it is worth using the term "view" when talking about this distinction, because it really is all about the view, not about the underlying object. **************************************************************** From: Edmond Schonberg Sent: Thursday, February 14, 2019 9:43 AM “Overt” seems perfect. Maybe “implicit” instead of latent? **************************************************************** From: Jean-Pierre Rosen Sent: Thursday, February 14, 2019 9:54 AM > I think it is worth using the term "view" when talking about this > distinction, because it really is all about the view, not about the > underlying object. Agreed, but if a full phrase is acceptable, then "components that are/are not part of the current view" would exactly describe what we mean. **************************************************************** From: Tucker Taft Sent: Thursday, February 14, 2019 11:16 AM >“Overt” seems perfect. Maybe “implicit” instead of latent? Alas, Ada already refers to the "implicit" components of a task or protected object, to represent entry queues. And implicit is already pretty heavily used for "implicit declarations" of inherited operations. I like "latent" in the sense of a "latent talent." It is there, but it just hasn't yet been brought forward. **************************************************************** From: Steve Baird Sent: Thursday, February 14, 2019 11:54 AM I agree. I don't think an antonym of "active" would be confusing even though we already have active priorities, active partitions, active locales, and active tasks. Interestingly, a variant part does not have an active variant; other terminology was used for that. **************************************************************** From: Tucker Taft Sent: Thursday, February 14, 2019 12:52 PM Yes. Let's leave "active" for something relating to tasks. **************************************************************** From: Gary Dismukes Sent: Thursday, February 14, 2019 12:49 PM > Alas, Ada already refers to the "implicit" components of a task or protected > object, to represent entry queues. And implicit is already pretty heavily > used for "implicit declarations" of inherited operations. I like "latent" > in the sense of a "latent talent." It is there, but it just hasn't yet been > brought forward. I had thought of mentioning "latent" at the meeting (as well as "concealed"), but didn't because it seemed to have too much of the sense of hidden, which was objected to. I would be OK with that choice, but J-P's suggestion along the lines of "components that are part of the current view" seems reasonable, and would avoid the need to introduce another new term. **************************************************************** From: Tucker Taft Sent: Thursday, February 14, 2019 1:24 PM > I had thought of mentioning "latent" at the meeting (as well as > "concealed"), but didn't because it seemed to have too much of the > sense of hidden, which was objected to. "Latent" doesn't imply any sort of hiding in my view. It just means it hasn't been recognized yet. > I would be OK with that choice, but J-P's suggestion along the lines > of "components that are part of the current view" seems reasonable, > and would avoid the need to introduce another new term. I agree, it may be that if we use the term "current view" explicitly, that everything will be quite clear -- "part of the current view," "a component of the current view," etc. all seem pretty clear. **************************************************************** From: Steve Baird Sent: Thursday, February 14, 2019 3:22 PM > I agree, it may be that if we use the term "current view" explicitly, that > everything will be quite clear -- "part of the current view," "a component > of the current view," etc. all seem pretty clear. I'll take another look at the AI with this approach in mind. **************************************************************** From: Steve Baird Sent: Thursday, February 21, 2019 9:56 PM I have attached two versions of this AI using the approach suggested by Jean-Pierre that Tuck referred to above. I like the idea of using a phrase instead of a single word to capture the property in question, but I don't like the suggested phrase. Nonetheless, in the attached v3 version (which I do not endorse) I used the suggested phrase. [This is version /04 of the AI - Editor.] It seems wrong to say that (by definition!) in a situation like package P1 is type T1 is private with Type_Invariant => ... ; package P2 is type T2 is private; private type T2 is record T1_Comp : T1; end record; end P1; procedure Foo (X : out P2.T2); private ... end P1; when we are deciding what type invariant checks to perform as part of a return from Foo, X.T2 is a component of the view of X. To me, it seems clear that if we are at a point when we can see only the partial view of P2.T2, then saying that X.T2 is a component of the view of X will lead to confusion or worse. So I used a different phrase in the attached v4 variant ("hidden by the nominal tag"). [This is version /05 of the AI - Editor.] That's the one I endorse, although others might suggest better phrases now that we seem to have given up on single words like "latent" or "screened". **************************************************************** From: Tucker Taft Sent: Friday, February 22, 2019 11:49 AM ... > when we are deciding what type invariant checks to perform as part of > a return from Foo, X.T2 is a component of the view of X. I presume you meant "T1 is a component of the view of X." And yes, I can see how partial views and the notion of "view" inherent in a "view conversion" could get confused with one another. > To me, it seems clear that if we are at a point when we can see only > the partial view of P2.T2, then saying that X.T2 is a component of the > view of X will lead to confusion or worse. Again, I presume you meant "... saying that T1 is a component of the view of X will lead ..." > So I used a different phrase in the attached v4 variant ("hidden by > the nominal tag"). Hmm.. You are bringing back the notion of "hiding" and introducing the notion of a "nominal tag." "Nominal tag" seems like a strange combination, because the tag is a run-time concept and never changes in the lifetime of the object. I could see using the term "nominal type" where "nominal" is what is expressing the notion of "view," and "type" is what determines what components are relevant. So I would suggest "part of the nominal type" or "components of the nominal type" both of which seem unambiguous. **************************************************************** From: Steve Baird Sent: Friday, February 22, 2019 11:58 AM > So I would suggest "part of the nominal type" or "components of the > nominal type" both of which seem unambiguous. Sounds good to me. I'll try to produce a version using this phrasing. **************************************************************** From: Steve Baird Sent: Friday, February 22, 2019 2:59 PM See attached. [This is version /06 of the AI - Editor.] This still suffers from the same problem I complained about (and thanks, Tuck, for deciphering the typos in my complaint) with the "part of the current view" phrasing (that was version v3). That is, there seems to be some misleading (at best) confusion with visibility/privacy rules, but this seems slightly better than that earlier v3 version. **************************************************************** From: Tucker Taft Sent: Friday, February 22, 2019 3:21 PM Another confusion, at least for me, is sometimes we say "a part of type T" and it is not clear whether we mean "a part *having* the type T" or a "part of some object O where O is of type T." I wonder whether we could simplify the phraseology a bit further, as sentences like this: "... the check is performed on the part(s) of type T that are parts of the nominal type of the object..." with: "... the check is performed on the part(s) of the nominal type of the object that have type T ..." **************************************************************** From: Steve Baird Sent: Friday, February 22, 2019 5:03 PM I agree, that is clearer. It is past the homework deadline, but I'll try to incorporate this approach. **************************************************************** From: Randy Brukardt Sent: Friday, February 22, 2019 5:21 PM I still have to file all of the previous attempts on this topic, so you probably have an hour or a bit more. **************************************************************** From: Steve Baird Sent: Friday, February 22, 2019 5:53 PM See attached. [This is version /07 of the AI - Editor.] **************************************************************** From: Tucker Taft Sent: Saturday, February 23, 2019 6:57 AM Looks good in general. I wonder about the new normative wording after 3.9.1(4.1/2). The first sentence uses a double negative, and the illustrative example doesn't read quite like normal normative RM text, and might better be an AARM note. Currently you propose: append after 3.9.1(4.1/2) (i.e., at the end of the Static Semantics section): 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 not be "components of the nominal type" of the object. For example, if T2 is an undiscriminated extension of T1 which declares a component named Comp, then X.Comp is not a component of the nominal type of X. Similarly, a part (respectively, subcomponent) of an object might or might not be a part (respectively, subcomponent) of the nominal type of the object. Here is a possible re-wording: In the case where the (compile-time) view of an object X is of a tagged type T1 or T1'Class and the (run-time) tag of X is T2'Tag, only the components (if any) of X that are components of T1 (or that are discriminants which correspond to a discriminant of T1) are said to be "components of the nominal type" of X. Similarly, only parts (respectively, subcomponents) of T1 are parts (respectively, subcomponents) of the nominal type of X. AARM Ramification: For example, if T2 is an undiscriminated extension of T1 which declares a component named Comp, then X.Comp is not a component of the nominal type of X. **************************************************************** From: Steve Baird Sent: Monday, February 25, 2019 1:08 PM I like it, and I agree that getting rid of the double negatives is a significant improvement. **************************************************************** From: Randy Brukardt Sent: Monday, February 25, 2019 8:10 PM Sigh. OK, I've posted an update [/08 of the AI] with this wording for discussion tomorrow. **************************************************************** From: Randy Brukardt Sent: Friday, May 10, 2019 7:25 PM I was asked to research the uses of the term "nominal type" in the RM and AARM, and check that they are compatible with the proposed definition: The *nominal type* of a view is the type of the nominal subtype of the view. The search engine finds only two uses in AARM notes: 4.3.4(14.b/5): This requires that the underlying tag (if any) associated with the delta_aggregate is that of the base_expression in the delta_aggregate and not that of the nominal type of the base_expression in the delta_aggregate. 6.1.1(26.b/4): This means that the underlying tag associated with X'Old is that of X and not that of the nominal type of X. These are compatible with the proposed definition. I note in passing that both of these notes are in areas that Steve Baird was a primary author of, as was the case of this AI. I detect a pattern. :-) **************************************************************** From: Randy Brukardt Sent: Tuesday, May 14, 2019 1:51 AM One of the wording changes of AI12-0191-1 is: * Upon successful return from a call on any subprogram or entry which is type-invariant preserving for T, an invariant check is performed on each part of {the nominal type of the object that has} type T which is subject to an invariant check for T. ... "*the* object"??? We're talking about a call, and suddenly "the object" appears out of nowhere. The original wording carefully avoided talking about specific objects, probably because the pile of bullets calling out what is subject to invariant checks is massive. On top of which, there's very likely to be multiple objects here, so "the" is wrong in any case. We're probably talking about some object that is "subject to an invariant check", so perhaps we need to say that somehow: * Upon successful return from a call on any subprogram or entry which is type-invariant preserving for T, an invariant check is performed on each object which is subject to an invariant check for T for each part of the nominal type of the object that has type T . ... However, this is all rather bogus, since the entire point of the "part of the nominal type of the object" rule is that such parts are *not* subject to an invariant check. Indeed, it seems bizarre to say such parts are subject to a check and then essentially erase that check at the last instant. You could even imagine cases where entire subprograms qualify as type-invariant preserving only because of components that aren't even known at compile-time. That seems completely wrong. So I'm thinking that this wording change is applied in the wrong place (7.3.2(15/5) rather than 7.3.2 (8.8-8.11/5). I could even make the argument that since 7.3.2(8.8-8.11/5) is labeled as a "static semantics" rule, there's no issue in the first place: the parts talked about in 7.3.2(8.8-8.11/5) are clearly compile-time views [that is, "parts of the nominal type"] and other parts aren't "subject to an invariant check" in the first place (regardless of if they have a part of T). (Note that the rewording of 7.3.2(8.8-8.11/5) probably happened after AI12-0191-1 was opened, so this later rewording inadvertently fixed the AI-191's issue.) So the easiest fix is to completely eliminate the change to 7.3.2(15/5), and then just fix up the existing AARM note (probably reclassifying as a Ramification): Invariant checks are only performed on parts of the nominal type of objects. We don't have to say that for calls, since the objects that are "subject to an invariant check" are determined at compile-time (as the appropriate rules are Static Semantic rules), and parts not known at compile-time (that is, those not parts of the nominal type) are never subject to an invariant check. This is preferable anyway, as we don't want overhead associated with the possibility that there *might* exist an extension of a tagged type that has a part of type T. (See the "leaks" note below for avoidance advice.) [Note: The "holes" AARM note needs to be updated to mention this hole, but there is a complete overhaul of that note proposed in AI12-0210-1 (including talking about "leaks" rather than "holes}. We were supposed to discuss these two AIs together (since they're related), but we ran out of time before doing that. And I just noticed that that AI used "screened" several times. So I just updated it.] Thoughts on this wording? **************************************************************** From: Jean-Pierre Rosen Sent: Tuesday, May 14, 2019 4:03 AM > call on any subprogram or entry Nitpicking: isn't "callable entity" the official term rather than "subprogram or entry" ? **************************************************************** From: Steve Baird Sent: Tuesday, May 14, 2019 8:11 PM ... > Thoughts on this wording? Makes sense. An object which is "subject to an invariant check for T" is known to be of type T (this follows from the definition of the term). So could we eliminate the "of type T" qualifier in the "Upon successful return from a call" paragraph on the grounds that it is redundant? This would leave us with Upon successful return from a call on any subprogram or entry which is type-invariant preserving for T, an invariant check is performed on each object that is subject to an invariant check for T. It's always nice to eliminate wording like "a part of type T" because, strictly speaking, there is an ambiguity there (even if the resolution is "obvious"). ****************************************************************