!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 WG9 Approved 22-06-22 !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) @drepl @xbullet @dby @xbullet; or> !corrigendum 8.5.1(4.6/2) @dinsa @xbullet@fa shall exclude null. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.> @dinst In the case where the @i@fa is a @fa with a nominal subtype @i and whose @fa is a @fa that denotes an object @i: @xbullet is an elementary subtype, then:> @xinbull<@i shall be a constant other than a dereference of an access type; or> @xinbull shall be statically compatible with @i; or> @xinbull<@i shall statically match the base subtype of its type if scalar, or the first subtype of its type if an access type.> @xbullet is a composite subtype, then @i shall be known to be constrained or @i shall statically match the first subtype of its type.> !corrigendum 8.5.1(5/3) @drepl 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 @fa 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. @dby 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 @fa 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. ****************************************************************