Version 1.3 of ai12s/ai12-0256-1.txt
!standard H.4.1(0) 18-07-06 AI12-0256-1/02
!standard 13.1.1(18.7/5)
!class Amendment 18-01-31
!status Amendment 1-2012 18-07-06
!status ARG Approved 10-0-0 18-06-23
!status work item 18-01-31
!status received 18-01-21
!priority Very_Low
!difficulty Easy
!subject Aspect No_Controlled_Parts
!summary
Aspect No_Controlled_Parts is added to Ada.
!problem
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).
!proposal
(See Summary.)
!wording
[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_Parts
Static Semantics
For a type, the following type-related, operational aspect may be specified:
No_Controlled_Parts
The type of this aspect is Boolean. If True, requires that the type and any
descendants do not have any controlled parts. If specified, the
value of the expression shall be static. If not specified, the value of
this aspect is considered False.
The No_Controlled_Parts aspect is nonoverridable (see 13.1.1).
Legality Rules
If No_Controlled_Parts is True for a type, no component of the type
shall have a controlled part nor shall the type itself be controlled. 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 part.
AARM Reason: This is a typical generic assume-the-worst rule.
Modify 13.1.1(18.7/5) to include aspect No_Controlled_Parts.
!discussion
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.
!corrigendum 13.1.1(18.6/5)
!comment This was the original paragraph number, AI12-0211-1 changed it.
!comment We have to use the original number here so that a conflict is
!comment properly detected.
@drepl
The Default_Iterator, Iterator_Element, Implicit_Dereference,
Constant_Indexing, Variable_Indexing, and Max_Entry_Queue_Length aspects are
nonoverridable.
@dby
The Default_Iterator, Iterator_Element, Implicit_Dereference,
Constant_Indexing, Variable_Indexing, Max_Entry_Queue_Length, and
No_Controlled_Parts aspects are nonoverridable.
!corrigendum H.4.1(0)
Insert new clause:
Static Semantics
For a type, the following type-related, operational aspect may be specified:
- No_Controlled_Parts
-
The type of this aspect is Boolean. If True, requires that the type and any
descendants do not have any controlled parts. If specified, the
value of the expression shall be static. If not specified, the value of
this aspect is considered False.
The No_Controlled_Parts aspect is nonoverridable (see 13.1.1).
Legality Rules
If No_Controlled_Parts is True for a type, no component of the type
shall have a controlled part nor shall the type itself be controlled. 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 part.
!ASIS
[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.
!appendix
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.
****************************************************************
From: Bob Duff
Sent: Sunday, April 15, 2018 4:54 PM
[He's replying to an off-hand remark on a Letter Ballot - Editor.]
> I don’t see any of them as important, and the ones I haven’t voted for
> at all as possibly even being harmful, but here’s my 5 most useful.
...
> ______ AI12-0256-1/01 2018-01-31 -- Aspect No_Controlled_Subcomponents
Why do you consider that one harmful? There's the usual (every new feature
causes implementation cost, and cost to define it in the RM, and adds
complexity to the language). Anything else?
****************************************************************
From: Jeff Cousins
Sent: Monday, April 16, 2018 2:12 AM
I should have said apart from that one (which I'm neutral about).
****************************************************************
Questions? Ask the ACAA Technical Agent