Version 1.2 of ai12s/ai12-0079-2.txt

Unformatted version of ai12s/ai12-0079-2.txt version 1.2
Other versions for file ai12s/ai12-0079-2.txt

!standard 6.1.2(0)          20-01-13 AI12-0079-2/01
!class Amendment 19-10-05
!status work item 19-10-05
!status received 19-10-05
!priority High
!difficulty Hard
!subject Global-in and global-out annotations
!summary
Annotations are provided to describe the use of global objects by subprograms, entries, tasks, and protected units.
!problem
Here is the original problem statement:
Ada 2012 added many kinds of assertions to Ada in order to increase the ability of a programmer to specify contracts for types and subprograms. These contracts are defined to be checked at runtime, but are intended to be potentially checked (at least in part) statically.
However, without knowledge of side effects of functions used in the aspects, a tool has to assume the worst about any user-defined functions. For example, that the result of a function can change even when called with the same operands. Other assumptions could cause incorrect programs to be accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution. Both of these results are unacceptable for a feature intended to improve the correctness of programs.
The worst-case assumptions pretty much prevent any analysis unless the bodies of any user-defined functions used in the aspects are available. This is troublesome, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body requires creating implicit body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again).
Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side effects is needed in the specification of subprograms in order to accomplish that goal.
---
Additional challenges addressed in this version of the AI:
Simplify the proposal, at least in the core, so few if any Global aspects need to be specified by the typical user. Provide a way for more advanced users to impose on themselves stricter requirements should they so choose, but minimize the burden on programmers who want to use the new features of Ada 202X without worrying about Global specifications. Allow more sophisticated implementations, like the SPARK tools, to do additional analysis without requiring the user to specify explicitly all of the Global effects. In so far as possible, achieve compatibility with use of Global in existing SPARK code, so that no significant change in syntax or semantics is required for existing SPARK code to make it Ada 202X compatible.
!proposal
** TBD. Similar to AI12-0079-1 and it's later fixups (AI12-0240-6 [overriding], AI12-0303-1, AI12-0310-1, and AI12-0334-2), but with some in the core and some in an annex.
!wording
Add the following section:
6.1.2 The Global and Global'Class Aspects
For a subprogram, an entry, a named access-to-subprogram type, a task unit, a protected unit, or a library package or generic package, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
Global
The syntax for the aspect_definition used to define a Global aspect is as follows:
global_aspect_definition ::=
NULL
| Unspecified | global_group_designator | global_mode global_designator | (global_aspect_element{, global_aspect_element}) | extended_global_aspect_definition -- see H.7
global_aspect_element ::= global_mode global_set | extended_global_aspect_element -- see H.7
global_mode ::= [ overriding ] basic_global_mode | implementation_defined_mode
basic_global_mode ::= in | in out | out
global_set ::= global_designator {, global_designator}
global_designator ::= global_group_designator | global_name
global_group_designator ::= all | synchronized | aliased
global_name ::= /object_/name | /package_/name
The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) global to an operation, task unit, or protected unit, that are potentially read or updated as part of the execution of the operation or of the execution of the body of the task or a protected operation of the protected unit. Constants of any type may also be mentioned in a Global aspect. if not specified or otherwise defined below, the aspect defaults to the Global aspect for the enclosing library unit if the entity is declared at library level, and to Unspecified otherwise. if not specified for a library unit, the aspect defaults to Global => null for a library unit that is declared Pure, and to Global => Unspecified otherwise.
For a dispatching subprogram, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
Global'Class
The syntax for the aspect_definition used to define a Global'Class aspect is the same as that defined above for global_aspect_definition. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the dispatching subprogram.
Name Resolution Rules
A global_name shall resolve to statically denote an object or a package (including a limited view of a package).
Static Semantics
A global_aspect_definition defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side effect of executing the operation(s) associated with the entity. The Global'Class aspect associated with a dispatching operation of type T represents a restriction on the Global aspect on a corresponding operation of any descendant of type T.
The Global aspect for a callable entity defines the global variables that might be referenced as part of a call on the entity, including any assertion expressions that might be evaluated as part of the call, including preconditions, postconditions, predicates, and type invariants.
The Global aspect for an access-to-subprogram object (or subtype) identifies the global variables that might be referenced when calling via the object (or any object of that subtype) including assertion expressions that apply.
For a predefined operator of an elementary type, or the function representing an enumeration literal, the Global aspect is NULL. For a predefined operator of a composite type, the Global aspect of the operator defaults to that of the enclosing library unit (unless a Global aspect is specified for the type -- see H.7).
The following is defined in terms of operations; the rules apply to all of the above kinds of entities.
The global variables associated with any global_mode can be read as a side effect of an operation. The IN OUT and OUT global_modes together identify the set of global variables that can be updated as a side effect of an operation. The presence of the reserved word OVERRIDING indicates that the specification is overriding the mode of a formal parameter with another mode to reflect the overall effect of an invocation of the callable entity on the state associated with the corresponding actual parameter.
An implementation-defined global_mode may be specified, which limits the use of the global objects to which it applies according to an implementation-defined rule.
The overall set of objects associated with each global_mode includes all objects identified for the mode in the global_aspect_definition.
A global_set identifies a global variable set as follows:
* ALL identifies the set of all global variables;
* ALIASED identifies the set of all aliased variables, which includes any dereference of a value of an access-to-object type;
* SYNCHRONIZED identifies the set of all synchronized variables (see 9.10), as well as variables of a composite type all of whose non-discriminant subcomponents are synchronized;
* global_name{, global_name} identifies the union of the sets of variables identified by the global_names in the list, for the following forms of global_name:
+ /object_/name that is not associated with an OVERRIDING mode identifies the specified global variable (or constant);
+ /object_/name that is associated with an OVERRIDING mode identifies the variable parts associated with the specified formal parameter whose parameter mode is being overridden;
+ /package_/name identifies the set of all variables declared in the private part or body of the package or of a descendant of the package, or anywhere within a private descendant of the package.
Legality Rules
Within a global_aspect_definition, a given global_mode shall be specified at most once. Similarly, within a global_aspect_definition, a given entity shall be named at most once by a global_name.
If an entity (other than a library package or generic package) has a Global aspect other than Unspecified or IN OUT ALL, then the execution of the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the IN, IN OUT, or OUT modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the IN OUT or OUT global_modes. This includes any possible Global effects of calls occurring during the execution of the operation, except for the following excluded calls:
* calls to formal subprograms;
* calls associated with operations on formal subtypes;
* calls through formal objects of an access-to-subprogram type;
* calls through access-to-subprogram parameters;
* calls on operations with Global aspect Unspecified.
The possible Global effects of these excluded calls (other than those that are Unspecified) are taken into account by the caller of the original operation, by presuming they occur at least once during its execution. For calls that are not excluded, the possible Global effects of the call are those permitted by the Global aspect of the associated entity, or by its Global'Class aspect if a dispatching call.
AARM Ramification: For a predefined equality operator of a composite type, the possible Global effects includes those of the equality operations called by the operator (which might not be predefined and thus might have a different Global specification than the component types).
For the purposes of these checks:
* if a formal parameter P of a callable entity C is of an anonymous access-to-object type, no check against the Global aspect occurs within C for the dereference of P, but a check against the Global aspect applies at the point of call of C, presuming that P is dereferenced at least once and then read if of an access-to-constant type or updated if of an access-to-variable type; if the actual parameter is of the form X'Access (explicitly or implicitly), then at the point of call the presumed dereference of P is treated as a read or update of X; if the actual parameter A is of any other form, it is treated as a read or update of A.all;
AARM Ramification: An access parameter ACCESS T is treated somewhat like a parameter specified as IN OUT T while access constant T is treated somewhat like IN T. There is no burden to mention the dereference of an access parameter in the Global aspect, as the effects of the dereference are presumed at the call site, just like the effects on “normal” parameters.
* if a function returns an object of a type for which the Implicit_Dereference aspect is True (see 4.1.5), or an object of an anonymous access-to-object type, the Global aspect of the function shall reflect the effects of dereferencing the result of the function, if these are over and above reads or updates of parts of aliased formal parameters (or dereferences of access parameters) passed to the function. The effects to be reflected include reading the designated object, and updating the designated object in the case of an access-to-variable result or an Implicit_Dereference result with an access-to-variable access discriminant. A dereference (explicit or implicit) of a function_call on such a function is not further checked at the point of call against any Global or Global'Class aspects that apply to the caller.
AARM Reason: The function is in a better position than the caller to enumerate the objects affected by dereferencing the result. Because the access discriminant is often of an anonymous type, there is no other place to declare these effects. In most cases, these effects will already be reflected in the aliased or access parameters passed to the function, so nothing need be added to the Global aspect for these.
AARM Ramification: The last sentence is talking specifically about dereferences associated directly with a function_call. Other dereferences (such as those associated with a rename of a call, or an allocated result of a call) are not included — they have to be covered in the Global or Global'Class aspect in the normal way.
* if an object of a pool-specific access-to-object type is dereferenced within an operation, and the dereference would violate the restrictions inherent in a Global aspect applicable to the operation, the dereference is nevertheless permitted under the following circumstances:
+ the pool-specific access type is declared within the private part or body of an enclosing package;
+ the dereferenced object:
* is a part of a formal parameter of the operation whose mode (after any overriding) would allow the operation performed on the dereference;
* is a part of a dereference of an object that satisfies these same circumstances; or
* is a local object of the operation all of whose assignments are from an object that satisfies these same circumstances.
AARM Ramification: This exemption of Global checks for dereferences of pool-specific access-to-object values is intended to allow the typical case where a private type uses multiple objects connected internally with access values to represent a single logical object. Here we allow the operation if the access value is reached from a formal parameter whose parameter mode would have allowed the operation. We give an implementation permission below to extend these exemptions to other dereferences based on additional analysis (such as that provided by newer versions of SPARK).
If an implementation-defined global_mode applies to a given set of objects, an implementation-defined rule determines what sort of references to them are permitted.
For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the IN OUT mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of T, unless the aspect of that ancestor is Unspecified.
Implementation Permissions
For a call on a subprogram that has a Global aspect that indicates that there are no references to global variables, the implementation may omit the call:
* if the results are not needed after the call; or
* simply reuse the results produced by an earlier call on the same subprogram, provided that none of the parameters nor any object accessible via access values from the parameters have any part that is of a type whose full type is an immutably limited type, and the addresses and values of all by-reference actual parameters, the values of all by-copy-in actual parameters, and the values of all objects accessible via access values from the parameters, are the same as they were at the earlier call.
[Redundant: This permission applies even if the subprogram produces other side effects when called.]
AARM Discussion: This permission doesn't really allow a compiler to do anything that it couldn't do anyway (as any optimization that gives the required semantics for program executions that aren't erroneous is always allowed), but we considered it important to make Ada programmers aware that such optimizations are possible. Specifically, an implementation can trust the information given in a Global aspect, as any subprogram that violates it is either illegal or would result in erroneous execution. Specifically, the Global contract can be violated by erroneous execution resulting from dereferencing a dangling reference (see 13.11.2), by giving an incorrect contract on an interfaced subprogram (see B.1), by specifying the address of a global object for a local object (see 13.1), or by using Unchecked_Conversion (see 13.9) or Address_to_Access_Conversions (see 13.7.2) to create local accesses to global objects.
Since optimizations like these don't require a special permission, implementations can also use similar optimizations that go beyond the permission above. For instance, if there are two calls with the same parameters on a subprogram whose Global aspect only indicates reading of a global object G, then the second call can be omitted and reuse the result of the first call if the compiler can prove (with the help of the Global aspect of any subprograms called) that G is not written to between the calls.
Implementations may perform additional checks on calls to operations with an Unspecified Global aspect to ensure that they do not violate any limitations associated with the point of call.
AARM Discussion: In this sense, Global => Unspecified is not permission to violate the caller's Global restrictions. It is rather that the implementor of the subprogram is presuming other means are being used to ensure safety. Note the No_Unspecified_Globals Restriction (H.4) to prevent the use of Unspecified with the Global aspect in a given partition.
Implementations may provide additional (or fewer) exemptions to Global aspect checks on dereferences based on additional analysis of safety.
Implementations may extend the syntax or semantics of the Global aspect in an implementation-defined manner.
AARM Reason: This is intended to allow preexisting usages from SPARK 2014 to remain acceptable in conforming implementations, as well as to provide flexibility for future enhancements. Note the word “extend” in this permission; we expect that any aspect usage that conforms with the (other) rules of this clause will be accepted by any Ada implementation, regardless of any implementation-defined extensions.
NOTES
7 For an example of the use of these aspects and attributes, see the
Vector container definition in A.18.2.
----
Add after H.4 (23):
No_Unspecified_Globals
No library-level entity shall have a Global aspect of Unspecified, either explicitly or by default. No library-level entity shall have a Global'Class aspect of Unspecified, explicitly or by default, if it is used as part of a dispatching call.
AARM Ramification: Global'Class need not be specified on an operation if there are no dispatching calls to the operation, or if all of the dispatching calls are covered by dispatching_operation_specifiers for operations with such calls (see H.7).
Add the following section:
H.7 Extensions to Global and Global'Class Aspects
In addition to the entities specified in 6.1.2, the Global aspect may be specified for a subtype (including a formal subtype), formal package, formal subprogram, and formal object of an anonymous access-to-subprogram type.
The following additional syntax is provided for specifying Global and Global'Class aspects, to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation:
extended_global_aspect_definition ::= use formal_parameter_designator | do dispatching_operator_specifier
extended_global_aspect_element ::= use formal_parameter_set | do dispatching_operation_set
formal_parameter_designator ::= formal_group_designator | formal_parameter_name
formal_parameter_set ::= formal_group_designator | formal_parameter_name{, formal_parameter_name}
formal_group_designator ::= null | all
formal_parameter_name ::= /formal_/subtype_mark | /formal_subprogram_/name | /formal_access_to_subprogram_object_/name
dispatching_operation_set ::= dispatching_operation_specifier{, dispatching_operation_specifier}
dispatching_operation_specifier ::= /dispatching_operation_/name (/object_/name)
Name Resolution Rules
A formal_parameter_name shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type.
The /object_/name of a dispatching_operation_specifier shall resolve to statically denote an object (including possibly a formal parameter) of a tagged class-wide type T'Class; the /dispatching_operation_/name of the dispatching_operation_specifier shall resolve to statically denote a dispatching operation associated with T.
Static Semantics
The extended_global_aspect_definition and extended_global_aspect_element can be used to define as part of the Global aspect the *formal parameter set* and the *dispatching operation set* used within an operation. The formal parameter set is identified by a set of formal parameter names after the reserved word USE. Alternatively, the reserved word NULL may be used to indicate none of the generic formal parameters, or ALL to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) might be used within the execution of the operation. If there is no formal parameter set specified for an operation declared within a generic unit, it defaults to USE ALL.
The dispatching operation set is identified by a set of dispatching_operation_specifiers after the reserved word DO. It indicates that the Global effects of dispatching calls that match one of the specifiers need not be accounted for by other elements of the Global aspect, but are instead to be accounted for by the invoker of the operation. A dispatching call matches a dispatching_operation_specifier if the prefix of the call statically denotes the same operation(s) as that of the dispatching_operation_specifier, and at least one of the objects controlling the call is denoted by a name that statically denotes the same object as that denoted by the /object_/name of the dispatching_operation_specifier. In the absence of any dispatching_operation_specifiers, all dispatching calls within the operation are presumed to have the effects determined by the set of Global'Class aspects that apply to the invoked dispatching operation.
The Global aspect for a subtype identifies the global variables that might be referenced during default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. If not specified for the first subtype of a derived type, the aspect defaults to that of the ancestor subtype; if not specified for a nonderived first subtype the aspect defaults to that of the enclosing library unit. If not specified for a nonfirst subtype S, the Global aspect defaults to that of the subtype identified in the subtype_indication defining S.
The Global'Class aspect may be specified for the first subtype of a tagged type T, indicating an upper bound on the Global aspect of any descendant of T. If not specified, it defaults to Unspecified.
Legality Rules
For a tagged subtype T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the in out mode, of the Global'Class aspect of the first subtype of any ancestor of T.
If the formal parameter set is anything but ALL in the Global aspect for an operation declared within a generic unit, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set.
Any dispatching call occurring within the operation that does not match a dispatching_operation_specifier is checked using the Global'Class aspect(s) applicable to the dispatching operation; if there is a match, there is no checking against other elements of the Global aspect(s) applicable at the point of call.
!discussion
Global annotations are critical to being able to perform any sort of modular static analysis.
The intent is that all of the global IN, IN OUT, OUT, USE, and DO annotations proposed can be statically checked.
This new version of this AI incorporates changes defined by AI12-0240-6 (overriding), AI12-0303-1 (mutable constants), AI12-0310-1 (package private part), and AI12-0334-2 (subtypes and predicates).
In this new version, we have dropped the notion of a Global attribute (i.e. X'Global) in favor of somewhat different defaults, and have incorporated more precise forms of Global aspect elements (USE ... and DO ...) into the High-Integrity Annex H where they need not be supported in initial implementations of the new standard. We have also added a restriction in H.4 to allow users to disallow use of the new Unspecified value for the Global aspect for any library-level entities. We allow Global specifications on packages or generic packages only if they are library units, analogous to the same limitation of where Pure can be specified, to establish a default for library-level entities. More details on the new defaults are detailed below. The overall goal is that a programmer who specifies nothing gets something reasonable. Another goal is that existing SPARK programs use of Global should be acceptable largely as is, except for the slight change in syntax to use reserved words "IN" and "OUT" rather than the non-reserved "Input", "In_Out", and "Output" currently used in the SPARK Global aspect. In any case, a compiler could accept both the old syntax and the new syntax, as they are unambiguously distinguishable at compile time.
The most critical new "default" in this new version is that entities not within a declared-pure library unit, or not at library-level, have Unspecified as their default Global aspect. This effectively implies that the caller may assume the best, but no checking is necessarily being performed at the point of call (though implementations are permitted to effectively inline the call to do additional checks). We provide a restriction of No_Unspecified_Globals in Annex H to allow a user to disallow any library-level entities with Global => Unspecified within a partition. Note that for non library-level entities, even if their own Global aspect is Unspecified, they must still honor any Global aspects of lexically enclosing entities, if these entities have an explicit or implicit Global aspect other than Unspecified. For example, a nested subprogram with Global => Unspecified still cannot violate the Global aspect of its enclosing subprogram, so if the enclosing subprogram specifies Global => SYNCHRONIZED, the nested subprogram cannot reference a variable that is global to its enclosing subprogram unless it is synchronized. It may reference variables local to its enclosing subprogram with no restrictions.
The next critical new "default" is that entities declared within a generic unit are presumed to make use of all generic formal parameters associated with any enclosing generic unit, while not worrying about any of the possible Global effects of that usage in their Global aspect. These additional effects are handled at the point of instantiation, rather than at the point of definition of the generic, much in the same way that "purity" of an instantiation is determined by a combination of the "purity" of the generic and the purity of the actual parameters to the generic. In annex H, we provide ways to specify upper bounds on the effects of generic formal parameters, and we provide an ability to limit which generic formal parameters are actually used within an entity defined within a generic unit (USE formal_parameter_name, ...). This allows us to say that all entities declared at library level within a declared-pure library unit default to Global => null, even if they are within a generic unit, because the USE => ALL is implicit for such entities.
The final critical new "default" is that private types are presumed to be "Compound" in the sense that any components of a pool-specific access type declared in the same private part are presumed to be "Internal" to the type, and only give access to other elements of the same conceptual Compound object. Visible access types, and general access types (as opposed to pool-specific ones) are never considered to be "Internal" and any dereference of such an access value is presumed to reference some aliased object which might not be part of the current conceptual "Compound" object and must be accounted for in the Global aspect of the operation. We give an implementation permission to allow other special cases of dereferences to be exempted from normal checks, based on additional analysis.
We have also included in Annex H an ability to specify that certain dispatching calls might be performed as part of the execution of an entity, allowing the invoker to more precisely deal with the possible effects of such a call, rather than the entity itself having to fall back on the Global'Class effects, which are likely to be very pessimistic, if specified at all.
Some overal notes on the above:
This version of this AI was based on work done by Tuck and Claire to reach some kind of simpler consensus position on Global. Probably the biggest change that came from that work was the introduction of the notion of Global => Unspecified to better match existing SPARK usage where few if any Global specifications are required. We have coupled that with a restriction No_Unspecified_Globals to accommodate those users who want to impose on themselves a requirement to specify Global, explicitly or implicitly, at least on all library-level entities. A related change was to move concerns about use of generic formals to the point of instantiation, so operations in a "pure" generic unit can be (implicitly or explicitly) simply "Global => null".
The additions relative to the consensus report are very few, and are justified based on a strong belief we need to ensure that even if very imprecise, the Global aspect can be presumed to be an over approximation of the true set of global effects. This led us to add ALIASED as an option, to cover all dereferences of general access types without going all the way to ALL. We also held on to a way to establish an overall default, but we now limit it to a library unit as a whole, as that is the level at which Pure can be declared, and the default only applies to library-level elements, not to any non library-level declarations. Non library-level entities always default to Global => Unspecified, but we believe that that is not a significant loss in functionality, as these nested entities must still abide by any Global aspect of their enclosing library-level entity.
We have exempted certain dereferences of pool-specific access values from being accounted for in the Global aspect. We do not require any special aspect specifications to make use of these exemptions. We only require that the access type be declared in a private part or a body, and that any dereference be reachable from a formal parameter whose parameter mode allows for the operation performed on the dereference. This meets the expressed goal that existing code that "does the right thing" as far as using access types for implementing abstract data types does not need any additional aspect specifications and can still specify a Global aspect of NULL on primitive operations of the abstract data type.
We have eliminated the need for a Global attribute (X'Global) and moved all functionality that depended on that into Annex H. We have ensured that the functionality in the Annex is optional in the sense that it only adds precision; it doesn't provide critical functionality for typical use. Certain of the language-defined packages (such as those related to streaming) might use these features to describe their effects more precisely, but implementations that do not support these Annex H features can choose how to reflect the Global effects of these language-defined packages in a way that is appropriate to typical usage patterns.
!example
** TBD.
!ASIS
** TBD.
!ACATS test
ACATS tests should be created to test that the new annotations are correctly enforced.
!appendix

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

Questions? Ask the ACAA Technical Agent