CVS difference for ai12s/ai12-0191-1.txt

Differences between 1.13 and version 1.14
Log of other versions for file ai12s/ai12-0191-1.txt

--- ai12s/ai12-0191-1.txt	2019/05/14 07:03:41	1.13
+++ ai12s/ai12-0191-1.txt	2019/06/05 05:54:32	1.14
@@ -1,4 +1,4 @@
-!standard 3.9.1(4.1/2)                                      19-05-10  AI12-0191-1/09
+!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
@@ -80,6 +80,35 @@
   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 
@@ -89,30 +118,50 @@
    performed on the part(s) of {the nominal type of the object that 
    have }type T;
 
-Modify 7.3.2(15/5):
+Replace 7.3.2(15/5) with: [most recent version for AI12-0075-1]
 
-   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
-   part of {the nominal type of the object that has } 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 only for parts of
-     the nominal type of the object, as opposed for all parts of the object
-     (whether part of the nominal type or not),
-     are motivated by a desire to avoid overhead associated with the
-     possibility that there *might* exist an extension of the tagged type
-     in question that has a part of type T.
+   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,
@@ -145,6 +194,22 @@
 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;
@@ -187,6 +252,7 @@
 
 end Derived;
 
+
 !corrigendum 3.3(23/3)
 
 @drepl
@@ -234,6 +300,54 @@
 (respectively, subcomponents) of the nominal type of @i<X>.
 
 
+!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<expression> or @fa<aggregate> of the 
+@fa<expression_function_declaration>, shall not be statically deeper
+than that of the master that elaborated the @fa<expression_function_declaration>.
+@dinss
+Aspect Static shall be specified to have the value True only if the
+associated @fa<expression_function_declaration>:
+@xbullet<is not a completion;>
+@xbullet<has an @fa<expression> that is a potentially static expression;>
+@xbullet<contains no calls to itself;>
+@xbullet<each parameter (if any) is of mode @b<in> and is of a static subtype;>
+@xbullet<has a result subtype that is a static subtype;>
+@xbullet<has no applicable precondition or postcondition expression; and>
+@xbullet<for result type @i<R>, if the function is a boundary entity for type 
+@i<R> (see 7.3.2), no type invariant applies to type @i<R>; if @i<R> has a 
+component type @i<C>, a similar rule applies to @i<C>.>
+
+
+!corrigendum 7.3.2(8/3)
+
+@drepl
+If the Type_Invariant'Class aspect is specified for a tagged type @i<T>,
+then the invariant expression applies to all descendants of @i<T>.
+@dby
+If the Type_Invariant'Class aspect is specified for a tagged type @i<T>,
+then a @i<corresponding expression> also applies to each nonabstract
+descendant @i<T1> of @i<T> (including @i<T> itself if it is nonabstract).
+
+For a nonabstract type @i<T>, a callable entity is said to be a @i<boundary entity>
+for @i<T> if it is declared within the immediate scope of @i<T> (or by an
+instance of a generic unit, and the generic is declared within the immediate
+scope of type @i<T>), or is the Read or Input stream-oriented attribute of type
+@i<T>, and either:
+
+@xbullet<@i<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 @i<T>; or>
+
+@xbullet<@i<T> is a record extension, and the callable entity is a primitive 
+operation visible outside the immediate scope of type @i<T> or overrides an 
+inherited operation that is visible outside the immediate scope of @i<T>.>
+
 !corrigendum 7.3.2(10.1/4)
 
 @drepl
@@ -257,13 +371,39 @@
 the type @i<T>, the check is performed on the object initialized by the
 stream attribute;>
 @dby
-@xbullet<Upon successful return from a call on any subprogram or entry which is
-type-invariant preserving for @i<T>, an invariant check is
-performed on each part of the nominal type of the object that has type @i<T> 
-which is subject to an invariant check
-for @i<T>. In the case of a call to a protected operation, the check is
+@xbullet<Upon successful return from a call on any callable entity which is
+a boundary entity for @i<T>, an invariant check is performed on each object 
+which is subject to an invariant check for @i<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;>
+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<T>:
+
+@xinbull<a result with a nominal type that has a part of type @i<T>;>
+
+!corrigendum 7.3.2(17/4)
+
+@drepl
+@xinbull<is declared within the immediate scope of type @i<T> (or by an
+instance of a generic unit, and the generic is declared within the
+immediate scope of type @i<T>),>
+@dby
+@xinbull<an @i<out> or @i<in out> parameter whose nominal type 
+has a part of type @i<T>;>
+
+@xinbull<an access-to-object parameter or result whose designated nominal 
+type has a part of type @i<T>; or>
+
+!corrigendum 7.3.2(19/3)
+
+@drepl
+@xinbull<has a result with a part of type @i<T>, or one or more
+parameters with a part of type @i<T>, or an access to variable
+parameter whose designated type has a part of type @i<T>.>
+@dby
+@xinbull<for a procedure or entry, an @b<in> parameterwhose nominal type 
+has a part of type @i<T>.>
 
 
 !corrigendum 13.13.2(9/3)
@@ -1306,5 +1446,105 @@
 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").
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent