Version 1.5 of ai12s/ai12-0311-1.txt

Unformatted version of ai12s/ai12-0311-1.txt version 1.5
Other versions for file ai12s/ai12-0311-1.txt

!standard 11.4.2(23.5/5) 19-02-26 AI12-0311-1/03
!standard 11.5(23)
!standard 11.5(26)
!reference AI12-0112-1
!reference AI12-0208-1
!reference AI12-0309-1
!class Amendment 19-02-06
!status Amendment 1-2012 19-02-26
!status ARG Approved 9-0-1 19-02-26
!status work item 19-02-06
!status received 19-02-06
!priority Low
!difficulty Easy
!subject Suppressing client-side assertions for language-defined units

!summary

A set of check names is defined for suppressing client-side assertions (preconditions, static predicates, and dynamic predicates) in language-defined units.

!problem

Both the containers contract AI (AI12-0112-1) and the Bignum AI (AI12-0208-1) propose allowing the suppression of client-side assertions for language-defined units. But they both do it somewhat differently. We ought to have a single solution for this capability.

!proposal

(See Summary.)

!wording

Add after 11.4.2(23.5/5):

Any precondition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1) unless suppressed (see 11.5). Similarly, any predicate checks for a subtype occurring in the specification of a language-defined unit are enabled (see 3.2.4) unless suppressed.

AARM Reason: This allows the Standard to express runtime requirements on the client of a language-defined unit as preconditions or predicates (which are invariably clearer than English prose would be). Some such requirements can be Suppressed. Ada 2012 and before did not provide a mechanism to suppress such code.

[Editor's note: This was added to AI12-0112-1 after a suggestion by Tucker.]

Add after 11.5(23):

Redundant[The following checks correspond to situations in which the exception Assertion_Error is raised upon failure of a language-defined check.] For a language-defined unit @i<U> associated with one of these checks in the list below, the check refers to performance of checks associated with the Pre, Static_Predicate, and Dynamic_Predicate aspects associated with any entity declared in a descendant of @i<U>, or in an instance of a generic unit which is, or is declared in, a descendant of @i<U>. Each check is associated with one or more units:

Calendar_Assertion_Check: Calendar. Characters_Assertion_Check: Characters, Wide_Characters, and Wide_Wide_Characters. Containers_Assertion_Check: Containers. Interfaces_Assertion_Check: Interfaces. IO_Assertion_Check: Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, Storage_IO, Streams.Stream_IO, and Directories. Numerics_Assertion_Check: Numerics. Strings_Assertion_Check: Strings. System_Assertion_Check: System.

AARM Ramification: Any unit U is a descendant of itself.

AARM To be honest: The preceding rule about an instance of a generic where the generic is declared in U really extends recursively to handle the case of a generic package G1 which declares another generic package G1.G2, which declares another generic package G1.G2.G3, and so on. So if G1 is declared in some predefined unit U then, for purposes of defining these checks, Some_Instance_Of_G1.G2 is also considered to be declared in U.

Modify 11.5(26):

If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. {Similarly, if an assertion check has been suppressed and the evaluation of the assertion would have raised an exception, execution is erroneous.}

AARM Reason: It's unclear that a precondition or predicate expression that executes /raise/ some_exception is an "error situation"; the assertion never actually evaluates to False in that case. Thus, we spell out that case. We only allow suppressing assertions associated with checking client requirements for language-defined units; other assertions follow the rules of the appropriate Assertion_Policy. Note that a predicate expression that evaluates to False and uses aspect Predicate_Failure falls under the "error situation" case.

!discussion

Normally, assertions are Ignored rather than suppressed. However, the Ignore state of an assertion is determined when a unit is compiled. We do not want to force implementations to provide a way to allow users to recompile language-defined units in order to change this state.

Additionally, we want to be able to use preconditions and predicates to describe requirements on the clients of language-defined units, as such a description is both more useful (it is available to tools whereas an English language description is not) and less likely to be misunderstood (by both the implementor and the user).

However, we certainly do not want to require implementations to have to repeat checks in the implementation of a language-defined unit -- the implementer needs to be able to assume that the preconditions and predicates have been checked. (This is why assertions are Checked/Ignored in the originating unit.) For example, we do not want to require an implementation to protect against a cursor being null even though the precondition includes a check that the provided cursor is not null.

Thus, we want to declare that a failed precondition or predicate that has been omitted rather than checked for a language-defined unit makes program execution erroneous. This is of course the semantics of pragma Suppress, so we want to provide check names for the language-defined units.

We do not want to provide too many check names, as that carries an implementation cost, so one name per package is too many. However, a single name for all of the language-defined units (which are quite different in purpose and use) is not enough.

Therefore, we choose to provide one name per subsystem (counting IO as a subsystem). Note that not all of these subsystems currently contain packages with preconditions and predicates. However, we intend to continue to add additional preconditions and predicates in the future, including possibly to existing packages like Ada.Strings.Unbounded and Ada.Text_IO. (This is a compatible change in the case of preconditions.) So we are future-proofing the language by providing all of these names now.

We have not provided names for a handful of single packages: Tags, Assertions, Exceptions, Command_Line, Environment_Variables, and Locales, as well as Unchecked_Conversion and Unchecked_Deallocation. Most of these aren't going to have much in the way of assertions anyway. We could consider grouping Command_Line, Environment_Variables, and Locals into "Target_Assertion_Check" or "Environment_Assertion_Check".

We also don't provide names for any packages defined in Annexes (like Decimal, Dispatching, Execution_Time, and so on).

---

We use <subsystem_name>_Assertion_Check for the name. Two points about that chosen name:

(1) If the subsystem name is plural, we use that plural in the name. We could have used a singular form instead, but that seems weird (especially in the case of Numerics).

(2) We use "check" rather than "checks". While "checks" would make more sense, all of the existing names other than "All_Checks" use "check". Many of the existing names cover multiple vaguely related checks, so we already have many cases of the wrong plurality. Using "checks" for some of these and "check" for others would make it harder for users to know which to use for a particular check.

!corrigendum 11.4.2(23.1/3)

Insert after the paragraph:

It is a bounded error to invoke a potentially blocking operation (see 9.5.1) during the evaluation of an assertion expression associated with a call on, or return from, a protected operation. If the bounded error is detected, Program_Error is raised. If not detected, execution proceeds normally, but if it is invoked within a protected action, it might result in deadlock or a (nested) protected action.

the new paragraph:

!corrigendum 11.5(23)

Insert after the paragraph:

Storage_Check: Check that evaluation of an allocator does not require more space than is available for a storage pool. Check that the space available for a task or subprogram has not been exceeded.

the new paragraphs:

The following checks correspond to situations in which the exception Assertion_Error is raised upon failure of a language-defined check. For a language-defined unit U associated with one of these checks in the list below, the check refers to performance of checks associated with the Pre, Static_Predicate, and Dynamic_Predicate aspects associated with any entity declared in a descendant of U, or in an instance of a generic unit which is, or is declared in, a descendant of U. Each check is associated with one or more units:

Calendar_Assertion_Check: Calendar.

Characters_Assertion_Check: Characters, Wide_Characters, and Wide_Wide_Characters.

Containers_Assertion_Check: Containers.

Interfaces_Assertion_Check: Interfaces.

IO_Assertion_Check: Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, Storage_IO, Streams.Stream_IO, and Directories.

Numerics_Assertion_Check: Numerics.

Strings_Assertion_Check: Strings.

System_Assertion_Check: System.

!corrigendum 11.5(26)

Replace the paragraph:

If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous.

by:

If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. Similarly, if a precondition check has been suppressed and the evaluation of the precondition would have raised an exception, execution is erroneous.

!ASIS

[Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.]

!ACATS test

ACATS B- and C-Tests are needed to check that the new capabilities are supported.

!appendix


From: Randy Brukardt
Sent: Friday, February 1, 2019  7:32 PM

[Part of a thread about AI12-0208-1 - Editor.]

However, you neither addressed nor dismissed my technical concerns over the
11.5(23) wording. At a bare minimum, you need to adjust the wording to mention 
instances of these packages and drop the mention of Type_Invariants (since 
they're treated like Post -- must be True or else). The "Reason"
talks about the non-existent package "Ada.Big_Numbers".

I had suggested totally replacing the 11.5(23) change with the following:

Numeric_Check

Perform the checks associated with the Pre, Static_Predicate, or 
Dynamic_Predicate aspects associated with an entity declared in a descendant 
unit of Numerics or in an instance of a generic unit that is declared in, or 
is, a descendant unit of Numerics.

AARM Reason: One could use the Assertion_Policy to eliminate such checks, but 
that would require recompiling the Ada.Numerics packages (the assertion 
policy that determines whether the checks are made is that used to compile the 
unit). In addition, we do not want to specify the behavior of the Ada.Numerics 
operations if a precondition or predicate fails; that is different than the 
usual behavior of Assertion_Policy.
By using Suppress for this purpose, we make it clear that suppressing a check 
that would have failed results in erroneous execution.

----

But this is way too big a change from me to make without concurrence from 
others. In particular, I don't know if my "subsystem suppression" plan was 
really adopted by the group or if I just invented it and really only the 
containers were approved. (BTW, I think it is likely that I will change the 
containers to use wording like the above, if we go forward with this; the 
containers wording is more targeted to just Pre, as we can't add predicates 
to existing packages. But I'd rather that each such check was described the
same.)

Below is the relevant part of my original message on this topic:

-----

My intent was that there was one such suppression check per subsystem, so this 
would be:

Numeric_Check

Perform the checks associated with Pre, Static_Predicate, Dynamic_Predicate, 
or Type_Invariant aspect specifications occurring in the visible part of 
package Numerics or of any of its descendants.

The idea is that there would also be "String_Check" (for Ada.Strings), 
"Character_Check" (for Ada.Characters), "IO_Check" (for the packages that 
should have been in Ada.IO, Text_IO, Sequential_IO, etc.), "System_Check"
(for System), and "Interface_Check" (for Interfaces). Of course, those only 
matter if we start defining preconditions and the like for them.

----

Type_Invariants are required to be followed by 1.1.3(17.1/5); there's no 
reason to suppress them as they can't fail for a correct implementation (same 
reason we don't include postconditions here). I could see a compiler 
generating them for debugging purposes, but that wouldn't be the standard 
mode (what compiler wants to generate unnecessary code??).

----

Aspect specifications are "associated" with a declaration, it would be clearer 
to use that wording I think (it's certainly closer to the Containers wording).

----

We need to mention instances of generic units here as well. Adapting the 
current wording of the Containers version with all of the above:

Perform the checks associated with the Pre, Static_Predicate, or 
Dynamic_Predicate aspects associated with an entity declared in a descendant 
unit of Numerics or in an instance of a generic unit that is declared in, or 
is, a descendant unit of Numerics.

****************************************************************

From: Tucker Taft
Sent: Saturday, February 2, 2019  7:58 AM

I agree that having a "_Check" name per "subsystem" is a reasonable solution, 
giving roughly the right granularity.  But perhaps we should use plural, 
since these are clearly a pretty broad collection of checks, rather than a 
single check.  And perhaps we should include the word "Assertion" in the name 
since we aren't really suppressing all checks.  Hence:

   Container_Assertion_Checks
   Numeric_Assertion_Checks
   IO_Assertion_Checks
   String_Assertion_Checks

We should probably also try to enumerate all of the interesting subsystem 
check names, even if we don't use them all right away.  The above four were 
about all I could find where there were enough to make it worthwhile.

****************************************************************

From: Steve Baird
Sent: Monday, February 4, 2019  1:28 PM

> However, you neither addressed nor dismissed my technical concerns 
> over the
> 11.5(23) wording. At a bare minimum, you need to adjust the wording to 
> mention instances of these packages and drop the mention of 
> Type_Invariants (since they're treated like Post -- must be True or else). 
> The "Reason" talks about the non-existent package "Ada.Big_Numbers".
> 
> I had suggested totally replacing the 11.5(23) change with the following:

Sorry I overlooked that. Your changes (i.e., moving the focus from Big_Numbers 
to Numerics, as well as eliminating mention of type invariants) look good to 
me.

Tuck's ideas about
>    Container_Assertion_Checks
>    Numeric_Assertion_Checks
>    IO_Assertion_Checks
>    String_Assertion_Checks
also seem reasonable, although perhaps not as part of this AI.

However, if that is the route we are going to go then we don't want to 
unnecessarily introduce eventual compatibility problems here.
We would still need to decide what to do about the existing Container_Check 
if we take this approach, but there is no point in making these compatibility 
issues worse than necessary by choosing a name in this AI that we already 
plan to abandon.

Thoughts?

****************************************************************

From: Tucker Taft
Sent: Monday, February 4, 2019  2:31 PM

I agree with not trying to solve the "_Check" name piecemeal.  We should have 
a separate AI on this issue.

****************************************************************

From: Steve Baird
Sent: Monday, February 4, 2019  3:52 PM

Makes sense, but the question remains of what name to use in this AI.

Corn_Checks?

Which in turn reminds of the sign, copied from one on the wall at a restaurant 
we used to frequent, that was presented to an Ada compiler developer I worked 
with upon reaching some milestone or other:
   No Checks
   No Exceptions

****************************************************************

From: Randy Brukardt
Sent: Monday, February 4, 2019  4:12 PM

> I agree that having a "_Check" name per "subsystem" is a reasonable 
> solution, giving roughly the right granularity.
> But perhaps we should use plural, since these are clearly a pretty 
> broad collection of checks, rather than a single check.  And perhaps 
> we should include the word "Assertion" in the name since we aren't 
> really suppressing all checks.  Hence:
> 
>    Container_Assertion_Checks
>    Numeric_Assertion_Checks
>    IO_Assertion_Checks
>    String_Assertion_Checks
> 
> We should probably also try to enumerate all of the interesting 
> subsystem check names, even if we don't use them all right away.  The 
> above four were about all I could find where there were enough to make 
> it worthwhile.

This makes sense, but:
* You skipped the System and Interfaces subsystems. Yes, they're not 
  subsystems of Ada, but so what? Still might want to suppress stuff in them.
* I couldn't decide whether to use "Container_" or "Containers_" -- note that 
  the subsystem names are plural. I find when writing about this that 
  "Containers_" and "Numerics_" are more natural, even though I proposed other 
  names previously. (I've stuck with the original proposal to avoid
  confusion.)

Note that "Container_Check" is quite correct, in that there are no other 
checks in a container other than the (single, possibly complex) precondition 
(there might be impldef tests associated with bounded errors or erroneous 
execution, but these don't count as "checks" in any case). But that's not 
necessarily true of the other subsystems. So I don't have any objection to 
adding "Assertion_", other than the length.

Also note that Ada uses singular "Index_Check" and "Range_Check" even though 
there are a number of different checks that are covered by each of these. So 
I though that for consistency, the name should be singular. (Either that, or 
all of the names should be changed to be plural -- it seems weird to have a 
half-and-half usage).

Moral: nothing about this is particularly obvious. I'll try to find time to 
write up an AI.

****************************************************************

From: Randy Brukardt
Sent: Monday, February 4, 2019  4:20 PM

...
> However, if that is the route we are going to go then we don't want to 
> unnecessarily introduce eventual compatibility problems here.
> We would still need to decide what to do about the existing 
> Container_Check if we take this approach, but there is no point in 
> making these compatibility issues worse than necessary by choosing a 
> name in this AI that we already plan to abandon.

Existing Container_Check? Do you mean the one in AI12-0112-1 (which is 
infinitely mallable, of course, not having appeared anywhere other than an
RM draft), or the GNAT-defined Container_CheckS?

The latter is irrelevant, as it (a) has a different name, and (b) has 
different semantics than what we are proposing. The only this I care about it 
is that we don't chose exactly the same name as it has, so that we don't get 
a virtual incompatibility with existing uses.

(About (b): the GNAT Container_Checks applies to the instance, and turns off 
checks on all uses of that instance. That's not how suppression typically 
works in Ada, and I have proposed a direct analog to typical suppression, the 
check being suppressed specifically where it appears [in this case, on 
individual calls].)

Anyway, based on this thread, I'm presuming you agree with the need to open a 
specific AI on this topic to supersede AI12-0112-1 and AI12-0208-1 ramblings 
on these points. (I still would prefer that AI12-0208-1 be closer to the 
thinking noted in this thread, but the details aren't critical.)

****************************************************************

From: Steve Baird
Sent: Monday, February 4, 2019  5:41 PM

> Do you mean the one in AI12-0112-1 (which is infinitely mallable, of 
> course, not having appeared anywhere other than an RM draft),

Yes, but I forgot how recently that was introduced.

****************************************************************

Questions? Ask the ACAA Technical Agent