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

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

--- ai12s/ai12-0210-1.txt	2018/10/19 05:59:55	1.5
+++ ai12s/ai12-0210-1.txt	2019/02/07 03:46:07	1.6
@@ -1,8 +1,5 @@
-!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
+!standard 7.3.2(23/3)                                 19-02-06  AI12-0210-1/02
+!class ramification 16-12-19
 !status work item 16-12-19
 !status received 16-09-29
 !priority Very_Low
@@ -11,7 +8,8 @@
 !subject Type Invariants and Generics
 !summary
 
-** TBD **
+A nested/child generic of a generic can cause a hole in type invariant 
+protection; it is added to the list of possible leaks.
 
 !question
 
@@ -92,69 +90,64 @@
 
 Should there be some wording adjustment to fix this? (Yes.)
 
-!recommendation
+!response
 
-(See Summary.)
+It is well known (see AARM 7.3.2(23.a/5)) that there are "holes" in the 
+protection provided by type invariants. Our rule of thumb for "holes" is that
+any hole which can be created solely by the action of a client needs to be 
+plugged, but holes that cannot occur unless the designer of the package does
+something to allow the hole do not need to be plugged.
+
+Since the holes identified by this AI are in the second category (if there
+are no nested/child generics declared, this hole cannot happen), and there
+is potentially a significant implementation cost (especially in the case of
+shared generic bodies), we choose to not fix it.
 
 !wording
 
-Insert ahead of 7.3.2(8.3/5) (i.e., immediately before the definition of
-"type-invariant preserving"):
+Replace AARM 7.3.2(23.a/5) with:
 
-  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;
+  Type invariants are intended to prevent invariant-violating
+  values from inadvertently "leaking out"; that is, code which
+  cannot see the completion of the private type should not be
+  able to reference invariant-violating values of the type
+  (assuming the type invariant condition itself is well behaved -
+  for example, no uses of global variables during evaluation of the
+  invariant expression). This goal is not completely acheieved;
+  such leaking is possible but, importantly, it requires
+  assistance (deliberate or not) of some form from the package that
+  declares the invariant-bearing private type (or a child unit thereof);
+  a client of a well-crafted package cannot use these holes to obtain an
+  invariant-violating value without help.
+
+  The list of known techniques for achieving this kind of leak
+  (ignoring things like erroneous execution and the various
+  forms of unchecked type conversion) consists of:
+    - A type-invariant preserving subprogram might assign
+     an invariant-violating value to a global variable that is
+     visible to client code.
+   - Invariant checks on subprogram return are not performed on objects
+     that are accessible only through access-valued components of other
+     objects.
+   - A client could call through an access-to-subprogram value and reach a
+     subprogram body that has visibility on the full declaration of a type;
+     no invariant checks will be performed if the designated subprogram is
+     not itself type-invariant preserving.
+   - No invariant checks are performed for screened (see AI-191) parts of
+     tagged parameters and function results.
+   - Consider a package P which declares an invariant-bearing private type T
+     and a generic package P.G1, which in turn declares another generic package
+     P.G1.G2. Outside of package P, there are declarations of an
+     instantiation I1 of P.G1 and an instantiation I2 of I1.G2. I2
+     can declare visible subprograms whose bodies see the full
+     view of T and yet these subprograms are not type-invariant
+     preserving (because the generic I1.G2 is not declared within the
+     immediate scope of T - G1.G2 is, but that's irrelevant). So a call to
+     one of these subprograms from outside of P could yield an
+     invariant-violating value.
 
-    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.
+  All of these holes require cooperation of some form from
+  within the immediate scope of the invariant-bearing type. 
 
 !discussion
 
@@ -240,7 +233,7 @@
 
 ---
 
-This change does not address the issue Randy raised in the AI having to do
+We also do 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
@@ -259,8 +252,11 @@
 
 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?
+Note that this AI includes a reference to screened components, which are
+defined in AI12-0191-1.
 
 !ASIS
 
@@ -508,5 +504,143 @@
 Type_Invariant'Class) can be specified in the private part on the full type 
 declaration for a private type.  So my instinct is not to try to fix this 
 problem, or fix it by addressing the formal derived type case directly.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Wednesday, February 6, 2018  7:28 PM
+
+Attached is another attempt at wording for AI12-0210, reflecting the group's 
+decision to take no action other than to add an explanatory AARM note.
+
+As before, thanks to Randy for preliminary review but don't blame him if you 
+think it still stinks.
+
+[This is version /02 of the AI - Editor.]
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, February 6, 2018  9:43 PM
+
+...
+> As before, thanks to Randy for preliminary review but don't blame him 
+> if you think it still stinks.
+
+Well, I was the one that reviewed it, but I am thinking differently today. :-)
+
+First, a couple "for the record" thoughts:
+
+(1) We decided to reformat this into a Ramification. This requires a !response 
+section. I took your proposed !discussion and used it to create that 
+!response:
+
+  It is well known (see AARM 7.3.2(23.a/5)) that there are "holes" in the
+  protection provided by type invariants. Our rule of thumb for "holes" is that
+  any hole which can be created solely by the action of a client needs to be
+  plugged, but holes that cannot occur unless the designer of the package does
+  something to allow the hole do not need to be plugged.
+
+  Since the holes identified by this AI are in the second category (if there
+  are no nested/child generics declared, this hole cannot happen), and there
+  is potentially a significant implementation cost (especially in the case of
+  shared generic bodies), we choose to not fix it.
+
+(2) We clearly need a new summary, too:
+
+  A nested/child generic of a generic can cause a hole in type invariant
+  protection; it is added to the list of possible leaks.
+
+(3) AARM section references are always supposed to include "AARM" before 
+    the paragraph number.
+
+---
+
+Now the technical issue:
+
+You have proposed:
+
+ The list of known techniques for achieving this kind of leak
+  (ignoring things like erroneous execution and the various
+  forms of unchecked type conversion) consists of:
+    - A type-invariant preserving subprogram might assign
+     an invariant-violating value to a global variable that is
+     visible to client code.
+   - Invariant checks on subprogram return are not performed on objects
+     that are accessible only through access-valued components of other
+     objects.
+   - A client could call through an access-to-subprogram value and reach a
+     subprogram body that has visibility on the full declaration of a type;
+     no invariant checks will be performed if the designated subprogram is
+     not itself type-invariant preserving.
+   - No invariant checks are performed for screened (see AI-191) parts of
+     tagged parameters and function results.
+   - Consider a package P which declares an invariant-bearing private type T
+     and a generic package P.G1, which in turn declares another generic package
+     P.G1.G2. Outside of package P, there are declarations of an
+     instantiation I1 of P.G1 and an instantiation I2 of I1.G2. I2
+     can declare visible subprograms whose bodies see the full
+     view of T and yet these subprograms are not type-invariant
+     preserving (because the generic I1.G2 is not declared within the
+     immediate scope of T - G1.G2 is, but that's irrelevant). So a call to
+     one of these subprograms from outside of P could yield an
+     invariant-violating value.
+
+  All of these holes require cooperation of some form from
+  within the immediate scope of the invariant-bearing type. 
+
+This last paragraph is definitely true, but it isn't obvious for most of these 
+bullets as to what to avoid. I wonder if we should add a sentence to each of 
+these bullets (other than the first, "don't do that" doesn't seem valuable) to 
+described how it can happen (and thus how to avoid it). Otherwise, authors and 
+the like won't know how to avoid the holes, either.
+
+This was especially true for the access-valued component and screened component 
+issues. It's not immediately obvious that (in the first case) the type has to 
+be declared in the same package as T and (in the second case) the parent type 
+has to be used in an operation of T (thus in P) *and* the extension has to be 
+visible in the body of P. (If it's not visible, one would have use an 
+operation that is checked to put the value into the type.)
+
+So, how about adding something like the following (marked with {} in the 
+below):
+
+   - Invariant checks on subprogram return are not performed on objects
+     that are accessible only through access-valued components of other
+     objects. {This can only cause a leak if there is a type with 
+     access-valued components that is used as a parameter or result type
+     of a type-invariant preserving subprogram. For a type T that has a type
+     invariant, avoiding the declaration of types with 
+     access-valued components of T in the package that contains T is 
+     sufficient to prevent this leak.}
+   - A client could call through an access-to-subprogram value and reach a
+     subprogram body that has visibility on the full declaration of a type;
+     no invariant checks will be performed if the designated subprogram is
+     not itself type-invariant preserving. {This leak can only happen if
+     an access-to-subprogram value of a subprogram that is not visible to
+     clients is passed out to clients.}
+   - No invariant checks are performed for screened (see AI-191) parts of
+     tagged parameters and function results. {For this leak to occur for a
+     type T that has a type invariant, the body of a type-invariant preserving 
+     subprogram of T needs to have visibility on a type extension that has
+     components of T or access-to-T and also has an ancestor type (or class)
+     as a parameter or result of the subprogram.}
+   - Consider a package P which declares an invariant-bearing private type T
+     and a generic package P.G1, which in turn declares another generic package
+     P.G1.G2. Outside of package P, there are declarations of an
+     instantiation I1 of P.G1 and an instantiation I2 of I1.G2. I2
+     can declare visible subprograms whose bodies see the full
+     view of T and yet these subprograms are not type-invariant
+     preserving (because the generic I1.G2 is not declared within the
+     immediate scope of T - G1.G2 is, but that's irrelevant). So a call to
+     one of these subprograms from outside of P could yield an
+     invariant-violating value. {So long as a nested generic of a
+     nested generic unit of P is not declared, no such leaks are possible.}
+
+  All of these {leaks}[holes] require cooperation of some form {(as detailed
+  above)} from within the immediate scope of the invariant-bearing type. 
+
+Since in this wording, you only used "leak" (rather than "hole"), we should 
+use "leak" in this trailing type.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent