[Ada] Implement new attribute Restriction_Set

This attribute allows compile time testing of restrictions that
are currently in effect. It is primarily intended for specializing
code in the run-time based on restrictions that are active (e.g.
don't need to save fpt registers if restriction No_Floating_Point
is known to be in effect), but can be used anywhere.

There are two forms:

   System'Restriction_Set (partition_boolean_restriction_NAME)

   System'Restriction_Set (No_Dependence => library_unit_NAME);

In the case of the first form, the only restriction names
allowed are parameterless restrictions that are checked
for consistency at bind time. For a complete list see the
subtype System.Rident.Partition_Boolean_Restrictions.

The result returned is True if the restriction is known to
be in effect, and False if the restriction is known not to
be in effect. An important guarantee is that the value of
a Restriction_Set attribute is known to be consistent throughout
all the code of a partition.

This is trivially achieved if the entire partition is compiled
with a consistent set of restriction pragmas. However, the
compilation model does not require this. It is possible to
compile one set of units with one set of pragmas, and another
set of units with another set of pragmas. It is even possible
to compile a spec with one set of pragmas, and then WITH the
same spec with a different set of pragmas. Inconsistencies
in the actual use of the restriction are checked at bind time.

In order to achieve the guarantee of consistency for the
Restriction_Set pragma, we consider that a use of the pragma
that yields False is equivalent to a violation of the
restriction.

So for example if you write

   if System'Restriction_Set (No_Floating_Point) then
      ...
   else
      ...
   end if;

And the result is False, so that the else branch is executed,
you can assume that this restriction is not set for any unit
in the partition. This is checked by considering this use of
the restriction pragma to be a violation of the restriction
No_Floating_Point. This means that no other unit can attempt
to set this restriction (if some unit does attempt to set it,
the binder will refuse to bind the partition).

Technical note: The restriction name and the unit name are
intepreted entirely syntactically, as in the corresponding
Restrictions pragma, they are not analyzed semantically,
so they do not have a type.

Notes:

We abandoned the three state model (known_set, known_not_set,
unknown) since it is just too difficult to reason about. It
does allow more flexibility, but our discussions indicated
that this flexibility was not worth the complexity.

We abandoned the requirement for WITHing System'Restrictions.
We no longer need it for the result, and it seems fine since
this is our own attribute to intepret the restriction names
purely syntactically.

We allow only the restrictions that are checked by the binder,
because those are the only ones for which we can make the
important guarantee of consistent evaluation throughout
the partition.

The following program compiles with the indicated errors
using the switch -gnatq:

     1. with System;
     2. package RSetBad is
     3.    X1 : Boolean := Standard'Restriction_Set (No_IO);     -- ERR
                           |
        >>> prefix of "Restriction_Set" attribute must be System

     4.    X2 : Boolean := System'Restriction_Set (No_IO);       -- OK
     5.    X3 : Boolean := System'Restriction_Set (SPARK_05);    -- ERR
                                                   |
        >>> "SPARK_05" is not a boolean partition-wide restriction

     6.    X4 : Boolean := System'Restriction_Set ("No_IO");     -- ERR
                                                   |
        >>> attribute "Restriction_Set" requires restriction identifier

     7.    X5 : Boolean := System'Restriction_Set (RSetBad);     -- ERR
                                                   |
        >>> invalid restriction identifier "RSetBad"

     8.    X6 : Boolean := System'Restriction_Set
     9.                      (No_Dependence => Ada.Text_IO);     -- OK
    10.    X7 : Boolean := System'Restriction_Set
    11.                      (No_Dependence => "Ada.Text_IO");   -- ERR
                                               |
        >>> name expected
        >>> wrong form for unit name for No_Dependence

    12.    X8 : Boolean := System'Restriction_Set
    13.                      (No_IO => Ada.Text_IO);             -- ERR
                                    1     2
        >>> named parameters not permitted for attributes
        >>> attribute "Restriction_Set" requires restriction identifier

    14. end;

The following program compiles without errors, and the resulting
binder files do not mention Calendar.

     1. pragma Restrictions (No_Delay);
     2. pragma Restrictions (No_Dependence => Ada.Text_IO);
     3. with System;
     4. with GNAT.IO; use GNAT.IO;
     5. procedure RSetGood is
     6. begin
     7.     if System'Restriction_Set (No_Floating_Point) then
     8.       Put_Line ("ERROR 1");
     9.    else
    10.       Put_Line ("OK 1");
    11.    end if;
    12.
    13.    if System'Restriction_Set (No_Delay) then
    14.       Put_Line ("OK 2");
    15.    else
    16.       Put_Line ("ERROR 2");
    17.    end if;
    18.
    19.    if System'Restriction_Set (No_Dependence => Ada.Text_IO) then
    20.       Put_Line ("OK 3");
    21.    else
    22.       Put_Line ("ERROR 3");
    23.    end if;
    24.
    25.    if System'Restriction_Set (No_Dependence => Ada.Calendar) then
    26.       Put_Line ("ERROR 4");
    27.    else
    28.       Put_Line ("OK 4");
    29.    end if;
    30.
    31. end RSetGood;

The output of the above program is:

OK 1
OK 2
OK 3
OK 4

Finally given the two additional units:

     1. with RsetGood;
     2. with RsetGood2;
     3. procedure RsetGoodM is
     4. begin
     5.    null;
     6. end;

     1. pragma Restrictions (No_Dependence => Ada.Calendar);
     2. pragma Restrictions (No_Floating_Point);
     3. package RsetGood2 is
     4. end;

The attempt to build RsetGoodM as a main program fails
at bind time with the output:

error: "rsetgood2.ads" has restriction No_Floating_Point
error: but the following files violate this restriction:
error:   "rsetgood.adb"
error: file "rsetgood.adb" violates restriction
  No_Dependence => "ada.calendar"

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-07-08  Robert Dewar  <dewar@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference): Add dummy entry
	for Restriction_Set.
	* gnat_rm.texi: Add missing menu entry for Attribute Ref Add
	documentation for attribute Restriction_Set.
	* lib-writ.adb (Write_With_Lines): Generate special W lines
	for Restriction_Set.
	* lib-writ.ads: Document special use of W lines for
	Restriction_Set.
	* lib.ads (Restriction_Set_Dependences): New table.
	* par-ch4.adb (Is_Parameterless_Attribute): Add Loop_Entry to
	list (Scan_Name_Extension_Apostrophe): Remove kludge test for
	Loop_Entry (Scan_Name_Extension_Apostrophe): Handle No_Dependence
	for Restricton_Set.
	* restrict.adb (Check_SPARK_Restriction): Put in Alfa order
	(OK_No_Dependence_Unit_Name): New function.
	* restrict.ads (OK_No_Dependence_Unit_Name): New function.
	* rtsfind.adb: Minor reformatting Minor code reorganization.
	* sem_attr.adb (Analyze_Attribute): Add processing for
	Restriction_Set.
	* sem_prag.adb (Process_Restrictions_Or_Restriction_Warnings):
	Remove Check_Unit_Name and use new function
	OK_No_Dependence_Unit_Name instead.
	* sinfo.ads: Minor comment updates.
	* snames.ads-tmpl: Add entry for Restriction_Set attribute.

[Ada] Implement new attribute Restriction_Set

Commit Message

Patch