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

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

!standard 7.3.2(10/3)          13-05-08 AI12-0049-1/03
!class binding interpretation 12-12-03
!status Amendment 202x 12-12-27
!status ARG Approved 9-0-1 12-12-07
!status work item 12-12-03
!status received 12-09-10
!priority Medium
!difficulty Easy
!subject Invariants need to be checked on the initialization of deferred constants
!summary
Invariants are checked on the initialization of deferred constants.
!question
Consider:
package R is type T is private with Type_Invariant => Non_Null (T); function Non_Null (X : T) return Boolean; Zero : constant T; private type T is new Integer; function Non_Null (X : T) return Boolean is (X /= 0); Zero : constant T := 0; end R;
Zero violates the invariant, but this will not be detected because there is no rule in the Standard that says this should be checked.
Should this be fixed? (Yes.)
!recommendation
(See summary.)
!wording
Add after RM 7.3.2(10/3):
After successful explicit initialization of the completion of a deferred constant with a part of type T, if the completion is inside the immediate scope of the full view of T, and the deferred constant is visible outside the immediate scope of T, the check is performed on the part(s) of type T;
!discussion
We want every value that can "escape" from the visible part of the package to have the invariant checked. There certainly shouldn't be any easy end runs around the checking.
This wording seems more complicated than necessary, but a number of considerations arise.
First, we have to talk about "the completion of a deferred constant" as the deferred constant itself has no initializer (and thus nothing to check).
Second, we have to check more than just deferred constants of type T. Deferred constants can be of any type, and thus T could have been used as a component:
package R2 is type T is private with Type_Invariant => Non_Null (T); function Non_Null (X : T) return Boolean; type Conditional_T is record Valid : Boolean; Data : T; end record; Invalid : constant Conditional_T; private type T is new Integer; function Non_Null (X : T) return Boolean is (X /= 0); Invalid : constant Conditional_T := (Valid => False, Data => 0); end R2;
This has the same leak as the original example. Thus, we have to talk about "a part of type T".
Third, we have to also make the check in visible child packages. Consider this child of the original example:
package R.C is Zero : constant T; private Zero : constant T := 0; end R.C;
This also has the same hole as in the original example. The wording here talks about "immediate scope", so that the check does not apply to private child packages (which cannot leak values out of the "subsystem").
!corrigendum 7.3.2(10/3)
Insert after the paragraph:
the new paragraph:
!ACATS test
An ACATS C-Test should be created to test that the invariant check fails in the example from the !question.
!appendix

From: Tucker Taft
Sent: Monday, September 10, 2012  10:14 AM

One of our engineers just came up with a way to bypass type invariants.
This clearly violates the "Dewar" reasonableness rule, and so some sort of RM
fix is needed.  Initializing a visible deferred constant should probably be
treated like returning a value from a visible parameterless function for the
purposes of invariant checks.


> I just discovered a way to bypass a type invariant by declaring a
> public deferred constant initialized with a value that violates the type invariant:
>
> --
> package R is
> type T is private with Type_Invariant => Non_Null (T); function
> Non_Null (X : T) return Boolean; Zero : constant T; private type T is
> new Integer; function Non_Null (X : T) return Boolean is (X /= 0);
> Zero : constant T := 0; end R;
>
> with R; use R;
> procedure Main is
> X : T := Zero;
> begin
> null;
> end Main;
> --
>
> The code above compiled with assertions executes without any error:
>
> $ gnatmake -gnat12 -gnata main.adb
> $ ./main
> <no error>
>
> This is as designed in Ada 2012 RM, although a bit surprising.
> I just wanted to share the info with other people interested.

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

From: Erhard Ploedereder
Sent: Tuesday, September 11, 2012  1:00 PM

> Initializing a visible deferred constant should probably be treated
> like returning a value from a visible parameterless function for the
> purposes of invariant checks.

Indeed.

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

From: Randy Brukardt
Sent: Saturday, December 1, 2012  5:37 PM

...
> package R is
>    type T is private with Type_Invariant => Non_Null (T);
>    function Non_Null (X : T) return Boolean;
>    Zero : constant T;
> private
>    type T is new Integer;
>    function Non_Null (X : T) return Boolean is (X /= 0);
>    Zero : constant T := 0;
> end R;

Followed by some code showing that GNAT does not make an invariant check in
Zero.

I was just going to write up this up as an AI, when after trying to figure out
what wording needed to be changed, I don't think there is any problem with the
Standard (GNAT, not so much ;-).

The rules in question are 7.3.2(9-10/3):

If one or more invariant expressions apply to a type T, then an invariant check
is performed at the following places, on the specified object(s):

* After successful default initialization of an object of type T, the check is
  performed on the new object;

(It's nice that the example uses T as the type name, no translation is needed.
:-)

This says that an invariant check is performed on Zero at the point where its
default initialization is evaluated. This is in the private part of the package,
but there is no wording in the above to restrict this check only to visible
parts! (Other checks do have such wording.) So the check should be performed on
Zero; there surely is no language hole.

If there *is* a problem, it's that this wording implies that the check ought to
be made on all objects, regardless of where they are declared. That means that
objects declared in the package body also get such a check, which probably isn't
intended (think temporaries used to create objects - one would hope that they
could violate the invariant while being constructed).

So maybe we *do* need an AI, but it is exactly the reverse of what is implied by
the original question.

What do the rest of you think?? If we need a change, what should the wording
be??

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

From: Tucker Taft
Sent: Saturday, December 1, 2012  6:04 PM

But Zero is not "default initialized," it is "explicitly initialized."
See RM 3.3.1(18/2) for definition of "default initialization."
Zero doesn't qualify.

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

From: Randy Brukardt
Sent: Saturday, December 1, 2012  6:35 PM

OK, now I'm officially confused. Where is the rule that an object has its
invariant checked after it is (explicitly) initialized? We surely don't want to
be creating objects without checking the invariant (other that in the body of
the package). How is that prevented?

Could you propose wording to fix the problem (whatever it is)? I am way, way
behind on AI creation and it is unlikely I will get back to this one before the
meeting.

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

From: Tucker Taft
Sent: Saturday, December 1, 2012  7:13 PM

> OK, now I'm officially confused. Where is the rule that an object has
> its invariant checked after it is (explicitly) initialized? We surely
> don't want to be creating objects without checking the invariant
> (other that in the body of the package). How is that prevented?

Outside of the package, a private type can only be initialized from another
existing value of the private type, so there is no need for another
type-invariant check, unless it is controlled.  If it is controlled, then an
invariant check will be performed upon return from the Adjust procedure, since
the mode is in-out.

> Could you propose wording to fix the problem (whatever it is)? I am
> way, way behind on AI creation and it is unlikely I will get back to
> this one before the meeting.

How about:

Modify RM 7.3.2(10/3):

   After successful default initialization of an object of type T{, or explicit
   initialization of a deferred constant of type T}, the check is performed on
   the new object;

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

From: Randy Brukardt
Sent: Tuesday, December 4, 2012  12:28 AM

Well, I did manage to get back to this one. Unfortunately, the above doesn't
work, because 7.4(2/3) defines a "deferred constant" thusly: A deferred constant
declaration is an object_declaration with the reserved word constant but no
initialization expression. The constant declared by a deferred constant
declaration is called a deferred constant.

I'm pretty sure that Adam or Steve or both will be happy to tell us that the
above change has no effect at all, as there cannot be an explicit initialization
of a declaration with no initialization expression. So no check would ever be
required.

I think we have to talk about the completion somehow ("or explicit
initialization of the completion of a deferred constant of type T").

But this *still* isn't enough. Let's move somewhat in the Bairdian territory,
and consider a small expansion of the original example:

package R is
   type T is private with Type_Invariant => Non_Null (T);
   function Non_Null (X : T) return Boolean;
   type Conditional_T is record
       Valid : Boolean;
       Data  : T;
   end record;
   Invalid : constant Conditional_T;
private
   type T is new Integer;
   function Non_Null (X : T) return Boolean is (X /= 0);
   Invalid : constant Conditional_T := (Valid => False, Data => 0);
end R;

Invalid has a component of type T, but it isn't a "deferred constant of type T".
So the component isn't checked and we still have the hole.

So we need to work "part" into the added wording somehow. I tried that a bit,
and didn't find a reasonable way to add it. Gack!

I'll leave it for the meeting unless some wonderful suggestion is in my inbox
tomorrow morning...

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

From: Tucker Taft
Sent: Wednesday, December 5, 2012  8:47 PM

Probably just need a new bullet:

    * After successful explicit initialization of the completion of a
      deferred constant with a part of type T, occurring immediately
      within immediate scope of the full view of type T, the check is
      performed on the part(s) of type T;

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

Questions? Ask the ACAA Technical Agent