Version 1.3 of ai12s/ai12-0333-1.txt

Unformatted version of ai12s/ai12-0333-1.txt version 1.3
Other versions for file ai12s/ai12-0333-1.txt

!standard 3.2.4(31/5)          19-05-31 AI12-0333-1/03
!class Amendment 19-05-07
!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.
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}.
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).
!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.

****************************************************************


Questions? Ask the ACAA Technical Agent