CVS difference for ai05s/ai05-0186-1.txt

Differences between 1.2 and version 1.3
Log of other versions for file ai05s/ai05-0186-1.txt

--- ai05s/ai05-0186-1.txt	2009/11/03 06:46:27	1.2
+++ ai05s/ai05-0186-1.txt	2010/01/21 05:13:50	1.3
@@ -1,4 +1,4 @@
-!standard 13.3.4 (0)                                09-11-02  AI05-0186-1/01
+!standard 13.3.4 (0)                                10-01-20  AI05-0186-1/02
 !class amendment 09-11-02
 !status work item 09-11-02
 !status received 09-11-02
@@ -18,15 +18,15 @@
 at runtime, but are intended to be potentially checked (at least in part)
 statically.
 
-However, without knowledge of side-effects of functions, 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.
+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 prevents any analysis unless the bodies
+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
@@ -42,8 +42,13 @@
 
 !proposal
 
-Add global_in and global_out annotations to Ada.
+Add global in and global out annotations to Ada, for subprograms and
+access-to-subprogram types. Add global_init in and global_init out annotations
+for packages and types.
 
+The global_init annotations cover default initialization/adjustment/finalization
+for types; and cover operations that occur as part of the elaboration for packages.
+
 !wording
 
 Semi-formal description (presumably in Section 13.3.4):
@@ -54,14 +59,14 @@
 
     Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
 
-    Annotation_Item ::= *object_*name | *access_subtype_*name |
+    Annotation_Item ::= *object_*name | *access_*subtype_mark |
                          NULL | OTHERS [IN *package*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.
 
-Aspect Global is defined.
+Aspects Global and Global_Init are defined.
 
 Static Semantics
 
@@ -70,12 +75,12 @@
     * O statically denotes a part of an object named in the Annotation_List;
     * The annotation OTHERS without a package name occurs in the list;
     * The annotation OTHERS with a package name P occurs in the list, and
-      O denotes an object declared in P, or O denotes a part of an object
+      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 access type declared in P; or
     * O denotes a part of an object produced by a dereference of an object of
       an access type named in the Annotation_List.
 
-AARM Ramification: "private" by itself allows anything to be read or written.
+AARM Ramification: "others" by itself allows anything to be read or written.
 
 An annotation A1 is *compatible* with another annotation A2 if:
     * A1 contains NULL; or
@@ -90,6 +95,11 @@
 
 Legality Rules
 
+An annotation_list can be given if and only if the aspect is Global or Global_Init.
+
+The aspect Global shall be given only on subprograms and on access-to-subprogram types.
+The aspect Global_Init shall be given only on types, packages, and generic packages.
+
 The Annotation_Item NULL has to be the only item in an Annotation_List if
 it is given.
 
@@ -97,40 +107,324 @@
 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, or be covered by the Global in annotation.
-  * every call in the subprogram body shall have a compatible Global in annotation.
-
-[The first part means that the object has the accessibility of the function
-call.]
-
-AARM Ramification: Local objects and the parameters of the call do not need to
-appear in a Global in annotation.
-
-If a subprogram contains a Global out annotation, then:
-  * every object that is written by the subprogram body shall either be accessible
-    from the function call, or be covered by the Global out annotation.
-  * every call in the subprogram body shall have a compatible Global out annotation.
-
+  * 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 in annotation;
+    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 have
+    a compatible Global_Init in annotation.
+  * Every nested package and package instantiation declared by the subprogram
+    shall have a compatible Global_Init in annotation.
+  * The type of each assignment_statement shall have a compatible Global_Init in
+    annotation.
+  * The Allocate routine associated with the storage pool for the type of
+    each allocator in the subprogram body shall have a compatible Global in
+    annotation.
+  * 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.
+
+[I can't find any way to share these rules amongst the various kinds of entities.
+The first rule is slightly different for each kind of thing, depending on the
+accessibility or other rule needed.
+
+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. End 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.
+
+Analogous rules apply to a Global_init 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 in
+annotation, subprogram P shall have a compatible Global in annotation. Similarly,
+for a type S that has a Global out annotation, subprogram P shall have a compatible
+Global out annotation.
+
+Global'Class annotations shall be given only on primitive subprograms of
+a tagged type Redundant[; they 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_init in annotation:
+  * If the full type is composite, the type of each component shall have a compatible
+    Global_init in 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_init 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 in
+       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.
+     * 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 body shall conform to the rules for a subprogram
+     body (given previously).
+
+[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_init out annotation (replacing "in" by "out" and
+"read" by "written" everywhere).
+
+
+If a package or generic package includes a Global_init 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_init 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 in
+       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.
+     * 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 have
+    a compatible Global_Init in annotation.
+  * Every nested package and package instantiation declared by the package
+    shall have a compatible Global_Init in annotation.
+  * The type of each assignment_statement in the sequence_of_statements of the
+    package body shall have a compatible Global_Init in annotation.
+
+Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and
+"read" by "written" everywhere).
+
+
+[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_Init
+annotations for a formal type are assumed to be (others); the Global annotations
+for formal subprograms and formal access types are assumed to be (others); the
+Global annotations on the storage pool operations for formal access types are
+assumed to be (others).
+
+[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.]
 
 ---
 
+[Define the default annotations. Effectively, all annotations default to  "others"
+because all of the rules above treat absense of an annotation like "others", unless
+we say otherwise. - Editor.]
+
+Add to 3.5:
+
+Elementary types of the language have implied annotations of Global_Init in => (null),
+Global_Init out => (null).
+
 Add to 4.5:
+
+Unless otherwise specified, the predefined operators of the language that have
+at operands of an elementary type all have implied annotations of Global in => (null),
+Global out => (null).
 
-Unless otherwise specified, the predefined operators of the language all have
-implied annotations of Global in => (null), Global out => (null).
+Add after 4.5.2:
 
-[Do we want to give annotations to other operations, such as some of those
-in the containers?]
+The predefined equality and ordering operators for discrete array types have implied
+annotations of Global in => (null), Global out => (null).
 
-[We could define that language-defined Pure subprograms that do not have access
-parameters have implied annotations of Global in => (null), Global 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.
 
+Add after 4.5.3:
 
+If C is an elementary type, the predefined concatenation operators have implied
+annotations of Global in => (null), Global 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 of
+Global in => (null), Global out => (null) unless the subprogram has one or
+more parameters of an access type.
+
+AARM Compatibility Note: This could be imcompatible 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 packages.
+
+[Editor's note: I'm not sure the exception is actually needed, but I didn't
+check.
+
+Here the list of such packages approved 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
+
+
+I'm assuming that we adopt AI-142-4 and/or AI-139-2, both of
+which require the bounded containers to be preelaborable (so that the
+accessors and iterators work). We would like to explicitly provide annotations
+for the bounded containers as appropriate (I suspect unbounded is nasty because
+of the access types involved).
+
+I suspect that we need to exclude 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. Not sure of the best way to do that.
+
+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 they'd be hard to implement within the
+restrictions of Pure).
+
+End really long Editor's note. Probably should move some of this to !discussion
+after we make decisions.]
+
+** Wording TBD:
+
+I don't quite see how to take into account (or if we have to) the storage pool
+of an access type.
+
+The intended rules are:
+
+For pool-specific types, only the storage pool can be accessed by a dereference.
+For general access types, any aliased object of the designated type (and the
+storage pool) can be accessed by a dereference.
+
+The current wording "covers" dereferences by naming their access type. The above
+rules would seem necessary for tools depending on these annotations, but doesn't
+seem necessary for the rules defining the annotations themselves. I handled
+calls to Allocate and Storage_Size explicitly. This latter set of rules doesn't
+handle implicitly called Allocate/Deallocate calls in assignement statements,
+but that could be handled explicitly as well if the approach is OK.
+
+If there is a problem with this strategy, it is that there isn't any way to
+localize access types to a particular pool (when that is known but the type
+isn't visible). You would have to use a package name for a local access type
+(usually youself). For instance, all of the operations of Ada.Containers.Vectors
+would need Global in => (others in Vectors) because of the (presumably) local
+access type declared to implement the unbounded-ness.
+
+I don't think there is enough benefit to further complications here (especially
+as the containers example, the pool isn't visible either, so I can't imagine any
+other annotation that would work), but I am willing to be convinced otherwise.
+
+An alternative approach 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 ??? for general access object ["others" is the only
+current thing, which would be nasty]. That would be easier for tools to use, I
+suspect, but harder to write and less specific. Which doesn't seem to be an
+improvement to me.
+
+---
+
+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 applied. But I continually got stuck by the fact that there are essentially
+4 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];
+the kind of annotation (either "in" or "out"); and which annotation it is (Global
+or Global_Init). 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.
+
 !discussion
 
 The global in and global out annotations are intended to be descriptive.
-That is, the annotations describe the behavior of the subprogram body.
+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).
@@ -142,10 +436,10 @@
 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 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.
+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.
 
 ---
 
@@ -164,6 +458,8 @@
 correct, but if the subprogram is called, then the compiler must use the actual
 side-effects, not any assumed because of annotations.
 
+[I didn't try to word this. - Randy]
+
 ---
 
 It might make the most sense to define these in Annex H (High-Integrity Systems),
@@ -173,6 +469,33 @@
 for future analysis when improved tools are available. The legality rules
 ensure that the information is accurate.
 
+---
+
+We have two kinds of global annotations, one for callable entities (Global)
+and one for the initialization/elaboration of entities. We need both as
+there is a (small) overlap for access-to-subprogram types, which is both a
+type and an callable entity.
+
+Global_Init 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_Init annotations for types requires this. 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_Init (along
+with default initialization), and explicitly talking about the operations
+of storage pools.
 
 !example
 
@@ -580,5 +903,98 @@
 
 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.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent