!standard 3.2.4(31/5) 19-07-03 AI12-0333-1/04 !standard 4.6(51/4) !standard 6.4.1(14) !class Amendment 19-05-07 !status Amendment 1-2012 19-07-03 !status ARG Approved 10-0-0 19-06-14 !status work item 19-05-07 !status received 19-05-06 !priority Low !difficulty Easy !subject Predicate checks on out parameters !summary Predicate checks are never performed on inbound out parameters. !problem The language rules require that an out parameter of a composite type undergoes a predicate check when passed in. The wording of 6.4.1 triggers predicate checks when passing in an OUT parameter of a composite type by talking about conversions of the objects. According to the current Standard, all conversions cause predicate checks. However, this means that even uninitialized composite objects are checked. This is bizarre. !proposal (See Summary.) !wording Modify 3.2.4(31/5) as follows: [Redundant:On [every] {a} subtype conversion, a check is performed that the operand satisfies the predicates of the target subtype{, unless it is a conversion for an actual parameter of mode out (see 4.6)}. [This includes all parameter passing, except for certain parameters passed by reference, which are covered by the following rule: ]] {In addition, after}[After] normal completion and leaving of a subprogram, for each in out or out parameter that is passed by reference, a check is performed that the value of the parameter satisfies the predicates of the subtype of the actual. For an object created by an object_declaration with no explicit initialization expression, or by an uninitialized allocator, if the types of any parts have specified Default_Value or Default_Component_Value aspects, or any subcomponents have default_expressions, a check is performed that the value of the created object satisfies the predicates of the nominal subtype. AARM Ramification: Most parameter passing is covered by the subtype conversion rule: all inbound *in* and *in out* parameters are converted to the formal subtype, and the copy-back for by-copy *out* and *in out* parameters are converted to the actual subtype. The remaining parameter passing cases are covered by special rules: by-reference *out* and *in out* parameters by the rule given above, and we don't want any predicate checks on inbound *out* parameters, accomplished in part by a special rule in 4.6. Modify 4.6(51/4) as follows: After conversion of the value to the target type, if the target subtype is constrained, a check is performed that the value satisfies this constraint. If the target subtype excludes null, then a check is made that the value is not null. If predicate checks are enabled for the target subtype (see 3.2.4), a check is performed that the value satisfies the predicates of the target subtype{, unless the conversion is: * a view conversion that is an actual parameter of mode out; or * an implicit subtype conversion of an actual parameter of mode out to the nominal subtype of its formal parameter}. AARM Ramification: The reverse conversion applied to by-copy out parameters is /not/ a view conversion and it is to the nominal subtype of the /actual/ parameter, therefore any enabled predicate checks /are/ performed. Modify 6.4.1(14) as follows: For a composite type with discriminants or that has implicit initial values for any subcomponents (see 3.3.1), the behavior is as for an in out parameter passed by copy{, except that no predicate check is performed}. !discussion The original Ada 83 model of out parameters is that they are uninitialized on input. One can see this in the fact that elementary types are never checked for any constraint, exclusion, or predicate. That model didn't quite work for composite types, as bounds and discriminants have to be passed in (and checked). The representation of a parameter can depend on the form of constraint it has (for instance, statically constrained arrays are usually represented differently than unconstrained arrays), so avoiding checks could cause objects with an incompatible representation to be passed. On the other hand, no such issue applies to predicates. As such, it makes the most sense to avoid any checking of predicates for inbound out parameters (of course, the predicates will be checked when the subprogram returns). !corrigendum 3.2.4(31/4) @drepl @xindent or @b parameter that is passed by reference, a check is performed that the value of the parameter satisfies the predicates of the subtype of the actual. For an object created by an @fa with no explicit initialization @fa, or by an uninitialized @fa, if any subcomponents have @fas, a check is performed that the value of the created object satisfies the predicates of the nominal subtype.> @dby @xindent or @b parameter that is passed by reference, a check is performed that the value of the parameter satisfies the predicates of the subtype of the actual. For an object created by an @fa with no explicit initialization @fa, or by an uninitialized @fa, if the types of any parts have specified Default_Value or Default_Component_Value aspects, or any subcomponents have @fas, a check is performed that the value of the created object satisfies the predicates of the nominal subtype.> !corrigendum 4.6(51/4) @drepl After conversion of the value to the target type, if the target subtype is constrained, a check is performed that the value satisfies this constraint. If the target subtype excludes null, then a check is made that the value is not null. If predicate checks are enabled for the target subtype (see 3.2.4), a check is performed that the value satisfies the predicates of the target subtype. @dby After conversion of the value to the target type, if the target subtype is constrained, a check is performed that the value satisfies this constraint. If the target subtype excludes null, then a check is made that the value is not null. If predicate checks are enabled for the target subtype (see 3.2.4), a check is performed that the value satisfies the predicates of the target subtype, unless the conversion is: @xbullet; or> @xbullet to the nominal subtype of its formal parameter.> !corrigendum 6.4.1(14) @drepl @xinbull parameter passed by copy.> @dby @xinbull parameter passed by copy, except that no predicate check is performed.> !ASIS No new ASIS capabilities. !ACATS test An ACATS C-Test is needed to check that predicates are not checked when passing composite out parameters inbound. !appendix From: Tucker Taft Sent: Monday, May 6, 2019 1:21 PM Some folks at AdaCore noticed that the rules for when an OUT parameter undergoes a predicate check (on the way in, that is) are somewhat bizarre. After discussion, we came to the conclusion that the new rules adopted for handling stand-alone objects without an explicit initialization should be used for OUT parameters. That is: declare X : T; begin and procedure Foo (X : out T; ...) should use the same rules for deciding whether a predicate check should occur when X comes into existence. The relevant paragraph is RM 3.2.4(31/5), which currently says: On every subtype conversion, a check is performed that the operand satisfies the predicates of the target subtype.[Redundant:[ This includes all parameter passing, except for certain parameters passed by reference, which are covered by the following rule: ] After normal completion and leaving of a subprogram, for each in out or out parameter that is passed by reference, check is performed that the value of the parameter satisfies the predicates of the subtype of the actual. For an object created by an object_declaration with no explicit initialization expression, or by an uninitialized allocator, if the types of any parts have specified Default_Value or Default_Component_Value aspects, or any subcomponents have default_expressions, a check is performed that the value of the created object satisfies the predicates of the nominal subtype. Here is a possible revision: On every subtype conversion, other than one prior to the call on the actual parameter for an out parameter, a check is performed that the operand satisfies the predicates of the target subtype. In addition, after normal completion and leaving of a subprogram, for each in out or out parameter that is passed by reference, a check is performed that the value of the parameter satisfies the predicates of the subtype of the actual. For an object created by an object_declaration with no explicit initialization expression, an object created by an uninitialized allocator, or a formal out parameter, if the types of any parts have specified Default_Value or Default_Component_Value aspects, or any subcomponents have default_expressions, a check is performed that the value of the object satisfies the predicates of the nominal subtype. **************************************************************** From: Randy Brukardt Sent: Monday, May 6, 2019 1:58 PM ... > should use the same rules for deciding whether a predicate check > should occur when X comes into existence. Makes sense, but since I am against making holes in the predicate rules for anything (including the original rule), I will definitely oppose expanding them. Allowing uninitialized objects to have any sort of constraint is a mistake that Ada 83 made. We're forced to live with that mistake, but we don't need to expand that mistake for things that are new (like predicates). ... > Here is a possible revision: > > On every subtype conversion, other than one prior to the call on the > actual parameter for an out parameter, a check is performed that the > operand satisfies the predicates of the target subtype. In addition, > after normal completion and leaving of a subprogram, for each in out > or out parameter that is passed by reference, a check is performed > that the value of the parameter satisfies the predicates of the > subtype of the actual. For an object created by an object_declaration > with no explicit initialization expression, an object created by an > uninitialized allocator, or a formal out parameter, if the types of > any parts have specified Default_Value or Default_Component_Value > aspects, or any subcomponents have default_expressions, a check is > performed that the value of the object satisfies the predicates of the > nominal subtype. This doesn't work, because the "subtype conversion" sentence is intended to be "redundant". The semantics of subtype conversions are defined in 4.6, and if you leave those unchanged, the rules for out parameters would be unchanged as well (other than that you've now added a second predicate check). At a minimum, you'd have conflicting rules. To make this change (which I'm against making anyway), you would need to rewrite 6.4.1 so that "out" parameters of composite types do not do a subtype conversion, but rather make the needed constraint checks explicitly (arguably, that's a better idea anyway, but it is very complex if accessibility checks get into the mix). Or you would have to completely redo 4.6 to make it conditional on "out" parameters (I think that is a very bad idea). Ergo, making this change will require a massive rewrite of the rules, and since it is a bad idea anyway (see above), I definitely think we should pass. **************************************************************** From: Tucker Taft Sent: Monday, May 6, 2019 2:16 PM > This doesn't work, because the "subtype conversion" sentence is > intended to be "redundant". The semantics of subtype conversions are > defined in 4.6, and if you leave those unchanged, the rules for out > parameters would be unchanged as well (other than that you've now > added a second predicate check). At a minimum, you'd have conflicting rules. Good point. But I don't see this as a very big deal. We already have a special case for OUT parameter in paragraph 56/4: "56/4 Reading the value of the view yields the result of converting the value of the operand object to the target subtype (which might raise Constraint_Error), except if the object is of an elementary access type and the view conversion is passed as an out parameter; in this latter case, the value of the operand object may be isused to initialize the formal parameter without checking against any constraint of the target subtype (as described more precisely in see 6.4.1)." I agree we need to update 4.6, but that seems like very doable. I'll propose the needed update. > To make this change (which I'm against making anyway), you would need > to rewrite 6.4.1 so that "out" parameters of composite types do not do > a subtype conversion, but rather make the needed constraint checks > explicitly (arguably, that's a better idea anyway, but it is very > complex if accessibility checks get into the mix). Or you would have > to completely redo > 4.6 to make it conditional on "out" parameters (I think that is a very > bad idea). > > Ergo, making this change will require a massive rewrite of the rules, > and since it is a bad idea anyway (see above), I definitely think we > should pass. I think I understand your concern, but I believe we want consistency at a minimum. The current rule seems weird and inconsistent. I think we should fix that. **************************************************************** From: Tucker Taft Sent: Monday, May 6, 2019 2:23 PM Randy points out that 4.6 also talks about predicate checks. Neither the words in 4.6 nor the words in 3.2.4 were marked as redundant, so I believe we can decide which one to make official. Elsewhere in 4.6 we "pass the buck" on details of what happens on a view conversion of an OUT parameter. So I would propose we do the same thing here in 4.6 (51/4): After conversion of the value to the target type, if the target subtype is constrained, a check is performed that the value satisfies this constraint. If the target subtype excludes null, then a check is made that the value is not null. If predicate checks are enabled for the target subtype [(see 3.2.4)], a check is performed {(except in certain cases -- see 3.2.4)} that the value satisfies the predicates of the target subtype. **************************************************************** From: Randy Brukardt Sent: Monday, May 6, 2019 2:35 PM > Good point. But I don't see this as a very big deal. We already have > a special case for OUT parameter in paragraph 56/4: > > "56/4 Reading the value of the view yields the result of converting > the value of the operand object to the target subtype (which might > raise Constraint_Error), except if the object is of an elementary > access type and the view conversion is passed as an out parameter; in > this latter case, the value of the operand object may be isused to > initialize the formal parameter without checking against any > constraint of the target subtype (as described more precisely in see > 6.4.1)." You are talking about 4.6(56/4), which confused me for a while. This is not a "special case", it follows directly from the wording in 6.4.1. Indeed, I don't know why it's here, since the wording in 6.4.1 does not include any subtype conversion. Maybe it's worrying about *explicit* type conversions of out parameters, but IMHO that's also a bug (probably a necessary compatibility hack). > I agree we need to update 4.6, but that seems like very doable. I'll > propose the needed update. OK. And then I'll vote against it. :-) **************************************************************** From: Tucker Taft Sent: Monday, May 6, 2019 3:00 PM >> I agree we need to update 4.6, but that seems like very doable. I'll >> propose the needed update. > > OK. And then I'll vote against it. :-) Yes, I understand your concern. But I believe this improves consistency. Note also that this issue came from SPARK folks, who actually use these predicates on a regular basis. **************************************************************** From: Randy Brukardt Sent: Monday, May 6, 2019 3:54 PM ... > Note also that this issue came from SPARK folks, who actually use > these predicates on a regular basis. Understood. But we have to be really careful to not let the SPARK tail wag the dog. The needs of SPARK (100% static checking for an Ada subset) are often very different than for Ada (the full language, dynamic checks are possible and sometimes preferable). For instance, "contract cases" makes sense for SPARK because of the static completeness requirements vis-a-vis the precondition, but changing that to a dynamic requirement (or none at all) for full Ada is downright harmful. Similarly, static ownership checking is necessary for SPARK, but the requirements of full Ada make a fully static model inappropriate (one cannot use such a model to implement containers or many other ADTs). In both of these cases, the requirements for SPARK and for (full) Ada are almost disjoint; attempting to share the same feature for both leads to lousy results. Our job is to do what's right for Ada; we probably ought to do that without causing unnecessary pain for SPARK, but that is a secondary concern at best. **************************************************************** From: Tucker Taft Sent: Monday, May 6, 2019 4:49 PM > ... >> Note also that this issue came from SPARK folks, who actually use >> these predicates on a regular basis. > > Understood. But we have to be really careful to not let the SPARK tail > wag the dog. The needs of SPARK (100% static checking for an Ada > subset) are often very different than for Ada (the full language, > dynamic checks are possible and sometimes preferable). But this is not that case. SPARK also cares about dynamic checks, as they are important when proof is not doable, and to make sure that on a boundary between proved code and tested code, that all of the assumptions made by the proved code are properly checked by the tested code. > ... > Similarly, static ownership checking is necessary for SPARK, but the > requirements of full Ada make a fully static model inappropriate (one > cannot use such a model to implement containers or many other ADTs). Well I beg to differ somewhat, as I believe various versions of AI12-0240 do provide static checking in almost all cases. > In both of > these cases, the requirements for SPARK and for (full) Ada are almost > disjoint; attempting to share the same feature for both leads to lousy > results. I think you are overstating this. SPARK folks care a lot about the fact that there are well-defined dynamic semantics in the absence of proof. > Our job is to do what's right for Ada; we probably ought to do that > without causing unnecessary pain for SPARK, but that is a secondary concern at > best. I would agree with the first part, but I believe we should learn from SPARK folks because they are wait out ahead in terms of using contracts, including dynamic aspects thereof. **************************************************************** From: Yannick Moy Sent: Tuesday, May 7, 2019 3:33 AM >>Note also that this issue came from SPARK folks, who actually >>use these predicates on a regular basis. > >Understood. But we have to be really careful to not let the SPARK tail wag >the dog. The needs of SPARK (100% static checking for an Ada subset) are >often very different than for Ada (the full language, dynamic checks are >possible and sometimes preferable). This does not apply here. We can support any choice here in SPARK (meaning in the proof tool). It just seems bad semantics to impose a predicate check on a value that is possibly not initialized. Both for dynamic checks and static checks. That will lead to unprovable checks in SPARK and failing runtime checks in plain Ada. **************************************************************** From: Randy Brukardt Sent: Tuesday, May 7, 2019 2:30 PM It's bad practice to put any sort of constraint (which includes predicates) on an uninitialized object. There is a significant mistake in Ada that it is even allowed (of course, we can't fix that mistake as doing so would be too incompatible). Ergo, I don't much care what happens with such things, and would like to discourage their use as much as possible. The proposed rule (and the rule on which it is based, one that I have always disagreed with) is a significant maintenance hazard, as a change to some library out of the control of the author can change whether or not predicate checks are applied. The only way to avoid that hazard is to either avoid the using predicates on a type with uninitialized components, or to initialize everything that the predicate depends upon. But of course that makes the rule itself unnecessary. (One could also avoid the hazard by avoiding any abstractions in the data type, but I hope we're still encouraging code reuse and abstraction.) I would be OK with suppressing predicates on ALL out parameters, as the only reason to make checks on inbound out parameters is to ensure that bounds/discriminants are compatible with the subtype. Those can affect the generated code, while a predicate is just an assertion. The wording is easiest if one makes all of the checks in that case, but that seems like a lousy reason to design a language. Note that this would be consistent with the handling of elementary types, which check no sorts of constraints inbound. **************************************************************** From: Tucker Taft Sent: Tuesday, May 7, 2019 3:02 PM At this point I propose we agree to disagree. I don't see either of us convincing the other. You apparently dislike the basic idea of any sort of constraint or predicate being allowed on a subtype that has uninitialized fields. We prefer consistency between the rule we recently agreed on for default-initialized objects, and for checks applying to OUT parameters. Let's leave it at that until we have the ARG meeting. **************************************************************** From: Tucker Taft Sent: Thursday, May 30, 2019 3:12 PM Here is the updated AI12-0333-1, where we decided to eliminate all predicate checks on OUT parameters. [This is version /02 of the AI - Editor.] **************************************************************** From: Tucker Taft Sent: Friday, May 31, 2019 4:07 PM Randy and Steve had some comments on the wording. Here is another version. [This is version /03 of the AI - Editor.] This one simplifies the wording where it is redundant, in 3.2.4, and adds more detail where the normative wording appears, in 4.6. **************************************************************** From: Randy Brukardt Sent: Monday, June 3, 2019 7:08 PM A few editorial-ish fixes to this: >!summary > > Predicate checks are never performed on out parameters. Umm, no, predicate checks are never performed on *inbound* out parameters, they're still performed on return. ... > conversions of the objects. According to the current RM, all We say "Standard", not RM, in AIs. ... > That model didn't quite work for composite types, as bounds > and discrimiants have to be passed in (and checked). The "discriminants". (Thanks to Steve for pointing this out privately; the error was in my original version of this AI, so I can't even blame Tucker for the error.) ... > An ACATS C-Test is needed to check that predicates are not > checked when passing composite out parameters. We need "inbound" here, too. All of these are fixed in the posted version. **************************************************************** From: Tucker Taft Sent: Monday, June 3, 2019 7:27 PM Thanks! ****************************************************************