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

Differences between 1.3 and version 1.4
Log of other versions for file ai12s/ai12-0210-1.txt

--- ai12s/ai12-0210-1.txt	2017/11/17 20:14:20	1.3
+++ ai12s/ai12-0210-1.txt	2018/10/17 01:36:39	1.4
@@ -1,4 +1,6 @@
-!standard 7.3.2(17/4)                                 16-12-19  AI12-0210-1/00
+!standard 7.3.2(8.3/5)                                 18-10-16  AI12-0210-1/01
+!standard 7.3.2(8.4/5)
+!standard 7.3.2(12/3)
 !standard 7.3.2(20.1/4)
 !class binding interpretation 16-12-19
 !status work item 16-12-19
@@ -19,7 +21,7 @@
     (including T itself), a check is performed on the part of the object
     that is of type T.
 
-What does "occurring within the immediate scope" mean in the case where the 
+What does "occurring within the immediate scope" mean in the case where the
 view conversion occurs in an instance of a generic unit? (Who knows?)
 
 One can also have the opposite situation where it is the generic unit body
@@ -96,12 +98,66 @@
 
 !wording
 
-** TBD **
+Insert ahead of 7.3.2(8.3/5) (i.e., immediately before the definition of
+"type-invariant preserving"):
 
-!discussion
+  Given a declaration D, the "extended immediate scope"
+  of the declaration is defined to be
+    - the immediate scope of D; and
+    - for any generic unit G declared within the extended immediate
+      scope of D, the extended immediate scope of any instance of G
+      [Redundant: , other than a formal package].
+
+In 7.3.2(8.4/5), add the word "extended":
+   (or by an instance of a generic unit, and the generic is declared within
+   the {extended} immediate scope of type T)
+
+In 7.3.2(12/3), add the word "extended":
+   For a view conversion, outside the {extended} immediate scope of T, ...
+
+In 7.3.2(20.1/4), add the word "extended":
+   For a view conversion to a class-wide type occurring within the {extended}
+   immediate scope of T, ...
+
+Add after 7.3.2(24.a/3) (i.e., as another note at the end of the
+Dynamic Semantics section).
+
+AARM note:
+   In the following example
+
+       package Pkg is
+         type T is private with Type_Invariant => Is_Ok (T);
+	 function Is_Ok (Arg : T) return Boolean;
+         generic
+         package G1 is
+            generic
+            package G2 is
+               generic
+               package G3 is
+                  procedure Foo (X : in out T);
+               end G3;
+            end G2;
+         end G1;
+       private
+          ...
+       end Pkg;
+
+       with Pkg;
+       pragma Elaborate (Pkg);
+       package Pkg_Client is
+          package I1 is new Pkg.G1;
+          package I2 is new I1.G2;
+          package I3 is new I2.G3;
+       end;
 
-Does anyone care? Pick something. :-)
+    the body of the procedure G1.G2.G3.Foo sees the full view of the type T,
+    so we want I3.Foo to be type-invariant preserving for T. That illustrates
+    the motivation for defining the term "extended immediate scope" and then
+    using that term instead of "immediate scope" in some of the rules in
+    this section.
 
+!discussion
+
 [Editor's musings:
 
 For the third issue, one needs to be careful with the wording lest a type
@@ -133,7 +189,7 @@
      package body Pkg2 is
         package body G1 is
            package body G2 is
-              procedure Proc2 (X : in out Der) is	
+              procedure Proc2 (X : in out Der) is
               begin
                  X.Yy := Integer'First; -- This can see the components of T.
               end Proc2;
@@ -156,6 +212,56 @@
 
 End Editor's musings.]
 
+---
+
+It seems ok, but worth noting, that we can have a generic whose body
+can see the full view of some private type but which is not in immediate
+scope of the private type (because the declaration of the generic package
+spec precedes that of the partial view of the private type).
+
+   package Pkg is
+      generic
+      package G1 is
+         procedure Foo;
+      end G1;
+
+      type T is private with Type_Invariant => ...;
+   private
+      ...
+   end Pkg;
+
+An instance of such a generic will not be in the "extended immediate scope"
+of the private type and so any visible subprograms that the instance might
+declare will not be "type-invariant preserving" for the private type.
+But the private type can't be mentioned in the profile of such a subprogram
+unless incomplete types and access types are involved somehow. We are not
+trying to plug all such holes (for example, we also don't worry about
+the access-to-access-to-private case).
+
+---
+
+This change does not address the issue Randy raised in the AI having to do
+with generic formal derived types. One alternative is to ignore this problem
+- we've already acknowledged that type invariants are not bulletproof
+(which means that the SPARK folks are going to have to add additional
+verification conditions not corresponding to Ada-defined runtime checks
+in order to make them bulletproof, but that's ok).
+
+Another alternative would be to take the RM text
+
+   and at least one of the following applies to the callable entity:
+      has a result with a part of type T;
+      has one or more out or in out parameters with a part of type T;
+      has an access-to-object parameter or result whose designated type
+      has a part of type T; or
+      is a procedure or entry that has an in parameter with a part of type T.
+   Each such part of type T is said to be subject to an invariant check for T.
+
+and replace each occurrence of "of type T" with
+"of type T or a descendant thereof" or something equivalent.
+
+Do we want to do that?
+
 !ASIS
 
 No ASIS effect.
@@ -174,7 +280,7 @@
     (including T itself), a check is performed on the part of the object
     that is of type T.
 
-What does "occurring within the immediate scope" mean in the case where the 
+What does "occurring within the immediate scope" mean in the case where the
 view conversion occurs in an instance of a generic unit?
 
 Consider the following example:
@@ -222,12 +328,12 @@
 Does the call to Nested.Swap_T2 fail an invariant check?
 
 Tuck said (in private communication):
-> Should an external generic, instantiated locally, be able to do 
-> something that a normal external package could *not* do. I believe the 
-> answer is yes, presuming the type with the invariant is only visible 
-> to the generic as a formal type, as opposed to being named directly. 
-> When you instantiate a generic with an actual type that has an 
-> invariant, and you do it within the full view of the type, then the 
+> Should an external generic, instantiated locally, be able to do
+> something that a normal external package could *not* do. I believe the
+> answer is yes, presuming the type with the invariant is only visible
+> to the generic as a formal type, as opposed to being named directly.
+> When you instantiate a generic with an actual type that has an
+> invariant, and you do it within the full view of the type, then the
 > generic should not be affected by the invariant.
 
 A general design principle is that invariants don't come into play very much
@@ -271,7 +377,7 @@
 Sent: Thursday, September 29, 2016  6:41 PM
 
 ...
-> As usual, we should decide first what behavior we want before worrying 
+> As usual, we should decide first what behavior we want before worrying
 > about interpreting the current wording.
 
 When it comes to type invariants, pretty much the only thing we care about is
@@ -284,5 +390,111 @@
 I suspect that these checks in instances will be hell on generic code sharing,
 but I have a hard time caring because I doubt that I'll ever have a customer
 who cares. (Ergo, probably these will never be implemented in Janus/Ada.)
+
+****************************************************************
+
+From: Steve Baird
+Sent: Tuesday, October 16, 2016  2:38 PM
+
+Attached is some proposed wording for AI12-0210. [This is version /01 of the
+AI - Editor.]
+
+As usual, thanks to Randy for preliminary review but don't blame him if you
+think it stinks.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, October 16, 2016  3:16 PM
+
+You had a question at the end, but you didn't express your own opinion.  Do you
+recommend we make the generalization to "T or a descendant thereof" (note that
+saying "a descendant of T" includes T itself, so this could be simplified).  If
+not, why not?
+
+****************************************************************
+
+From: Steve Baird
+Sent: Tuesday, October 16, 2016  5:28 PM
+
+First, a minor point - I considered the phrasing you mentioned but it seemed
+awkward. Consider, for example, replacing
+    has a result with a part of type T;
+with
+    has a result with a part of a descendant of T;
+
+It sounds (at least to me) like we are talking about a "part of a descendant"
+(as opposed to the entire descendant). That's why I suggested "T or a descendant
+thereof". But I agree that phrasing is redundant and I'd be very open to any
+suggestions about improving it.
+
+On to the main question.
+
+I think the arguments about this possible change come down to cost/benefit
+analysis. What is the benefit associated with plugging this particular hole in
+type invariant enforcement (while leaving other holes unplugged) and what is the
+cost associated with the fix?
+
+At first I thought this was simply a problem with derived types, orthogonal to
+any problems involving generics. IMO, that would raise the priority of plugging
+this hole.
+
+Suppose we have a type-invariant-bearing type T1 and another type T2 derived
+from it. T2 has operations whose bodies can see the implementation of T1 and
+thereby create invariant-violating values of type T2 that can leak out of the
+immediate scope of T1.
+
+It's analogous to the case where T2 is a one-field record type with a component
+of type T1, except that invariant checking for that case is already handled
+correctly in the RM.
+
+But we've got the rule that the parent type of a derived type must be completely
+defined (unlike the case of a component type), so I think that means that in
+order to run into this problem we have to use either
+    a) a formal derived type, as in Randy's example or
+    b) A child unit, as in
+
+          package Pkg is
+             type T is private with Type_Invariant => ...;
+          private
+             ...;
+          end;
+
+          package Pkg.Child is
+             type D is new T;
+             procedure Op (X : in out D);
+          end;
+
+       RM 7.3(7.a) says:
+       Note that deriving from a partial view within its immediate scope
+       can only occur in a package that is a child of the one where the
+       partial view is declared.
+
+These are less common constructs, so the benefit of plugging these holes is
+smaller than I thought initially.
+
+But still, a hole is a hole; why wouldn't be want to plug it?
+
+The costs in run-time overhead, compile-time overhead, and compiler
+implementation effort do not seem to be large.
+
+I mainly held off on including this change in the proposed wording because of
+FUD and, specifically, the fear of unintended consequences. In looking at this
+AI, I focused on the original problem with generics that spawned the AI. I
+haven't looked as closely at this "descendants" problem and the possible
+consequences of the change I outlined. That's the main reason that I didn't
+include this change in the proposal - I think it is probably the right way to
+go, but I am less sure about this than about the rest of the AI (i.e., the
+"extended immediate scope" stuff).
+
+The other reason (which I forgot to mention earlier) is that another approach
+occurred to me, but that approach is even less well thought out in my mind.
+Perhaps we can say that if a type invariant applies to a type T1 and if a type
+T2 is derived from T1, then the type invariant also applies to T2. With that
+approach, we might be able to get the desired effect without having to talk
+about descendants in so many places. Or maybe not - perhaps this is a
+fundamentally flawed idea. But it seems like it would be worth considering it
+before committing ourselves to another approach. OTOH, I understand that we
+don't have much time left for this revision.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent