Version 1.1 of acs/ac-00294.txt

!topic Preconditions for accessibility of function results
!reference Ada 2012 RM6.1.1
!from Simon Belmont 17-08-03
!keywords precondition access discriminant function
!discussion

ARG,

Functions returning record types containing access discriminants are 
subject to runtime accessibility checks (6.5~21/3), however for private 
types and pass-by-reference arguments (which have been expanded with Ada 
2012's explicitly aliased parameters and in/out functions), this check 
is often not apparent to clients (except through comments). Ada 2012 
also includes membership tests for accessibility, which can be used as 
preconditions to solve the identical problem concerning type conversions 
of access parameters, however it is impossible to specify similar 
preconditions on functions returning types with access discriminants.

A similar feature would provide similar benefits, that is, "improving 
facilities for program correctness by communicating the contract to the 
user", but also provide enhanced compiler warnings, potential 
elimination of runtime checks, possible use in future proofing software, 
et al.

For example:

package P is

   type T (<>) is private;
   function F (i : aliased in out Integer) return T;

private
   type T (ip : access Integer) is null record;
end P;

package body P is

   function F (i : aliased in out Integer) return T is
   begin
     return T'(ip => i'Access); -- runtime check
   end F;

end P;

In this case, clients using P have no visibility that a runtime check 
will occur within F, or even that the type contains a discriminant at 
all.  Consequently, if the client tries creates an object of type T that 
outlives the parameter i, the user would be surprised by runtime check 
failing, as in:

declare
   type T_Ptr is access P.T;
   tp : T_Ptr;
begin
   declare
     dangly : aliased Integer := 42;
   begin
     tp := new T'(P.F(dangly));  --runtime check failure
   end;
   -- tp.all.ip would be a dangling pointer
end;

It would be beneficial to explicitly state this requirement as a 
precondition of F; that is, conceptually, "The lifetime of argument i 
must not be less than the lifetime of the result of F".

Perhaps something along the lines of "with Pre => i in F'Result", with 
the understanding that use of 'Result in a precondition of a function 
refers to accessibility of the master of the call, or similar.

Thank you for your consideration.

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

From: Randy Brukardt
Sent: Wednesday, September 6, 2017  10:23 PM

...
> For example:
> 
> package P is
> 
>    type T (<>) is private;
>    function F (i : aliased in out Integer) return T;
> 
> private
>    type T (ip : access Integer) is null record; end P;
> 
> package body P is
> 
>    function F (i : aliased in out Integer) return T is
>    begin
>      return T'(ip => i'Access); -- runtime check
>    end F;
> 
> end P;
> 
> In this case, clients using P have no visibility that a runtime check 
> will occur within F, or even that the type contains a discriminant at 
> all.  Consequently, if the client tries creates an object of type T 
> that outlives the parameter i, the user would be surprised by runtime 
> check failing, as in:

Actually, in this exact example, there is no runtime check on the return type.
An aliased parameter is always guaranteed to live long enough to be returned
this way (or to return a portion of it, as in the containers, or to return as
an anonymous access return, which has to the same accessibility rules). If
there is a runtime check coming from this return statement, there is a bug
either in the compiler or in the language, and in either case that should be
fixed.

To get a true runtime check here, you have to have passed and returned an
access type -- but then you can use the existing accessibility membership
to write the precondition.

> declare
>    type T_Ptr is access P.T;
>    tp : T_Ptr;
> begin
>    declare
>      dangly : aliased Integer := 42;
>    begin
>      tp := new T'(P.F(dangly));  --runtime check failure
>    end;
>    -- tp.all.ip would be a dangling pointer end;

There is a runtime check that fails here, but it is on the parameter passing
of the aliased parameter. An aliased parameter always is required to have the
same or longer life than the function result that it is a parameter to.
This happens whether or not the return object contains an access
discriminant!!

For instance, you'll get the same accessibility check failure if you had
written the example as:

    function Foo (i : aliased in out Integer) return Integer is
    begin
      return i; -- Return the value of i.
    end Foo;
 
 declare
    type I_Ptr is access Integer;
    ti : I_Ptr;
    OK : aliased Integer := 12;
 begin
    declare
      dangly : aliased Integer := 42;
    begin
      ti := new Integer'(Foo(dangly));  -- Raises Program_Error
    end;
    ti := new Integer'(Foo(OK)); -- OK.
 end;

The assumption is that part of an aliased parameter is returned from the
function, and the checks made flow from that. (Note that there aren't any
checks on aliased parameters passed to procedures or entries; it's just
functions that have this fun.)

Anyway, my point is that the inclusion of "aliased" in the function
specification is what is triggering the runtime check, and that the check
will happen is "obvious" to someone who understands the model of aliased
parameters. So there's no more reason to mention that in the precondition
than there is to test a null-excluding parameter for null in a precondition.

Now, I realize that the number of people that understand the accessibility of
aliased parameters is probably just me and Tucker, and I'm not sure about
Tucker. ;-) OTOH, this check is very rare -- in 99% of the cases, the check
is made at compile-time (and in fact cannot fail). The allocator case above
was the primary reason that the check was defined in the first place. (I
believe that there are a couple of other obscure cases where it could trigger
-- one is a direct type conversion of an anonymous access return to a
library-level type. See AI12-0095-1 for a bit of discussion on this topic;
venture into the Heart of Darkness if you want the actual details.)

My point here is that one has to work rather hard to have this happen; hardly
anyone will see it in practice. And it's clearly declared in the function
specification that this will happen -- that's better than in the precondition
as it is language-defined. So there doesn't seem to be any need to specify
this in the precondition.

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

From: Randy Brukardt
Sent: Wednesday, September 6, 2017  10:41 PM

Additionally: 

> declare
>    type T_Ptr is access P.T;
>    tp : T_Ptr;
> begin
>    declare
>      dangly : aliased Integer := 42;
>    begin
>      tp := new T'(P.F(dangly));  --runtime check failure
>    end;
>    -- tp.all.ip would be a dangling pointer end;

This call (and the Integer one in my message) is supposed to be illegal, as
the aliased parameter accessibility check statically fails. (6.4.1(6.4/3) -
dangly is statically deeper than the master of the call (T_Ptr's master)
here).

The only time that a runtime check could fail for such a call is if the
allocator is in a generic body and the type is outside of the instance (and
even then, a compiler like GNAT ought to give a warning, Janus/Ada would have
to give a runtime failure).

My point being that it would be very unlikely to encounter a case in practice
where the check might fail and the code is still legal. (There aren't ACATS
tests for the dynamic checks on aliased parameters for this reason.)

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