!standard 7.3.2(23/3) 19-06-03 AI12-0210-1/04 !class ramification 16-12-19 !status work item 16-12-19 !status received 16-09-29 !priority Very_Low !difficulty Medium !qualifier Omission !subject Type Invariants and Generics !summary 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 7.3.2(20.1/4) says For a view conversion to a class-wide type occurring within the immediate scope of T, from a specific type that is a descendant of T (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 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 (or private part, in the case of a generic child unit) which can see the completion of the invariant-bearing type and the instance which occurs outside of that scope. 7.3.2(17/4) is about that case, but that rule doesn't address the other cases in which invariant checking rules depend on being or not being "in the immediate scope": view conversions (including conversion to classwide) and deferred constants. Should it? (Yes.) 7.3.2(17/4) also seems unclear in the case of a nested generic unit. Consider: procedure Invtest is package Pkg is type T is private; generic package G1 is generic package G2 is procedure Proc (X : in out T); end G2; end G1; private type T is record Xx, Yy : Integer := 0; end record with Type_Invariant => (T.Xx <= T.Yy); end Pkg; package body Pkg is package body G1 is package body G2 is procedure Proc (X : in out T) is begin X.Yy := Integer'First; end Proc; end G2; end G1; end Pkg; package I1 is new Pkg.G1; package I2 is new I1.G2; Var : Pkg.T; begin I2.Proc (Var); -- If we reach this point without raising an exception, then -- Var has an invariant-violating value. end Invtest; The relevant wording of 7.3.2(17/4) is ... is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is declared within the immediate scope of type T), ... I2.Proc is not declared within the immediate scope of type Pkg.T (G1.G2.Proc is, but that's irrelevant). So we need to look at the wording in parentheses. Is I2.Proc declared by an instance of a generic unit? Yes it is. So far so good. Is that generic declared within the immediate scope of T? No it isn't! G1.G2 is declared within the immediate scope of T, but that's irrelevant. The generic unit we are interested in is I1.G2, which is not declared within the immediate scope of T. Should there be some wording adjustment to fix this? (Yes.) !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. !wording Replace AARM 7.3.2(23.a/5) with: 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 boundary 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. 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 boundary subprogram. For a type T that has a type invariant, avoiding the declaration of types with access-valued components designating objects with parts 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 a boundary subprogram. 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. - Invariant checks are only performed for parts of the nominal type for tagged parameters and function results. For this leak to occur for a type T that has a type invariant, the body of a boundary 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 boundary subprograms (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 require cooperation of some form (as detailed above) from within the immediate scope of the invariant-bearing type. !discussion [Editor's musings: For the third issue, one needs to be careful with the wording lest a type declared within the outer generic get swept up in the special case (such a type should always be checked in this case). There is also an issue with derived generic formal types. procedure Invtest2 is package Pkg2 is type T is private; generic type Der is new T with private; package G1 is generic package G2 is procedure Proc2 (X : in out Der); end G2; end G1; private type T is record Xx, Yy : Integer := 0; end record with Type_Invariant => (T.Xx <= T.Yy); end Pkg2; package body Pkg2 is package body G1 is package body G2 is procedure Proc2 (X : in out Der) is begin X.Yy := Integer'First; -- This can see the components of T. end Proc2; end G2; end G1; end Pkg2; package I1 is new Pkg.G1(Pkg.T); package I2 is new I1.G2; Var : Pkg.T; begin I2.Proc (Var); -- If we reach this point without raising an exception, then -- Var has an invariant-violating value. end Invtest2; I don't see how the existing rules deal with this, and it's not listed in the case of holes, either. 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 "boundary subprogram" 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). --- 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 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. --- Note that this AI includes a reference to parts of the nominal type, a term which was defined in AI12-0191-1. !ASIS No ASIS effect. !ACATS test !appendix From: Steve Baird Sent: Thursday, September 29, 2016 6:31 PM Ada RM 7.3.2(20.1/4) says For a view conversion to a class-wide type occurring within the immediate scope of T, from a specific type that is a descendant of T (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 view conversion occurs in an instance of a generic unit? Consider the following example: procedure Invariant_Test is pragma Assertion_Policy (Check); type T1 is tagged record Aaa : Natural := 0; Bbb : Natural := 100; end record; procedure Swap_T1 (X1 : in out T1) is begin X1 := (Aaa => X1.Bbb, Bbb => X1. Aaa); end; generic type D is new T1 with private; procedure Swap_View_Conversion (X : in out D); procedure Swap_View_Conversion (X : in out D) is begin Swap_T1 (T1 (X)); -- a view conversion end; package Pkg is type T2 is private; private type T2 is new T1 with null record with Type_Invariant => T2.Aaa < T2.Bbb; package Nested is procedure Swap_T2 is new Swap_View_Conversion (T2); end; end; package body Pkg is Y : T2; begin Nested.Swap_T2 (Y); pragma Assert (Y.Aaa = 100); end; begin null; end; 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 > generic should not be affected by the invariant. A general design principle is that invariants don't come into play very much as long as you stay inside the body of the package that implements the private type and don't call subprograms which are callable (directly or via overriding) from outside of that package. There are exceptions to that (e.g., default initialization of an object declared in the package body), but that's the general idea. Tuck's suggestion that no exception should be raised in this case is consistent with that principle. Note that 7.3.2(20.1/4) is somewhat unusual in talking about being "within" some scope in the context of a dynamic semantics rule. Any time the RM does this, there are going to be questions about generics vs. instances. One can also have the opposite situation where it is the generic unit body (or private part, in the case of a generic child unit) which can see the completion of the invariant-bearing type and the instance which occurs outside of that scope. 7.3.2(17/4) is about that case, but that rule doesn't address the other cases in which invariant checking rules depend on being or not being "in the immediate scope": view conversions (including conversion to classwide) and deferred constants. These cases just need to be well-defined; all that is needed is a clarification one way or the other. The fact that 7.3.2(17/4) is a rule and not a ramification *suggests* that no checks should be performed in these cases, but that seems far from conclusive. As usual, we should decide first what behavior we want before worrying about interpreting the current wording. 7.3.2(17/4) also doesn't really deal well with a case like package I1 is new G1; package I2 is new I1.G2; When it says "and the generic is declared within the immediate scope of type T", in what scope is the generic I1.G2 declared? Inside (the expansion of) I1 or inside G1? The point of this rule is to deal with generic bodies that can see the completion of the private type; this suggests that we want to think of I1.G2 as being declared inside of G1, as opposed to inside I1, but the current wording seems unclear. **************************************************************** From: Randy Brukardt Sent: Thursday, September 29, 2016 6:41 PM ... > 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 that the rule is well-defined and doesn't cause horrible implementation problems. These are a distant fourth out of the four kinds of contracts; the fact that GNAT had completely implemented them wrong until Jeff wrote some ACATS tests tells me that no real users really care about the details of this feature. 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. **************************************************************** From: Tucker Taft Sent: Tuesday, October 16, 2016 9:31 PM Thanks for the explanation. It seems like we might be losing the distinction between Type_Invariant and Type_Invariant'Class when we start saying that a type invariant applies to descendants. Also, Type_Invariant (unlike 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, 2019 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, 2019 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. **************************************************************** From: Tullio Vardanega Sent: Thursday, February 7, 2019 2:06 AM I find the "avoidance advice" text that Randy proposed adding very useful indeed. ****************************************************************