Version 1.4 of ai12s/ai12-0401-1.txt

Unformatted version of ai12s/ai12-0401-1.txt version 1.4
Other versions for file ai12s/ai12-0401-1.txt

!standard 3.3(23.2/3)          20-12-11 AI12-0401-1/04
!standard 8.5.1(4.7/5)
!standard 8.5.1(5/3)
!class binding interpretation 20-10-15
!status Amendment 1-2012 20-10-21
!status ARG Approved 15-0-0 20-12-09
!status work item 20-10-29
!status ARG Approved 13-0-1 20-10-21
!status work item 20-10-15
!status received 20-10-15
!priority Low
!difficulty Easy
!qualifier Omission
!subject Renaming of a qualified expression of a variable
!summary
We restrict renaming of a qualified expression to cases where the operand is a constant, or the target subtype statically matches the nominal subtype of the operand, or is unconstrained with no predicates.
We correct "known to be constrained" so that the nominal subtype of a qualified expression does not necessarily make a prefix "known to be constrained" even thought the operand would not be "known to be constrained".
!question
Consider the following situation:
X : T := ...; Y : S renames S'(X);
If X is a variable and its nominal subtype is not the same as S, and in particular has a subtype that includes values that do not all satisfy S, then a later update to X to give it a value that is not within the subtype S could create a bizarre situation where Y no longer satisfies its nominal subtype S. Should this be detected? (Yes.)
!recommendation
Disallow renaming of a qualified expression if the operand denotes a variable with a nominal subtype that does not statically match the target subtype of the qualified expression, unless the target subtype imposes no constraints or predicates.
!wording
Modify 3.3(23.2/3)
[to ensure known-to-be-constrained is not influenced by the nominal
subtype of the qualified_expression]
* its nominal subtype is constrained[,] and [is] not an untagged partial view{, and it is neither a value conversion nor a qualified_expression}; or
Delete 8.5.1(4.7/5) [moved below]
Add after 8.5.1(4.7/5):
In the case where the /object_/name is a qualified_expression with a nominal subtype S and whose expression is a name that denotes an object Q:
* if S is an elementary subtype, then:
* Q shall be a constant other than a dereference of an access type; or
* the nominal subtype of Q shall be statically compatible with S; or
* S shall statically match the base subtype of its type if scalar, or the first subtype of its type if an access type.
* if S is a composite subtype, then Q shall be known to be constrained or S shall statically match the first subtype of its type.
AARM Ramification: There's no restriction if the expression is a value.
AARM Reason: This check prevents the renamed object from violating its nominal subtype. As the subtype is only checked when the object is renamed, we make it illegal if the actual object is a variable whose value could be changed afterwards to violate the subtype. This is messy as "known to be constrained" is only defined for composite objects, so we have to handle elementary objects and all values separately.
Modify 8.5.1(5/3):
The renamed entity shall not be a subcomponent that depends on discriminants of an object whose nominal subtype is unconstrained unless the object is known to be constrained. A slice of an array shall not be renamed if this restriction disallows renaming of the array. [In addition to the places where Legality Rules normally apply, these rules apply also in the private part of an instance of a generic unit.]
In addition to the places where Legality Rules normally apply (see 12.3), these rules also apply in the private part of an instance of a generic unit.
AARM Discussion: This applies to all of the Legality Rules in this subclause.
!discussion
This is analogous to the rule in 8.5.1(5/3) that disallows renaming of a discriminant-dependent component unless the enclosing object is known to be constrained.
This issue arose when looking at what sort of compile-time checks the SPARK tools would have to perform in a renaming of a qualified expression. It became clear that there was an erroneous situation lurking here, if we allow a renaming of a constant view of a variable that could later be altered to no longer satisfy the nominal subtype of the qualified expression.
We modify the rule in 3.3(23.2/3) so that known-to-be-constrained is determined by the operand of a conversion or a qualified_expression (as specified in 3.3(23.8.5)), rather than by the nominal subtype. This change will make some 'Access prefixes and renamings illegal when the qualified (or converted) object is not itself "known to be constrained". That was always intended, but not captured by the rules.
Both of these changes are incompatible with Ada 2012 as defined, but are necessary to meet the design goal that a legal renaming cannot be of something that can be changed in a way that can cause erroneous execution.
Note that we don't need to worry about generic formal in-out objects, even though they are effectively renames of the generic actual object, because a qualified_expression is a constant view, so it would not be permitted as the actual for a generic formal in-out object.
!example
In a situation analogous to the one mentioned in the !problem:
X : Integer := ...; Y : Positive renames Positive'(X);
This renaming will be illegal since Positive statically matches neither Integer nor Integer'Base. That is good, because in the following we would have trouble because the nominal subtype of Y is the static subtype Positive, so without this rule, the following case statement would be legal:
X := -1; case Y of when 1 .. Positive'Last => pragma Assert (Y > 0); end case;
even though the case choices do not cover all of the possible values of Y.
!corrigendum 3.3(23.2/3)
Replace the paragraph:
by:
!corrigendum 8.5.1(4.6/2)
Insert after the paragraph:
the new paragraph:
In the case where the object_name is a qualified_expression with a nominal subtype S and whose expression is a name that denotes an object Q:
!corrigendum 8.5.1(5/3)
Replace the paragraph:
The renamed entity shall not be a subcomponent that depends on discriminants of an object whose nominal subtype is unconstrained unless the object is known to be constrained. A slice of an array shall not be renamed if this restriction disallows renaming of the array. In addition to the places where Legality Rules normally apply, these rules apply also in the private part of an instance of a generic unit.
by:
The renamed entity shall not be a subcomponent that depends on discriminants of an object whose nominal subtype is unconstrained unless the object is known to be constrained. A slice of an array shall not be renamed if this restriction disallows renaming of the array.
In addition to the places where Legality Rules normally apply (see 12.3), these rules also apply in the private part of an instance of a generic unit.
!ASIS
No ASIS effect.
!ACATS test
An ACATS B-Test is needed to check that the illegal cases are detected.
!appendix

Editor's note: I changed the version provided by Tucker to a Binding
Interpretation, since this is plugging holes caused by the introduction
of qualified expressions as names in Ada 2012. It seems to me that it
should apply to Ada 2012 as well, even if that is (very) marginally
incompatible.

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

From: Tucker Taft
Sent: Wednesday, October 21, 2020  3:55 PM

Below is the example I promised for AI12-0401-1 about renaming a qualified 
expression.

------------------

!example

In a situation analogous to the one mentioned in the !problem:

   X : Integer := ...;
   Y : Positive renames Positive'(X);
   
This renaming will be illegal since Positive statically matches neither 
Integer nor Integer'Base.  That is good, because in the following we would 
have trouble because the nominal subtype of Y is the static subtype Positive, 
so without this rule, the following case statement would be legal:

   X := -1;
   case Y is
      when 1 .. Positive'Last => 
         pragma Assert (Y > 0);
   end case;
   
even though the case choices do not cover all of the possible values of Y.

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

From: Jeff Cousins
Sent: Thursday, October 22, 2020  1:10 PM

> case Y of
 
case Y is

methinks!

> Y : Positive renames Positive'(X);
 

Is this currently legal ?  GNAT only seems to allow renaming of an object, 
not of a qualified expression.

>  case Y {is}[of]

Wouldn’t the compiler require case alternatives for all values of X anyway, 
not just of Y, as renaming doesn’t require subtype conformance ?  As stated 
in the !problem of AI12-0275, “the constraints ... of the subtype_mark are 
ignored in favor of those of the renamed object”, so any constraints in the 
subtype of Y are irrelevant, and indeed given AI12-0275 the subtype mark no 
longer even has to be given in the renaming ?

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

From: Tucker Taft
Sent: Thursday, October 22, 2020  1:48 PM

>>  case Y of
 
>case Y is
> 
>methinks!

Youthinks right!
 
>> Y : Positive renames Positive'(X);
 
>Is this currently legal ?  GNAT only seems to allow renaming of an object, 
>not of a qualified expression.

GNAT apparently never implemented this feature.

>>  case Y {is}[of]
 
>Wouldn’t the compiler require case alternatives for all values of X anyway, 
>not just of Y, as renaming doesn’t require subtype conformance ?  As stated 
>in the !problem of AI12-0275, “the constraints ... of the subtype_mark are 
>ignored in favor of those of the renamed object”, so any constraints in the 
>subtype of Y are irrelevant, and indeed given AI12-0275 the subtype mark no 
>longer even has to be given in the renaming ?

That's all true, but in the sentence you quoted, the "renamed object" is 
"Positive'(X)" which has nominal subtype Positive.  We could have written 
"Y : Natural renames Positive'(X);" and Y would still have the nominal subtype 
Positive.  Unfortunately, X has the nominal subtype Integer, so we can set X 
to a negative value while the rename of it exists, and the renaming has the 
nominal subtype Positive.

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

From: Jeff Cousins
Sent: Thursday, October 22, 2020  3:41 PM

Thanks Tuck.

>>>  case Y {is}[of]

>> Wouldn’t the compiler require case alternatives for all values of X anyway, 
>> not just of Y, as renaming doesn’t require subtype conformance ?  As stated 
>> in the !problem of AI12-0275, “the constraints ... of the subtype_mark are 
>> ignored in favor of those of the renamed object”, so any constraints in the
>> subtype of Y are irrelevant, and indeed given AI12-0275 the subtype mark no
>> longer even has to be given in the renaming ?

>That's all true, but in the sentence you quoted, the "renamed object" is 
>"Positive'(X)" which has nominal subtype Positive.  We could have written 
>"Y : Natural renames Positive'(X);" and Y would still have the nominal 
>subtype Positive.  Unfortunately, X has the nominal subtype Integer, so we 
>can set X to a negative value while the rename of it exists, and the renaming 
>has the nominal subtype Positive.

Whether Y is Natural or Positive, does it actually matter ?

The compiler will check that there are case alternatives for all possible 
values of the subtype of X, regardless of whatever the subtype of Y is: 
Positive, Natural, or anything else.

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

From: Tucker Taft
Sent: Thursday, October 22, 2020  4:59 PM

> The compiler will check that there are case alternatives for all possible 
> values of the subtype of X, regardless of whatever the subtype of Y is: 
> Positive, Natural, or anything else.

You seem to have faith that the compiler will do the "right thing" but the 
RM says that you only need case alternatives to cover the nominal subtype (if
it is static -- see 5.4(7/4)), hence why we are focusing on the question of 
what is the nominal subtype of the renaming of a qualified_expression.

For reference, the wording of 5.4(7/4) is:

  "If the selecting_expression is a name [(including a type_conversion, 
   qualified_expression, or function_call)] having a static and constrained 
   nominal subtype, then each non-others discrete_choice shall cover only 
   values in that subtype that satisfy its predicates (see 3.2.4), and each 
   value of that subtype that satisfies its predicates shall be covered by 
   some discrete_choice [(either explicitly or by others)]."

That "static and constrained nominal subtype" phrase is the key one.

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

From: Randy Brukardt
Sent: Thursday, October 22, 2020  7:10 PM

>> Y : Positive renames Positive'(X);

>Is this currently legal ?  GNAT only seems to allow renaming of an 
>object, not of a qualified expression.

Yes, that's legal Ada 2012. (It would be legal in Ada 202x even without the 
qualification change, since one can now rename values.)

I guess the C-Test for this AI needs a higher priority than I originally 
assigned it. ;-) The B-Test has a rather high priority since it represents 
an incompatibility with Ada 2012, the C-Test is lower since it doesn't seem 
to be a particularly important capability.

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

From: Randy Brukardt
Sent: Thursday, October 22, 2020  7:26 PM

...
> You seem to have faith that the compiler will do the "right thing" but 
> the RM says that you only need case alternatives to cover the nominal 
> subtype (if it is static -- see 5.4(7/4)), hence why we are focusing 
> on the question of what is the nominal subtype of the renaming of a 
> qualified_expression.

Yup.

One thing that may not be clear is why renames are different from other uses
of qualified_expressions. The reason for that is that the subtype check is 
performed at the point that the qualified_expression is evaluated.

So if you had directly written:

   X := -1;
   case Positive'(X) is
      when 1 .. Positive'Last => 
         pragma Assert (Y > 0);
   end case;

The qualified expression will perform a check that X is in Positive (which 
will fail, of course), so there is no problem with the case statement not 
having choices for negative numbers. (Indeed, choices for negative numbers 
would be illegal in this case statement -- they're out of the range of the 
nominal subtype of the expression.)

However, for a renames, the check is performed when the renames is evaluated, 
and is never repeated. That's why we need restrictions on what can be renamed 
(Ada 83 has such rules for discriminant-dependent components, so this was 
always intended). Otherwise, one would need to repeat the checks at every use, 
and that was clearly not the model intended by Ada 83 (renaming was intended 
in part to improve efficiency by avoiding re-evaluation of expensive names), 
and certainly is not something that compilers could support without quite a 
bit of extra work.

Hope this helps.

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

From: Jeff Cousins
Sent: Friday, October 23, 2020  3:07 AM

Thanks Tuck and Randy for your replies.

>You seem to have faith that the compiler will do the "right thing" but the 
>RM says that you only need case alternatives to cover the nominal subtype 
>(if it is static -- see 5.4(7/4)), hence why we are focusing on the question
>of what is the nominal subtype of the renaming of a qualified_expression.
> 
>For reference, the wording of 5.4(7/4) is:
> 
>"If the selecting_expression is a name [(including a type_conversion, 
>qualified_expression, or function_call)] having a static and constrained 
>nominal subtype, then each non-others discrete_choice shall cover only values
>in that subtype that satisfy its predicates (see 3.2.4), and each value of 
>that subtype that satisfies its predicates shall be covered by some 
>discrete_choice [(either explicitly or by others)]."
> 
>That "static and constrained nominal subtype" phrase is the key one.
 
Sorry to labour the point, but isn’t it the subtype of X that matters, not 
the subtype of Y?

Otherwise, how do you square this with the !problem of AI12-027 saying, 
“the constraints ... of the subtype_mark are ignored in favor of those of
the renamed object”

procedure Test_401 is
   subtype My_Subtype          is Integer range 3 .. 5;
   subtype Garbage_Subtype is Integer range -19 .. -7;
   X : My_Subtype;
   Y : Garbage_Subtype renames X;
begin
   X := 3;
   case Y is
      when 3 .. 5 => 
         pragma Assert (Y in 3 .. 5);
   end case;
end Test_401;

Clean compiles.  The compiler is clearly using the subtype of X not subtype 
of Y when checking the case statement.

The subtype of Y is virtually irrelevant, that’s why AI12-0275 makes it 
optional.

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

From: Arnaud Charlet
Sent: Friday, October 23, 2020  3:48 AM

> > Is this currently legal ?  GNAT only seems to allow renaming of an object,
> > not of a qualified expression.
> 
> GNAT apparently never implemented this feature.

You guys are either using an old version of GNAT (for Jeff, which is expected 
since Jeff is no longer a customer), or didn't bother to check with a current 
GNAT.

The latest GNAT Pro (which is the only version with reasonable support for Ada 
202x and therefore relevant in such discussions) supports the above construct 
with -gnat2020 and will yield:

$ gcc -c p.ads -gnat2020 -gnatl

     1. package P is
     2.
     3.    X : Natural := 0;
     4.    Y : Positive renames Positive'(X);
                                        |
        >>> warning: value not in range of type "Standard.Positive"
        >>> warning: "Constraint_Error" will be raised at run time

     5.
     6. end P;

FWIW if you compile without -gnat2020 you'll get:

$ gcc -c p.ads
p.ads:4:33: warning: value not in range of type "Standard.Positive"
p.ads:4:33: warning: "Constraint_Error" will be raised at run time
p.ads:4:33: value in renaming requires -gnat2020

So yes, this was legal in Ada 202x up to AI12-0401 and will now become illegal.

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

From: Tucker Taft
Sent: Friday, October 23, 2020  7:19 AM

>Sorry to labour the point, but isn’t it the subtype of X that matters, not 
>the subtype of Y? Otherwise, how do you square this with the !problem of 
>AI12-027 saying, “the constraints ... of the subtype_mark are ignored in 
>favor of those of the renamed object”

The "renamed object" is the qualified expression, since that is what is 
denoted by the object_name in the object renaming.  It is true that the 
subtype specified for the renaming is irrelevant, but the subtype specified
in the qualified expression is *not* irrelevant.  It determines the nominal 
subtype of the renamed object.  And that is what we are worried about.
 
>procedure Test_401 is
>   subtype My_Subtype          is Integer range 3 .. 5;
>   subtype Garbage_Subtype is Integer range -19 .. -7;
>   X : My_Subtype;
>   Y : Garbage_Subtype renames X;
>begin
>   X := 3;
>   case Y is
>      when 3 .. 5 => 
>         pragma Assert (Y in 3 .. 5);
>   end case;
>end Test_401;
> 
>Clean compiles.  The compiler is clearly using the subtype of X not subtype 
>of Y when checking the case statement. The subtype of Y is virtually 
>irrelevant, that’s why AI12-0275 makes it optional.

Yes, but the above is not a renaming of a qualified expression.  That is the 
only case we are talking about in this entire thread.  If you change this to:

   Y : Garbage_Subtype renames Bizarro_Subtype'(X);

then in "case Y is" what will matter is the range of Bizarro_Subtype, even 
though X might be changed to be outside the Bizarro_Subtype.

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

From: Jeff Cousins
Sent: Friday, October 23, 2020  7:38 AM

Many thanks Tuck, that makes more sense.

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


Summary of private discussion, October 22-25, 2020

A number of issues are missed by the approved wording:

(1) The rules should be after paragraph 4.7 rather than 4, in order to
put the rules closer to similar requirements and to avoid renumbering existing
paragraphs.

(2) "variable" isn't the only case that causes problems. The "known to be
constrained" rules encapulate those cases for composite types; for elementary
types, it would be enough to require a constant other than a dereference of
an access type (an access-to-constant can designate a variable).

(3) We don't want to make more cases illegal than necessary as this is an
incompatibility and a potential annoyance. As such, we should use "static
compatibility" for elementary types (the "known to be constrained" rules
do that for composite types).

(4) The generic boilerplate should apply to these new rules. Rather than
duplicating it, we make it apply to all of the Legality Rules in this 
subclause. (The paragraph 4 and 4.1-4.3 rules probably don't need the
boilerplate, but it is harmless for them.)

We have reopened the AI to allow the ARG to review the updated wording.

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

Questions? Ask the ACAA Technical Agent