!standard 13.12(0) (00)                               99-07-27  AI95-00190/03
!standard D.7 (15)
!class binding interpretation 98-10-09
!status Corrigendum 2000 99-07-27
!status WG9 approved 99-06-12
!status ARG approved (6-0-0) 98-10-09
!status work item 98-09-26
!status received 97-08-19
!priority Medium
!difficulty Hard
!subject Compile-time enforcement of pragma Restrictions

!summary

Whenever enforcement of a restriction imposed by pragma Restrictions
is not required by the Standard prior to execution, but left to
implementation-defined behaviour of dynamic semantics, it is
reasonable to interpret pre-execution enforcement as a valid
implementation-defined behaviour, provided that every execution of the
partition will violate the restriction.

!question

Shall we allow implementations to reject (i.e. refuse to run) programs
that have run-time detected violations of pragma Restrictions, when they
are detectable at compile time? (Yes.)

!recommendation

(see summary)

!wording

Add an Implementation Permission after 13.12(9):

"Whenever enforcement of a restriction is not required prior to
execution, but left to implementation-defined behaviour of dynamic
semantics, an implementation may enforce the restriction prior to
execution of a partition to which the restriction applies, provided
that every execution of the partition would violate the restriction."

!discussion

For the particularly critical rejection of programs that violate
restrictions imposed by pragma Restrictions, the Standard provides for
implementation-defined behaviour in lieu of a compile- or link-time
check otherwise required by 13.12(8). It is reasonable to interpret
pre-execution enforcement of a configuration pragma as a valid
implementation-defined behaviour, even if such enforcement is not
required to occur prior to execution. This is particularly true for
D.7(15), as this clause recommends the raising of a Storage_Error
exception but does not specify the place where such an exception is to
be raised.

!corrigendum 13.12(9)

@dinsa
An implementation may place limitations on the values of the expression
that are supported, and limitations on the supported combinations of
restrictions. The consequences of violating such limitations are
implementation defined.
@dinst
Whenever enforcement of a restriction is not required prior to
execution, but left to implementation-defined behavior of dynamic
semantics, an implementation may enforce the restriction prior to
execution of a partition to which the restriction applies, provided
that every execution of the partition would violate the restriction.

!ACATS test

This is not testable, as is an implementation permission.

!appendix

!section 13.12(0)
!subject rejecting violations of pragma Restrictions
!reference RM95 13.12
!from Ted Baker 97-04-20
!reference 1997-15747.a Ted Baker  1997-4-20>>
!discussion

At the April 1997 ARG meeting, the issue came up of whether a
compiler that detects a violation of a restriction specified in a
Restrictions pragma may reject the input at compile time or link
time, as compared to being required to compile and link the code,
so that it can run and raise Program_Error at run time.

At issue is the treatment of those restrictions where the ARM
gives permission for a language-defined restriction to be checked
at run time, e.g.  D.7 (16-19).  There seems to be agreement that,
for example, a compiler can reject a compilation that violates the
static semantic restrictions in D.7 (2-13), or that violates an
implementation-defined restriction.

Bob Duff argued that the ARM consistently makes a strong
separation between what can cause a program to be rejected prior
to execution time, and what can cause a runtime error.  He argued
that to allow a compiler to reject a program for the violation of
the restrictions in D.7 (2-13) would be inconsistent with this
policy.

I do know know for certain that this putative strong separation
exists, but assuming it does, I question its value and
appropriateness in this case.

There are at least two reasonable lines of argument to support
allowing a compiler to reject compilations where it detects a
violation of a restriction:

1) Treatment of other implementation restrictions by the ARM95.
2) The language describing the restrictions pragma, itself.

| 13.12 Pragma Restrictions
| 1   A pragma Restrictions expresses the user's intent to abide by certain
| restrictions.  This may facilitate the construction of simpler run-time
| environments.
...
|                            Post-Compilation Rules
...
| 8   A pragma Restrictions is a configuration pragma; unless otherwise
| specified for a particular restriction, a partition shall obey the
                                                      ^^^^^
| restriction if a pragma Restrictions applies to any compilation unit included
| in the partition.
...
|                          Implementation Permissions
...
| 9   An implementation may place limitations on the values of the expression
| that are supported, and limitations on the supported combinations of
| restrictions.  The consequences of violating such limitations are
| implementation defined.

It is reasonable to interpret an occurrence of the Restrictions
pragma as (at least) giving the implementation permission to
impose the stated restrictions or (capacity limits) on the
compilation.  If those restrictions are violated, it should have
the range of options available for other implementation
restrictions and capacity limits.

Throughout the ARM, there are references to places where an
implementation may impose capacity limits or other forms of
restrictions.  The usual correct reaction to a program that violates
a capacity limit or other restriction is to reject the compilation,
if it is detected at compile time.  For example, consider the
declaration of a numeric type whose range exceeds that supported
by the implementation.

RM95 says, regarding capacity limits:

| 1.1.1 Extent
| 9   This International Standard does not specify:
| ....
|    15  The size of a program or program unit that will exceed the
|        capacity of a particular conforming implementation.
...
| 1.1.3 Conformity of an Implementation with the Standard
| 1   A conforming implementation shall:
...
|     3  Identify all programs or program units that are so large as to
|        exceed the capacity of the implementation (or raise an
|        appropriate exception at run time);

Note that the implementation is given the CHOICE here of raising an
appropriate exception at run time, or rejecting the compilation.

Some of the examples of uses of the term "restriction" for
implementation limitations are in 10.1 (4) [compilations with
multiple compilation units], 10.1.5 (9) [configuration pragmas],
10.1 (29) [main subprograms], 13.1 (20) [representation items],
13.7.2 (6) [address_to_access_conversions], 13.8 (8) [machine code
insertions], 13.9 (13) [unchecked_conversion], B.1 (42)
[interfacing pragmas].

In the most of these cases it is conventionally accepted that
violation of the restriction is grounds for rejecting of a
compilation or linkage.  (In the case of
address_to_access_conversions, it is not clear whether the
compiler might reject an instantiation at compile time or cause an
exception to be raised at the point of instantiation.)

Note that the description of the effect of the pragma restrictions
says "unless otherwise specified for a particular restriction, a
partition shall obey the restriction".  This requires a pre-runtime
check, unless specified otherwise.

Here is some of the relevant ARM95 text about pre-runtime checks:

| 1.1.5 Classification of Errors
|                          Implementation Requirements
| 1   The language definition classifies errors into several different
| categories:
|     2   Errors that are required to be detected prior to run time by
|        every Ada implementation;
|        3   These errors correspond to any violation of a rule given in
|        this International Standard, other than those listed below.  In
|        particular, violation of any rule that uses the terms shall,
                                                               ^^^^^
|        allowed, permitted, legal, or illegal belongs to this category.
|        Any program that contains such an error is not a legal Ada
|        program; on the other hand, the fact that a program is legal does
|        not mean, per se, that the program is free from other forms of
|        error.

As I read it, the qualifying phrase "unless otherwise specified
for a particular restriction" is intended to give the
implementation permission not to detect certain violations prior
to run time, not to prevent them from doing so and rejecting the
program earlier if that is possible.

[As one of the authors of the material on tasking restrictions,
I can add that that is consistent with my own understanding of the
intent behind splitting up the list of tasking restrictions.]

Note also that in D.7 (15) we have, for the "dynamic" restrictions,
the following wording:

| 15   If the following restrictions are violated, the behavior is
| implementation defined.  If an implementation chooses to detect such a
| violation, Storage_Error should be raised.

It can be argued that the phase "the behavior is implementation
defined" gives the implementation the right to reject the violation
of the restriction prior to run time.

--Ted Baker

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