AI22-0165-1/02

Pragmas Static_Checks and Strict_Static_Checks are defined as checking pragmas; these pragmas specify that specified language-defined checks are illegal unless the checks are known to succeed. Strict_Static_Checks assumes that the only unneeded checks are those known to succeed by language rules; Static_Checks allows the implementation to determine if other checks are unneeded.

!issue

Some languages require explicit "unwrapping" of optional types before they can be used. That makes the check for optionality explicit. Ada would handle such things similar to an access check, where the user would use an if statement (or possibly case statement, if a suggested extension is provided) to test the optional component for existence. A static version of this check would have the effect of requiring "unwrapping" without requiring a new feature.

We also have a suggestion for a static version of accessibility checking, which can eliminate much of the overhead of dynamic accessibility checks.

It seems that we need some form of static checking to augment the dynamic checking

!recommendation

!wording

[Editor's note: Some of the introductory material in 11.5 also needs changes, along with the detailed description of Unsuppress. I've skipped that for now, working mainly on the "meat" of this proposal.]

A language-defined check (or simply, a “check”) is one of the situations defined by this document that requires a check to be made at run time to determine whether some condition is true. A check {succeeds when the condition being checked is True, and }fails when the condition being checked is False, causing an exception to be raised.

pragma Static_Checks(identifier);

pragma Strict_Static_Checks(identifier);

A construct where a named language-defined check^[a]^[b] is required to succeed for a given entity is illegal if a pragma Static_Checks or Strict_Static_Check applies for that entity at that point and the check is not known to succeed. A check is known to succeed under circumstances defined within this document where a given check is defined.

[Editor's note: This rule is full of forward references, the rules which define how a checking pragma applies are found later. We would prefer to put it later, but that would require moving the Legality Rules later in 11.5, and adding "in a checking pragma" to the text of 11.5(6/2) (or having two Legality Rules categories, which we usually avoid).^[c]^[d]

Note that the definition of “named check” and where it applies is in 11.5(7.1), so we only need to talk about where pragmas Static_Checks and Strict_Static_Checks apply. It does seem weird that “named check” doesn’t seem to be tied to the pragmas, but that is done by a general rule for all checking pragmas, of which these are.]

An implementation may determine that other checks are known to succeed^[e] for any named checks on any entities to which a Static_Checks pragma applies. Any such check will succeed for any possible non-erroneous execution of the check.^[f]

AARM Ramification: If a compiler can prove that a check is known to succeed at compile-time, then the compiler does not need to make the entity illegal because of the presence of the check. Note that this permission does not apply to pragma Strict_Static_Checks, for that pragma, only checks defined as known to succeed according to the language are allowed in legal code.

We have carefully avoided describing this permission as being implementation defined, as "implementation defined" requires documentation, and it is likely that it would be very difficult to explain precisely when a compiler can prove a check will always succeed. (If it is easy, we already have defined it as "known to succeed".) For a compiler using a proof engine or advanced optimization technology, it is likely that any useful description is impossible. Therefore, we don't want to require that.

[Editor's note: I do not know where best to put the following rules (see the !discussion, below). I have provided a couple of sample rules; we may want to put these definitions into one or more separate AIs, and potentially nearer to the dynamic checks to which they apply.]

An Index_Check is known to succeed if the index expression of an array A is a name that denotes one of an in parameter, a stand-alone constant, or a loop parameter^[g]^[h]^[i]^[j], and the nominal subtype of the name of the index expression statically matches the index subtype of A.

AARM Discussion: This rule is conservative^[k]^[l]. Note that we don't allow parts, only whole objects, as parts of composite objects can be modified by other paths and potentially can become invalid. We don't want to have to deal with potential modifications so that we can allow indexing in entire loops and subprogram bodies.

[Editor's note: Static matching does most of the work here, especially the new AI22-0142-1 rules. I am assuming that if the prefix of a Range attribute is an array object whose bounds can change (as proposed in AI22-0148-1), A'Range will not statically match A'Range. We might want to go beyond static matching in the specific case where both subtypes are range attributes, or perhaps we ought to adjust static matching itself (if A statically names an entity and A is not mutable, then why shouldn't A'Range match A'Range?? That's even true for an unconstrained parameter).]

A subprogram potentially writes objects if it has any in out or out parameters, has any parameters with an access-to-variable part, or if it has a global specification that allows writing of globals[Redundant:, such as in out all or out synchronized] or overrides any parameters to modes in out or out (see H.7).

AARM Discussion: We don't care about writing of objects that are local to the subprogram here, only objects possibly visible at the callsite.

An expression is defined to be side-effect free if it does not contain any calls to a function that potentially writes objects.

An Access_Check is known to succeed if it applies to an object that excludes null.

AARM Ramification: Unlike scalar objects, it is not possible for a null-excluding object to be "deinitialized" without erroneous execution. If a null-excluding component is read as null, then the read object is abnormal (see 13.9.1) and subsequent use causes erroneous execution. Thus, we can always trust null exclusions, and there is no need to make access checks on null excluding objects.

An Access_Check is known to succeed if it applies to an object P named in a dependent_expression D of an if expression, and:

AARM Ramification: "A test that P is not null" might be an inequality (P /= null)

or a membership against null (P not in null) or against a null-excluding subtype.

This can be anded with any other side-effect free expression (but not ored or noted!)

The second condition allows else branches or any other arbitrary conditions that follow

P can be anything that doesn't itself have a side-effect, since we have ensured that no side-effects can happen between the test(s) and the usage. That means it can contain an array indexing, or dereferences, as later evaluations must get the same result.

This allows an expression like (if P /= null then P.all else 0) to be legal even when pragma Strict_Static_Checks is applied.

[Editor's note: I didn't try to allow the negative of tests as the logic starts to get complex. This is one of the many cases where a compiler is likely to be able to do better.]

expression in a statement S (or in a declaration in a block_statement S) in a sequence_of_statements Q of an if_statement, and:

AARM Ramification: Note that the prohibitions against procedure calls and assignment statements only apply before the statement S that includes the check in question. The same applies for a block_statement. Checks associated with the evaluation of the source or target of an assignment, with expressions in the declarations of a block_statement, and with the evaluation of parameters to a call (but not the copy-back), are included in this rule.

The goal of this rule is to allow if_statements with a single dependent statement to have access checks be known to succeed without requiring the introduction of a name. Users would tar and feather us if the following was illegal when pragma Strict_Static_Checks is in effect:

Additionally, we want to be able to introduce a name immediately in a block that is the first statement of an if statement, so it can be used in the remainder of the statements of that if branch.

!discussion

These pragmas can be thought of as a stricter version of Suppress. Rather than having failed checks make the program erroneous, they make the program illegal if it contains a check that can fail. That makes it natural to define these pragmas with Suppress.

There are two additional reasons for defining these pragmas as checking pragmas:

(A) We need to have names to define which checks we are talking about, these are already present in 11.5 and it makes no sense to start over.

(B) We likely need to be able to turn off these pragmas in limited areas where we want to use an actual dynamic check. For instance, a saturation math package is likely to handle an overflow check for multiply in order to determine saturation; it would be difficult to define the cases that saturate statically. Moreover, it should be clear that there is no risk of an unhandled exception occurring from:

With static checks being a checking pragma, this code can be used in a project that uses one of the static checking pragmas.

We define the semantics of these pragmas in terms of checks that are known to succeed, so that we need do nothing in order to have them properly defined for every check that has a name in 11.5 (which is supposed to be all of them). For most checks, there will not be any language-defined cases of checks that are known to succeed, so pragma Strict_Static_Checks (All_Checks); will make any unit it is applied to illegal.

We define two static checking pragmas so that we have a fully portable version and a version that uses the compiler's best efforts at check removal. All Ada compilers try to remove unneeded language-defined checks (with various levels of effectiveness). It would be malpractice to not take advantage of those efforts. However, Ada has made portability between implementations an important goal. Therefore, we also define a version of these checks which apply to all implementations (thus giving portability at the cost of needing additional code to avoid checks).

We considered having a Static_Checking_Policy instead of two pragmas. But that seemed to add a lot of complication for little gain over just having two pragmas.^[o]^[p]

We expect that most users will prefer the looser and thus easier to work with checks provided by implementers. Thus we gave the simpler name to the less portable but more usable pragma. The strict checks are likely to have users complaining about the "stupid language" a lot, when checks are not allowed that are perfectly obvious that they will always succeed.

We have shown a few definitions of checks that are known to succeed as examples. These are unlikely to be the only cases defined to be known to succeed (the author would not recommend that!).

The best location to define known to succeed checks is also unclear. Most such cases require a combination of features (as described above); should they be placed with one of those features (which one?), the check itself (which would often require a lot of forward references in the RM), in subclauses of 11.5 (those could get pretty large), or somewhere else?

A suggestion has been made that this information be put in "static checks" categories in each section, similar to "implementation permissions" and "usage". That would be one option for structuring the actual rules, but it doesn't answer where the best place to write those rules would be.

Note that many checks probably can't be usefully defined to be known to succeed. For instance, Storage_Error can be raised by any operation (even the null statement). We could try to eliminate a few obvious cases (like the null statement), but even if we did, pragma Strict_Static_Checks(Storage_Check) would make any non-trivial program illegal. Similarly, it doesn't seem possible to usefully say anything about arbitrary preconditions and predicates associated with the various language defined packages. Even so, a specific compiler might be able to prove that some such checks will always succeed, and they are allowed to use that information with pragma Static_Checks.

We could probably define a large number of "known to succeed” rules, but it seems likely that whatever rules we come up with will still have cases where a human reader would say that it is obvious that the check is unneeded. Our intent is to let implementers decide how important it is to handle additional "obvious" cases (thus the more weakly defined pragma Static_Checks).

"Unsuppress" is a bit of a weird name for turning off static checks. We could instead introduce a pragma Dynamic_Checks that turns off static checks. But that seems like extra overhead, and as the example above shows, the cases where Unsuppress and Dynamic_Checks would be used are often the same. One alternative would be to introduce the pragma Dynamic_Checks, but have it be a synonym for Unsuppress: both pragmas would remove suppression and static checks -- which name to use would be the one that seems most comfortable for the usage. The author thought that didn't seem to introduce enough value, thus it was left out.^[q]^[r]^[s]^[t]^[u]^[v]^[w]

!example

Because of side-effects, most access uses will require the introduction of a null-excluding name somewhere. Since uses of null-excluding objects never need checks (and thus never need to be illegal), they provide a way to handle any situation (at the cost of introducing an extra name):

pragma Strict_Static_Checks (Access_Check);

type Acc is access Desig;
P : Acc := ...;

if P /= null then
declare
NNP : not null Acc := P; -- OK:
-- Unneeded, immediately follows test.
begin
Ada.Text_IO.Put_Line ("Got before Do_It call");
-- Writes (global) objects.
Do_It (NNP.all); -- Unneeded, of null-excluding subtype.
end;
end if;

Because of the Put_Line call, if the call of Do_It directly dereferenced P, that dereference would not be known to succeed, and thus the code would be illegal.

Of course, this tracing might be temporary. If so, the user could have used Unsuppress instead to turn off the static checking here until after the debugging is complete:

pragma Strict_Static_Checks (Access_Check);

type Acc is access Desig;
P : Acc := ...;

if P /= null then
declare
pragma Unsuppress (Access_Check);
begin
Ada.Text_IO.Put_Line ("Got before Do_It call");
-- Writes (global) objects.
Do_It (P.all); -- No static check here.
end;
end if;

!ACATS test

ACATS B-Tests are needed to check that checks that are not known to succeed are illegal. ACATS C-Tests are needed to check that checks that are defined to be known to succeed do not make the program illegal when either Static_Checks or Strict_Static_Checks are used. These tests cannot be exhaustive, but they can test common cases, and should test “known to succeed” cases carefully.

!appendix

[a]Niklas had asked why this is restricted to "language-defined" checks, since check names can be implementation-defined. His comment got deleted when this text was replaced, but we had not come up with an answer.

[b]It seems odd that 11.5(27/2) allows implementation-defined check names (some of which presumably could apply to implementation-defined checks), yet 11.5(1/5) and 11.5(9) say that checking pragmas only apply to language-defined checks. Of course, an implementation could just ignore that (since everything implementation-defined can do almost anything), but why have more words that can only cause confusion? We need to discussion (and possibly look at the AIs that described checking pragmas to see if there is a reason for this wording).

[c]We allow definitions in the Legality Rules sections, so why not just move the unneeded definitions here?

[d]Because the some of references I was talking about are in existing rules in 11.5(7.1-2). You missed "named check" altogether, we certainly don't want Static_Checks to apply to every check in a scope, ignoring the named check kind!

[e]Perhaps should be italicized since it is in some sense extending the definition of this term.

[f]We have to explain what "known to succeed" means in general. The Legality Rule above just describes it as one specified in the Standard, which gives the implementor no guidance at all. I didn't mean to give implementers carte blanche to do whatever they like! The wording I came up with doesn't fit into the Legality Rule very well, so I stuck it here. (I would have preferred to use "must" or "shall" here, but those can't be used in a definition.)

[g]I worry that I am assuming that these objects are always valid. These could be invalid if an implementation allowed that (it appears that 13.9.1's Bounded Error would allow that, even though it would be excessively unfriendly). Similarly, a range could be invalid if an implementation allowed that (via the same rule). All of these things certainly are always checked for validity in Janus/Ada, but that might not be true in other compilers. Check elimination can only be done when the source (and target range!) is known to be valid.

[h]I would be very tempted to change the validity rules to require checks on these sorts of objects (as well as ranges), rather than leaving it to chance (which would make it nearly impossible to define any unneeded checks for scalar types). The 13.9.1 rule is extremely broad, essentially allowing all range checks to be ignored except those associated with array indexing. That doesn't make sense from a usability perspective, as any error would be widely separated from the source of the problem (and even the ranges themselves might be invalid).

[i]It seems to me reasonable that these pragmas can add checks as well as eliminate unneeded checks, if the added checks increase the number of eliminated unneeded checks. [Edit:] Ah, I forgot that if the purpose of these pragmas is to leave no checks that could fail, then also those added validity checks would have to be made unneeded so that they can be eliminated, right? Or would you say that an execution in which the validity checks fail is erroneous?

An alternative is to define another new pragma for adding those validity checks, leaving the choice of only eliminating checks, or also adding some checks, to the programmers. The pragma for validity checks could also be useful on its own.

[j]The objects in question could be from another unit where Static_Checks does not apply (think parameters passed to a local subprogram from a call in some other unit, which therefore did not get checked), so it doesn't seem very practical to tie it solely to the pragma. (It could only be used on local constants in that case.) My preference is to require these objects to be valid always, that would allow more checks to be eliminated elsewhere anyway.

[k]Should the "in" parameter be required to not be explicitly aliased? Should the stand-alone constant be required to not be Volatile?

[l]As noted in the previous comment, we need some new wording to require these to be valid before this works. Whatever restrictions we put on that rule would be repeated here.

[m]I will send an e-mail to the ARG list (not the WG 9 list as I first wrote) that suggests a more formal definition of these kinds of expressions and conditions, and widens them a little.

[n]We could have a special case for if_statements, but that would require some form of recursion in this definition. As always, how hard do we want to work and make implementers work?

[p]Note that would interfere with adding the usual second parameter to checking pragmas (even though we don't formally define that parameter anymore).

[r]For a project or user who *never* suppresses checks, but does use static checks regularly, a pragma named "Unsuppress" makes little sense in my view. I would agree that if you specify, say, Dynamic_Checks, that might imply Unsuppress, though they are sufficiently different in meaning that I suspect they should be controlled independently.

[s]If you say "Dynamic_Checks", it would be pretty odd for you to get no checks at all because they are suppressed. That's why I thought it and Unsuppress should have the essentially same meaning (and that also keeps the wording needed to a minimum). I suppose we could have Suppress also cancel Static_Checks (they're really three mutually exclusive states).

[t]I suppose we could have a Check_Policy pragma with various values: Dynamic_Checks, Static_Checks, Strict_Static_Checks, and Suppress_Checks. Pragma Suppress and Unsuppress could effectively "push" and "pop" the state.

Another approach is to presume you are in one of the three states, and only allow an Unsuppress if you are in the Suppressed state, and only allow a Dynamic_Checks if you are in the [Strict_]Static_Checks state. Both Suppress and [Strict_]Static_Checks would push the current state, and Unsuppress/Dynamic_Checks would pop the current state.

[u]I think there are three (or four if you consider strict a state) states, and Unsuppress and Dynamic_Checks represent the same state, and are completely equivalent. I don't want to see both somewhere because someone is protecting against global settings. That seems simplest to me. (But I haven't figured out the wording for that yet, I'd prefer to settle on the important parts of Static_Checks first.)

[v]I think it would be odd to label a state "Unsuppress" since that is more of an action than a state, and even the adjective "Unsuppressed" could be seen as describing any state other than Suppressed.

The three states seem to me to be "Suppressed", "Static_Checks", and "Dynamic_Checks". Unsuppress is a way to move from one state to another, but would be an odd name for a state.

In any case, it seems you are willing to support the notion of a "Dynamic_Checks" pragma/state. We are still not fully in agreement when you should be *allowed* to use the Unsuppress pragma.

[w]I didn't name the states (that would be part of the wording), so I don't quite get the leap to an "unsuppress" state, but otherwise I think we've mostly converged.