Version 1.3 of ai22s/ai22-0013-1.txt

Unformatted version of ai22s/ai22-0013-1.txt version 1.3
Other versions for file ai22s/ai22-0013-1.txt

!standard 5.1(12.1/3)          21-11-12 AI22-0013-1/01
!standard 5.6(1)
!standard 5.6(2)
!standard 5.6(3)
!standard 5.6(4)
!standard 5.6(5)
!standard 5.6(6)
!class binding interpretation 21-11-12
!status work item 21-11-12
!status received 21-06-23
!priority Low
!difficulty Easy
!qualifier Clarification
!subject Pragma after a final label
!summary
A pragma is permitted after a label, even if there are no statements following the label. A goto jumps to a target "label" rather than a target statement.
!question
Is the following legal:
begin if Some_Test then goto label; end if; Do_This; Do_That; <<label>> pragma Assert (X = Y); end;
(Yes.)
!recommendation
A pragma is allowed immediately after a label, even if there are no statements after the label. This is a ramification of 2.8(7.1/3) which says that a pragma is allowed:
* In place of a statement in a sequence_of_statements.
Clearly if the pragma in the example above were replaced with a statement it would be syntactically legal, so that implies the pragma is legal even if there are no statements following it.
However, there is other wording that depends on a statement following a label. In particular, a goto statement jumps to a target statement rather than a target label, and for that reason, the change to allow a label at the end of a sequence of statements introduced the notion of an implicit null statement in 5.1(12.1/3):
If one or more labels end a sequence_of_statements, an implicit null_statement follows the labels before any following constructs.
An alternative approach is to say that a goto statement jumps to a label rather than a statement. This seems more intuitive in any case.
Delete 5.1(12.1/3) [see !recommendation above]
Modify 5.8(1-6) as follows:
[A goto_statement specifies an explicit transfer of control from this statement to a target [statement with a given] label.]
Syntax
goto_statement ::= goto label_name;
Name Resolution Rules
The label_name shall resolve to denote a {target} label[; the statement with that label is the target statement].
Legality Rules
The innermost sequence_of_statements that encloses the target [statement]{label} shall also enclose the goto_statement. Furthermore, if a goto_statement is enclosed by an accept_statement or a body, then the target [statement]{label} shall not be outside this enclosing construct.
Ramification: The goto_statement can be a statement of an inner sequence_.
It follows from the second rule that if the target [statement]{label} is enclosed by such a construct, then the goto_statement cannot be outside.
Dynamic Semantics
The execution of a goto_statement transfers control to the target [statement]{label}, completing the execution of any compound_statement that encloses the goto_statement but does not enclose the target.
NOTES
9 The above rules allow transfer of control to a [statement]{label} of
an enclosing sequence_of_statements but not the reverse. Similarly, they prohibit transfers of control such as between alternatives of a case_statement, if_statement, or select_statement; between exception_handlers; or from an exception_handler of a handled_sequence_of_statements back to its sequence_of_statements.
!discussion
It seems clear that a pragma immediately after a label makes sense, no matter where the label might be. The current wording for placement of pragmas already allows that, so this requires no change.
However, the existing wording for goto statements talks about a target statement, and that becomes more confusing if that target statement is actually a pragma. Hence, we propose to eliminate the notion of a target statement, and instead simply have the goto jump to the target label.
!ACATS test
An ACATS C-Test should try an example similar to that in the !question.
!appendix

From: Tucker Taft
Sent: Wednesday, June 23, 2021  3:51 PM

We recently bumped into a problem where we wanted to write:

 begin
     if Some_Test then
         goto label;
     end if;
     Do_This;
     Do_That;
     <<label>>
     pragma Assert (X = Y);
  end;

and GNAT rejected it.  For Ada 2012 we made a change to allow labels at the 
end of a sequence-of-statements (AI05-179-1) but we didn't revise the
placement rules for pragmas to take advantage of this.  I would suggest we
add to the list defining the places where a pragma is allowed, after
2.8(7.1/3), the following:

   * Immediately after a label.

This will allow a pragma between a label and its associated statement, and 
will also allow it at the very end of a sequence of statements that ends with
one or more labels.

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

From: John Barnes
Sent: Thursday, June 24, 2021  1:28 AM

I approve of that. I have a sneaking approval of labels in some circumstances.

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

From: Steve Baird
Sent: Thursday, June 24, 2021  1:50 PM

>  I would suggest we add to the list defining the places where a pragma is 
>  allowed, after 2.8(7.1/3), the following:
>
>   * Immediately after a label.

Do we also need a corresponding change to the 5.1 rule you mentioned earlier
    If one or more labels end a sequence_of_statements, an implicit 
    null_statement follows the labels before any following constructs.
to say that we also get an implicit null_statement when a label is followed by
a pragma?

We want to be clear that in a case like

    <<L>>
     pragma Assert (Some_Condition);
     X := X + 1;

either the pragma is the target statement (which would be odd)
or the target statement is an implicit null statement that precedes the pragma
(which seems better to me).

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

From: Tucker Taft
Sent: Thursday, June 24, 2021  3:13 PM

I am tempted to change "target statement" to "target label" in 5.8 and 
eliminate the implicit null.  I don't think there would be any confusion.
Transferring control to a label seems just as reasonable as transferring 
control to a statement.

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

From: Steve Baird
Sent: Thursday, June 24, 2021  4:19 PM

> change "target statement" to "target label" in 5.8 

Sounds good to me.

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

From: Jeff Cousins
Sent: Friday, June 25, 2021  7:36 AM

I think so. More intuitive, the Wiki definition of a goto talks of jumping to
a label not a statement.

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

From: Randy Brukardt
Sent: Friday, November 12, 2021  9:34 PM

> I am tempted to change "target statement" to "target label" in 5.8 and 
> eliminate the implicit null.  I don't think there would be any confusion.
> Transferring control to a label seems just as reasonable as 
> transferring control to a statement.

The problem with that is that labels aren't executed (at least in the model
described in 5.1), only statements are. So if you say that execution
"continues at a target label", that isn't tied in any way to the definition
of execution in 5.1. Indeed, there isn't anything about associating a label
with a place in the current text (once you delete all of the references to 
statement being labeled, as in the proposed AI). So once you jump to a label,
you have no idea (formally) where to continue execution.

So you have to introduce that sort of description somewhere (probably in 5.1),
lest we end up with another construct like a parenthesized expression where
there is no actual description but rather "everyone knows what it means".
This seems like it is getting unnecessarily messy.

---

I'd also note that a pragma gets executed because it is "at the place" of a 
statement, so for the purposes of defining execution, it is a statement. So I 
think don't think that there is any language problem at all with the current 
rules. A pragma following a label is indeed the target statement (even if
Steve thinks that is weird - something else would be much weirder, since a
sequence_of_statements only executes statements, at least as far as 5.1 is
concerned). And a pragma following a label at the end of a construct is at the
place of the implicit null statement, so 2.8(7.1/3) (arguably) allows this.

Maybe we should add an AARM note and an ACATS test, but leave the language 
alone. Even if the model of gotos and pragmas is a bit weird, there's no 
requirement to change it.

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

From: Tucker Taft
Sent: Saturday, November 13, 2021  3:53 PM

> So you have to introduce that sort of description somewhere (probably in
> 5.1), lest we end up with another construct like a parenthesized expression
> where there is no actual description but rather "everyone knows what it
> means". This seems like it is getting unnecessarily messy.

I think we could easily adjust 5.1(13) to say:

The execution of a null_statement {or a label} has no effect.

> I'd also note that a pragma gets executed because it is "at the place" of a
> statement, so for the purposes of defining execution, it is a statement. So
> I think don't think that there is any language problem at all with the
> current rules. 

I had come pretty much to the same conclusion, though using the notion of a 
target label actually simplifies the wording a bit.  But if it is an 
unnecessary change, then probably not worth making it.
 
> A pragma following a label is indeed the target statement
> (even if Steve thinks that is weird - something else would be much weirder,
> since a sequence_of_statements only executes statements, at least as far as
> 5.1 is concerned). And a pragma following a label at the end of a construct
> is at the place of the implicit null statement, so 2.8(7.1/3) (arguably)
> allows this.
>
> Maybe we should add an AARM note and an ACATS test, but leave the language
> alone. Even if the model of gotos and pragmas is a bit weird, there's no
> requirement to change it.

We could be somewhat more explicit (in an AARM note, perhaps) to say that a 
pragma in the place of a statement is considered a statement for the purpose
of rules relating to gotos, description of the execution of a sequence of
statements, etc.  Or we could make such a normative statement in 2.8(7.1/3):

 In place of a statement in a sequence_of_statements{, in which case it is 
 considered a statement for the purposes of other rules of the language}.

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

From: Randy Brukardt
Sent: Sunday, November 14, 2021  12:01 AM

>>in 5.1), lest we end up with another construct like a parenthesized 
>>expression where there is no actual description but rather "everyone 
>>knows what it means". This seems like it is getting unnecessarily messy.
		
>I think we could easily adjust 5.1(13) to say:
>
>	The execution of a null_statement {or a label} has no effect.

An alternative would be to leverage the implicit null statement model by
simply saying that *every* label is associated with an implicit null
statement. Then, one can say that execution continues at the "implicit
null statement associated with the label" or something like that.

I note that neither 5.8(5) nor 5.1(14/2) really say what it means to 
transfer control to a statement, in particular that execution continues
with that statement and then any following ones in the same 
sequence_of_statements (but not any preceding statements). (5.1(15) tells 
us how to execute an *entire* sequence_of_statements, but not really 
anything about how to execute just a part of it.)

That's the sort of thing I'd prefer to fix if we're going to change the 
wording anyway, but otherwise it isn't worth fixing. Another reason not to
put the hood up in the first place...

...
		
>We could be somewhat more explicit (in an AARM note, perhaps) to say 
>that a pragma in the place of a statement is considered a statement for 
>the purpose of rules relating to gotos, description of the execution of 
>a sequence of statements, etc.  Or we could make such a normative 
>statement in 2.8(7.1/3):
>
>    In place of a statement in a sequence_of_statements{, in which case
>    it is considered a statement for the purposes of other rules of the
>    language}.

Makes sense. Probably would want something similar if it is in place of a 
declaration (otherwise, a similar question could arise and it would be weird
to have answered it for execution of statements but not elaboration of
declarations. After all, the elaboration of a declarative_part is the 
"elaboration of the declarative_items, if any, in the order that they are
given" (3.11(7)). Nothing about pragmas in there, either; a declarative_item
isn't a pragma any more than a statement is.

The wording of the rules makes that harder than the above. I'd probably 
suggest a blanket rule, but it would be pretty similar to the existing 
Dynamic Semantics. More thought needed.

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

From: Randy Brukardt
Sent: Sunday, November 14, 2021  7:19 AM

> An alternative would be to leverage the implicit null statement model by
> simply saying that *every* label is associated with an implicit null
> statement. Then, one can say that execution continues at the "implicit null
> statement associated with the label" or something like that.

Implicit stuff tends to be harder to understand.  The target label approach 
eliminates implicit nulls, and so if we make any change, I would prefer to 
go that direction.

> I note that neither 5.8(5) nor 5.1(14/2) really say what it means to
> transfer control to a statement, in particular that execution continues with
> that statement and then any following ones in the same
> sequence_of_statements (but not any preceding statements). (5.1(15) tells us
> how to execute an *entire* sequence_of_statements, but not really anything
> about how to execute just a part of it.)
>
> That's the sort of thing I'd prefer to fix if we're going to change the
> wording anyway, but otherwise it isn't worth fixing. Another reason not to
> put the hood up in the first place...

Agreed.  A lot of the wording in this general area is pretty sloppy, but none
of it is sufficiently broken to deserve fixing on its own. 

...
 
>Or we could make such a normative statement
>>in 2.8(7.1/3):
>>
>>    In place of a statement in a sequence_of_statements{, in which case
>>    it is considered a statement for the purposes of other rules of the
>>    language}.
>
>Makes sense. Probably would want something similar if it is in place of a
>declaration (otherwise, a similar question could arise and it would be weird
>to have answered it for execution of statements but not elaboration of
>declarations. After all, the elaboration of a declarative_part is the
>"elaboration of the declarative_items, if any, in the order that they are
>given" (3.11(7)). Nothing about pragmas in there, either; a declarative_item
>isn't a pragma any more than a statement is.
>
>The wording of the rules makes that harder than the above. I'd probably
>suggest a blanket rule, but it would be pretty similar to the existing
>Dynamic Semantics. More thought needed. 

Yes, probably a blanket rule would be better, but it is a bit painful to word
it.  Perhaps modify 2.8(12):

 Any pragma that appears at the place of an executable construct is executed{,
 and is treated for the purposes of other rules of the language as being of
 the same sort of executable construct}. Unless otherwise specified for a
 particular pragma, this execution consists of the evaluation of each
 evaluable pragma argument in an arbitrary order.

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

Questions? Ask the ACAA Technical Agent