!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 WG9 Approved 22-06-22 !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 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, or in an instance of a generic unit which is, or is declared in, a descendant of @i. 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 _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) @dinsa 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. @dinst 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. !corrigendum 11.5(23) @dinsa @xhang<@xterm Check that evaluation of an @fa 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.> @dinss @xbullet 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, or in an instance of a generic unit which is, or is declared in, a descendant of @i. Each check is associated with one or more units:> @xhang<@xtermCalendar.> @xhang<@xtermCharacters, Wide_Characters, and Wide_Wide_Characters.> @xhang<@xtermContainers.> @xhang<@xtermInterfaces.> @xhang<@xtermSequential_IO, Direct_IO, Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, Storage_IO, Streams.Stream_IO, and Directories.> @xhang<@xtermNumerics.> @xhang<@xtermStrings.> @xhang<@xtermSystem.> !corrigendum 11.5(26) @drepl If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. @dby 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. ****************************************************************