Preelaborable_Initialization and contract aspects

[ARG-Editor]

One of the Hold AIs (AI12-0420-1) was for a language bug that did not have an obvious solution. We decided to Hold it as we were too close to the submission date for Ada 2022. And we essentially forgot to move it to the AI22s.

I've done that now. You can read the complete AI (AI22-0051-1) in the usual places (arg.adaic.org and www.ada-auth.org).

The gist of the problem is that aspect Preelaborable_Initialization (P_I) is supposed to be True for a type only when a default-initialized object of that type is preelaborable -- that is, doesn't execute any actions on the prohibited list starting at 10.2.1(5) when it is elaborated. However, P_I doesn't take into account any contracts that might be checked, in particular Default_Initial_Condition (D_I_C).

Checking most contracts involves making one or more function calls, and function calls are not preelaborable (outside of a handful of static functions that are allowed). So, in almost all cases, the evaluation of a contract makes a construct not preelaborated.

Note that there are actually 5 known ways for a contract to be involved in default initialization that are not covered by current wording. For most of those cases, it would be sufficient to simply say that the existence of a contract makes the type ineligible for setting aspect P_I to True. While it is possible in theory for some specific contracts to not cause problems, it probably isn't worth it to try to come up with wording (and implementation complexity) to allow them. (Again, the vast majority of contracts involve at least one function call, the cases where there is no call and no "evaluation of a name of an object" seem uninteresting.)

However, D_I_C is different, in particular because the Ada Containers have both D_I_C and P_I on each container type. We need some way to allow D_I_C in this case (or we have to remove preelaboration from the containers, which could be a significant incompatibility for some).

So much for the facts of the case. Let me indulge in some musings on a possible way to solve this problem.

D_I_C (like a Postcondition) is somewhat different from other contracts and assertions in that it's primary purpose is to define the initial state of objects for clients (similarly to how postconditions tell clients what state they can expect upon normal return from a subprogram). For both D_I_C and postconditions, the actual check is of secondary importance. it exists mainly to keep the programmer of the abstraction honest (preventing lying by causing an exception). Failure of a D_I_C is a bug, and a bug in the abstraction - a client cannot do anything to fix or prevent such a failure. (The same is true for postconditions.) Contrast this to most other contracts and assertions, which are about enforcing restrictions on the client. If a pecondition or predicate fails, that is a bug of the client's; they have to fix it.

Since the enforcement of D_I_C is of secondary importance, we could simply not do it when a default-initialized object of a type with P_I is declared in the context of a preelaborated unit. Since it still would be enforced in all other contexts. any bugs in the implementation would most likely be detected. The effect would be the same as an automatic Ignore when the type is used in a preelaborated unit. This would prevent the evaluation of function calls in a preelaborated unit, but still allow the use of D_I_C to describe the initial state.

This "solution" has me holding my nose, as I hate Suppressing/Ignoring any checks (I prefer that the compiler eliminate most of them, and the left are left permanently to catch any latent bugs). But I cannot think of any other way to allow D_I_C to describe the initial state of objects of private types without making the code fail to be preelaborable.

Note that implementations and tools may be making assumptions based on knowing that the elaboration of a package does not make any function calls. (For instance, the elaboration model can be simplified.) We cannot just start allowing some violations of that model, as that could invalidation some of those assumptions, introducing hard-to-find bugs into implementations that did not previously exist. So I think we have to find a way to ensure that no such calls are made.

                                    Randy.

Because of this difference, it would be OK to avoid enforcing D_I_C

[sttaft]

I like your proposed solution. It also means that a tool should not presume that the D_I_C is true for an object declared in a pre-elaborated package, unless of course the tool can prove its truth by looking through privacy.

[Richard-Wai]

So this doesn't quite smell right to me.. It would seem that making a type P_I makes D_I_C potentially pointless wherever it is used for a preelaboration-initialized object, and this to me is not what a typical Ada programmer would expect, either as the one writing such a contract, or as one creating such an object.

This is obviously a really hard problem, and I have a poor track-record so far for having a great solution to such problems, but for the sake of conversation:

Is it possible that we could introduce something like a "deferred check" for contracts like this? Basically every time an object is created in true preelaboration, the compiler also adds associated contract checks to a list of sorts that forms an implicit procedure that is executed as part of the elaboration of the Environment_Task. That way we know the check still happens, and there'd also be an easy-enough way to disable it if we really don't want to run those. Another benefit is that you'd find out about a failure very quickly indeed!

[sttaft]

Is it possible that we could introduce something like a "deferred check" for contracts like this? Basically every time an object is created in true preelaboration, the compiler also adds associated contract checks to a list of sorts that forms an implicit procedure that is executed as part of the elaboration of the Environment_Task.

Interesting suggestion, Richard. But this feels like an annoying implementation burden, requiring a completely new sort of "late" elaboration routine. In any case I would think we could at least allow this approach in the near term, and then perhaps in the next standard require it if the implementation burden was found to be not too bad.

We already know that various of the aspects, such as Dynamic_Predicate and Type_Invariant, are not perfect in terms of being enforced everywhere (e.g. you can change the value of a component of a record and the Dynamic_Predicate associated with the record as a whole will not be rechecked), so saying that D_I_C is not guaranteed to be enforced on preelaborated objects seems similar.

Note that the SPARK toolset does enforce full checking for things like Dynamic_Predicates, though this is a static check for SPARK. We probably ought to allow implementations to do "full" checking for these as well, then D_I_C and Dynamic_Predicate would be treated similarly.

[Richard-Wai]

I am slowly accepting that most of these more complex contract mechanisms are far more useful in the formal verification space than they are as run-time assertions, particularly when comparing their cost against the more traditional checks.

Agree it would be nice to suggest something of that nature. My main point of concern is that Ada itself starts to move towards "here is a bunch of language-specific stuff that is only really applicable to formal verification and/or high-end static analysis". I already had a hard time with how/when subtype predicates are checked, but in this case it ends up being a bit more insidious where checking of a contract is not controlled reliably through a configuration pragma (or similar), but is disabled because it happens to be too hard to check under certain circumstances.

[ARG-Editor]

I agree with Tucker that trying to make this check "late" would be pretty expensive, being unlike anything that already exists. One would have to call this routine after the elaboration of all preelaborated units (otherwise the assumptions of preelaboration would be violated), and before any use of anything in any preelaborated unit. So this would be a whole new concept.

And I think you are overthinking what might not get checked here. D_I_C only describes the default-initialized state of an ADT. This almost always is simply a bunch of constant initializations, and some function calls to read them abstractly. It doesn't take "high-end static analysis" to determine that they can't fail.

For instance, in the container example I gave initially, it's highly likely that there is a component called Length in the container object, default initialized to zero. And the function length does nothing but return that component. So any compiler that does simple inlining and constant propagation (which is almost all of them) is going to reduce the D_I_C check to "0 = 0", which hardly needs code to verify!

Having language stuff for "high-end static analysis" is a good thing. Every Ada compiler has always done quite a bit of static analysis (for checking elimination, at a minimum). Having more information to feed into that is always a good thing. Indeed, I'd argue that every compiler for every language should be doing some static analysis these days -- we've got the CPU and memory resources needed, we should be detecting problems as early as possible (rather than making programmers debug and debug and debug forever). Of course, Ada makes that easier than most languages, so we should especially be taking advantage of that.

[sttaft]

Richard writes:

... here is a bunch of language-specific stuff that is only really applicable to formal verification and/or high-end static analysis ...

I think you are ignoring perhaps the most important benefits -- human understanding and program correctness.

Even though Dynamic_Predicates (and perhaps now D_I_C) are not always checked, they are checked enough that it is highly likely they are always true. And the more important thing is that they explain the intent of the program to the human reader, and if the intent makes sense, and the intent is checked against reality sufficiently often, then it is much more likely that the program is correct in the sense that it actually matches its intent.

[ARG-Editor]

This issue was covered in AI22-0051-1 and then later in AI22-0051-2. The first was approved, then rejected by WG 9, and now the second has been approved at meeting #63B. So I'm closing this issue.