Version 1.4 of ai12s/ai12-0210-1.txt
!standard 7.3.2(8.3/5) 18-10-16 AI12-0210-1/01
!standard 7.3.2(8.4/5)
!standard 7.3.2(12/3)
!standard 7.3.2(20.1/4)
!class binding interpretation 16-12-19
!status work item 16-12-19
!status received 16-09-29
!priority Very_Low
!difficulty Medium
!qualifier Omission
!subject Type Invariants and Generics
!summary
** TBD **
!question
7.3.2(20.1/4) says
For a view conversion to a class-wide type occurring within the
immediate scope of T, from a specific type that is a descendant of T
(including T itself), a check is performed on the part of the object
that is of type T.
What does "occurring within the immediate scope" mean in the case where the
view conversion occurs in an instance of a generic unit? (Who knows?)
One can also have the opposite situation where it is the generic unit body
(or private part, in the case of a generic child unit) which can see the
completion of the invariant-bearing type and the instance which occurs
outside of that scope. 7.3.2(17/4) is about that case, but that rule doesn't
address the other cases in which invariant checking rules depend on being or
not being "in the immediate scope": view conversions (including conversion
to classwide) and deferred constants. Should it? (Yes.)
7.3.2(17/4) also seems unclear in the case of a nested generic unit.
Consider:
procedure Invtest is
package Pkg is
type T is private;
generic
package G1 is
generic
package G2 is
procedure Proc (X : in out T);
end G2;
end G1;
private
type T is record
Xx, Yy : Integer := 0;
end record with
Type_Invariant => (T.Xx <= T.Yy);
end Pkg;
package body Pkg is
package body G1 is
package body G2 is
procedure Proc (X : in out T) is
begin
X.Yy := Integer'First;
end Proc;
end G2;
end G1;
end Pkg;
package I1 is new Pkg.G1;
package I2 is new I1.G2;
Var : Pkg.T;
begin
I2.Proc (Var);
--
--
end Invtest;
The relevant wording of 7.3.2(17/4) is
... is declared within the immediate scope of type T (or by an
instance of a generic unit, and the generic is declared within the
immediate scope of type T), ...
I2.Proc is not declared within the immediate scope of type Pkg.T (G1.G2.Proc
is, but that's irrelevant). So we need to look at the wording in parentheses.
Is I2.Proc declared by an instance of a generic unit? Yes it is. So far so
good. Is that generic declared within the immediate scope of T? No it isn't!
G1.G2 is declared within the immediate scope of T, but that's irrelevant. The
generic unit we are interested in is I1.G2, which is not declared within the
immediate scope of T.
Should there be some wording adjustment to fix this? (Yes.)
!recommendation
(See Summary.)
!wording
Insert ahead of 7.3.2(8.3/5) (i.e., immediately before the definition of
"type-invariant preserving"):
Given a declaration D, the "extended immediate scope"
of the declaration is defined to be
- the immediate scope of D; and
- for any generic unit G declared within the extended immediate
scope of D, the extended immediate scope of any instance of G
[Redundant: , other than a formal package].
In 7.3.2(8.4/5), add the word "extended":
(or by an instance of a generic unit, and the generic is declared within
the {extended} immediate scope of type T)
In 7.3.2(12/3), add the word "extended":
For a view conversion, outside the {extended} immediate scope of T, ...
In 7.3.2(20.1/4), add the word "extended":
For a view conversion to a class-wide type occurring within the {extended}
immediate scope of T, ...
Add after 7.3.2(24.a/3) (i.e., as another note at the end of the
Dynamic Semantics section).
AARM note:
In the following example
package Pkg is
type T is private with Type_Invariant => Is_Ok (T);
function Is_Ok (Arg : T) return Boolean;
generic
package G1 is
generic
package G2 is
generic
package G3 is
procedure Foo (X : in out T);
end G3;
end G2;
end G1;
private
...
end Pkg;
with Pkg;
pragma Elaborate (Pkg);
package Pkg_Client is
package I1 is new Pkg.G1;
package I2 is new I1.G2;
package I3 is new I2.G3;
end;
the body of the procedure G1.G2.G3.Foo sees the full view of the type T,
so we want I3.Foo to be type-invariant preserving for T. That illustrates
the motivation for defining the term "extended immediate scope" and then
using that term instead of "immediate scope" in some of the rules in
this section.
!discussion
[Editor's musings:
For the third issue, one needs to be careful with the wording lest a type
declared within the outer generic get swept up in the special case (such a
type should always be checked in this case).
There is also an issue with derived generic formal types.
procedure Invtest2 is
package Pkg2 is
type T is private;
generic
type Der is new T with private;
package G1 is
generic
package G2 is
procedure Proc2 (X : in out Der);
end G2;
end G1;
private
type T is record
Xx, Yy : Integer := 0;
end record with
Type_Invariant => (T.Xx <= T.Yy);
end Pkg2;
package body Pkg2 is
package body G1 is
package body G2 is
procedure Proc2 (X : in out Der) is
begin
X.Yy := Integer'First; --
end Proc2;
end G2;
end G1;
end Pkg2;
package I1 is new Pkg.G1(Pkg.T);
package I2 is new I1.G2;
Var : Pkg.T;
begin
I2.Proc (Var);
--
--
end Invtest2;
I don't see how the existing rules deal with this, and it's not listed in the
case of holes, either.
End Editor's musings.]
---
It seems ok, but worth noting, that we can have a generic whose body
can see the full view of some private type but which is not in immediate
scope of the private type (because the declaration of the generic package
spec precedes that of the partial view of the private type).
package Pkg is
generic
package G1 is
procedure Foo;
end G1;
type T is private with Type_Invariant => ...;
private
...
end Pkg;
An instance of such a generic will not be in the "extended immediate scope"
of the private type and so any visible subprograms that the instance might
declare will not be "type-invariant preserving" for the private type.
But the private type can't be mentioned in the profile of such a subprogram
unless incomplete types and access types are involved somehow. We are not
trying to plug all such holes (for example, we also don't worry about
the access-to-access-to-private case).
---
This change does not address the issue Randy raised in the AI having to do
with generic formal derived types. One alternative is to ignore this problem
- we've already acknowledged that type invariants are not bulletproof
(which means that the SPARK folks are going to have to add additional
verification conditions not corresponding to Ada-defined runtime checks
in order to make them bulletproof, but that's ok).
Another alternative would be to take the RM text
and at least one of the following applies to the callable entity:
has a result with a part of type T;
has one or more out or in out parameters with a part of type T;
has an access-to-object parameter or result whose designated type
has a part of type T; or
is a procedure or entry that has an in parameter with a part of type T.
Each such part of type T is said to be subject to an invariant check for T.
and replace each occurrence of "of type T" with
"of type T or a descendant thereof" or something equivalent.
Do we want to do that?
!ASIS
No ASIS effect.
!ACATS test
!appendix
From: Steve Baird
Sent: Thursday, September 29, 2016 6:31 PM
Ada RM 7.3.2(20.1/4) says
For a view conversion to a class-wide type occurring within the
immediate scope of T, from a specific type that is a descendant of T
(including T itself), a check is performed on the part of the object
that is of type T.
What does "occurring within the immediate scope" mean in the case where the
view conversion occurs in an instance of a generic unit?
Consider the following example:
procedure Invariant_Test is
pragma Assertion_Policy (Check);
type T1 is tagged record
Aaa : Natural := 0;
Bbb : Natural := 100;
end record;
procedure Swap_T1 (X1 : in out T1) is
begin
X1 := (Aaa => X1.Bbb, Bbb => X1. Aaa);
end;
generic
type D is new T1 with private;
procedure Swap_View_Conversion (X : in out D);
procedure Swap_View_Conversion (X : in out D) is
begin
Swap_T1 (T1 (X)); -- a view conversion
end;
package Pkg is
type T2 is private;
private
type T2 is new T1 with null record
with Type_Invariant => T2.Aaa < T2.Bbb;
package Nested is
procedure Swap_T2 is new Swap_View_Conversion (T2);
end;
end;
package body Pkg is
Y : T2;
begin
Nested.Swap_T2 (Y);
pragma Assert (Y.Aaa = 100);
end;
begin null; end;
Does the call to Nested.Swap_T2 fail an invariant check?
Tuck said (in private communication):
> Should an external generic, instantiated locally, be able to do
> something that a normal external package could *not* do. I believe the
> answer is yes, presuming the type with the invariant is only visible
> to the generic as a formal type, as opposed to being named directly.
> When you instantiate a generic with an actual type that has an
> invariant, and you do it within the full view of the type, then the
> generic should not be affected by the invariant.
A general design principle is that invariants don't come into play very much
as long as you stay inside the body of the package that implements the
private type and don't call subprograms which are callable (directly or via
overriding) from outside of that package. There are exceptions to that (e.g.,
default initialization of an object declared in the package body), but that's
the general idea. Tuck's suggestion that no exception should be raised in this
case is consistent with that principle.
Note that 7.3.2(20.1/4) is somewhat unusual in talking about being "within"
some scope in the context of a dynamic semantics rule. Any time the RM does
this, there are going to be questions about generics vs. instances.
One can also have the opposite situation where it is the generic unit body (or
private part, in the case of a generic child unit) which can see the
completion of the invariant-bearing type and the instance which occurs
outside of that scope. 7.3.2(17/4) is about that case, but that rule doesn't
address the other cases in which invariant checking rules depend on being or
not being "in the immediate scope": view conversions (including conversion to
classwide) and deferred constants. These cases just need to be well-defined;
all that is needed is a clarification one way or the other. The fact that
7.3.2(17/4) is a rule and not a ramification *suggests* that no checks should
be performed in these cases, but that seems far from conclusive. As usual, we
should decide first what behavior we want before worrying about interpreting
the current wording.
7.3.2(17/4) also doesn't really deal well with a case like
package I1 is new G1;
package I2 is new I1.G2;
When it says "and the generic is declared within the immediate scope of type
T", in what scope is the generic I1.G2 declared? Inside (the expansion of) I1
or inside G1? The point of this rule is to deal with generic bodies that can
see the completion of the private type; this suggests that we want to think of
I1.G2 as being declared inside of G1, as opposed to inside I1, but the current
wording seems unclear.
****************************************************************
From: Randy Brukardt
Sent: Thursday, September 29, 2016 6:41 PM
...
> As usual, we should decide first what behavior we want before worrying
> about interpreting the current wording.
When it comes to type invariants, pretty much the only thing we care about is
that the rule is well-defined and doesn't cause horrible implementation
problems. These are a distant fourth out of the four kinds of contracts; the
fact that GNAT had completely implemented them wrong until Jeff wrote some
ACATS tests tells me that no real users really care about the details of this
feature.
I suspect that these checks in instances will be hell on generic code sharing,
but I have a hard time caring because I doubt that I'll ever have a customer
who cares. (Ergo, probably these will never be implemented in Janus/Ada.)
****************************************************************
From: Steve Baird
Sent: Tuesday, October 16, 2016 2:38 PM
Attached is some proposed wording for AI12-0210. [This is version /01 of the
AI - Editor.]
As usual, thanks to Randy for preliminary review but don't blame him if you
think it stinks.
****************************************************************
From: Tucker Taft
Sent: Tuesday, October 16, 2016 3:16 PM
You had a question at the end, but you didn't express your own opinion. Do you
recommend we make the generalization to "T or a descendant thereof" (note that
saying "a descendant of T" includes T itself, so this could be simplified). If
not, why not?
****************************************************************
From: Steve Baird
Sent: Tuesday, October 16, 2016 5:28 PM
First, a minor point - I considered the phrasing you mentioned but it seemed
awkward. Consider, for example, replacing
has a result with a part of type T;
with
has a result with a part of a descendant of T;
It sounds (at least to me) like we are talking about a "part of a descendant"
(as opposed to the entire descendant). That's why I suggested "T or a descendant
thereof". But I agree that phrasing is redundant and I'd be very open to any
suggestions about improving it.
On to the main question.
I think the arguments about this possible change come down to cost/benefit
analysis. What is the benefit associated with plugging this particular hole in
type invariant enforcement (while leaving other holes unplugged) and what is the
cost associated with the fix?
At first I thought this was simply a problem with derived types, orthogonal to
any problems involving generics. IMO, that would raise the priority of plugging
this hole.
Suppose we have a type-invariant-bearing type T1 and another type T2 derived
from it. T2 has operations whose bodies can see the implementation of T1 and
thereby create invariant-violating values of type T2 that can leak out of the
immediate scope of T1.
It's analogous to the case where T2 is a one-field record type with a component
of type T1, except that invariant checking for that case is already handled
correctly in the RM.
But we've got the rule that the parent type of a derived type must be completely
defined (unlike the case of a component type), so I think that means that in
order to run into this problem we have to use either
a) a formal derived type, as in Randy's example or
b) A child unit, as in
package Pkg is
type T is private with Type_Invariant => ...;
private
...;
end;
package Pkg.Child is
type D is new T;
procedure Op (X : in out D);
end;
RM 7.3(7.a) says:
Note that deriving from a partial view within its immediate scope
can only occur in a package that is a child of the one where the
partial view is declared.
These are less common constructs, so the benefit of plugging these holes is
smaller than I thought initially.
But still, a hole is a hole; why wouldn't be want to plug it?
The costs in run-time overhead, compile-time overhead, and compiler
implementation effort do not seem to be large.
I mainly held off on including this change in the proposed wording because of
FUD and, specifically, the fear of unintended consequences. In looking at this
AI, I focused on the original problem with generics that spawned the AI. I
haven't looked as closely at this "descendants" problem and the possible
consequences of the change I outlined. That's the main reason that I didn't
include this change in the proposal - I think it is probably the right way to
go, but I am less sure about this than about the rest of the AI (i.e., the
"extended immediate scope" stuff).
The other reason (which I forgot to mention earlier) is that another approach
occurred to me, but that approach is even less well thought out in my mind.
Perhaps we can say that if a type invariant applies to a type T1 and if a type
T2 is derived from T1, then the type invariant also applies to T2. With that
approach, we might be able to get the desired effect without having to talk
about descendants in so many places. Or maybe not - perhaps this is a
fundamentally flawed idea. But it seems like it would be worth considering it
before committing ourselves to another approach. OTOH, I understand that we
don't have much time left for this revision.
****************************************************************
Questions? Ask the ACAA Technical Agent