AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63 stars 28 forks source link

[RFC]: Simpler accessibility rules #47

Closed yannickmoy closed 1 year ago

yannickmoy commented 4 years ago

Full text here: https://github.com/yannickmoy/ada-spark-rfcs/blob/accessibility/considered/rfc-simpler-accessibility.md

clairedross commented 3 years ago

It is not clear to me what the new accessibility rules would imply for the return statement of a function with a result of an anonymous access type. It would be nice to have some examples. Would the following be allowed for example: function Id (X : T_Ptr) return access T is begin return X; end Id;

AdaDoom3 commented 3 years ago

Claire, the answer as to whether the function you describe is legal is "it depends".

As the document states, anonymous access function result types have the same accessibility level of their designated type and so they are equivalent to declaring a named access type at the point of the designated type's declaration.

As in:

type T is ...; type T_Anon_Types is access all T;

So, your example would be equivalent to:

type T is ...; type T_Anon_Types is access all T; type T_Ptr is access all T;

function Id (X : T_Ptr) return T_Anon_Types is begin return X; end;

..and this would be 100% legal. However, imagine T_Ptr would be declared in a more nested scope as in:

type T is ...; type T_Anon_Types is access all T;

procedure Outter is type T_Ptr is access all T;

function Id (X : T_Ptr) return access T is begin return X; end; begin ... end;

This second example would be illegal.

clairedross commented 2 years ago

On Thu, Sep 23, 2021 at 7:06 AM yannickmoy @.***> wrote:

@.**** commented on this pull request.

In considered/rfc-simpler-accessibility.md https://github.com/AdaCore/ada-spark-rfcs/pull/47#discussion_r714473875:

+ +For example: + +```ada +declare

  • type T is record
  • Comp : aliased Integer;
  • end record;
  • function Identity (Param : access Integer) return access Integer is
  • begin
  • return Param; -- Legal
  • end;
  • X : access Integer; +begin
  • X := Identity (X); -- Illegal
  • X := Identity (X).all'Unchecked_Access; -- Legal

Can you explain how the call to Identity could return a pointer to data whose lifetime is shorter than the smallest enclosing declaration block? I understand how the wording forces Unchecked_Access here, but I don't understand what problems it avoids.

I think the issue would be with a parameter which is local to the call, like: X := Identity (Create_T'Access); Is that it? If it is so, maybe we could have some rule stating that if the access parameters are parts of an object, then we don't need this check, or is it too complicated? -- Claire Dross Senior Software Engineer, AdaCore

swbaird commented 2 years ago

Yannick wrote:

yes, I think we should prevent that by some other rule, so that you can only pass in an actual for an anonymous constant formal if the actual has a lifetime at least as long as the current scope.

As Claire pointed out, the issue I identified in a very contrived example using an aggregate can also occur in a slightly more plausible use-case involving a function call.

I agree that we could allow the example you asked about if we are willing to impose these sorts of restrictions on callers. If a formal parameter of a function is of an anonymous access type, the result type of meets the "any part" condition of RM 6.5(21), and typing information alone does not (somehow) rule out the possibility of a value of the function result type containing an anonymous-access-type reference to some part of the formal parameter's designated object (at least we don't have to deal with coextensions here), then we could require that the actual parameter must meet a "no newly constructed stuff" restriction similar to that of 4.5.9(6) (although limitation would not be a factor here).

Do you want to explore this further?

-- Steve

On Fri, Sep 24, 2021 at 1:07 AM Claire Dross @.***> wrote:

On Thu, Sep 23, 2021 at 7:06 AM yannickmoy @.***> wrote:

@.**** commented on this pull request.

In considered/rfc-simpler-accessibility.md <https://github.com/AdaCore/ada-spark-rfcs/pull/47#discussion_r714473875 :

+ +For example: + +```ada +declare

  • type T is record
  • Comp : aliased Integer;
  • end record;
  • function Identity (Param : access Integer) return access Integer is
  • begin
  • return Param; -- Legal
  • end;
  • X : access Integer; +begin
  • X := Identity (X); -- Illegal
  • X := Identity (X).all'Unchecked_Access; -- Legal

Can you explain how the call to Identity could return a pointer to data whose lifetime is shorter than the smallest enclosing declaration block? I understand how the wording forces Unchecked_Access here, but I don't understand what problems it avoids.

I think the issue would be with a parameter which is local to the call, like: X := Identity (Create_T'Access); Is that it? If it is so, maybe we could have some rule stating that if the access parameters are parts of an object, then we don't need this check, or is it too complicated?

Claire Dross Senior Software Engineer, AdaCore

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/47#issuecomment-926431569, or unsubscribe https://github.com/notifications/unsubscribe-auth/AMDGMTEIXSYB3EMMEQP6UN3UDQWTRANCNFSM4OAZGKVA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

yannickmoy commented 2 years ago

@swbaird yes please! I think it's worth it, to avoid systematic use of Unchecked_Access in otherwise perfectly safe SPARK code in particular.

AdaDoom3 commented 2 years ago

@yannickmoy Ok Yannick, we will explore additional restrictions mentioned by @swbaird above