AI22-0076-2/04

AI22-0076-2

!standard H.4(10) 26-04-17 AI22-0076-2/04

!class Amendment 23-06-05

!status work item 23-06-05

!status received 23-06-05

!assigned author Steve Baird and Tucker Taft

!submitter Tucker Taft

!priority High

!difficulty Hard

!subject No_Dynamic_Accessibility_Checks restriction

!summary

A new restriction, No_Dynamic_Accessibility_Checks, is defined which uses more conservative compile-time accessibility checking to ensure that language-defined dynamic accessibility checks associated with access types are guaranteed to pass.

!issue

Dynamic accessibility checks are difficult to reason about and check failures can be unexpected. Program reliability could be improved in some cases if these checks could be replaced with compile-time checks, even if these new checks would have to be more restrictive in some cases.^[a]^[b]^[c]^[d]^[e]^[f]^[g]^[h]

!recommendation

Define a new restriction, No_Dynamic_Accessibility_Checks, which eliminates the need for dynamic accessibility checking associated with access types by means of more conservative compile-time checks.

!wording

Add after H.4(8.3/3):

No_Dynamic_Accessibility_Checks

[Redundant: This restriction ensures statically that dynamic accessibility checks associated with access types will pass. This is accomplished by redefining the accessibility level of certain entities more conservatively. As a result, certain constructs that would otherwise have been legal (but might require a dynamic accessibility check) will instead fail compile-time accessibility (legality) checks. The dynamic semantics of a program which remains legal when this restriction is in effect are unchanged by the presence or absence of the restriction.]

A No_Dynamic_Accessibility_Checks restriction imposes the following requirements:

A No_Anonymous_Allocators restriction shall be in effect.

For a membership test where the tested type is a general access-to-object type, the accessibility level of the access type shall be the same as or statically deeper than the accessibility level of the type of the tested_simple_expression.

AARM note: This disallows the case where the result of a membership test depends on a dynamic accessibility test. Without this rule, the accessibility level redefinitions associated with this restriction could change the outcome of a membership test (at runtime).

A type having an access discriminant with a default value shall not be used as a component type in the declaration of a composite type.

If a type has an nondiscriminated partial view, then the full view of that type shall not have an access discriminant with a default value.

A type having an access discriminant with a default value shall not be passed as an actual parameter in an instantiation if the corresponding formal type lacks discriminants.

The "statically deeper" relationship does apply to the accessibility level of the type of a stand-alone object of an anonymous access type. The accessibility level of such an access type depends on whether the object's declaration includes an explicit initial value expression having at least one operative constituent which is neither a null literal nor a call on a function having an access result type. If it does then the level of the anonymous access type is the deepest of the levels of the types of those operative constituents. Otherwise, the level of the anonymous access type is that of the object.

The accessibility level of an anonymous access type of a formal parameter of a subprogram (or of a protected entry), as seen from within that callable entity, is defined to be statically deeper than the level of the callable entity, but not statically deeper than the level of the parameter itself, unless the subprogram is a function with an anonymous access result type.

If the function has an access result, the accessibility level of the type of the access parameter is considered to be the same level as that of a (notional) explicitly aliased formal parameter of the function. In the context of a return statement, it is subject to the same accessibility rules as for returning an Access attribute reference whose prefix is a part of an explicitly aliased formal parameter of the function in question.

When calling such a function, the accessibility level of the type of the actual parameter shall not be statically deeper than that of the master of the call (see 3.10.2).

AARM Discussion:

This implies that the following example is legal:
function Identity (X : access T) return access T is (X);

In the case of a call to a function with an anonymous access result type, the accessibility level of the function shall not be statically deeper than that of the master of the call.

If the accessibility level of a tagged type is statically deeper than that of its parent type, or of a progenitor, then no primitive operation inherited from that parent or progenitor (whether overridden or not) shall have an anonymous access type as either a formal parameter type or as a function result type.

A function is said to depend on the master of the call if the result type of the function is an anonymous access type, a type that has one or more access discriminants, a class-wide type, or a type with unknown discriminants. For a call to a function which depends on the master of the call, the level of the master of the call shall be the same as or statically deeper than that of the called function. For a return statement returning from such a function, the level of the master of the call is considered (for purposes of legality checks associated with the return statement) to be that of the function.

A No_Dynamic_Accessibility_Checking restriction may be specified with an

optional Restriction_Parameter_Argument which, if present, shall be either

the identifier Global or the identifier Local. If omitted, the implicit

default value for this argument is Local. If Local is specified (explicitly

or implicitly), then the restriction applies only to the current compilation

or environment, not to the entire partition. If Global is specified, then the

restriction applies to the entire partition.

If the restriction applies to the entire partition, then the associated

post-compilation check (see 13.12) may treat any compilation unit that

was not compiled with the partition-wide form of the restriction in effect

(excluding predefined units) as a violation.

!discussion

To illustrate the general idea, consider the following example:

type Ref is access all Integer;
Ptr : Ref;

procedure Proc (Param : access Integer) is
begin
Ptr := Ref (Param);
end Proc;

If no restrictions are in effect, this example is legal. Evaluation of the type conversion includes the dynamic accessibility check described in RM 4.6(48); that check might fail (depending on the caller). But if the No_Dynamic_Accessibility_Checks restriction is in effect, then the type conversion is instead rejected at compile time. One of the effects of the restriction is that the accessibility level of the anonymous access type of a formal parameter of a subprogram is defined to be statically deeper than the level of the subprogram. With this change, the previously-legal example now violates the compile-time check of RM 4.6(24.17).

This is one example of the general approach of imposing a more conservative definition of the accessibility level of some entity in order to ensure statically that a related dynamic accessibility check cannot possibly fail. Note that no new legality rules are introduced here - instead, existing legality rules are enforced more conservatively.

This new restriction is unrelated to the "dangling tag" dynamic accessibility check of RM 6.5(8/5) for a function with a class-wide result type (and the similar check for allocators, RM 4.8(10.1/6)). The exclusion of “dangling tag” checks is what is implied when we talk about accessibility checks "for access types" or "associated with access types". This should not be interpreted to mean that providing a way to replace dynamic “dangling tag” checks with (appropriately conservative) static legality checks is undesirable or unimportant^[i]; only that such a language change is outside of the scope of this AI.

Do we really want the special rules needed to allow

function Identity (Param : access T) return access T is (X);

? If we don't mind rejecting this function, then we can simplify the rules about access parameters (both for the caller and the callee) in the case of a function with an anonymous access result type. It might make sense to get feedback from SPARK implementers regarding this point.

To see the need for the rule about membership tests, consider the following example. If the membership test in function In_Int_Ref were legal with the restriction in effect (it isn't), then the restriction could cause the first assertion to fail at runtime (which would be a change in the runtime behavior).

procedure Main_Proc is
pragma Assertion_Policy (Check);

Int1 : aliased Integer;
type Int_Ref is access Integer;

function In_Int_Ref (X : access Integer) return Boolean is
(X in Int_Ref);

procedure Test
Int2 : aliased Integer;
pragma Assert (In_Int_Ref (Int1'Access));
pragma Assert (not In_Int_Ref (Int2'Access));
begin null; end;

begin
Test;
end Main_Proc;

This change in behavior (i.e., the failure at runtime of the first Assert pragma) would be a consequence of the way that the restriction changes the accessibility level of In_Int_Ref.X.

The 3 rules about default values for access discriminants are intended to disallow the case of an unconstrained component subtype that has one or more access discriminants. This significantly simplifies the treatment of return statements by eliminating the need to consider the accessibility levels of access discriminants of components of the value being returned. A single simpler rule forbidding default expressions for access discriminants was considered, but was viewed as being unnecessarily restrictive. To illustrate why allowing such component subtypes would cause problems, consider the following example:

with Text_IO;
procedure Accessibility_Test is

type Drec (Disc : access Integer := null) is limited null record;
type Vec is array (Positive range <>) of Drec;

function Foo return Vec is
Local_To_Foo : aliased Integer := 12345;
function Nested return Vec is
begin
return (1 .. 49 | 51 .. 123 => (Disc => null),
50 => (Disc => Local_To_Foo'Access));
end Nested;
OK : Vec := Nested; -- accessibility check inside Nested should pass
begin
return Nested^[j]; -- accessibility check inside Nested should fail
end Foo;

Attempted_Dangler : Vec := Foo;
begin
Text_IO.Put_Line (Attempted_Dangler (50).Disc.all'Image);
-– we should not get here
end Accessibility_Test;

The comments in the code about whether a dynamic check should pass or fail refer to the case where the restriction is not in effect. If the restriction is in effect, then the declaration of type Vec is (fortunately) illegal.

This new restriction may be defined to be partition-wide.^[k] In this case, a conservative rule is defined in order to avoid having to detect violations of the restriction via a post-compilation check in the case where the restriction was not in effect when a violation was compiled.

The definition of this new restriction is similar to, but not identical to, that of the GNAT-defined restriction of the same name.

!example

** TBD **.

!ACATS test

An ACATS B-test using the restriction should be constructed. It should use constructs that are legal without the restriction, but which are illegal when the restriction is in effect.

!appendix

[This is based on the RFC from https://github.com/AdaCore/ada-spark-rfcs/blob/master/prototyped/rfc-simpler-accessibility.md?plain=1]

[a]This seems to suggest that code performance is not a goal here. Is that true? I ask because I personally am more worried about the substantial performance hit from the implementation model of AI22-0034-2. I thought this restriction was intended to address that, and I would expect others to feel the same.

[b]Did you really mean AI22-0016-1, or perhaps did you mean AI22-0017-1, which is about long-lived temporaries?

[c]In any case, I don't think we focused on implementation overhead. I had always presumed that eliminating the various run-time accessibility checks would almost certainly reduce run-time overhead. Also, there is the modest savings from not having to pass an accessibility level along with an access parameter.

Can you clarify our concerns?

[d]AI22-0034-2, sorry. Corrected it above.

[e](1) I would like a statement somewhere that this is not intended to allow eliminating the systematic overhead of AI22-0034-2 (although it might help in that regard when combined with other restrictions) [I'll update my suggestion accordingly];

(2) If this is intended mostly to improve safety, the making it partition-wide is a major detriment, because it means that I can't use it in something like Claw (I can't impose restrictions on the clients)

[f]If we look at what AI22-0034-2 implies when the *only* dynamic checks are for nested extensions, then it indicates we only need to create level objects in scopes where a nested extension is declared. That doesn't seem like a lot of overhead, especially compared with the overhead of declaring a nested extension.

Admittedly the check might involve following a linked list, but given the various optimizations such as having all unnested extensions have a "null" in their pointer to their level object, in very many cases you will reach the end of the linked-list walk immediately, or in just one step. You will need to have a thread-local pointer to the "current" level object for each task, but that will in many cases also be null.

So although the primary goal was to improve safety, it seems likely that it would also remove overhead from implementations using level objects, simply because there will be so few of them if their only purpose is for nested-extension checks.

[g]I don't completely buy this, a lot of the overhead is necessary because the mechanism exists at all. For instance, a dynamic accessibility check cannot be done at the point of the check, it has to call some sort of subprogram (since there is too much code to stick at the point of a check). And I believe that you need overhead in at least every task in order to be able to track the relationships between the tasks. And of course the substantial burden on the implementation is the same even if no one ever writes a program with a nested extension. Moreover, given that the restriction is partition-wide, a lot of code won't be able to use it (if any piece of code is incompatible, it can't be used), so it won't help many large systems.

[h]Another option I see is to go with your suggestion of allowing this restriction on a subset of the program, but then *not* require that the dynamic checks be removed, simply require that the specified static checks be added. It would then be an optimization to remove the dynamic checks when the compiler can be sure they are not needed. From my perspective, this would address my concern about potential complexity of calls between restricted and non-restricted portions of the program. Clearly if the restriction is imposed partition-wide, then the optimization becomes easier, and the compiler could go further and avoid passing around accessibility levels, etc. But that would all be considered an optimization, rather than a requirement of the restriction.

Given this, I might suggest we change the name of the restriction to "Static_Accessibility_Checks" to emphasize the effect is to add static checks, without any guarantee that we are removing dynamic checks.

[i]Its actually impossible without eliminating the reason one uses tagged types in the first place (inheritance and dispatching). The only possible fix is a restriction No_Nested_Extensions (although I think we could exclude direct extensions of Controlled and Limited_Controlled from such a restriction). Details on request (but they belong in the separate AI).

[j]Would return OK; also fail?

[k]Partition-wide restrictions should only be used if there is a system-wide overhead to be eliminated (as in No_Allocators) or if there are substantial semantic problems with mixed environments. Applying them otherwise is lazy and prevents reuse as most reusable code and third-party libraries won't have the restriction (and any that do will not be usable with systems that don't use the restriction).