Version 1.1 of ai12s/ai12-0289-1.txt

Unformatted version of ai12s/ai12-0289-1.txt version 1.1
Other versions for file ai12s/ai12-0289-1.txt

!standard 3.10(26)          18-08-06 AI12-0289-1/01
!class ramification 18-08-06
!status Amendment 1-2012 16-02-29
!status work item 18-08-06
!status received 18-08-03
!priority Low
!difficulty Easy
!subject Implicitly null excluding anonymous access types and conformance
!summary
Conformance strictly enforces whether or not a parameter is null excluding when it is declared, even through it might change later. In such cases, an explicit null exclusion is required.
!question
Consider:
package Pack is
type Priv is private;
procedure PPA (X : access Priv); -- (A)
private
type Priv is tagged record Int : Integer := 99; end record;
end Pack;
package body Pack is
procedure PPA (X : access Priv) is -- (B) begin null; end PPA;
end Pack;
The development version of our compiler rejects (A), saying that it does not fully conform to the specification (A).
This appears to be true for this code. The parameter X of (A) is not a controlling parameter, and thus it does not exclude null. On the other hand, the parameter X of (B) is a controlling parameter (since Priv is tagged here), and thus it does exclude null.
Full conformance requires the subtypes to statically match, and static matching here is defined by the third sentence of 4.9.1(2/5): "Two anonymous access-to-object subtypes statically match if their designated subtypes statically match, and either both or neither exclude null, and either both or neither are access-to-constant."
This is clearly False, and thus matching fails. Is this intended? (Yes.)
!response
The code given would be legal in Ada 95 (because there is no such thing as "exclude null" in Ada 95. However, it seems that allowing them to match brings up semantic issues.
The public specification of PPA (at (A)) clearly does not exclude null. Thus, a caller could reasonably try to pass null to it. However, the body clearly does exclude null, and thus may not expect to get null. (Note that this is true both for user-written code and the code generated by the compiler - compilers generally omit null checks for null excluding subtypes.)
We could also consider that there is an implicit null exclusion for the specification. However, this would be a privacy leakage, as a null excluding subtype would allow a rename like:
procedure Ren (X : not null access Pack.Priv) renames Pack.PPA;
...and there is nothing in the visible part which should allow this renames.
We could imagine having a double-secret null exclusion applying here that didn't affect renames Legality (but does affect conformance!), but that's getting crazy complicated for a unlikely case.
Ada requires full conformance so that a specification and the body are defining precisely the same thing -- that is clearly not the case here if we were to allow the declarations.
So we conclude that the incompatibility (which is easily fixed by adding "not null" to the declaration of parameter X) is the least of the possible evils. Explicitly requiring "not null" in this case is better for readers AND compilers, and is unlikely to cause many problems.
!wording
Add after AARM 3.10(26.f/2): [Incompatibilities with Ada 95]
Static matching (see 4.9.1) requires that both anonymous access types exclude null; and full conformance requires statically matching subtypes. Therefore, an access parameter that designates an untagged private type P (which does not exclude null) does not match its completion if P is completed with a tagged type (in that case, the parameter is controlling and thus excludes null, regardless of whether there is an explicit null exclusion on the body).
!discussion
Existing compilers seem to break privacy in this case, allowing the renames despite the fact that no null exclusion appears in the specification.
---
The incompatibility can be worked around by adding an explicit null exclusion to (A).
!ASIS
No ASIS effect.
!ACATS test
An ACATS B-Test should be created to check that the conformance check fails in examples like the one on the question. (Note that ACATS B413004.A did this in an unrelated test, but that's been eliminated.) A simple test is found in !appendix, and could be used.
!appendix

From: Randy Brukardt
Sent: Friday, August 3, 2018  6:12 PM

I'm tracking a regression problem in Janus/Ada, and it makes me wonder if 
there is a language problem. The example looks like:

package Pack is

    type Priv is private;

    procedure PPA (X : access Priv);

private

    type Priv is tagged record
        Int : Integer := 99;
    end record;

end Pack;

package body Pack is

    procedure PPA (X : access Priv) is
    begin
        null;
    end PPA;

end Pack;

The up-to-the-minute Janus/Ada compiler rejects the completion of PPA, saying
that the types of the parameter do not match (needed for full conformance).

I've tracked this down to a literal implementation of static matching. The 
specification of PPA does not have a controlling parameter, so the access 
type there does not exclude null. However, the body of PPA does have a 
controlling parameter, so the access type there does exclude null 
(implicitly). Since the third sentence of 4.9.1(2/5) is "Two anonymous 
access-to-object subtypes statically match if their designated subtypes 
statically match, and either both or neither exclude null, and either both or
neither are access-to-constant.", static matching has failed and thus the 
error. (Remember that every access_definition makes a new type, so these 
parameters are of different types and thus require matching rules.)

I figure to add some code to ignore implicit null exclusions when static 
matching (the above error being nonsense, of course). But that doesn't seem
to strictly follow the language definition.

Moreover, there seems to be a dynamic semantic issue associated with this.
The specification of PPA will not have a null exclusion, so it will allow 
passing null. But the body will not be expecting to get null. One cannot just
change the specification to be null excluding, because that would be a privacy
leakage -- specifically because it affects legality. Specifically:

      procedure Ren (X : not null access Pack.Priv) renames Pack.PPA;

is legal if "X : access Priv" is considered null excluding, and is not legal 
if it is not considered null excluding.

Similarly, if one just changes the body to not be null excluding, then the 
renames becomes illegal, and we have to deal with the possibility of 
dispatching on null (in the body and children of Pack).

One could imagine "fixing" this bizarreness by inventing a subtype that 
dynamically excludes null but doesn't "exclude null" for legality checks, then
using that in the specification of PPA. But (besides the substantial amount of
work involved, since it touches almost everything involving exclusions), I 
don't see any language reason for such a thing to exist (we require full 
conformance specifically so that the specs and bodies have the same properties
- that would seem to be broken here).

The only other thought that I had is that PPA maybe is never supposed to 
become a dispatching operation (although that would be different than the
behavior of virtually every other characteristic); in that case, there'd 
never be an (implicit) exclusion on X. But the wording in 3.9.2 seems to imply
otherwise (although it depends on when a "type is declared", which is not a 
single point!). And such an interpretation would make "tagged" almost 
irrelevant in such cases (almost nothing would dispatch).

Any ideas what the intent is here? I'm unsure even what I should be trying to 
implement in this case (and I wanted to ship a new compiler by today - 
obviously not making it).

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

From: Steve Baird
Sent: Friday, August 3, 2018  7:07 PM

> The specification of PPA will not have a null exclusion, so it will 
> allow passing null. But the body will not be expecting to get null.

That would indeed be a problem, so it is a good thing that your latest 
compiler is correctly rejecting this example.

Wouldn't this example be legal if the procedure declaration included an 
explicit null exclusion (even though the completion does not have an 
*explicit* null exclusion)?

If so, then it seems like all is well and there is no language problem.

An AARM note confirming that implicit null exclusions participate in 
conformance checking might be worthwhile.

If you don't like this resolution, then we could consider tightening up the 
conformance rule to require an explicit null exclusion for the procedure body
(as well as for the spec) in cases like this one. In order to conform, the 
spec and the body would have to agree in two different ways: the would have to
agree with respect to null exclusions and also with respect to *explicit* null
exclusions. We'd have to discuss the compatibility implications of this 
approach.

I think no change is needed, but there may be some implementation issue I am 
overlooking that would argue for the tighter conformance rule described above.

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

From: Randy Brukardt
Sent: Friday, August 3, 2018  9:00 PM

> > The specification of PPA will not have a null exclusion, so it will 
> > allow passing null. But the body will not be expecting to get null.
> 
> That would indeed be a problem, so it is a good thing that your latest 
> compiler is correctly rejecting this example.

Correctly? GNAT 18.1 allows this example, as it is in a relatively old ACATS
test. Probably so do any other Ada 2005 compilers (it is an Ada 2005 B-Test,
testing that untagged prefixed notation isn't allowed). No one has complained.

> Wouldn't this example be legal if the procedure declaration included 
> an explicit null exclusion (even though the completion does not have 
> an *explicit* null exclusion)?

Yes, that would be legal (at least as I read the RM).

> If so, then it seems like all is well and there is no language 
> problem.

There would be a potential compatibility problem with Ada 95 code, though, 
since there is no explicit null exclusion anywhere. So this is legal Ada 95
code, but we'd be rejecting it (of course, in Ada 95 anonymous parameters 
are always null excluding, so it doesn't have this issue).

> An AARM note confirming that implicit null exclusions participate in 
> conformance checking might be worthwhile.
> 
> If you don't like this resolution, then we could consider tightening 
> up the conformance rule to require an explicit null exclusion for the 
> procedure body (as well as for the
> spec) in cases like this one.
> In order to conform, the spec and the body would have to agree in two 
> different ways: the would have to agree with respect to null 
> exclusions and also with respect to
> *explicit* null exclusions. We'd have to discuss the compatibility 
> implications of this approach.

I'm worried about the compatibility implications of making the original
example illegal; how to fix it isn't a major concern.
 
> I think no change is needed, but there may be some implementation 
> issue I am overlooking that would argue for the tighter conformance 
> rule described above.

No, there's no problem if you argue that rejecting this test (and others 
like it) is OK. I was assuming that an 11 year old ACATS test is correct, 
especially when it clearly was legal in Ada 95.

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

From: Tucker Taft
Sent: Saturday, August 4, 2018  12:21 PM

Interesting problem!

I see various solutions:
1) Make it illegal in Ada 2005+ -- require explicit "not null" on visible 
   declaration.

2) Make it illegal in Ada 2005+ -- require explicit "not null" on both 
   visible and private declarations.

3) Make it legal, but with the semantics that the body may *not* assume the
   parameter is non-null, presuming that a call might come via the 
   non-dispatching visible declaration, so a call with a null parameter
   might actually succeed.

4) Make it legal, but with the semantics that a Constraint_Error is raised 
   if null is passed as an actual parameter, even in a call via the 
   non-dispatching visible declaration, so that a call with a null parameter
   will always raise an exception.

As far as renaming, (1) and (2) would clearly require "not null" (unless 
renaming as a dispatching operation).  (3) and (4) would not allow "not null"
if renaming the visible declaration, but would have the same dynamic semantics
as described.

---

I would probably recommend (1).  This avoids creating a new kind of 
conformance, which (2) would require, and just requires "honesty in 
advertising" which is generally a good thing.  The incompatibility is
easy to handle for the user -- just add "not null" on the visible routine.
Of course, in "Ada 95 mode" no changes are required. (3) and (4) just seem too 
confusing.

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

From: Steve Baird
Sent: Monday, August 6, 2018  11:10 AM

> I see various solutions:
...
> I would probably recommend (1).

That is also what I recommended in my earlier message.

I agree with Randy that compatibility is an issue here, but I agree with Tuck
about the set of alternatives that would be reasonable to consider and that #1
is the best of the bunch.

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

From: Randy Brukardt
Sent: Monday, August 6, 2018  5:52 PM

OK. I think there is a fairly strong argument that #1 is precisely what the 
language wording says. I had wondered if the Dewar rule about nonsense applied
here (because of the compatibility issue), but it sounds like the conclusion
is that the language is correct as written (even if no one other than me - by
accident - actually implemented it that way).

Therefore, I conclude that a Ramification AI is needed to confirm that the 
language says #1 and really means that (probably with a AARM Ramification note
somewhere, either 3.10, 4.9.1, or 6.3.1).

As far as the ACATS test goes, since it's not testing anything related to any 
of these clauses and it is an Ada 2005 test, I think the best plan is to put 
explicit "not null" on both the spec and the body. (Then it won't need 
modification regardless of what the result is.)

Someday, we'll need an ACATS test to test that compilers actually implement
#1, but that obviously can wait for the Ada 2020 test suite.

Any objections to this plan??

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

From: Randy Brukardt
Sent: Monday, August 6, 2018  8:26 PM

For the record, given the following program:

with Ada.Text_IO;
procedure TestUgh is
    -- Tests for GNAT interpretation of AI12-0289-1 problem.

    package Pack is

        type Priv is private;

        procedure PPA (X : access Priv); -- (A)

        procedure Ugh;

    private

        type Priv is tagged record
            Int : Integer := 99;
        end record;

    end Pack;

    package body Pack is

        procedure PPA (X : access Priv) is -- (B)

        begin
            null;
        end PPA;

        procedure Ren (X : not null access Pack.Priv) renames Pack.PPA; -- OK.

        type PAC is access all Priv'Class;

        procedure Ugh is
            V : PAC := null;
        begin
            PPA (V); -- Dispatching call!
        end Ugh;

    end Pack;

begin
    Ada.Text_IO.Put_Line ("--- TestUgh - Conformance of anonymous access types with implicit null exclusions.");

    begin
        Pack.PPA (null); -- Appears legal, what happens?
        Ada.Text_IO.Put_Line ("?? No exception raised when passing null.");
    exception
        when Constraint_Error =>
            Ada.Text_IO.Put_Line ("?? Contraint_Error raised when passing null");
    end;

    begin
        Pack.Ugh; -- Try to dispatch on null.
        Ada.Text_IO.Put_Line ("** No exception raised when dispatching on null.");
    exception
        when Constraint_Error =>
            Ada.Text_IO.Put_Line ("?? Contraint_Error raised when dispatching on null.");
    end;

    declare
       procedure Ren (X : not null access Pack.Priv) renames Pack.PPA; -- ERROR:
    begin
       null;
    end;

end TestUgh;

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

GNAT 18.1 compiles and gives:

--- TestUgh - Conformance of anonymous access types with implicit null exclusions
?? Contraint_Error raised when passing null 
?? Contraint_Error raised when dispatching on null

...which tells us that GNAT is essentially making the subtype null excluding 
(and thus is leaking privacy). [Alternatively, it might just be implementing 
the renames Legality Rules wrong.]

------

Janus/Ada 3.2.1 gives:

D:\Testing\Win\console>janus testugh.adb Janus/Ada [for Ada 95/07/12] - Version 3.2.0dev (Windows x86)
  Copyright (c) 1981 - 2003, 2007, 2010 - 2016, 2017 by R.R. Software, Inc.
    P.O. Box 1512, Madison WI  53701.  All Rights Reserved.
  Serial Number:  RRS1-0000
Input File Is D:\Testing\Win\console\testugh.adb
####
Strspace ptr - 3197 Usage - 1%
Hash Table - 327 buckets used, usage - 1% Parsing Completed - 66 lines found Pass II
5 strings loaded
Open Failed
%

In File D:\Testing\Win\console\testugh.adb at line 23
--------------
   22:
   23:          procedure PPA (X : access Priv) is -- (B)
-------------------------------^
*ERROR* Type does not match original specification (6.4.14) [RM 6.3.1(15)] Continue <Sp> or Abort <^C>?
%%

In File D:\Testing\Win\console\testugh.adb at line 35
--------------
   34:          begin
   35:              PPA (V); -- Dispatching call!
-------------------------^
*ERROR* Expression type must be specific (6.4.7) [RM 3.9.2(9)] Continue <Sp> or Abort <^C>?

In File D:\Testing\Win\console\testugh.adb at line 60
--------------
   59:      declare
   60:         procedure Ren (X : not null access Pack.Priv) renames Pack.PPA; -- ERROR:
--------------------------------------------------------------------------^
*ERROR* For parameter X
        Subtype must be null excluding (6.4.7) [RM07 8.5.4(4.3/2)] Continue <Sp> or Abort <^C>?

Compiler Table Usage:
                Current     Max.     Limit
Symbol Table  00034920H 00034920H 03274600H
Type Table                   153     20000
Procedure Table              257     32000
Parse Stack          3        19       200
Compiler aborted due to Pass II errors

...that is, rejecting both the conformance and the (public) renames. It also 
seems to have decided that PPA is not dispatching (which makes allowing the 
body renames incorrect). Sigh.

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

From: Randy Brukardt
Sent: Monday, August 6, 2018  8:32 PM

...
>         when Constraint_Error =>
>             Ada.Text_IO.Put_Line ("?? Contraint_Error raised when 
> passing null");
 
Please, no comments on my spelling capabilities. :-)
 
...
> Janus/Ada 3.2.1 gives:
> 
> D:\Testing\Win\console>janus testugh.adb Janus/Ada [for Ada 95/07/12] 
> - Version 3.2.0dev (Windows x86)
 
I haven't changed the version number on the compiler yet -- but it will be 
3.2.1 tomorrow. Really. :-)
 
****************************************************************

From: Tucker Taft
Sent: Monday, August 6, 2018  9:17 PM

> ...
> As far as the ACATS test goes, since it's not testing anything related 
> to any of these clauses and it is an Ada 2005 test, I think the best 
> plan is to put explicit "not null" on both the spec and the body. 
> (Then it won't need modification regardless of what the result is.)
> 
> Someday, we'll need an ACATS test to test that compilers actually 
> implement #1, but that obviously can wait for the Ada 2020 test suite.
> 
> Any objections to this plan??

Looks good to me.

****************************************************************
 
From: Jeff Cousins
Sent: Tuesday, August 7, 2018  4:24 PM

Sounds like a plan to me.

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

Questions? Ask the ACAA Technical Agent