Version 1.1 of ai12s/ai12-0256-1.txt

Unformatted version of ai12s/ai12-0256-1.txt version 1.1
Other versions for file ai12s/ai12-0256-1.txt

!standard H.4.1(0)          18-01-31 AI12-0256-1/01
!class Amendment 18-01-31
!status work item 18-01-31
!status received 18-01-21
!priority Very_Low
!difficulty Easy
!subject Aspect No_Controlled_Subcomponents
Aspect No_Controlled_Subcomponents is added to Ada.
In high-integrity, embedded applications, it is usually necessary to prove that the program will not run into stack overflow or other problems. It is often required to prove these properties at the machine code level with a special tool. The use of dynamic finalization greatly complicates such analysis as it depends on implicit dynamic dispatching. Thus many such applications ban finalization.
On the other hand, it is desirable, and becoming accepted, to use tagged types and dynamic dispatching even in high-integrity applications. Static analysis tools for stack usage can usually deal with the dynamic dispatching (even if it introduces some over-estimation), but a harder problem is that dynamic dispatching requires class-wide subtypes.
In general, class-wide subtypes are compiled such that any possible future extension will work. That includes, of course, extensions that include controlled components. This brings in finalization overhead, even if none of the current types use any finalization.
It would be desirable to be able to declare that a type and any descendants will not use any finalization, so this overhead can be eliminated (and thus, eliminated from analysis).
(See Summary.)
[Editor's note: I'm not sure where this goes in the Standard. It seems related to H.4, High-Integrity Restrictions, and it IS a restriction, but only on a single type and its descendants. So I've put it there pending discussion.
H.4.1 Aspect No_Controlled_Subcomponents
Static Semantics
Given a type T, the following type-related, operational aspects may be specified:
The type of this aspect is Boolean. If True, requires that the type and any descendants do not have any controlled subcomponents. If specified, the value of the expression shall be static. If not specified, the value of this aspect is considered False.
The No_Controlled_Subcomponents aspect is nonoverridable (see 13.1.1).
AARM Note: This effectively requires that the aspect is specified (other than as confirming) only on ultimate ancestor types that have no parent or progentitor types.
Legality Rules
If No_Controlled_Subcomponents is True for a type, no component of the type shall have a controlled subcomponent. In addition to the places where Legality Rules normally apply (see 12.3), this rule also applies in the private part of an instance of a generic unit.
When enforcing the above rule within a generic body, a generic formal private type and a generic formal derived type of a composite type are considered to have a controlled subcomponent.
AARM Reason: This is a typical generic assume-the-worst rule.
Modify 13.1.1(18.7/5) to include aspect No_Controlled_Subcomponents.
We could have extended this aspect to allow it to be given on generic formal types. If specified True there, then only types with this aspect specified True would match. This would allow declaring types with the aspect in a generic body which have components of generic formal private types. However, most such types can be declared in the private part of the generic (where assume-the-best is used and a recheck is made if necessary). So this was considered overkill.
The only Ada 2012 way to eliminate finalization is to use pragma Restrictions (No_Dependence => Ada.Finalization); However, this requires the entire program (including the runtime) to avoid using finalization. This means that features like storage pools and the bounded indefinite container(s) [see AI12-0254-1] cannot be used in such programs, even if they are designed with trivial finalization. (Most compilers can eliminate finalization overhead from objects with trivial finalization.)
The proposed aspect allows eliminating overhead specifically from class-wide type hierarchies while still allowing controlled types to appear in the runtime and elsewhere.
[Not sure. Not sure how aspects are handled - Editor.]
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.

This AI was split from AI12-0254-1. The original request for this aspect
can be found in the !appendix of that AI, in a message dated Sunday, January
21, 2018, 9:48 AM.


Questions? Ask the ACAA Technical Agent