AI22-0051-2/03

We add requirements to the two contract checks that can be associated with a type with preelaborable initialization, so that these contracts can be used in preelaborable units.

!issue

A Default_Initial_Condition (D_I_C) expression is evaluated when a default-initialized object is created. The aspect Preelaborable_Initialization (P_I) does not take into account any such evaluation when it determines whether a component has P_I. That means that such an evaluation could execute operations not otherwise allowed during the elaboration of a preelaborated package (in particular, calling a function other than the few allowed for preelaboration). This seems to circumvent the purpose of aspect P_I.

!recommendation

We allow evaluation of aspects Type_Invariant and Default_Initial_Condition that are associated with a type that has aspect Preelaborable_Initialization specified true, even though the expressions would not normally be considered preelaborable, in order that the expectations of P_I are preserved.

In order to preserve the invariant that no elaboration checks are needed in preelaborable units, we require that all of the functions called from the expressions of aspects Type_Invariant and Default_Initial_Condition be ones that are known (to the compiler) to be ones that cannot fail an elaboration check.

We do not attempt to do this for aspect Dynamic_Predicate, so an object of a subtype that has a non-trivial Dynamic_Predicate is not preelaborable, even if the type has preelaborable initialization. Similarly, we don’t attempt to do this for aspect Type_Invariant’Class, as ensuring elaboration of bodies of subprograms called via a dispatching call is impossible in general (they could occur anywhere in the program, including after the current unit).

In both of these cases, we prevent “lying” about preelaborable initialization when it is explicitly specified. We do not want a type that has an explicit Preelaborable_Initialization aspect specification to not actually be usable in a context that requires preelaboration.

!wording

The actions of checks associated with Default_Initial_Condition, Type_Invariant, and Static_Predicate aspects are not considered when determining if a construct is preelaborable.

AARM Reason: These aspects have restrictions to make them safe to evaluate during elaboration. For Static_Predicate, the usual static predicate restrictions are sufficient; for the other aspects, additional restrictions are defined below. The checks are evaluated in the normal way; only the Legality Rules prohibiting evaluation of objects and function calls are omitted.

AARM Ramification: This does not apply to other aspects that might need to be evaluated, in particular Dynamic_Predicate.

AARM To Be Honest: Aspect Type_Invariant'Class is not included in this exception. We cannot ensure that no elaboration check can fail for a dispatching call.

AARM Reason: We want to disallow any Dynamic_Predicate expressions that are not preelaborable; since the current instance itself is not preelaborable, we simplify the rule to just banning Dynamic_Predicates altogether. Static_Predicates cannot contain anything that causes trouble, so we allow them. We don't need similar rules for types, as the usual object declaration rules take care of those at the point of use.

[Author's note: It's a bit uncomfortable that applying a Dynamic_Predicate to a type that has P_I effectively makes the type unusable in a preelaborated package (but still visibly have P_I). We could instead do something more similar to the below rules, but that seemed too incompatible (since it would need to apply to types like elementary types that just happen to have P_I, whether anyone cares or not). The rules below are safer, since they only need to apply to types that explicitly have P_I.]

AARM Reason: Any non-trivial Type_Invariant'Class aspect of an interface has to contain at least one dispatching call; those are never preelaborable. Since interface types are abstract (and class-wide interface types are indefinite), they cannot be used in object or component declarations. This definition prevents types derived from an interface that has one or more Type_Invariant’Class aspects from "lying" (as such a type can never declare a preelaborable object).

If the Preelaborable_Initialization aspect is specified True for a private type or a private extension{ T},{ then:

}If the aspect is specified True for a protected type, the protected type shall not have entries, and each component of the protected type shall have preelaborable initialization. If the aspect is specified True for a generic formal type, then in a generic_instantiation the corresponding actual type shall have preelaborable initialization. If the aspect definition includes one or more Preelaborable_Initialization attribute_references, then the full view of the type shall have preelaborable initialization presuming the types mentioned in the prefixes of the attribute_references all have preelaborable initialization. For any other composite type, the aspect shall be specified statically True or False only if it is confirming. In addition to the places where Legality Rules normally apply (see 12.3), these rules apply also in the private part of an instance of a generic unit.

AARM Reason: The restrictions on the contents of Type_Invariant or Default_Initial_Condition expressions prevent any case where evaluation of one of these contracts could cause an elaboration failure. It does not try to prevent such evaluation from having side effects (such as writing memory in some other package, or raising an exception). These restrictions allow us to ignore these contracts when determining whether a declaration is preelaborable.

The restriction against having Type_Invariant'Class or Dynamic_Predicate aspects exist to prevent "lying", where a type is explicitly specified to have preelaborable initialization, but no object of the type could be preelaborable.

{For a type T that has Preelaborable_Initialization specified True, an object_declaration of type T shall not appear before the completion of any function that can be called by the evaluation of the expression of any Type_Invariant or Default_Initial_Condition that applies to T.}^[c]^[d]

AARM Ramification: Only the completions of functions declared in the current library unit need be checked; functions declared in other units necessarily have been completed by the time of any such object declaration.

AARM To Be Honest: A function "can be called" from a call of another function which is directly called by contract expression. Since all of the functions that need to be checked for completion are required to be local expression functions (by the definition of callable from preelaborable initialization), all such calls that are possible can be determined at compile time of the local library unit.

!discussion

(1) The Default_Initial_Condition is evaluated for any default-initialized object of the type associated with the aspect (see 7.3.3(7/5)).

(2) The Type_Invariant is evaluated for any default-initialized object of the type associated with the aspect (see 7.3.2(10/4)).

(3) A Dynamic_Predicate can be evaluated for any default-initialized object of a type with a Default_Value (since the value is converted to the appropriate subtype, and that subtype can have a Dynamic_Predicate, see 3.3.1(11.1/5)). [Note: A Static_Predicate cannot evaluate anything that is not preelaborable.]

(4) A Dynamic_Predicate can be evaluated for any default-initialized object of a type with a Default_Component_Value (since the component value is converted to the appropriate subtype, see 3.3.1(13/5)). Case (3) can also happen for an array object (that also is mentioned in 3.3.1(13/5)).

(5) A Dynamic_Predicate can be evaluated for any component of a default-initialized object if the component has a default expression; again, the component is converted to the appropriate subtype, see 3.3.1(13/5).

None of these cases are covered by the current wording in 10.2.1. It might appear that case (5) is covered by 10.2.1(11.3/2), but it is not; that paragraph talks about the evaluation of the default expression; it does not say anything about the subtype conversion that happens afterward.

On the other hand, declaration of an object in any of these cases clearly violates 10.2.1(8) [the evaluation of the current instance is not allowed by that rule, even if there is no function call], so none of these are currently allowed in preelaborated code. Thus, the Preelaborable_Initialization aspect is ineffective for any type with one of these contracts; one still cannot declare an object at library-level in a preelaborated package. This is bad, especially for private types where there is an explicit declaration that intends to allow such objects. We don't want declarations that effectively lie.

The Default_Initial_Condition contract is only allowed on private types and extensions, and the Type_Invariant contract is mainly allowed on such types (it is also allowed on the full type of private types).

When a contract is given on a private type, the components aren't directly available. That means that the contract expression necessarily has to call a function that takes an object of the private type in order to query the state.

This means that simply enforcing the preelaboration rules on contracts would make

Default_Initial_Condition and Type_Invariant contracts impossible to use on private types that have Preelaborable_Initialization. This is a problem, both for usability, and especially as the Ada.Containers have such contracts. We can't have rules that make the containers impossible to write in Ada.

Therefore, we need a solution which will allow writing these contracts on types with Preelaborable_Initialization. We only have to have a solution for D_I_C; other contracts are less necessary but it is preferable to allow as many as possible.

Recall that contracts provide a requirement on one side and a promise on the other side. The contracts in question here are providing a promise to the client of a package, and a requirement on the author of the package. As such, such contracts should almost never fail; such a failure means a requirement was not met. Since this is totally under the control of the author of the package, this should be considered a bug in the package. In particular, nothing a client might do can change whether these contracts succeed or fail.

Additionally, contracts that operate on default-initialized objects of types that have preelaborable initialization (a PI type) almost always will be very simple. The components of a PI type can only be initialized with constants. As such, any D_I_C will ultimately be testing some constants, and as such should very simple. Indeed, they should be simple enough that most compilers can completely optimize them away. Type_Invariant and Dynamic_Predicate contracts might have a more complex part, but the part associated with default-initialized objects also has to be simple for the same reasons.

Since the contract expressions are likely to be simple, limiting what is allowed in them should not matter in the vast majority of cases.

The primary purpose (and effect) of declaring a package as preelaborated is to ensure that no elaboration check failures are possible in the package. (Note that this does not mean that all checks succeed during elaboration; other kinds of checks can fail.) In fact, C.4(3) requires that no code or data is used for elaboration checks in preelaborated library units. Unfortunately, evaluating contracts during elaboration can cause elaboration failures. This can happen in two ways for a type T with a contract expression. First, if an object is declared of type T in the package P containing the declaration of T, and the contract contains a call on a function F whose body has not yet been seen (this necessarily is the case if the body of F is in the body of P, and the object is in the specification of P).

Second, it can happen for a function declared in another package PP if the body of the function is in the body of PP and that body has not been elaborated when P is elaborated. (Most Ada implementations try to avoid this situation when determining an elaboration order, but it is not always possible, especially when limited withs are used in the program.)

We adopt a number of Legality Rules to prevent these situations for the contracts associated with any type that has Preelaborable_Initialization and is declared at library level in a preelaborated library unit. Otherwise, preelaboration becomes worthless if any contracts appear in any package.

These rules are (mildly) incompatible, but it should be easy to fix the vast majority of such contracts (by introducing an expression function in the private part of a package specification, by adding pragma Elaborate_All appropriately, or by moving function completions to an earlier point).

The net effect of these rules is to add cases where runtime checks need to be made during the elaboration of a preelaborated package.

This might seem to be a new idea, but it is not. Nothing in the rules for preelaboration makes it impossible for (most) language-defined checks to fail. (It does make it impossible for elaboration checks to fail, but of course Ada has many more kinds.) Indeed, C.4 already allows code to be executed for language-defined checks.

This declaration is preelaborable, and thus is allowed at library level in a preelaborated package, but it will always raise Constraint_Error when elaborated. So long as appropriate restrictions exist to prevent introducing elaboration failures (see the previous item in this discussion), there does not seem to be any problem with allowing other checks to be performed during elaboration (checks have no effect on whether the data can be initialized at "load time").

We wondered if the "load time" rules of C.4 needed modification. Contract evaluation clearly requires code to be executed. Luckily, C.4(11) excludes any case where a language-defined check can fail from the requirement. Contract checks are "language-defined checks" by

the definition given in 11.5(2/3), so this rule clearly applies. Ergo, the requirements of C.4(3) do not apply if any contracts apply to the object declaration.

The author is a bit sorry about this, as he would have preferred to use the need to update this code as an excuse to greatly simplify this section. He believes that C.4(4-12) be deleted and C.4 replaced by "A preelaborated package should be implemented in such a way that there should be little or no code executed at run time for the elaboration of the package." (Implementation Advice requires documentation, so C.4(12) is redundant with this advice.)

The last needs a bit of explanation. On a space-limited target, it's very possible that elaboration code would take up much less room than a copy of the data for an object. For instance, consider an array of 10000 4-byte records. Elaboration code for that array probably executes a loop and only takes a couple of dozen bytes of code (each iteration writing the 4-bytes of the record). A copy of the bytes of the array would take up 40,000 bytes in the ROM (and it still would have to be copied to the RAM area, probably with code of a similar size to the array initializer).

For all of these reasons, it would be better to simply have Implementation Advice that recommends an implementation. That leaves implementers flexibility; it wouldn't require anyone to change anything but would eliminate the need to invent a fiction (or invoke the Dewar Rule) to support some kinds of targets.

Note that the rules defined here do NOT mention Dynamic_Predicates. Thus, an object declaration that invokes a Dynamic_Predicate whose evaluation might include a function call is not preelaborable. We did not try to extend the new Legality Rules to Dynamic_Predicates out of concern for compatibility. If we had such rules, they would have to apply to any Dynamic_Predicate applied to any subtype of a type that has preelaborable initialization.

That includes all scalar types and many record and array types. It is better to reject the rare bad usage rather than the more common declaration which can be (and most likely is) used without problems in all contexts except library-level objects in preelaborated units.

We do prevent explicitly declaring a type with a Dynamic_Predicate as having preelaborable initialization, in order to prevent types that explicitly say they allow declaring preelaborable objects when they don't.

Similarly, we don't allow Type_Invariant'Class to apply to a type that explicitly is defined as having preelaborable initialization.

These latter rules are incompatible, but only for types that explicitly declare themselves as having preelaborable initialization but never are used to declare a library-level object in a preelaborable package. (Other cases are already illegal.)

Finally, we define interfaces to not have preelaborable initialization if a Type_Invariant'Class aspect applies, so that type derived from such an interface do not lie. This also is incompatible, but only if a type derived from an interface with a Type_Invariant'Class is explicitly declared to have preelaborable initialization and that derived type is never used to declare a library-level object in a preelaborated unit. (Again, other cases are already illegal.)

We considered deferring the checks rather than applying restrictions to them. However, in order to avoid any possible elaboration failures, those evaluations would have to be deferred until all preelaborable packages have been elaborated. (Any contract could call a function in some other preelaborated package whose body hasn't been elaborated yet.) That means the checks cannot be evaluated in the package that generated them, but rather much later. This would require involving the binder and putting the checks in a subprogram for the binder to call at an appropriate point in the elaboration order.

That would require a lot of mechanism, especially for checks that are never expected to fail

We also considered a simpler model where any function call that is callable from preelaborable initialization (we'd need a different term) can be called from preelaborable code. This would automatically allow any "safe" contracts as well as expand the capabilities of preelaborated packages. But there are some downsides. First, we'd still have types that are explicitly declared to have P_I that would not be usable in such contexts. Second, this would allow some non-constant initializations to occur, meaning that "load time" initialization would not always be possible. Even if we didn't require "load time" initialization (and we shouldn't, see above), it still should be possible. For these reasons, we followed the more complex approach.

We exclude dispatching calls from those that are allowed in this context. Thus we do not try to support Type_Invariant'Class (rather letting it prevent preelaboration). A dispatching call can execute many bodies, all of which could fail an elaboration check. Indeed, some could be in non-preelaborated packages, and may not have been imagined when the preelaborated unit is compiled. For a direct call, we can avoid problems with pragma Elaborate_All, but that cannot work for types added later. This shouldn't matter much in practical terms, since preelaborable objects cannot be class-wide (class-wide types cannot be declared as objects or components, and preelaboration does not allow allocators [an allocator calls a subprogram Allocate that is not one of the allowed ones]).

!example

The containers packages illustrate this issue nicely. Following is the specification of Ada.Containers.Vectors, showing just the parts relevant to this discussion:

generic
...
package Ada.Containers.Vectors
with Preelaborate, ... is
type Vector is tagged private
with ...
Default_Initial_Condition =>
Length (Vector) = 0 and then ...,
Preelaborable_Initialization;

The elaboration of a default-initialized Vector object will finish with the evaluation of the Default_Initial_Condition expression. That will call the function Length. However, that means that such an elaborable construct is not preelaborable by the rules given in 10.2.1(5, 7). Yet we are asserting that this construct is preelaborable by the use of the P_I aspect.

With the new rules, the Vector type can have both preelaborable initialization and a D_I_C aspect. Function Length will have to be implemented with an expression function given in the private part (it is probably just returning a component of a Vector object).

!corrigendum 10.2.1(9.1/5)

@xbullet{The elaboration of any elaborable construct that is not preelaborable.}

The actions of checks associated with Default_Initial_Condition, Type_Invariant, and Static_Predicate aspects are not considered when determining if a construct is preelaborable.

!corrigendum 10.2.1(11.3/2)

@xbullet{A component (including a discriminant) of a record or protected type has preelaborable initialization if its declaration includes a @fa{default_expression} whose execution does not perform any actions prohibited in preelaborable constructs as described above, or if its declaration does not include a default expression and its type has preelaborable initialization.}

@xbullet{A component (including a discriminant) of a record or protected type has preelaborable initialization if no Dynamic_Predicate specification applies to its subtype, and:}

@xinbull{its declaration includes a @fa{default_expression} whose execution does not perform any actions prohibited in preelaborable constructs as described above, or}

@xinbull{its declaration does not include a @fa{default_expression} and its type has preelaborable initialization.}

!corrigendum 10.2.1(11.5/2)

@xbullet{A view of a type has preelaborable initialization if it is an elementary type, an array type whose component type has preelaborable initialization, a record type whose components all have preelaborable initialization, or an interface type.}

@xbullet{An interface type has preelaborable initialization if and only if no Type_Invariant'Class aspects apply to it.}

@xbullet{A view of a type has preelaborable initialization if it is an elementary type, an array type whose component type has preelaborable initialization, or a record type whose components all have preelaborable initialization.}

!corrigendum 10.2.1(11.7/5)

@xhang{@xterm{S'Preelaborable_Initialization}This attribute is of Boolean type, and its value reflects whether the type of S has preelaborable initialization. The value of this attribute, the type-related Preelaborable_Initialization aspect, may be specified for any type for which the attribute is defined. The value shall be specified by a static expression, unless the type is not a formal type but is nevertheless declared within a generic package. In this latter case, the value may also be specified by references to the Preelaborable_Initialization attribute of one or more formal types visible at the point of the declaration of the composite type, conjoined with @b{and}.}

@xbullet{It is an expression function and all of the functions that occur in the return expression of the expression function are callable from preelaborable initialization of @i{T};}

@xbullet{It is completed by an expression function in the same package specification as the type @i{T}, and all of the functions that occur in the return expression of the expression function are callable from preelaborable initialization of @i{T};}

@xbullet{It is, or is declared in, a library unit which is named in a pragma Elaborate_All which applies to the compilation unit declaring @i{T}.}

!corrigendum 10.2.1(11.8/5)

If the Preelaborable_Initialization aspect is specified True for a private type or a private extension, the full view of the type shall have preelaborable initialization. If the aspect is specified True for a protected type, the protected type shall not have entries, and each component of the protected type shall have preelaborable initialization. If the aspect is specified True for a generic formal type, then in a @fa{generic_instantiation} the corresponding actual type shall have preelaborable initialization. If the aspect definition includes one or more Preelaborable_Initialization @fa{attribute_reference}s, then the full view of the type shall have preelaborable initialization presuming the types mentioned in the @fa{prefix}es of the @fa{attribute_reference}s all have preelaborable initialization. For any other composite type, the aspect shall be specified statically True or False only if it is confirming. In addition to the places where Legality Rules normally apply (see @ref{12.3}), these rules apply also in the private part of an instance of a generic unit.

If the Preelaborable_Initialization aspect is specified True for a private type or a private extension @i{T}, then:

@xbullet{no Type_Invariant'Class or Dynamic_Predicate aspect shall apply to the type;}

@xbullet{the @fa{expression} of any Type_Invariant or Default_Initial_Condition aspect that applies shall not contain any function calls that are not callable from preelaborable initialization of type @i{T}.}

If the aspect is specified True for a protected type, the protected type shall not have entries, and each component of the protected type shall have preelaborable initialization. If the aspect is specified True for a generic formal type, then in a @fa{generic_instantiation} the corresponding actual type shall have preelaborable initialization. If the aspect definition includes one or more Preelaborable_Initialization @fa{attribute_reference}s, then the full view of the type shall have preelaborable initialization presuming the types mentioned in the @fa{prefix}es of the @fa{attribute_reference}s all have preelaborable initialization. For any other composite type, the aspect shall be specified statically True or False only if it is confirming. In addition to the places where Legality Rules normally apply (see @ref{12.3}), these rules apply also in the private part of an instance of a generic unit.

For a type @i{T} that has Preelaborable_Initialization specified True, an @fa{object_declaration} of type @i{T} shall not appear before the completion of any function that can be called by the evaluation of the @fa{expression} of any Type_Invariant or Default_Initial_Condition that applies to @i{T}.

!ACATS test

An ACATS B-Test should check that an object of a subtype S with Dynamic_Predicate that calls a function is illegal at library-level in a preelaborated package (even if S has Preelaborable_Initialization).

An ACATS B-Test should check the new Legality Rules for contracts of private types.

An ACATS C-Test should check that D_I_C and Type_Invariants are allowed on types with P_I, and that library-level objects of such types can be created. Another test should check that a failed contract does raise Assertion_Error during the elaboration of the unit.

!appendix

[a]This puts the onus on the unit that mentions the library unit with the function in a with clause. It would seem OK if the function is declared in a library unit that has a pragma Elaborate_Body.

And what if the type with P_I is itself declared in a preelaborated or pure library unit? Does the guarantee that the aspects are OK?

[b]Elaborate_Body is not enough, the function can call something else that isn't elaborated. Elaborate_All is recursive. The GNAT static elaboration model ignores Elaborate_Body for this reason (Claw broke when they changed that). Moreover, it seems best to me that the user of something that needs a restriction can apply that restriction without having to change other code (which the user may not own).

Preelaborated units only get rid of elaboration problems by making it illegal to call a subprogram during elaboration (among other things). Since we have to allow that here, they are of no help.

[c]This is entering the domain of static elaboration-order checks. GNAT already does this, but I wonder about the implementation work for other implementations, and whether GNAT can do this on a piece-meal basis.

[d]Yes, I mentioned that somewhere (perhaps in one of my e-mails). These rules are fairly close to the ones for GNAT (at least circa 2003 when I studied them closely for Claw). The only difference I recall is the provisions for expression functions, which didn't exist in 2003.

I didn't want to adopt fully static elaboration for preelaborated packages mainly because of the compatibility problem. The GNAT rules broke Claw back in the day (twice, the second time when they eliminated Elaborate_Body from consideration), and they'd be likely to break other existing code. The easy "fix" of -GnatE wouldn't be available if it was a language requirement.

!summary