Version 1.5 of ai05s/ai05-0186-1.txt

Unformatted version of ai05s/ai05-0186-1.txt version 1.5
Other versions for file ai05s/ai05-0186-1.txt

!standard 13.3.4 (0)          10-02-01 AI05-0186-1/04
!class amendment 09-11-02
!status work item 09-11-02
!status received 09-11-02
!priority Medium
!difficulty Medium
!subject Global-in and global-out annotations
!summary
Annotations are provided to describe the use of global objects by subprograms.
!problem
We're considering adding many kinds of annotations to Ada (see AI05-0145-1 and AI05-0146-1) 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 annotations, a tool has to assume the worst about any user-defined functions. That is, 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" annotations, 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 annotations are available. This is bad, 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 require creating pseudo body dependencies (if the body is changed, any analysis depending on that properties of that body would have to be performed again); but the language does not allow these to be "real" body dependencies (any recompilation needed has to occur automatically).
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.
!proposal
Add global in and global out annotations to Ada, for subprograms, packages, and types. Add related annotations for dispatching subprograms and access-to-subprogram types.
The global annotations for types cover default initialization/adjustment/finalization. The global annotations for packages cover operations that occur as part of the elaboration for packages.
!wording
Add a new section:
13.3.4 Global usage annotation
Semi-formal description: [Editor's note: This part depends heavily on the unfinished AI05-0183-1; it's not worth trying to describe these rules until that AI is finished.]
Add to the aspect syntax given in AI05-0183-1:
Aspect_Mark [in|out|in out] => Annotation_List
Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
Annotation_Item ::= object_name | access_subtype_mark |
NULL | ACCESS subtype_mark | OTHERS [IN packagename] | GENERIC formal_parameter_name
The names in these items resolve with the same visibility as other aspect expressions (that usually is the end of the visible part). The names must resolve without context.
[Editor's note: We need the keyword GENERIC here, so that we can tell the difference between references to the initialization and the referenced data for formal pool-specific access types in annotations. Both use the access type name. An alternative would be to add a keyword to the access_subtype_mark case instead, but nothing that isn't ambiguous seems appropriate. My best idea was access_subtype_mark.ALL .]
Aspect_Mark in out => Annotation_List is semantically equivalent to Aspect_Mark in => Annotation_List, Aspect_Mark out => Annotation_List.
AARM Discussion: All of the rules are defined in terms of "Aspect_Mark in" and "Aspect_Mark out". The rules are applied twice (once for "in" and once for "out") to "Aspect_Mark in out".
Aspects Global, Global'Class, and Global'Access are defined.
[End semi-fomal description. From here to the end is intended to be actual wording.]
Static Semantics
A read or write of an object O is covered by an annotation in an Annotation_List if:
* O statically denotes a part of an object named in the Annotation_List;
* The annotation item OTHERS without a package name occurs in the list;
* The annotation item OTHERS with a package name P occurs in the list, and O denotes part of an object declared in P, or O denotes a part of an object produced by a dereference of an object of an pool-specific access type whose pool is declared in P;
* O denotes a part of an object produced by a dereference of an object with designated type T, and the type D given in an ACCESS D annotation item covers T; or
* O denotes a part of an object produced by a dereference of an object of a pool-specific access type named in the Annotation_List.
AARM Ramification: OTHERS by itself allows anything to be read or written.
AARM Discussion: ACCESS D represents reading/writing of any aliased or tagged object (including those allocated from pools) with a type covered by the type D.
"Statically denotes" does not include dereferences, so the first rule only applies to statically declared objects.
An annotation A1 is compatible with another annotation A2 if:
* A1 contains NULL; or
* A2 contains the annotation item OTHERS without a package name; or
* All of the following must be true: -- Each object_name in A1 is covered by an annotation item in A2 or is
an object that would not need to be included in A1 if it was explicitly referenced within the entity defining A1;
AARM Reason: The latter part means that local objects in a subprogram S do not need to be included its annotation when they are included in the annotation for a nested subprogram of S that S calls.
-- Each formal_parameter_name item in A1 is found in A2; -- Each access_subtype_mark item in A1 is found in A2 or, if the
the subtype_mark denotes a pool-specific access type, an OTHERS annotation item in A2 naming the package P in which the pool of the access type is declared; and
-- For each OTHERS annotation item with a package name P, there is
an OTHERS annotation item in A2 that statically denotes P.
AARM Ramification: This definition is not symmetrical; A2 may allow more than A1 requires (such as having an annotation of (others)).
A type T is compatible with an annotation A of an aspect if:
* T is a generic formal type, and A contains the *formal_parameter_*name of the formal type; or
* The annotation for the same aspect of T is compatible with A.
The result of a union of annotation A1 with annotation A2 is:
* if A1 contains NULL, A2;
* if A2 contains NULL, A1;
* if either A1 or A2 contains an OTHERS annotation without a package name, an annotation with a single item of OTHERS without a package name;
* Otherwise, an annotation with all of the Annotation_Items of A1 and A2 with any duplicates removed.
AARM Ramification: This definition is symmetrical; the order of the operands does not matter.
Unless otherwise specified (either explicitly or defined by this International Standard), the annotation for each defined aspect is (others).
AARM Ramification: (others) allows all global references, so it is completely compatible with earlier versions of Ada.
An inherited subprogram (see 3.4) inherits the annotations of the primitive subprogram of the parent or progenitor type. Redundant[The annotations can be changed on an overriding subprogram, with some restrictions.]
When determining the Global in annotations of entities declared in an instantiation of a generic G, each formal_parameter_name item F of every Global in annotation A of any entities declared in the instance that references a formal parameter of G is removed from A and:
* if F is a formal type, the result is the union of A and the Global in annotation of the actual type;
* if F is a formal subprogram, the result is the union of A and the Global in annotation of the actual subprogram;
* if F is a formal IN OUT parameter, the *object_*name of the actual parameter is added to A if that object_name would need to be included in a Global in annotation for the enclosing entity when it is read at the point of the instance, Redundant[and nothing is added otherwise].
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
AARM Discussion: At the point of an instance, all of the references to the formal parameters are replaced by the annotations of the actual. This does not require re-analyzing the generic.
Legality Rules
An annotation_list can be given if and only if the aspect is Global, Global'Class, or Global'Access.
The aspect Global shall be given only on subprograms, types, packages, and generic packages.
The aspect Global'Access shall be given only on access-to-subprogram types.
The aspect Global'Class shall be given only on primitive subprograms of a tagged type.
The Annotation_Item NULL shall appear alone in an Annotation_List.
An object_name given in an Annotation_List shall statically denote some object.
An access_subtype_mark given in an Annotation_List shall denote a pool-specific access type.
A formal_parameter_name given in an Annotation_List shall statically denote some generic formal parameter of an enclosing generic unit; the formal parameter shall be a formal type, a formal subprogram, or a formal IN OUT object.
If a subprogram contains a Global in annotation, then:
* Every object that is read by the subprogram body shall either be accessible from the function call, be a constant object of an elementary type, or be covered by the Global in annotation.
* The subprogram corresponding to each dispatching call in the subprogram body which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call of a dereference of an access value shall have a compatible Global'Access in annotation; the formal_parameter_name for each call of a formal subprogram is present in the annotation; and the subprogram corresponding to every other call in the subprogram body shall have a compatible Global in annotation.
* The type of every stand-alone object declared by the subprogram shall be compatible with the annotation.
* Every nested package and package instantiation declared by the subprogram shall have a compatible Global in annotation.
* The type of each assignment_statement in the subprogram body shall be compatible with the annotation. In addition, if the target of the assignment_statement is a dereference of some access type A, the Allocate and Deallocation routines associated with the storage pool of type A in the subprogram body shall have a compatible Global in annotation.
AARM Reason: Allocate and Deallocate can be called here if the implementation chooses; we have to assume the worst.
* The Allocate and Deallocate routines associated with the storage pool for the type of each allocator in the subprogram body shall have compatible Global in annotations.
AARM Reason: Again, Deallocate can be called here if the implementation chooses; we have to assume the worst.
* For each attribute A'Storage_Size in the subprogram body where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* If the subprogram contains a call on an instance of Unchecked_Conversion with a pool-specific access type A as the target type, the subprogram is illegal if the type A is named as an access_subtype_mark annotation item.
AARM Reason: We assume that objects of type A can only designate objects in the pool of A. The only way to violate this is to use Unchecked_Conversion from a general access type value; if such a conversion exists, we require the subprogram to be annotated as if A is a general access type.
AARM Ramification: Local objects, elementary constant objects (declared anywhere) and the parameters of the call do not need to appear in a Global in annotation. Note that this is referring to constant objects, not just constant views of an object.
A write of a dereference of an object P reads the object P (and writes the designated object).
The prefix of a protected function call is considered to be read; the prefix of a protected procedure or entry call is considered to be both read and written. The prefix of a task entry is considered to be read. These rules follow from the requirements in 9.5 on whether or not the prefix of a protected subprogram call or an entry call can be a constant; we don't want to be logically writing constants. End AARM Ramification.
AARM Discussion: We don't need a rule for Deallocate calls in Unchecked_Deallocation, as it is a call and does not have annotations defined. Thus the above rule will always fail and thus we don't care about the annotations on Deallocate. End AARM Discussion.
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
[Editor's note: I don't want to duplicate the rules, they're complex enough as it is.]
For an attribute P'Access of access-to-subprogram type S that has a Global'Access in annotation, subprogram P shall have a compatible Global in annotation. Similarly, for a type S that has a Global'Access out annotation, subprogram P shall have a compatible Global out annotation.
[Editor's note: One could argue that this belongs in 3.10.2; I put it here to keep all of the relevant rules together.]
Redundant[Global'Class annotations provide annotations for dispatching calls.] The Global in annotation of a subprogram shall be compatible with the Global'Class in annotation of the subprogram; similarly Global out annotation of a subprogram shall be compatible with the Global'Class in annotation of the subprogram.
AARM Ramification: The Global'Class annotations have to allow the same or more than the Global annotations, as they apply to all overriding subprograms as well.
For each primitive subprogram P of a tagged type that overrides another primitive subprogram PP of the type:
* If PP has a Global'Class in annotation, the annotation shall be compatible with the Global'Class in annotation for P. The Global in annotation for P shall be compatible with the Global'Class in annotation for PP.
* If PP has a Global'Class out annotation, the annotation shall be compatible with the Global'Class out annotation for P. The Global out annotation for P shall be compatible with the Global'Class out annotation for PP.
If a type includes a Global in annotation:
* If the full type is composite, the type of each component shall be compatible with the annotation.
* If the full type is controlled, the associated Initialize and Finalize routines shall have compatible Global in annotations.
* If the full type is controlled and not limited, the associated Adjust routine shall have a compatible Global in annotation.
* If the full type is composite, for each default expression E for a component of the type:
* every object that is read by E shall be a constant object of an elementary type, or be covered by the Global in annotation; and
* the subprogram corresponding to each dispatching call in E which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call in E of a dereference of an access value shall have a compatible Global'Access in annotation; the formal_parameter_name for each call of a formal subprogram in E is present in the annotation; the subprogram corresponding to every other call in E shall have a compatible Global in annotation; and
* the Allocate routine associated with the storage pool for the type of each allocator in E shall have a compatible Global in annotation.
* The Allocate and Deallocate routines associated with the storage pool for the type of each allocator in E shall have compatible Global in annotations.
* For each attribute A'Storage_Size in E where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* If the full type is a task type, the rules for a subprogram body (given previously) shall be applied to the task body and the Global in annotation.
[We do not need to worry about assignment, stand-alone objects, and instances here, none of those are possible inside of types, other than task bodies, which we handle by requiring the rules of a subprogram body to be checked.]
AARM Note: Adjust really doesn't belong here, but it seems to be overkill to have a special kind of annotation just for it (and composition means that trying to define it directly would be a mess - composition happens automatically for the above rules). In practice, Adjust and Finalize are usually very similar in design, and are likely to depend on the same set of globals, so this isn't much of a limitation.
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
If a package or generic package includes a Global in annotation:
* For each expression or call E in every declarative_item (but not including those in nested units) and the sequence of statements of the package body:
* every object that is read by E shall be declared in the package, a constant object of an elementary type, or be covered by the Global in annotation; and
* the subprogram corresponding to each dispatching call in E which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call in E of a dereference of an access value shall have a compatible Global'Access in annotation; the formal_parameter_name for each call of a formal subprogram is present in the annotation; the subprogram corresponding to every other call in E shall have a compatible Global in annotation; and
* the Allocate routine associated with the storage pool for the type of each allocator in E shall have a compatible Global in annotation.
* The Allocate and Deallocate routines associated with the storage pool for the type of each allocator in E shall have compatible Global in annotations.
* For each attribute A'Storage_Size in E where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* The type of every stand-alone object declared by the package shall be compatible with the annotation.
* Every nested package and package instantiation declared by the package shall have a compatible Global in annotation.
* The type of each assignment_statement in the sequence_of_statements of the package body shall be compatible with the annotation. In addition, if the target of the assignment_statement is a dereference of some access type A, the Allocate and Deallocation routines associated with the storage pool of type A in the subprogram body shall have a compatible Global in annotation.
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
** Wording TBD:
I hate the duplication of rules here. I tried and tried to find some way to eliminate the duplication for expressions and calls (for which most of the rules apply). But I continually got stuck by the fact that there are essentially 3 parameters: the expression E; the accessibility/locality of objects to exclude (that is, the definition of what is local is different for subprograms [we need to include the parameters], packages [we need to exclude anything outside of the package, even though at the same accessibility level, as packages are invisible to accessibility], and types [locals only for tasks, and nothing special needed otherwise]; and the kind of annotation (either "in" or "out"). It's just too much to do in any understandable way. And I couldn't find a way to factor out the accessibility without getting overlapping rules. Maybe someone else has a better idea.
** End Wording TBD.
[Generic rules; these apply to the entire Legality Rules section]
In addition to the places where Legality Rules normally apply, these rules also apply in the private part of an instance of a generic unit.
For the purposes of enforcing these rules in a generic body, the Global annotations on the storage pool operations for formal access types are assumed to be (others). The Global annotations on generic formal elementary types are assumed to be (null).
[This last paragraph is not talking about inside of instances; rechecking is done there with the actual annotations. This is the assume-the-worst rule needed in generic bodies. We can assume the (null) for formal elementary types because no elementary type can have a "significant" default initialization; and the actual has to be known to be elementary. Note that an elementary type could have some other annotations that are explicitly specified; those might be ignored inside of the generic. Other annotations are always assumed to be (others); note that we provide another way to annotate formal entities and those are recommended in most cases.]
Implementation Permissions
An implementation is permitted to omit a call on a subprogram whose Global out annotation is (null) and the results are not needed after the call. In addition, the implementation may omit the call on such a subprogram and simply reuse the results produced by an earlier call on the same subprogram provided: * No globals that are indicated as read by the Global in annotation for the
subprogram are modified between the earlier call and the omitted call;
* None of the parameters are of a limited type; * The addresses and values of all by-reference actual parameters, the values
of all by-copy-in actual parameters, and the values of all object accessible via the values of any access parameters, are the same as they were at the earlier call.
Redunant[This permission applies even if the subprogram produces other side-effects when called.]
AARM Discussion: This is intended to be the same rules as applies to calls on subprograms defined in declared Pure packages (see 10.2.1). Note that we don't need to talk about access values embedded in the parameter objects (as we have to for Pure), or about objects accessed from parameters of named access types, as those have to be covered by the Global annotations.
AARM Ramification: The part about indicating that no globals read are modified via Global in annotations is trivially true for Global in => (null). This makes this rule easier to use than the corresponding Pure rule.
The part about side-effects is barely necessary. The only possible side effects from a call with Global out => (null) would be through machine code insertions modifying objects, imported subprograms with untruthful annotations, Address_to_Access_Conversions, and similar features. The compiler may omit a call to such a subprogram even if such side effects exist; it is allowed to presume the annotations are accurate, even though this cannot be 100% certain.
---
[Now define the default annotations. Above we said that all entities default to having an annotation of (others); here we're going to say otherwise for particular cases where we can do better without introducing compatibility problems.]
Add to 3.5:
Unless otherwise specified, elementary types that do not have a partial view have annotations (see 13.3.4) of Global in out => (null).
AARM Ramification: If the elementary type does have a partial view, the type has annotations of Global in => (others), Global out => (others)); this is the default for all entities and is necessary to avoid breaking privacy. Annotations are part of the contract of the type, and should be carefully thought out to avoid problems with future maintenance.
Add to 3.6:
Unless otherwise specified, array types that do not have a partial view have Global in and out annotations (see 13.3.4) that are copies of those of the component type.
AARM Ramification: If the array type does have a partial view, the type has annotations of Global in => (others), Global out => (others)); this is the default for all entities and is necessary to avoid breaking privacy. Annotations are part of the contract of the type, and should be carefully thought out to avoid problems with future maintenance.
AARM Discussion: Note that there is no such rule for record or other composite types. The annotations needed for them are complex in general, and leaving them out of the source code is not going to help the human reader. [Editor's note: It is also fairly rare that they would be generated; most record types in well-designed programs do have partial views, so it is not a big hardship to write them by hand in the rare case where that is not the case.]
Add to 4.5:
Unless otherwise specified, the predefined operators of the language that have all operands of an elementary type all have implied annotations (see 13.3.4) of Global in out => (null).
Add after 4.5.2:
The predefined equality and ordering operators for discrete array types have implied annotations (see 13.3.4) of Global in out => (null).
AARM Ramification: The global rule means that equality and ordering operators for elementary types also have such annotations. Composition of equality for composite types means that they cannot have implied null annotations; that would be seriously incompatible. User-defined equality operators can have annotations, of course.
[Editor's note: We could use a rule more like the one for array components, inheriting the annotations from the "=" for the component type, if there is no partial view for the type. I didn't do that as the dependence of a partial view is a bit weird. Trying to come up with a rule for record types would be annoying; it would have to include the union of the "=" for all of the component types. Dispatching "=" would still have to use (others) so that future extensions would not be restricted.]
Add after 4.5.3:
If C is an elementary type, the predefined concatenation operators have implied annotations (see 13.3.4) of Global in out => (null).
[We could go further, but it gets messy, as any controlled component may drag Adjustment into the equation.]
Add after A(2)
Static Semantics
Each subprogram that is declared pure or is declared in a language-defined package or generic package that is declared pure has implied annotations (see 13.3.4) of Global in out => (null) unless the subprogram has one or more parameters of an access type or the annotations are specified elsewhere in this International Standard.
AARM Compatibility Note: This could be incompatible if a composite object passed as a parameter to such a subprogram has an access component. This does not seem likely for the language defined Pure packages.
[Editor's note: I'm not sure the exception is actually needed, but I didn't check.
Here the list of declared Pure packages as of this writing; I don't intend to put the list into the AARM as it would require constant maintenance. I'm ignoring Wide_ and Wide_Wide_ versions of packages for this list, as well as bounded and unbounded string versions.
Ada Ada.Assertions Ada.Characters Ada.Characters.Handling Ada.Characters.Latin_1 Ada.Characters.Conversions Ada.Containers -- No subprograms Ada.Containers.Generic_Array_Sort Ada.Containers.Generic_Constrained_Array_Sort Ada.Containers.Generic_Sort Ada.Decimal Ada.Dispatching Ada.IO_Exceptions -- No subprograms Ada.Numerics Ada.Numerics.Generic_Complex_Types Ada.Numerics.Generic_Complex_Elementary_Functions Ada.Numerics.Generic_Elementary_Functions Ada.Numerics.Generic_Real_Arrays Ada.Numerics.Generic_Complex_Arrays Ada.Streams Ada.Strings Ada.Strings.Equal_Case_Insensitive Ada.Strings.Hash Ada.Strings.Hash_Case_Insensitive Ada.Strings.Less_Case_Insensitive Ada.Strings.Maps Ada.Strings.Maps.Constants Ada.Strings.UTF_encoding Ada.Unchecked_Conversion Interfaces Interfaces.C Interfaces.Fortran Standard -- covered by the rules for predefined operators. System System.Storage_Elements
Containers are discussed below; I'm assuming that they will end up with explicit annotations.
I suspect that we need to give explicit annotations for the generic sorts, as the annotations of element types or the formal subprograms come into play for these, and we don't want to restrict them.
We probably also want to exclude the generic real and complex array packages; adding these annotations would prevent sparse matrix representations. I don't think we want to go that far (although sparse matrixes would be hard to implement within the restrictions of Pure, so maybe it doesn't matter).
End really long Editor's note. Probably should move some of this to !discussion after we make decisions.]
Replace to G.1.1(3) with:
type Complex is record Re, Im : Real'Base; end record with Global in => (null), Global out => (null);
[Editor's note: This is the only visible record type in the standard that I know of. We may want some annotation for many of the private types as well; that needs to be done on a case-by-case basis.]
[Editor's note: Annotations on the containers were assigned to Bob Duff. I'm providing suggested annotations for part of Bounded_Vectors in order to test that the generic mechanisms work.
Notes: We have to use the others in Vectors on all of the cursor forms because of the dereference of an access-to-vector type defined in this package (cursors include a reference to their associated container).
The annotations on the unbounded form of Vectors would be the same except that OTHERS IN Vectors would be added to any that could allocate/deallocate elements in order to reflect the allocated memory (from a presumably private but library-level access type).]
A.18.17 Bounded Vectors
generic type Index_Type is range <>; type Element_Type is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Bounded_Vectors is pragma Preelaborate(Bounded_Vectors); pragma Remote_Types(Bounded_Vectors);
subtype Extended_Index is Index_Type'Base range Index_Type'First-1 .. Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; No_Index : constant Extended_Index := Extended_Index'First;
type Vector (Capacity : Count_Type) is tagged private with Global in out => (generic Element_Type); pragma Preelaborable_Initialization(Vector); -- We're assuming an implementation something like: -- type Vector (Capacity : Count_Type) is tagged record -- Length : Count_Type; -- Data : array (1 .. Capacity) of Element_Type; -- end record;
type Cursor is private with Global in out => (generic Index_Type); pragma Preelaborable_Initialization(Cursor); -- We're assuming an implementation like: -- type Cursor is -- Vect : access Vector; -- Index : Extended_Index; -- end record;
Empty_Vector : constant Vector; No_Element : constant Cursor; function "=" (Left, Right : Vector) return Boolean with Global in out => (generic Element_Type, generic Ada.Containers.Bounded_Vectors."=");
function To_Vector (Length : Count_Type) return Vector with Global in out => (generic Element_Type); -- Every operation that needs to create a Vector object needs to -- include the annotations of the Vector object.
function To_Vector (New_Item : Element_Type; Length : Count_Type) return Vector with Global in out => (generic Element_Type);
function "&" (Left, Right : Vector) return Vector with Global in out => (generic Element_Type);
function "&" (Left : Vector; Right : Element_Type) return Vector with Global in out => (generic Element_Type);
function "&" (Left : Element_Type; Right : Vector) return Vector with Global in out => (generic Element_Type);
function "&" (Left, Right : Element_Type) return Vector with Global in out => (generic Element_Type);
function Capacity (Container : Vector) return Count_Type with Global in out => (null);
procedure Reserve_Capacity (Container : in out Vector; Capacity : in Count_Type) with Global in out => (null); -- This would be very different for other forms, where this does -- something.
function Length (Container : Vector) return Count_Type with Global in out => (null);
procedure Set_Length (Container : in out Vector; Length : in Count_Type) with Global in out => (generic Element_Type); -- We need to allow writing empty elements, if the implementation -- does something explicit for them. We have to allow Adjust, so -- we also need to include the reading portion.
function Is_Empty (Container : Vector) return Boolean with Global in out => (null);
procedure Clear (Container : in out Vector) with Global in out => (null); -- This just changes the length.
function To_Cursor (Container : Vector; Index : Extended_Index) return Cursor with Global in out => (null); -- No dereferences here.
function To_Index (Position : Cursor) return Extended_Index; Global in out => (null); -- No dereferences here.
function Element (Container : Vector; Index : Index_Type) return Element_Type with Global in out => (generic Element_Type); -- Creates an element.
function Element (Position : Cursor) return Element_Type with Global in => (access Vector, generic Element_Type), Global out => (generic Element_Type); -- The dereference of the container can touch any Vector object. -- This will prevent many optimizations. -- I knew I hated this implicit container semantics, I just -- couldn't explain why. Note that the previous routine has -- much stronger annotations. Apparently, tools will need to -- be container-aware to have any chance. Yuck.
procedure Replace_Element (Container : in out Vector; Index : in Index_Type; New_Item : in Element_Type) with Global in out => (generic Element_Type); -- Assigns an element; the type's Global annotations are also -- used for assignment.
procedure Replace_Element (Container : in out Vector; Position : in Cursor; New_item : in Element_Type) with Global in => (access Vector, generic Element_Type), Global out => (generic Element_Type); -- The access read is to access the cursor; it has to be -- the same as the Container item or we get an exception, -- but that is beyond the power of these annotations.
...
!discussion
The global in and global out annotations are intended to be descriptive. That is, the annotations describe the behavior of the subprogram body, initialization/finalization of a type, or elaboration of a package. As such, these annotations are checked. There is no benefit to be gained from lying about side-effects; such incorrect information could easily lead to incorrect code being generated (if the compiler uses the annotations). Moreover, if it is impractical to specify the correct annotations, it makes sense to specify none at all.
All of the global in and global out annotations proposed can be statically checked. It is possible to imagine annotations that cannot be statically checked, but these are assumptions as opposed to descriptive. Assumptions are a different set of annotations.
Note that it is possible to lie about the use of globals of subprograms and other entities that are imported. This is of course impossible to check, but thankfully is covered by B.1(38.1/2). Incorrect annotations on imported subprograms could cause a program to be erroneous.
---
The keywords in the syntax are necessary in order that the special syntax of this list can be recognized immediately. Otherwise, a massive amount of lookahead is needed to parse this (as the list would start the same way as the expression used for more typical aspects). We take advantage of the fact that Ada already has "in" and "out" keywords to make this syntax distinctive but still sensible.
---
It might make the most sense to define these in Annex H (High-Integrity Systems), rather than in Section 13. The most important thing is to define the syntax so that implementations can implement it and the checking (even if they are not doing semantic analysis now). The information is valuable to have in programs for future analysis when improved tools are available. The legality rules ensure that the information is accurate.
---
Annotations are defined in terms of "reading" and "writing" of objects. We use these terms in the same way as the rest of the standard; in particular, in the definitions of the semantics for Atomic objects and pragma Reviewable.
---
We have three kinds of global annotations, one for almost everything (Global), and two for special cases: Global'Access for calls through access-to-subprogram types, and Global'Class for dispatching calls.
Note that we need Global'Access to be a separate annotation as an access-to-subprogram type has both annotations (and we need to be able to talk about it for generics, as well as needed to support the unlikely possibility of it having a partial view).
Annotations are defined as aspects, and thus we are using the rules for aspects to simplify this description: there is only one per type (they are not view-specific) [although they can be given on private types, they then cannot be given on the full type];
Global annotations can be given on private types; if so, they are enforced on the full type as well.
---
The definition of preelaborable has legality rules depending on a runtime concept (elaboration). We tried to avoid that mistake with this set of rules.
That requires making composition of annotations explicit. The definition of the Global annotations for types requires this; the annotations of all of the components and all of the default expressions have to be compatible with the type's annotation. Once we have this, applying the rules just requires talking about the type of stand-alone objects and of assignment_statements; they include the annotations of any components by definition.
---
The rules are complicated by the need to include all implicit calls. That is done by folding Initialize/Finalize/Adjust into Global (along with default initialization), and explicitly talking about the operations of storage pools.
---
These annotations can be used by the compiler to guide code generation as well as for static analysis. The Implementation Permission provides rules similar to those for Pure subprograms -- it is OK to assume that the annotations are correct, but if the subprogram is called, then the compiler must use the actual side-effects, not any assumed because of annotations.
---
Annotations can explicitly include names of generic formal parameters; the annotations appropriate for the actual parameters are substituted when the generic is instantiated.
We originally tried to use an assume-the-worst rule for generic units, but that essentially requires any subprogram declaring in a generic that uses a formal parameter to be annotated with Global in => (others). That would totally prevent useful annotations on generic units, which is a complete nonstarter for obvious reasons.
Another option considered was to include the annotations as part of the generic contract. That would require some new matching rules, but otherwise is fairly simple. But it should be obvious that that does not work well for general-purpose generic units. For instance, consider the bounded Vector container. In order to be able to have the desired (null), (null) annotations on most routines, we would have to annotate the Element_Type with (null), (null) annotations. But that would prevent instantiating the container with many real types (any that include parts with Initialize/Adjusts that allocate memory, for instance). Not only is that incompatible, it also reduces the utility of the containers.
Luckily, annotations can be combined with the normal set operations. Thus, if we create a way to refer to the annotations of formal parameters without actually knowing what they are, we can then use the real annotations of the actual types when the generic is instantiated. This neatly solves the problem by making the annotations change as needed. For instance, when the bounded container is instantiated with Integer, all of the annotations will become (null), (null); but if the actual type has default annotations of (others), (others) all of the annotations will reflect that as well.
[I'm so smart to have figured this out myself. ;-) Just wish I had done so the first time. Editor.]
Note that we only provide generic annotations for formal entities that have interesting annotations. We don't provide annotations for in formal parameters, as they are copies of the actual made at the point of the instance. As such, they have no effect on the annotations of items declared in the generic (of course, the evaluation of the actuals could require them to be included in an annotation for a subprogram or package surrounding the instance).
Similarly, we don't provide annotations for formal packages, as the actuals for those are already elaborated instances. As such, their annotations will never be needed in the generic unit (they're only used at the point of the instance).
---
We allow specifying the name of a pool-specific access type as an Annotation_Item. This provides a convinient way to cover all possible target objects without discussing the pool. Note that conversions from other access types to a pool-specific type are not allowed (other than via Unchecked_Conversion, which we disallow explicitly). That means we can treat the pool as local to the package that declares the access type, even if the actual pool is allocated somewhere else. This allows using OTHERS IN <package_name> for types that are hidden from clients.
We do have to treat such a pool as a global object, even though in many cases objects allocated from such hidden access types are not shared and could be considered part of other objects. Since we are using static checked, properties that can only be verified dynamically effectively require "assume-the-worst" rules. See the example of February 1, 2010 found in the !appendix.
For all access types, we provide the ACCESS T annotation item. This item specifies any object that could be allocated for a general access type designating T: any aliased object of a type covered by T (including those allocated from any pool), and, if T is tagged, any object of a type covered by T. (Recall that 'Access can always be used on tagged type parameters, so they are effectively aliased for this purpose.)
Still, if the name of a designated type is not visible, the only annotation available is (OTHERS) (which covers everything).
An alternative approach that was considered would be to wrap up the entire set of items in Global in/out annotations for each access type (that would be disjoint with access-to-subprograms use for the same thing). That would include all of the Global annotations for the subprograms of the storage pool, an annotation for the storage pool object, and ACCESS designated_subtype_mark for general access objects. That doesn't seem to help anything for types that are hidden, thus we did not use that alternative.
!example
Following is a non-generic example that illustrates how these annotations work on a controlled type. There are some embedded comments that explain some details of the annotations.
with Ada.Finalization; package TestV02A is
type JSON_Data_Type is (JSON_NULL, JSON_BOOLEAN, JSON_NUMBER, JSON_STRING); -- As this is an elementary type, we don't need any annotations; -- they will default to Global in => null, Global out => null.
type Holder is tagged private with Global in => (TC_Count), Global out => (TC_Count, TC_Passed); -- Globals used by the default initialization/adjustment/finalization of -- the type.
Null_Holder : constant Holder;
Boolean_Holder : constant Holder;
String_Holder : constant Holder;
function Check_Holder (Container : in Holder; Kind : in JSON_Data_Type) return Boolean with Global in out => (null);
TC_Passed : Boolean := True;
TC_Final_Count : Natural := 0;
private
type Holder is new Ada.Finalization.Controlled with record Type_Kind : JSON_Data_Type := JSON_Null; end record; -- Since Global is an aspect and it was specified for the private type, -- we don't repeat it here. Aspects are the same for all views. subtype My_Holder is Holder;
procedure Initialize (Container : in out Holder) with Global in => (null), Global out => (TC_Passed);
procedure Adjust (Container : in out Holder) with Global in => (null), Global out => (TC_Passed);
procedure Finalize (Container : in out Holder) with Global in => (TC_Count), Global out => (TC_Count);
-- Neither Adjust nor Initialize should be called on the following: -- (Note: Program_Error probably will be raised here if the test fails.)
Null_Holder : constant Holder := (Ada.Finalization.Controlled with Type_Kind => JSON_NULL);
Boolean_Holder : constant Holder := Holder'(Ada.Finalization.Controlled with Type_Kind => JSON_BOOLEAN);
String_Holder : constant Holder := (My_Holder'(Ada.Finalization.Controlled with Type_Kind => JSON_STRING));
end TestV02A;
package body TestV02A is
function Check_Holder (Container : in Holder; Kind : in JSON_Data_Type) return Boolean is -- Only parameters are used, so the annotations are both (null). begin return Container.Type_Kind = Kind; end Check_Holder;
procedure Initialize (Container : in out Holder) is begin TC_Passed := False; end Initialize;
procedure Adjust (Container : in out Holder) is begin TC_Passed := False; end Adjust;
procedure Finalize (Container : in out Holder) is begin TC_Count := TC_Count + 1; end Finalize;
end TestV02A;
with TestV02A; package TestV02B is
function Generator return TestV02a.JSON_Data_Type with
Global in => (others in TestV02B), Global out => (others in TestV02B); -- We have to use others as the global object is not visible -- in the specification.
type Operand is record Kind : TestV02a.JSON_Data_Type := Generator; Obj : TestV02a.Holder; end record with Global in => (others in TestV02B, TestV02A.TC_Count), Global out => (others in TestV02B, TestV02A.TC_Passed, TestV02A.TC_Count); -- This annotation at least has to cover the annotations of the component -- types and anything used by the default expressions. But it can cover -- more: (others) could have been used, or (others in TestV02B, others in TestV02a).
procedure Do_It_Once (O : in Operand) with Global in => (others in TestV02B, TestV02A.TC_Count), Global out => (others in TestV02B, TestV02A.TC_Passed, TestV02A.TC_Count);
function OK return Boolean with Global in => (TestV02A.TC_Passed, TestV02A.TC_Count), Global out => (null);
end TestV02B;
package body TestV02B is
Seed : TestV02a.JSON_Data_Type := TestV02a.JSON_NULL;
function Generator return TestV02a.JSON_Data_Type is
use type TestV02a.JSON_Data_Type;
begin if Seed /= TestV02a.JSON_Data_Type'Last then Seed := TestV02a.JSON_Data_Type'Succ(Seed); else Seed := TestV02a.JSON_Data_Type'First; end if; return Seed; end Generator;
procedure Do_It_Once (O : in Operand) is Copy_of_O : Operand := O; -- The annotations of Operand are required to be covered -- because of this declaration. begin TestV02A.Check_Holder (Copy_of_O, TestV02a.JSON_NULL); end Do_It_Once;
function OK return Boolean is begin return TestV02A.TC_Passed and (TestV02A.TC_Count = 3); end OK;
end TestV02B;
---
Annotations of instances are substituted. For instance, for the following instantiation of Ada.Containers.Bounded_Vectors:
subtype Short_Int is Natural range 0 .. 1000; package Int_Vect is new Ada.Containers.Bounded_Vectors (Short_Int, Integer);
In this case, the annotations for the actual corresponding to "Generic Element_Type" would be "Global in out => (null)", as would the annotations for "=". That means that almost all of the annotations of the types and routines in the instance would become "Global in out => (null)", meaning that the permission to remove extra calls would be active.
On the other hand, if a type like Holder above was used as the element type:
package Holder_Vect is new Ada.Containers.Bounded_Vectors (Short_Int, TestV02a.Holder);
In this case, the annotations for the actual corresponding to "Generic Element_Type" would be "Global in => (TestV02A.TC_Count),
Global out => (TestV02A.TC_Passed, TestV02A.TC_Count)"
and the annotations for "=" would be "Global in out => (others)" (since they were not specified).
Thus the effective annotations for "=" in the Holder_Vect instance would be Global in out => (others), while those for Element (by index) would be Global in => (TestV02A.TC_Count), Global out => (TestV02A.TC_Passed, TestV02A.TC_Count), and those for function Length would still be Global in out => (null).
!ACATS test
!appendix

From: Randy Brukardt
Sent (privately): Wednesday, March 18, 2009  4:30 PM

As I understand it (mainly from an old message of John's about "exposing your
globals"), Global_In is a list of names of globals touched by the body of a
subprogram. It also ought to include two special names: "null" (for explicitly
stating that no globals are harmed by this subprogram :-); and "private" (for
globals that aren't visible at the point of the annotation). By default, all
subprograms have

    Global_In => private,

which says that they touch globals but we aren't going to say which ones.

Presumably, Global_Out are a similar list of globals written by a subprogram.

Do I have it so far?

Now, the problem with the SPARK definition is that it doesn't take into account
things like storage pools and tasks, which we'll have to do.

For the storage pool problem, I think that declaring any collections read would
be sufficient, and that could easily be done by mentioning the name of the
access type in the annotation. (Directly naming the pool has two problems: the
pool may not be visible while the access type is, and secondly, the default pool
does not have a name.)

I'm going to ignore tasks for now (not really relevant to my questions).

I do think that the compiler needs to check that this listing is correct. (And I
think that is fairly easy: any object whose accessibility is outside of that of
the subprogram call "shall be listed" in the Global_In annotation unless the
Global_In annotation includes "private". ["Subprogram call" allows
accessing/modifying the parameters.] That would of course include anything
listed in the Global_In annotation of any called routines. Language-defined
operators other than "=" for tagged types would be defined to have Global_In =>
null.) Having this information incorrect would lead to all kinds of bad
assumptions by the compiler and by the reader. And you can always use Global_In
=> private if you don't want to say - just don't lie.

I note that this gets the effect of the "strict" annotation that I was lobbying
for, but in a way which is much harder to argue with. ("Global_In => null" means
"I don't have a side effect other than as declared in the spec", and the
compiler and reader can depend on that.) We don't get the elaboration benefit (I
would have allowed early calls on strict functions, because so long as their
parameters are frozen, they are safe), but that is no big deal.


But I am wondering about accesses to sub-parts of parameters. My "strict"
definition would have banned that, because it would allow depending on
side-effects. The way I wrote the description above would also ban that, but I
worry that people would be annoyed. This problem comes from my recognition that
the Claw Is_Valid routine is not strict, even though it only depends on reading
its parameter. For example:

     type A_Window is private;

     function Is_Valid (A : A_Window) return Boolean
     when Global_In => ???;

  private

     type Data is record
        Valid : Boolean := False;
        Handle : HWnd := Null_HWnd;
        ...
     end record;
     type Data_Access is access all Data;

     type A_Window is record
         My_Data : Data_Access;
         ...
     end record;

The problem here is that the user of the GUI application can manually close a
window, at which point Valid gets set to False and the Handle gets set to
Null_HWnd (among other things, of course).

Is_Valid only reads its parameter, but the portion that is pointed at can be
modified asynchronously by another task. So it would be wrong for an analyzer to
depend on the value of Is_Valid not changing. (This is a huge challenge when
programming with Claw.)

So, does this mean that type Data_Access must be included in the Global_In list?
(In this particular case, since the type is defined in the private part, the
Global_In list would have to be "private").

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

From: Tucker Taft
Sent (privately): Wednesday, March 18, 2009  5:31 PM

...
> Do I have it so far?

I hadn't thought about it too much in detail yet.  As you know SPARK has
something like this.

The notion of "private" doesn't sound too useful.  I would suggest allowing the
names of packages as well as objects, where the name of a package means some
presumably non-visible "state" in the package (spec or body).  I suspect we
would need to parenthesize the list if there is more than one item, to avoid
creating a syntactic mess, with "null" substituting for the syntactically
illegal "()".

>
> Now, the problem with the SPARK definition is that it doesn't take
> into account things like storage pools and tasks, which we'll have to do.
>
> For the storage pool problem, I think that declaring any collections
> read would be sufficient, and that could easily be done by mentioning
> the name of the access type in the annotation. (Directly naming the
> pool has two
> problems: the pool may not be visible while the access type is, and
> secondly, the default pool does not have a name.)

Yes, an access type would seem reasonable as a stand-in for the collection it
represents.  And a package name would cover any non-visible *pool-specific*
access types declared within it.

If you are going through a non-visible *general* access type, then I think we
would want some notation for that if the access type is private, but the
designated type is not.  E.g. "all aliased T" might be a legal entry in the
list, and perhaps simply "all aliased" if the type is itself non-visible.

Alternatively, it might be appropriate in some cases to identify the particular
pointed-to object referenced/updated, e.g. Global_In => (X.all, Y.T.all),
Global_Out => (X.A, Y.B.all); Saying an entire access collection is affected is
too imprecise for some kinds of analysis.  And if the access type is a general
access type, then you are effectively "killing" all aliased objects of the
designated type (or types covered by it).

> I'm going to ignore tasks for now (not really relevant to my questions).

I don't see tasks as a big special case.  A task has state just like other
objects.  The slightly weird thing is that you can change the state of a task
even though you have it as an "IN" parameter.  Probably one way to think about
it is that every task has its own "collection", and the stack of the task is
allocated out of that collection, and the task object is really just a pointer
to that.  A call on an entry of a task passes an implicit dereference of that
pointer to the accept statement.

> I do think that the compiler needs to check that this listing is correct.
> (And I think that is fairly easy: any object whose accessibility is
> outside of that of the subprogram call "shall be listed" in the
> Global_In annotation unless the Global_In annotation includes "private". ["Subprogram call"
> allows accessing/modifying the parameters.] That would of course
> include anything listed in the Global_In annotation of any called routines.
> Language-defined operators other than "=" for tagged types would be
> defined to have Global_In => null.) Having this information incorrect
> would lead to all kinds of bad assumptions by the compiler and by the
> reader. And you can always use Global_In => private if you don't want to say - just don't lie.

Yes, I would agree with all of this.  But I would also try to define the
semantics so that if you manage to lie (e.g. by referencing imported
subprograms), the world doesn't implode. Instead it is like pragma Pure, the
compiler is allowed to avoid calling a subprogram again if it concludes
everything it takes as input is unchanged, and use the prior results of the
call.  It isn't allowed to assume that if it actually *makes* the call, it will
always get the same answer.

Something similar would be said about Global_Out, which would permit reusing
cached values after a call rather than reloading them from memory if they
supposedly wouldn't be affected by the call, but if you actually go to the
trouble of *reloading* the value from memory, you shouldn't presume this newly
loaded value is identical to the old one, and use the newly reloaded value to,
say, index into an array without rechecking against the bounds.

> I note that this gets the effect of the "strict" annotation that I was
> lobbying for, but in a way which is much harder to argue with.
> ("Global_In => null" means "I don't have a side effect other than as
> declared in the spec", and the compiler and reader can depend on
> that.) We don't get the elaboration benefit (I would have allowed
> early calls on strict functions, because so long as their parameters
> are frozen, they are safe), but that is no big deal.
>
>
> But I am wondering about accesses to sub-parts of parameters. My "strict"
> definition would have banned that, because it would allow depending on
> side-effects.

I don't really understand this last sentence.  I'm not sure what is a "sub-part"
and I'm not sure what you mean about "depending on side-effects."  I think I
understand what you mean in your example below, but I don't understand this
introductory sentence.

> ... The way I wrote the description above would also ban that, but
> I worry that people would be annoyed. This problem comes from my
> recognition that the Claw Is_Valid routine is not strict, even though
> it only depends on reading its parameter. For example:
>
>      type A_Window is private;
>
>      function Is_Valid (A : A_Window) return Boolean
>      when Global_In => ???;
>
>   private
>
>      type Data is record
>         Valid : Boolean := False;
>         Handle : HWnd := Null_HWnd;
>         ...
>      end record;
>      type Data_Access is access all Data;
>
>      type A_Window is record
>          My_Data : Data_Access;
>          ...
>      end record;
>
> The problem here is that the user of the GUI application can manually
> close a window, at which point Valid gets set to False and the Handle
> gets set to Null_HWnd (among other things, of course).
>
> Is_Valid only reads its parameter, but the portion that is pointed at
> can be modified asynchronously by another task. So it would be wrong
> for an analyzer to depend on the value of Is_Valid not changing. (This
> is a huge challenge when programming with Claw.)
>
> So, does this mean that type Data_Access must be included in the
> Global_In list? (In this particular case, since the type is defined in
> the private part, the Global_In list would have to be "private").
>
> Thanks in advance for your answer.

If you read something you get through an access value, then you will need to
account for it somehow, as "blah.all", the name of an access type, the name of a
package, or something like "all aliased [T]".

I think you are also talking about issues that have to multi-threading here.  If
the asynchronous event can happen at "any" time, then I would say you should
really declare the "Valid" field as volatile, in which case we would probably
want some way of stating that the result of a function is volatile and hence
essentially unpredictable.

If the aynchronous update can only happen during to some kind of
potentially-blocking or signaling operation, then it should be handled the
normal way things are handled at potential task signaling/blocking points, where
some appropriate part of the universe might be affected by the actions of other
tasks.

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

From: Randy Brukardt
Sent (privately): Wednesday, March 18, 2009  5:59 PM

...
> The notion of "private" doesn't sound too useful.  I would suggest
> allowing the names of packages as well as objects, where the name of a
> package means some presumably non-visible "state" in the package (spec
> or body).  I suspect we would need to parenthesize the list if there
> is more than one item, to avoid creating a syntactic mess, with "null"
> substituting for the syntactically illegal "()".

Well, it surely isn't useful for analysis, but it seems necessary to have a
default that says, yup, we have some side effects and we aren't going to say
which ones. Because we surely can't require this annotation on all subprograms,
but we do have to know what to do if such a subprogram is called from inside of
one that does have an annotation.

If there is a better way to express the default of "anything goes, assume the
worst", I'm happy to see it.

...
> > I do think that the compiler needs to check that this listing is correct.
> > (And I think that is fairly easy: any object whose accessibility is
> > outside of that of the subprogram call "shall be listed" in the
> > Global_In annotation unless the Global_In annotation includes "private".
> > ["Subprogram call" allows accessing/modifying the parameters.] That
> > would of course  include anything listed in the Global_In annotation
> > of any called routines.
> > Language-defined operators other than "=" for tagged types would be
> > defined to have Global_In => null.) Having this information
> > incorrect would lead to all kinds of bad assumptions by the compiler
> > and by the reader. And you can always use Global_In => private if
> > you don't want to say - just don't lie.
>
> Yes, I would agree with all of this.  But I would also try to define
> the semantics so that if you manage to lie (e.g. by referencing
> imported subprograms), the world doesn't implode.
> Instead it is like pragma Pure, the compiler is allowed to avoid
> calling a subprogram again if it concludes everything it takes as
> input is unchanged, and use the prior results of the call.  It isn't
> allowed to assume that if it actually
> *makes* the call, it will always get the same answer.

Well, for static analysis, either you have the truth or the world implodes. :-)
And that's also true for legality rules - if you depend on an incorrect
annotation when enforcing a legality rule (or more accurately not enforcing),
it's pretty much garbage in, garbage out. Probably would want to define that as
a bounded error if at all possible (either you get an error or the code works at
runtime).

But I agree that we pretty much have to leave the Duff door open: lying in
annotations on an imported subprogram can't be banned or detected.

I do agree that uses in optimizations and code selection should follow rules
like you give here.

> Something similar would be said about Global_Out, which would permit
> reusing cached values after a call rather than reloading them from
> memory if they supposedly wouldn't be affected by the call, but if you
> actually go to the trouble of *reloading* the value from memory, you
> shouldn't presume this newly loaded value is identical to the old one,
> and use the newly reloaded value to, say, index into an array without
> rechecking against the bounds.

Right. I'm not personally as interested in Global_Out, at least not right this
minute, but I can see how it would be useful.

...
> > But I am wondering about accesses to sub-parts of parameters. My "strict"
> > definition would have banned that, because it would allow depending
> > on side-effects.
>
> I don't really understand this last sentence.  I'm not sure what is a
> "sub-part" and I'm not sure what you mean about "depending on
> side-effects."  I think I understand what you mean in your example
> below, but I don't understand this introductory sentence.

I mean cases like the example below. In other words, ignore the above if it is
too confusing.

> > ... The way I wrote the description above would also ban that, but I
> > worry that people would be annoyed. This problem comes from my
> > recognition that the Claw Is_Valid routine is not strict, even
> > though it only depends on reading its parameter. For example:
> >
> >      type A_Window is private;
> >
> >      function Is_Valid (A : A_Window) return Boolean
> >      when Global_In => ???;
> >
> >   private
> >
> >      type Data is record
> >         Valid : Boolean := False;
> >         Handle : HWnd := Null_HWnd;
> >         ...
> >      end record;
> >      type Data_Access is access all Data;
> >
> >      type A_Window is record
> >          My_Data : Data_Access;
> >          ...
> >      end record;
> >
> > The problem here is that the user of the GUI application can
> > manually close a window, at which point Valid gets set to False and
> > the Handle gets set to Null_HWnd (among other things, of course).
> >
> > Is_Valid only reads its parameter, but the portion that is pointed
> > at can be modified asynchronously by another task. So it would be
> > wrong for an analyzer to depend on the value of Is_Valid not
> > changing. (This is a huge challenge when programming with Claw.)
> >
> > So, does this mean that type Data_Access must be included in the
> > Global_In list? (In this particular case, since the type is defined
> > in the private part, the Global_In list would have to be "private").
> >
> > Thanks in advance for your answer.
>
> If you read something you get through an access value, then you will
> need to account for it somehow, as "blah.all", the name of an access
> type, the name of a package, or something like "all aliased [T]".

Right. I suspect some people will not like that much (you have even argued wrt
to constants that such accessed parts are logically part of the passed object).
But in this case, they are *not* logically part of the passed object.

> I think you are also talking about issues that have to multi-threading
> here.  If the asynchronous event can happen at "any" time, then I
> would say you should really declare the "Valid" field as volatile, in
> which case we would probably want some way of stating that the result
> of a function is volatile and hence essentially unpredictable.
>
> If the aynchronous update can only happen during to some kind of
> potentially-blocking or signaling operation, then it should be handled
> the normal way things are handled at potential task signaling/blocking
> points, where some appropriate part of the universe might be affected
> by the actions of other tasks.

Claw uses locks so that the state can't change inside of a Claw-defined routine.
If a state change needs to happen, it is delayed until the lock is available,
meaning after the current routine is finished. But we don't lock things that
only read scalar components (and don't have dependencies), because those can't
be in an inconsistent state: the Valid component can only be True or False.

I suppose that they really ought to be declared volatile, but given the nasty
impact on code generation, and that we only care that Valid is not some value
other than True or False (which can't happen with any of the Ada compilers we've
used), we never did that.

In any case, the pool or object has to be identified somehow in Global_In. That
eliminates my concern.

It does seem that a real proposal would be valuable here. If I had it, I could
point to it rather than duplicating a lot of that in AI-144's discussion.

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

(Partial) Minutes of the Amendment subcommittee of the ARG conference call of
December 10, 2009

Attendees: Bob Duff, Tucker Taft, Randy Brukardt, Steve Baird, Gary Dismukes, Ed Schonberg

AI05-0186-1/01

Bob says that this is essential if you ever want to do any analysis of programs
without all of the source code available.

Bob comments that the write up talks about function too much, it should say
subprogram more. Tucker notes that this is mainly an issue in !problem. Randy
notes that the motivating case has to do with functions, so it just talks about
that there.

Bob wonders if we should talk about variables rather than constants. He doesn't
want to annotate reads of global constants. Not all constants are really
constants, however. Calling an entry of tasks if side-effect, even if the task
is a constant. He is not sure what the right answer is (we could except
elementary constants from the rules without problems).

Elementary Operators would have null annotations. Randy notes that composition
of equality means that we have to exclude composite operators, as they might
contain user-defined parts (even array "=" has that problem).

Bob wonders about annotations of the existing predefined packages. In an ideal
world, they would all have them, but that is a heck of a lot of work. Bob notes
that most of the pure packages could use global in/out => null. But access
parameters could cause problems, global in => null is stronger than Pure.

We would want all of the pure packages (like Generic_Elementary_Functions) to
have annotations. We'd like that for the containers, too, but they are mostly
preelaborable.

Randy notes that we'll all have to pitch in on this AI if we want to get it done
on time. Bob will investigate how these annotations could be used on the
unbounded vectors packages.

Ed doesn't like the idea too much. He thinks it is going halfway. If you don't
do data flow it is too imperfect.

Others disagree. You have explicitly include side effects of anything that you
call. That is the same as SPARK. No one thinks SPARK is "too imperfect".

Ed suggests that we might want this on task bodies. That could be used to
prevent/declare unsynchronized access. That seems useful.

Randy notes that in'Class and out'Class would be useful for dispatching calls.
We also would like to have this on access-to-subprogram types.

Bob leaves the call at this point.

We start wondering about the elaboration of entities. Calls that occur in
initialization are definitely included.

Steve notes that you need to worry about default initialization. That's at least
in the spec. It's the body that is hidden that is a problem.

What about instantiating a generic? You would like annotations for things that
happen in the body elaboration there.

That means we have to put aspect specs on bodys. Tucker already had an action
item to do that from St. Pete. He doesn't remember that, and asks for the
minutes draft.

Aspect specs need to be somewhere around the "is" - putting them at the very end
makes no sense. Tucker thinks before the "is". Ed thinks after the "is" makes
more sense. The current end is the ';' the end being the "is" makes more sense.
Gary thinks that would read OK.

Initialize procedures also need their side effects included.

Steve wonders about user-defined storage pools, those too ought be included.

Lots more wording to add, especially for implicit calls.

Access_subtype_name really ought to be Access_subtype_mark. For general access,
it would mean everything aliased covered by the designated type, plus the
storage pool. For all access types, also include the side effects of any
allocate/deallocate routines. (What about function Storage_Size?)

Is this privacy-preserving? In that case, a private type would need an
annotation for default initialization and finalization. But you can't really
have one without the other. Well, you could if you don't use the default
initialization. Tucker says that you ought to be responsible for them anyway. So
only a single annotation is needed for a private type.

Steve would like this to preserve the separation of static and dynamic
semantics. That is the intent - he notes that Pure does not do that. That means
the wording shouldn't talk about what happens at elaboration.

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

Example of access annotations, February 1, 2010, Randy Brukardt

It is often the case that access types hidden in package bodies allocate objects
that "belong" to particular parameter objects. Verifying this property is
not possible statically; thus access type annotations have to assume that
allocated objects are shared amongst top-level objects.

Following is an example of a type that would be problematic without the
requirement to annotate hidden access types.

package Clones is

    type Clonee is tagged private
       with Global in out => (others in Clones);

    procedure Create (Obj : in out Clonee; Cnt : Natural; Ave : Float) with
       Global in out => (others in Clones);

    function Cnt (Obj : in Clonee) return Natural with
       Global in => (others in Clones), Global out => (null);
 
    function Ave (Obj : in Clonee) return Natural with
       Global in => (others in Clones), Global out => (null);

    procedure Reset (Obj : in out Clonee; Cnt : Natural; Ave : Float) with
       Global in out => (others in Clones);

private

    type Data_Type is record
        Ref_Cnt : Natural := 0;
        Ave : Float;
        Cnt : Natural;
    end record;
    type Data_Access is access Data;

    type Clonee is tagged record
        Data : Data_Access;
    end record;

    procedure Adjust (Obj : in out Clonee) with
       Global in out => (others in Clones);

    procedure Finalize (Obj : in out Clonee)
       Global in out => (others in Clones);

end Clones;


package body Clones is

    procedure Create (Obj : in out Clonee; Cnt : Natural; Ave : Float) is
    begin
        Obj.Data := new Data_Type'(Ref_Cnt => 1, Ave => Ave, Cnt => Cnt);
    end Create;

    function Cnt (Obj : in Clonee) return Natural is
    begin
        return Obj.Data.Cnt;
    end Cnt;
 
    function Ave (Obj : in Clonee) return Natural is
    begin
        return Obj.Data.Ave;
    end Ave;

    procedure Reset (Obj : in out Clonee; Cnt : Natural; Ave : Float) is
    begin
        Obj.Data.Ave := Ave;
        Obj.Data.Cnt := Cnt;
    end Reset;

    procedure Adjust (Obj : in out Clonee) is
    begin
       Obj.Data.Ref_Cnt := Obj.Data.Ref_Cnt + 1;
    end Adjust;

    procedure Finalize (Obj : in out Clonee) is
    begin
       if Obj.Data /= null then
          Obj.Data.Ref_Cnt := Obj.Data.Ref_Cnt - 1;
          if Obj.Data.Ref_Cnt = 0 then
              Free (Obj.Data);
          end if;
       end if;
    end Finalize;

end Clones;

with Clones;
procedure Test is
    A, B : Clones.Clonee;
begin
    Clones.Create (A, 10, 1.5);
    B := A;
    if Clones.Cnt(B) = 10 then ... -- (1)
    Clones.Reset (A, 5, 2.5);
    if Clones.Cnt(B) = 10 then ... -- (2)
end Test;

Clones.Cnt(B) has the value 10 at (1), and 5 at (2). Since Clones.Cnt
has a Global out => (null), it is a candidate for the optimization of
removing the redundant call at (2), most so because the object B
is the same as before. However, it fails the check that the Global in
is not modified, so the optimization cannot be performed.

If we allowed the "hidden" access type to be ignored in the annotations,
this (incorrect) optimization would be allowed. That's no good.

Note that if the Reset operation would have been some call unrelated
to package Clones, the optimization would have been allowed, as the
value of B could not have changed (even though it contains "global" data).

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

Questions? Ask the ACAA Technical Agent