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

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

!standard 7.3.2(9/4)          15-08-07 AI12-0167-1/03
!class ramification 15-06-17
!status WG9 Approved 15-10-16
!status ARG Approved 11-0-1 15-06-27
!status work item 15-06-17
!status received 15-05-29
!priority Low
!difficulty Medium
!subject Type_Invariants and tagged-type View Conversions
!summary
If an object of type T that is a component of a class-wide object is modified within the scope of the full view of type T, then there is no invariant check for T at that point.
!question
Consider the following example:
procedure Type_Invariant_Breaker is
type Root is tagged null record;
package Pkg is type Has_Invariant is private;
procedure Oops (X : in out Root'Class); procedure Rely_On_Incoming_Invariant (Y : Has_Invariant); private type Has_Invariant is record Lo, Hi : Integer := 0; end record with Type_Invariant => (Has_Invariant.Lo <= Has_Invariant.Hi); end Pkg;
type Ext is new Root with record Field : Pkg.Has_Invariant; end record;
package body Pkg is procedure Break_It (Xx : out Has_Invariant) is begin Xx := (Lo => 1, Hi => 0); end;
procedure Oops (X : in out Root'Class) is begin if X in Ext'Class then Break_It (Ext (X).Field); ------ <<<<< danger, Will Robinson end if; end;
procedure Rely_On_Incoming_Invariant (Y : Has_Invariant) is begin pragma Assert (Y.Lo <= Y.Hi); end; end Pkg;
Ext_Var : Ext; begin Pkg.Oops (Ext_Var); Pkg.Rely_On_Incoming_Invariant (Ext_Var.Field); end;
At the danger spot, we are changing Field using a local procedure which is allowed to violate the Type_Invariant that applies to its type, Has_Invariant. Unfortunately Field is a component of a class-wide object, and this will violate the general principle that components of a class-wide object should satisfy their invariants (as implied by 7.3.2(20.1/4)).
Do we need an additional type invariant check to close this hole? (No.)
!response
We know that type invariants have holes. AARM 7.3.2(24.a/3) discusses the known holes. The principles are that holes should be unlikely, and that holes cannot be caused by a client of the type with the invariant without cooperation of the package author.
This hole clearly meets both criteria. It seems impossible to cause this problem without having two intertwined type hierarchies. As such, it won't occur very often since designers are trying to reduce, not increase, coupling.
Second, this can only happen when there is a conversion toward the leaves of a derivation tree. To be safe, such a conversion has to be protected with an explicit check of some type (or subclass). These also are discouraged in OOP code because they don't extend well (especially checks of a specific type).
Third, this check would be inside the body of the abstraction. Experience writing ACATS tests for type invariants shows that such checks surprise users (even experienced Ada users) because they violate the model of type invariant checking (that invariants are only checked when entering and leaving the abstraction, not inside). Existing checks that occur inside the package (such as the default initialization check) trip users, even those that think they know better (like the author of this AI).
The first two factors require help from the author of the abstraction with the type T having a type invariant. There has to be some subprogram that copies a broken value of type T into a component of some other type which does not visibly have a component of type T (if it is known to have a component of type T, then an invariant check would be performed on the object at the package boundary -- recall that the invariant check rules are on "parts of T"). This is unlikely and avoidable. (If all abstractions are private types, this problem can't happen, for instance.)
The third factor suggests that closing the hole would be as surprising as leaving it. Consider the following modification of the example:
if X in Ext'Class then
Set_Lo (Ext (X).Field, 1); Set_Hi (Ext (X).Field, 1);
end if;
Where the operations do the obvious thing. In this case, fixing the hole would also cause reasonable code to raise an invariant failure (the invariant would fail after the call to Set_Lo, but it is OK after the call to Set_Hi). It appears that the fix would cause more trouble than it would catch.
For all these reasons, we do not change the rules.
!wording
Add after 7.3.2(20/3):
AARM To Be Honest: In all of the above, for a class-wide object, we are only referring to the parts of the specific root type of the class. We don't want the overhead of checking every class-wide object in case some future extension component might have type T (contrast this to finalization, where we do intend that overhead).
Add after 7.3.2(20.a/4):
Despite this model, if an object of type T that is a component of a class-wide object is modified within the scope of the full view of type T, then there is no invariant check for T at that point.
Add to the end of 7.3.2(23.a/4):
Similar holes exist for class-wide objects as discussed above.
!discussion
(See Response.)
!ASIS
No ASIS effect.
!ACATS test
An ACATS C-Test could be created to check this, but we don't really care if an implementation makes an unrequired check in such a case.
!appendix

From: Tucker Taft
Sent: Friday, May 29, 2015  12:13 PM

Internal discussions at AdaCore about how to enforce statically the various
Type_Invariant rules led us to some questions about class-wide types and view
conversions.  Some of this might apply to Dynamic_Predicates applied to tagged
types as well.

Here is Steve's example of the problem:

procedure Type_Invariant_Breaker is

   type Root is tagged null record;

    package Pkg is
       type Has_Invariant is private;

       procedure Oops (X : in out Root'Class);
       procedure Rely_On_Incoming_Invariant (Y : Has_Invariant);
    private
       type Has_Invariant is record Lo, Hi : Integer := 0; end record
	with Type_Invariant => (Has_Invariant.Lo <= Has_Invariant.Hi);
    end Pkg;

    type Ext is new Root with record Field : Pkg.Has_Invariant; end record;

    package body Pkg is
       procedure Break_It (Xx : out Has_Invariant) is
       begin
	 Xx := (Lo => 1, Hi => 0);
       end;

       procedure Oops (X : in out Root'Class) is
       begin
	 if X in Ext'Class then
	    Break_It (Ext (X).Field);  ------ <<<<< danger, Will Robinson
	 end if;
       end;

       procedure Rely_On_Incoming_Invariant (Y : Has_Invariant) is
       begin
	 pragma Assert (Y.Lo <= Y.Hi);
       end;
    end Pkg;

    Ext_Var : Ext;
begin
    Pkg.Oops (Ext_Var);
    Pkg.Rely_On_Incoming_Invariant (Ext_Var.Field);
end;

-------

At the danger spot, we are changing Field using a local procedure which is
allowed to violate the Type_Invariant that applies to its type, Has_Invariant.
Unfortunately Field is a component of a class-wide object, and this will violate
the general principal that components of a class-wide object should satisfy
their invariants (as implied by 7.3.2(20.1/4)).  For SPARK we are considering
various rules.  In some sense the view conversion that converts X : Root'Class
to an object of type Ext, after the update to Field, undergoes an implicit
reverse view conversion.  If that reverse "view conversion" had the same checks
as an explicit forward conversion, that would catch the problem. However, the
conversion could have been written:

     Ext'Class(X).Field

in which case there is no specific-to-class-wide conversion to trigger 20.1/4.
So probably a more general rule is needed that disallows updating part of a
class-wide object in a way that violates any invariants.  Alternatively, this
would just be considered a "hole" in Type_Invariants, not caught until some
later point (if ever).

It would seem that a Dynamic_Predicate also should be checked after updating a
field via a view conversion, but we don't generally worry about predicates after
component updates, so perhaps that is beside the point...

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

From: Randy Brukardt
Sent: Friday, May 29, 2015  7:57 PM
...
> So probably a more general rule is needed that disallows updating part
> of a class-wide object in a way that violates any invariants.
> Alternatively, this would just be considered a "hole" in
> Type_Invariants, not caught until some later point (if ever).

I think it has to be a hole. I can't imagine what "updates in a way that
violates any invariants" means in terms of a real, enforcable language rule --
it would have to embody the entirety of the existing invariant rules. And we
have plenty of holes.

Besides, this sort of structure is quite dubious for a class-wide type. Not only
are you writing code that depends on a particular tag (always a bit dubious in
itself), but you're also doing so in the body of the type of the component. It
seems very strange to have an operation of Root'Class in this package that
defines a particular unrelated OOP -- seems like a nasty coupling. Usually
class-wide operations belong with the declaration of Root or in a separate
package. So this structure is completely avoidable, certainly it wouldn't exist
in "good" OOP code (because that never tests for specific tags, which might
break if a new extension is defined).

The big difference between the holes that we've plugged and the ones that we
haven't is that the ones we've left are (1) unlikely and (2) completely
avoidable by the author of the package. That is, if a hole can be caused by a
client without help from the package author, then we plug it. Otherwise, (and
especially if it requires Bairdian hoops), if the package author can avoid it
simply by ensuring that it doesn't unnecessarily couple operations and it
doesn't visibly export components, then it's hard to worry about it.

(A rule that avoids all holes for type invariants is the ensure that no parts of
any composite object envolved are visibly exported [from any package]. [Well,
you also need to avoid exporting access-to-subprograms of operations in a
package that has type invariants; that's sort of covered by the first rule.]
This example violates that because the parts of Ext are visibly exported.

> It would seem that a Dynamic_Predicate also should be checked after
> updating a field via a view conversion, but we don't generally worry
> about predicates after component updates, so perhaps that is beside
> the point...

Definitely. I can't imagine why this case would be more important than any other
assignment to a component.

Anyway, I don't think it is worth trying to fix this one. Type invariants aren't
useful enough (they're surely a distant 4th in the existing kinds of contract
assertions) to bust our brains over this Bairdian hole. (Besides, didn't I raise
something like this when we originally talked about what became 7.3.2(20.1/3)? I
couldn't quite write the example, but it seemed obvious that it existed.)

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

From: Tucker Taft
Sent: Friday, May 29, 2015  8:58 PM

> ...
>> So probably a more general rule is needed that disallows updating
>> part of a class-wide object in a way that violates any invariants.
>> Alternatively, this would just be considered a "hole" in
>> Type_Invariants, not caught until some later point (if ever).
>
> I think it has to be a hole. I can't imagine what "updates in a way
> that violates any invariants" means in terms of a real, enforcable
> language rule
> -- it would have to embody the entirety of the existing invariant
> rules. And we have plenty of holes. ...

It might be roughly:

    Within the immediate scope of a type T to which a Type_Invariant applies,
    any update to an object of type T that is a part of a class-wide object is
    immediately followed by a check that the object still satisfies its
    Type_Invariant.

I agree it is not clear it is worth closing this hole.

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

From: Randy Brukardt
Sent: Friday, May 29, 2015  9:23 PM

Wouldn't that have nasty distributed overhead? As proposed here, it could happen
on any assignment of a class-wide object:

    procedure Foo (A : in out Something'Class; B : Something'Class) is
    begin
       if Glarch(A) then
          A := B; -- (1)
       end if;
    end Foo;

(1) might be an update of an object of type T that is part of A, if some
extension of Something has a component of type T. And that could be true for any
class-wide type (in the absence of bind-time analysis) occuring anywhere in the
immediate scope of T (which includes children, doesn't it?). For a
dyed-in-the-wool OOP programmer, that could be a lot.

Probably you don't really mean *any* update, because an assignment like (1)
isn't going to cause trouble (the T within B has to be OK, or have been checked
via this rule). But I don't know how to narrow that down without likely missing
cases.

> I agree it is not clear it is worth closing this hole.

Doing nothing (other than an AARM note??) is clearly the easier solution, both
on us and on implementers. I think I'm in favor of that, 'cause I don't see this
biting many people (and we already tolerate holes in the Type_Invariant
checking).

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

From: Tucker Taft
Sent: Saturday, May 30, 2015  6:59 AM

> (1) might be an update of an object of type T that is part of A, if
> some extension of Something has a component of type T. And that could
> be true for any class-wide type (in the absence of bind-time analysis)
> occuring anywhere in the immediate scope of T (which includes
> children, doesn't it?). For a dyed-in-the-wool OOP programmer, that could be a lot.

Right, the wording would have to make it clear that it is only if the object
visibly has a part of type T, and that part is being updated.

> Probably you don't really mean *any* update, because an assignment
> like (1) isn't going to cause trouble (the T within B has to be OK, or
> have been checked via this rule). But I don't know how to narrow that
> down without likely missing cases.

See above.  No need to worry about class-wide assignments per-se, since we are
presuming that all parts of a class-wide object already satisfy their
invariants.  So we probably want to say an update *other than* by an assignment
to a class-wide object.

>> I agree it is not clear it is worth closing this hole.
>
> Doing nothing (other than an AARM note??) is clearly the easier
> solution, both on us and on implementers. I think I'm in favor of
> that, 'cause I don't see this biting many people (and we already
> tolerate holes in the Type_Invariant checking).

We try to minimize the holes, of course, but I agree that if the wording or the
implementation is too nasty, then we should ignore it (SPARK folks don't really
have that option, but they are talking about static analysis, not run-time
overhead).

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



Questions? Ask the ACAA Technical Agent