!standard 6.5(5.12/5)                                      20-01-15  AI12-0343-1/03
!standard 6.5(8/4)
!standard 6.5(8.1/3)
!standard 6.5(21/3)
!class binding interpretation 19-09-27
!status Amendment 1-2012 20-01-15
!status ARG Approved 13-0-1  20-01-15
!status work item 19-09-27
!status received 19-09-17
!priority Low
!difficulty Easy
!qualifier Clarification
!subject Return Statement Checks
!summary

The check of 6.5(8/4) is made immediately after the return object is
created.

The checks of 6.5(8.1/3) and 6.5(21/3) are made immediately before
an object is returned.

The predicate of the return subtype is checked on the return object
immediately before an object is returned.

!question

Suppose you have something like
 
      return Result : Root'Class := Local_Func do
         if not Ada.Tags.Is_Descendant_At_Same_Level
            (Descendant => Result'Tag,
             Ancestor => Root'Tag) then
             goto Do_Something_Else_Instead;
          end if;
       end return;
 
      <<Do_Something_Else_Instead>>
       ...;

Is the tag accessibility check performed before or after the
execution of the handled sequence of statements of the
extended return statement? 

!recommendation

The check of 6.5(8/4) is made immediately after the return object is
created (that is, immediately after the semantics of 6.5(5.12/5)
for an extended return).

The checks of 6.5(8.1/3) and 6.5(21/3) are made immediately before
an object is returned. If the return statement is prematurely completed
without returning, then these checks are not made. 

For an extended return statement, any predicate that applies to the
return subtype is checked immediately before an object is returned.

!wording

Move 6.5(22/3) and the AARM note 6.5(22.a/3) in front of the existing
6.5(8.1/3) [which will change the number of that paragraph].

Add after the moved AARM note:

   AARM Ramification: The check on the tag of the object occurs when
   the object is created (before any sequence_of_statements); the checks
   which follow occur after the execution of any sequence_of_statements.
   This is implicit in the order of definition of these Dynamic Semantics.

Replace the moved 6.5(22/3) with:

A check is performed that the return value satisfies the predicates of the 
return subtype. If this check fails, the effect is as defined in subclause
3.2.4, "Subtype Predicates".

   AARM Implementation Note: The subtype conversion of the return 
   expression for a simple_return_statement performs this same check. The 
   permissions of 11.4.2 ensure that duplicate evaluation of a predicate at
   a single point is never required, so a single evaluation of the predicate 
   is enough in this case.

!discussion

The issue is that the wording of 6.5(8/4) says "A check is made ..." without
specifying exactly where. The text is between the description of the
Dynamic Semantics of a simple return statement and that of an extended
return statement. One could argue that this order is significant, and thus
the check occurs before the execution of the sequence of statement for an
extended return, but after all of the execution of a normal return.

This interpretation would work fine (and might even be preferable) for the
check mentioned in the question, as once the tag is determined for the return
object it cannot be changed as part of the extended return statement.

However, we have similar wording for the access definition check (6.5(8.1/3)) 
and for the access discriminant checks (6.5(21/3)). These checks are in part
on the value returned, and they can be changed within an extended return.
[That might be hard to see for access discriminants, but since the check is on
any access discriminant in any part of the return object, one could put a
component with an access discriminant in a mutable variant. Yes, that requires
three levels of record types, but it is possible and we need to make sure
nothing bad happens in such cases.]

Moreover, if the 6.5(8.1/3) check is not performed on the actual object value
being returned, the purpose of the check would be lost. This check is 
attempting to preserve the semantics of tag-indeterminate functions, and 
failing to enforce the tag would cause nonsense results for dispatching in 
such cases.

We also have to consider build-in-place issues. For the 6.5(8/4) check, it
is preferable to raise an exception before setting the return object to the
"bad" tag. While there is a slight amount of functionality lost when that
is done (as is illustrated by the !question), it doesn't seem worth the 
complications to implementors to have "bad" tags in objects, however briefly.

For the 6.5(8.1/3) check, the return object is an elementary object and thus
build-in-place is never required; moreover there isn't any implementation
issue with build-in-place if it is used.

For the 6.5(21/3) check, the existing permissions (6.5(24-24.2/4)) cover the
cases of interest.

This analysis suggests that we want different answers for the 6.5(8/4) check
and the 6.5(8.1/3) and 6.5(21/3) checks, or at least a permission to do the
6.5(8/4) check early.

It also has been pointed out that the semantics described in 6.5(5.12/3)
makes it clear that any predicate check occurs at the beginning of an
extended return. This means that the object returned may not meet the
predicate of the return subtype. For instance:

    type Rec is record Count, Max : Natural; end record
       with Dynamic_Predicate => Rec.Count <= Rec.Max;

    function Foo return Rec is
    begin
       return Result : Rec := (Count => 5, Max => 10) do
          Result.Max := 0;
       end return;
    end Foo;

It seems odd that using an extended return statement removes a guarantee about 
the predicate of the return subtype. This sort of dependence on the exact way 
some code is written is uncomfortable. Thus we propose to make a predicate check
immediately before returning from an extended return statement; of course, if 
the compiler can prove that the return object hasn't been modified since the 
initial predicate check, then it can omit it. Note that this is similar to 
the predicate check on out/in out by-reference parameters -- 
there is not a natural predicate check at that location, but it seems nasty to
allow the return of objects that don't meet the indicated predicate.

---

We reorder the wording so that the text about the evaluation of the 
sequence_of_statements comes between the 6.5(8/4) check and the 6.5(8.1/3) 
check. This implicitly gives an order of evaluation of the checks, and we 
specify that explicitly by an AARM note so that no one is confused by our 
subtlety. Explicitly mentioning the order repeatedly would harm readability, 
and we'd probably want to define a term for something like "immediately before 
return" so that we wouldn't need a lengthy description of the exact point of 
the check.

We define the extra predicate check in 6.5 (and thus before the subprogram 
returns) so that a compiler can eliminate a potentially duplicate check (as a 
similar check will be required for the subtype conversion of any return 
expression). The checks mandated in 3.2.4(31/5) are done after return, which 
would make it much harder for the compiler to determine whether a check is a 
duplicate.

!corrigendum 6.5(8.1/3)

@drepl
If the result subtype of the function is defined by an @fa<access_definition>
designating a specific tagged type @i<T>, a check is made that the result value
is null or the tag of the object designated by the result value identifies
@i<T>. Constraint_Error is raised if this check fails.
@dby
For the execution of an @fa<extended_return_statement>, the
@fa<handled_sequence_of_statements> is executed. Within this
@fa<handled_sequence_of_statements>, the execution of a
@fa<simple_return_statement> that applies to the @fa<extended_return_statement>
causes a transfer of control that completes the
@fa<extended_return_statement>. Upon completion of a return statement that
applies to a callable construct by the normal completion
of a @fa<simple_return_statement> or by reaching the @b<end return>
of an @fa<extended_return_statement>, a transfer of control is performed
which completes the execution of the callable construct, and returns
to the caller.

If the result subtype of the function is defined by an @fa<access_definition>
designating a specific tagged type @i<T>, a check is made that the result value
is null or the tag of the object designated by the result value identifies
@i<T>. Constraint_Error is raised if this check fails.

!corrigendum 6.5(22/3)

@drepl
For the execution of an @fa<extended_return_statement>, the
@fa<handled_sequence_of_statements> is executed. Within this
@fa<handled_sequence_of_statements>, the execution of a
@fa<simple_return_statement> that applies to the @fa<extended_return_statement>
causes a transfer of control that completes the
@fa<extended_return_statement>. Upon completion of a return statement that
applies to a callable construct by the normal completion
of a @fa<simple_return_statement> or by reaching the @b<end return>
of an @fa<extended_return_statement>, a transfer of control is performed
which completes the execution of the callable construct, and returns
to the caller.
@dby
A check is performed that the return value satisfies the predicates of the 
return subtype. If this check fails, the effect is as defined in subclause
3.2.4, "Subtype Predicates".

!ASIS

No ASIS effect.

!ACATS test

ACATS tests need to be created and/or modified to ensure that the checks
are done as specified here.

!appendix

From: Steve Baird
Sent: Tuesday, September 17, 2019  6:32 PM

A while back, I was discussing something else with Randy and I
threw in this question:

> Incidentally, suppose you have something like
> 
>       return Result : Root'Class := Local_Func do
>          if not Ada.Tags.Is_Descendant_At_Same_Level
>           (Descendant => Result'Tag,
>            Ancestor => Root'Tag) then
>             goto Do_Something_Else_Instead;
>          end if;
>       end return;
> 
>      <<Do_Something_Else_Instead>>
>       ...;
> 
> Is the tag accessibility check performed before or after the
> execution of the handled sequence of statements of the
> extended return statement? The RM seems unclear. As the above
> example illustrates, it can make a difference. 

Randy pointed out that if there is an issue here (and there might
not be - I'll get to that) then this could also be an issue for some
of the other return-statement-related runtime checks defined in section
6.5.

I'm not talking about the well-defined sequence of actions defined
in 5.12/5 (which includes a check). It seems clear that those all occur
in the specified order and, if there is a statement list, before
executing the statement list.

Aside:
     This interpretation does open the door for returning a
     predicate-violating result by modifying the function result
     after the result subtype check is performed, as in

        type Rec is record Count, Max : Natural; end record
          with Dynamic_Predicate => Rec.Count <= Rec.Max;

        function Foo return Rec is
        begin
            return Result : Rec := (Count => 5, Max => 10) do
               Result.Max := 0;
            end return;
        end Foo;

     but holes in predicate checking associated with component
     assignments are nothing new.

I'm talking about
    - the tag accessibility check in the case of a class-wide result
      type;
    - the tag check in the case where the result type is an anonymous
      access type with a tagged specific designated type;
    - the "dangling discriminant" check.

I think it comes down to the question of whether the order of the
paragraphs in the Dynamic Semantics section of 6.5 is intended to
define the order in which the described actions are performed.

Possible resolutions of this question include
    - do nothing, because the answer is "obvious";
    - add an AARM clarification of some sort;
    - add normative RM text defining the order in which things happen.

The third choice seems like overkill to me, although I mention it as
an option.

Does it seem like some sort of brief AARM clarification is warranted
here or is this a non-issue?

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

From: Edward Fish
Sent: Monday, September 23, 2019  7:13 PM

Couldn't we just treat the Return as an Select [IIRC], denying the 
ability/legality of GOTOing outside it? This seems the most sensible, 
because the Return has already begun, and the programmer's logic should 
have already accounted for the "I don't want to return this" option, right?
Alternatively we could make the GOTO legal, and perhaps include an "ABORT 
RETURN" syntax to back out of the extended return without resorting to a GOTO.

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

From: Randy Brukardt
Sent: Monday, September 23, 2019  8:17 PM

We discussed this when extended return was designed. It *seems* sensible,
but then one remembers that one can always exit a return using an exception
(even in Ada 83!), so we have to account for what happens when that occurs.
We can't prevent the raising of exceptions, of course, from any construct.
Thus we have to deal with the possibility of an incomplete return and deal
with the issues that raises.

For instance, the following is legal (and occurs occasionally) Ada 83 code:

    function Foo ... return Type_Containing_Tasks is
    begin
       begin
           return <Something that can raise an exception>;
       exception
           when others =>
               return <Some default>;
       end;
    end Foo;

Thus just banning Gotos from extended returns [and exits and anything else
that is a completion] doesn't do anything other than make the programmer's
job harder and probably more expensive - we still have to deal with the
possibility of premature exit.

I think we considered not allowing local handling of exceptions raised in
return statements (and banning of gotos etc.), but that would have been
incompatible (and a hidden runtime-only incompatibility at that) since it
would not allow the above pattern, and it would cause a weird wart in both
the implementation of exception handling and in the user model. Ultimately,
the oddities with return objects getting de-initialized seemed less of a
problem (since they only matter with types with active components like
controlled and task components).

In any case, I think it is too late to ban gotos/exit inside of extended
returns, it's been allowed since 2007 and it would break reasonable
patterns. Ergo, it's likely to have occurred in real code.

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

From: Randy Brukardt
Sent: Monday, September 23, 2019  8:23 PM

...
> I think it comes down to the question of whether the order of 
> the paragraphs in the Dynamic Semantics section of 6.5 is 
> intended to define the order in which the described actions 
> are performed.
> 
> Possible resolutions of this question include
>     - do nothing, because the answer is "obvious";

If it is so obvious, what is it? :-) I couldn't figure that out from the
wording, and our private discussion didn't help any.

>     - add an AARM clarification of some sort;

At a minimum. "A check is made" without any indication of when other than
somewhere during evaluation of an extended return isn't sufficient.

>     - add normative RM text defining the order in which things happen.
> 
> The third choice seems like overkill to me, although I 
> mention it as an option.

This would be the best idea, other than that you and I couldn't decide on
when the checks ought to be made. (Which is why calling it "obvious" seems
like nonsense to me.)

> Does it seem like some sort of brief AARM clarification is 
> warranted here or is this a non-issue?

I think an AARM note is the minimum, but we have to decide what the
"obvious" point when these checks are made is. I think the ACATS assumes
that they are made when the object is ultimately returned, but since most
such ACATS tests use simple returns, one can't actually tell that.

I suppose I have to scratch out an AI about this (I was hoping that you
would have decided something, but no luck there).

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

From: Tucker Taft
Sent: Thursday, September 26, 2019  3:52 PM

To me, it is "clear" (;-) from reading the RM that all of the checks occur 
*before* the handled sequence of statements is executed.  Hence, an exception
will be raised before the handled sequence of statements is executed in the 
below case, if the tag's accessibility level is too "deep."  If you really 
want to support this case, it is easy enough to call the function before you 
enter the extended return statement and rename the result, and then do the 
various explicit tests, and only enter the extended return statement if the 
various tests have a satisfactory result.

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

From: Randy Brukardt
Sent: Thursday, September 26, 2019  4:21 PM

Fair enough. But that seems to open a window to return things that don't meet 
the checks (because of changes applied in the handled_sequence_of_statements).
That can't happen for tags because they can't be changed after the fact, but 
is that true of all of the checks in question here? (There are four of them, I
believe). Steve noted that the current definition already makes that true for 
predicates (in the part that is well-defined).

In any case, the AARM (at a minimum) needs to say where these checks occur.
The current wording just says that they occur somewhere during the execution 
of a return statement ("a check is made", without any indication of when), 
which is good enough for simple returns but clearly NOT good enough for 
extended returns where arbitrary other things are going on.

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

From: Tucker Taft
Sent: Thursday, September 26, 2019  4:47 PM

> Fair enough. But that seems to open a window to return things that 
> don't meet the checks (because of changes applied in the 
> handled_sequence_of_statements). That can't happen for tags because 
> they can't be changed after the fact, but is that true of all of the 
> checks in question here? (There are four of them, I believe). Steve 
> noted that the current definition already makes that true for 
> predicates (in the part that is well-defined).

Other than predicates, I don't see any other problems (off the top of my 
head), since the return object's subtype needs to statically match (or nearly 
so) the result subtype.  And for predicates, we will be rechecking at each 
assignment, I would think, since they involve an implicit conversion to the
return object's subtype, but if individual components are updated, a predicate 
violation can as usual go undetected.  At the final return, I see no further 
check, since there is no conversion happening at that point according to 
6.5(22/3), and no special case for function return given in 3.2.4(31/5). 
Of course there might be a conversion happening at the call site, if the 
result of the function is assigned to an object or passed as a parameter, so 
at that point yet another predicate check would occur.  For what it is worth,
SPARK performs predicate checks (from a "proof" point of view) in more places
than the Ada RM requires, including any time a subcomponent is changed.  But 
in Ada, we know that predicates can be violated in many places, and from this
analysis we know that includes upon function return.  We could of course add 
another special case to 3.2.4(31/5) if this gives us heartburn!

> In any case, the AARM (at a minimum) needs to say where these checks occur.
> The current wording just says that they occur somewhere during the 
> execution of a return statement ("a check is made", without any 
> indication of when), which is good enough for simple returns but 
> clearly NOT good enough for extended returns where arbitrary other things 
> are going on.

I agree, that at least an AARM note is required.  But I would say that when 
you specify a bunch of checks, and then say "for the execution of ..." as we
do here, we presume the checks are performed before the rest of the execution
semantics, unless we explicitly say the order is not specified.

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

From: Randy Brukardt
Sent: Thursday, September 26, 2019  6:46 PM

> Other than predicates, I don't see any other problems (off the top of 
> my head), since the return object's subtype needs to statically match 
> (or nearly so) the result subtype.

I didn't remember off the top of my head, either, but reading 6.5 for another 
reason turned up 6.5(8.1/3):

  If the result subtype of the function is defined by an access_definition 
  designating a specific tagged type T, a check is made that the result value 
  is null or the tag of the object designated by the result value identifies 
  T. Constraint_Error is raised if this check fails. 

Here, of course, the return subtype doesn't change, it's the value of the 
object that we're checking. And the body of the extended return can change
that value to anything it likes (including something that fails the check).
Indeed, that might be common in some uses, as the return object could be 
initialized to null and then set to a value in the 
handled_sequence_of_statements.

This particular check exists to make tag-indeterminate functions with access 
results work properly: getting it wrong messes up the entire dispatching model.

I wonder if there is a similar problem with inner access discriminants (which
can be changed by the statements if in a variant or the like - the check is 
6.5(20.1/2)), but don't ask me to provide an example.

Anyway, I don't think this is as simple as you describe. (Steve made the same 
error initially, although he pointed out the predicate issue.)

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

From: Tucker Taft
Sent: Friday, September 27, 2019  9:00 AM

So perhaps this argues for moving any "special" checks to the point of actual 
return.  I think that would require re-ordering the description in 6.5, so the
"for the execution of ..." paragraph precedes or incorporates the special 
checks.  Of course some checks happen automatically as part of a subtype 
conversion (e.g. a predicate check), and we can debate whether we think it is
worth effectively doing yet another conceptual subtype conversion at the point
of return.

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

From: Randy Brukardt
Sent: Friday, September 27, 2019  2:57 PM

Probably we'd also want a permission to make the checks "early" for 
build-in-place. (Or at least verify that the existing such permission works 
for these checks.) Especially for the tagged return object checks, there isn't 
any value to waiting (since the tag can't be changed after declaration) and it 
seems that it could be a painful thing to allow creating the "wrong" tag and 
yet successfully abandon the return before the check.

Anyway, thanks for thinking about this.

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

From: Randy Brukardt
Sent: Friday, September 27, 2019  9:21 PM

Attached find my AI [version /01 of AI12-0343-1] for this issue. I didn't 
propose detailed wording as I think the proposal needs a bit of discussion
before spending time on that. I'm proposing the following:

  The check of 6.5(8/4) is made immediately after the return object is
  created (that is, immediately after the semantics of 6.5(5.12/5)
  for an extended return).
 
  The checks of 6.5(8.1/3) and 6.5(21/3) are made immediately before
  an object is returned. If the return statement is prematurely completed
  without returning, then these checks are not made. 
  
  For an extended return statement, any predicate that applies to the
  return subtype is checked immediately before an object is returned.
  (This check probably should be added to 3.2.4, near the "in out" 
  by-reference check.)

There is a detailed discussion of why I'm making this particular proposal in 
the !discussion of the AI.

The last item might be a bit controversial (in that we know that dynamic 
predicates have holes when individual components are changed). However, we 
went out of our way to mandate a predicate check on return for in-out/out 
by-reference parameters, which otherwise would not naturally have one. The 
only reason for doing that is an assumption that we do not want the 
implementation of the subprogram to "leak" out vis-a-vis component 
modifications. It seems to be exactly the same case for the return object 
-- indeed it seems crazy to worry about ensuring that predicates are met 
for out parameters at the subprogram boundary and yet not enforce them on
the object returned from an extended return statement. One imagines those
two things are different ways of doing the same thing (return a value 
from a subprogram), and they probably ought to have the same requirements 
for predicate checks.

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

From: Randy Brukardt
Sent: Friday, January 24, 2020  10:12 PM

A "for the record" note:

In AI12-0343-1, I added the rule:

  A check is performed that the return value satisfies the predicates of the

  return subtype. 

But *of course* one cannot define a check without specifying the consequence 
of failure. Since that's pretty complex for predicate checks, we want to refer
to 3.2.4. Luckily, we already faced this problem in 4.6 (Type Conversions), so
we can use a version of that wording:

  A check is performed that the return value satisfies the predicates of the
  return subtype. If this check fails, the effect is as defined in subclause
  3.2.4, "Subtype Predicates".

Since "doing the usual thing" for a check we've already agreed to add should 
not be controversial, I'll just treat this as part of my editorial review of 
this AI.

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