Patchwork [Ada] Implement new aspects Dynamic_Predicate and Static_Predicate

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 1, 2011, 10:33 a.m.
Message ID <20110801103312.GA10499@adacore.com>
Download mbox | patch
Permalink /patch/107714/
State New
Headers show

Comments

Arnaud Charlet - Aug. 1, 2011, 10:33 a.m.
This patch introduces two new aspects. Dynamic_Predicate provides
a subtype predicate which can have any form, but the result cannot
be used in loops and case statements. Static_Predicate limits the
form of expressions to be static in the sense previously implemented
for the static case of Predicate previously, and the subtype can be
used in case and loop constructs. The previously implemented plain
Predicate aspect, which is implicitly static if the expression meets
the static requirements is retained as an impl-defined aspect.

The following test shows the diagnosis of errors:

     1. pragma Ada_2012;
     2. procedure statdynampred1 (A : Integer) is
     3.    subtype R1 is Integer with
     4.      Static_Predicate => R1 > A; -- not static
                                 |
        >>> expression does not have required form for
            static predicate

     5.
     6.    subtype R2 is Integer with
     7.      Dynamic_Predicate => R2 in 3 .. 7;
     8.
     9. begin
    10.    for J in R2 loop  -- not a static predicate
                    |
        >>> cannot use subtype "R2" with non-static
            predicate for loop iteration

    11.       null;
    12.    end loop;
    13. end;

The following test compiles clean:

     1. pragma Ada_2012;
     2. with Text_IO; use Text_IO;
     3. procedure statdynampred2 is
     4.    procedure SD (A : Integer) is
     5.       subtype R1 is Integer with
     6.         Dynamic_Predicate => R1 > A; -- not static
     7.
     8.       subtype R2 is Integer with
     9.         Static_Predicate => R2 in 3 .. 7;
    10.
    11.    begin
    12.       for J in R2 loop  -- not a static predicate
    13.          Put_Line (J'Img);
    14.       end loop;
    15.
    16.       Put_Line (Boolean'Image (100 in R1));
    17.       Put_Line (Boolean'Image (10 in R1));
    18.    end;
    19.
    20. begin
    21.    SD (23);
    22. end;

And generates output:

 3
 4
 5
 6
 7
TRUE
FALSE

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

2011-08-01  Robert Dewar  <dewar@adacore.com>

	* aspects.ads, aspects.adb: Add Static_Predicate and Dynamic_Predicate.
	* sem_ch13.adb (Analyze_Aspect_Specification): Add processing for
	Static_Predicate and Dynamic_Predicate.
	(Build_Predicate_Function): Add processing for Static_Predicate
	and Dynamic_Predicate.
	* sinfo.ads, sinfo.adb (From_Dynamic_Predicate): New flag
	(From_Static_Predicate): New flag
	* snames.ads-tmpl: Add Name_Static_Predicate and Name_Dynamic_Predicate

Patch

Index: sinfo.adb
===================================================================
--- sinfo.adb	(revision 177008)
+++ sinfo.adb	(working copy)
@@ -1360,6 +1360,22 @@ 
       return Flag6 (N);
    end From_Default;
 
+   function From_Dynamic_Predicate
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Pragma);
+      return Flag7 (N);
+   end From_Dynamic_Predicate;
+
+   function From_Static_Predicate
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Pragma);
+      return Flag8 (N);
+   end From_Static_Predicate;
+
    function Generic_Associations
       (N : Node_Id) return List_Id is
    begin
@@ -4388,6 +4404,22 @@ 
       Set_Flag6 (N, Val);
    end Set_From_Default;
 
+   procedure Set_From_Dynamic_Predicate
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Pragma);
+      Set_Flag7 (N, Val);
+   end Set_From_Dynamic_Predicate;
+
+   procedure Set_From_Static_Predicate
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Pragma);
+      Set_Flag8 (N, Val);
+   end Set_From_Static_Predicate;
+
    procedure Set_Generic_Associations
       (N : Node_Id; Val : List_Id) is
    begin
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 177008)
+++ sinfo.ads	(working copy)
@@ -497,13 +497,6 @@ 
    --    has been inserted at the flagged node. This is used to avoid the
    --    generation of duplicate checks.
 
-   --  Has_Local_Raise (Flag8-Sem)
-   --    Present in exception handler nodes. Set if the handler can be entered
-   --    via a local raise that gets transformed to a goto statement. This will
-   --    always be set if Local_Raise_Statements is non-empty, but can also be
-   --    set as a result of generation of N_Raise_xxx nodes, or flags set in
-   --    nodes requiring generation of back end checks.
-
    ------------------------------------
    -- Description of Semantic Fields --
    ------------------------------------
@@ -1108,6 +1101,14 @@ 
    --    declaration is treated as an implicit reference to the formal in the
    --    ali file.
 
+   --  From_Dynamic_Predicate (Flag7-Sem)
+   --    Set for generated pragma Predicate node if this is generated by a
+   --    Dynamic_Predicate aspect.
+
+   --  From_Static_Predicate (Flag8-Sem)
+   --    Set for generated pragma Predicate node if this is generated by a
+   --    Static_Predicate aspect.
+
    --  Generic_Parent (Node5-Sem)
    --    Generic_Parent is defined on declaration nodes that are instances. The
    --    value of Generic_Parent is the generic entity from which the instance
@@ -1132,6 +1133,13 @@ 
    --    handler is deleted during optimization. For further details on why
    --    this is required, see Exp_Ch11.Remove_Handler_Entries.
 
+   --  Has_Local_Raise (Flag8-Sem)
+   --    Present in exception handler nodes. Set if the handler can be entered
+   --    via a local raise that gets transformed to a goto statement. This will
+   --    always be set if Local_Raise_Statements is non-empty, but can also be
+   --    set as a result of generation of N_Raise_xxx nodes, or flags set in
+   --    nodes requiring generation of back end checks.
+
    --  Has_No_Elaboration_Code (Flag17-Sem)
    --    A flag that appears in the N_Compilation_Unit node to indicate whether
    --    or not elaboration code is present for this unit. It is initially set
@@ -2074,6 +2082,8 @@ 
       --  Aspect_Cancel (Flag11-Sem)
       --  Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
       --  Class_Present (Flag6) set if from Aspect with 'Class
+      --  From_Dynamic_Predicate (Flag7-Sem) Set if Dynamic_Predicate aspect
+      --  From_Static_Predicate (Flag8-Sem) Set if Static_Predicate aspect
 
       --  Note: we should have a section on what pragmas are passed on to
       --  the back end to be processed. This section should note that pragma
@@ -8390,6 +8400,12 @@ 
    function From_Default
      (N : Node_Id) return Boolean;    -- Flag6
 
+   function From_Dynamic_Predicate
+     (N : Node_Id) return Boolean;    -- Flag7
+
+   function From_Static_Predicate
+     (N : Node_Id) return Boolean;    -- Flag8
+
    function Generic_Associations
      (N : Node_Id) return List_Id;    -- List3
 
@@ -9356,6 +9372,12 @@ 
    procedure Set_From_Default
      (N : Node_Id; Val : Boolean := True);    -- Flag6
 
+   procedure Set_From_Dynamic_Predicate
+     (N : Node_Id; Val : Boolean := True);    -- Flag7
+
+   procedure Set_From_Static_Predicate
+     (N : Node_Id; Val : Boolean := True);    -- Flag8
+
    procedure Set_Generic_Associations
      (N : Node_Id; Val : List_Id);            -- List3
 
@@ -11775,6 +11797,8 @@ 
    pragma Inline (From_At_End);
    pragma Inline (From_At_Mod);
    pragma Inline (From_Default);
+   pragma Inline (From_Dynamic_Predicate);
+   pragma Inline (From_Static_Predicate);
    pragma Inline (Generic_Associations);
    pragma Inline (Generic_Formal_Declarations);
    pragma Inline (Generic_Parent);
@@ -12094,6 +12118,8 @@ 
    pragma Inline (Set_From_At_End);
    pragma Inline (Set_From_At_Mod);
    pragma Inline (Set_From_Default);
+   pragma Inline (Set_From_Dynamic_Predicate);
+   pragma Inline (Set_From_Static_Predicate);
    pragma Inline (Set_Generic_Associations);
    pragma Inline (Set_Generic_Formal_Declarations);
    pragma Inline (Set_Generic_Parent);
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 176998)
+++ aspects.adb	(working copy)
@@ -81,6 +81,7 @@ 
      (Name_Atomic_Components,            Aspect_Atomic_Components),
      (Name_Bit_Order,                    Aspect_Bit_Order),
      (Name_Component_Size,               Aspect_Component_Size),
+     (Name_Dynamic_Predicate,            Aspect_Dynamic_Predicate),
      (Name_Discard_Names,                Aspect_Discard_Names),
      (Name_External_Tag,                 Aspect_External_Tag),
      (Name_Favor_Top_Level,              Aspect_Favor_Top_Level),
@@ -101,6 +102,7 @@ 
      (Name_Read,                         Aspect_Read),
      (Name_Shared,                       Aspect_Shared),
      (Name_Size,                         Aspect_Size),
+     (Name_Static_Predicate,             Aspect_Static_Predicate),
      (Name_Storage_Pool,                 Aspect_Storage_Pool),
      (Name_Storage_Size,                 Aspect_Storage_Size),
      (Name_Stream_Size,                  Aspect_Stream_Size),
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 177005)
+++ aspects.ads	(working copy)
@@ -47,6 +47,7 @@ 
       Aspect_Alignment,
       Aspect_Bit_Order,
       Aspect_Component_Size,
+      Aspect_Dynamic_Predicate,
       Aspect_External_Tag,
       Aspect_Input,
       Aspect_Invariant,
@@ -55,9 +56,10 @@ 
       Aspect_Output,
       Aspect_Post,
       Aspect_Pre,
-      Aspect_Predicate,
+      Aspect_Predicate,                     -- GNAT
       Aspect_Read,
       Aspect_Size,
+      Aspect_Static_Predicate,
       Aspect_Storage_Pool,
       Aspect_Storage_Size,
       Aspect_Stream_Size,
@@ -128,6 +130,7 @@ 
                         Aspect_Alignment                    => Expression,
                         Aspect_Bit_Order                    => Expression,
                         Aspect_Component_Size               => Expression,
+                        Aspect_Dynamic_Predicate            => Expression,
                         Aspect_External_Tag                 => Expression,
                         Aspect_Input                        => Name,
                         Aspect_Invariant                    => Expression,
@@ -139,6 +142,7 @@ 
                         Aspect_Predicate                    => Expression,
                         Aspect_Read                         => Name,
                         Aspect_Size                         => Expression,
+                        Aspect_Static_Predicate             => Expression,
                         Aspect_Storage_Pool                 => Name,
                         Aspect_Storage_Size                 => Expression,
                         Aspect_Stream_Size                  => Expression,
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 177008)
+++ sem_ch13.adb	(working copy)
@@ -1054,9 +1054,12 @@ 
                --  declaration, to get the required pragma placement. The
                --  pragma processing takes care of the required delay.
 
-               when Aspect_Predicate =>
+               when Aspect_Dynamic_Predicate |
+                    Aspect_Predicate         |
+                    Aspect_Static_Predicate  =>
 
-                  --  Construct the pragma
+                  --  Construct the pragma (always a pragma Predicate, with
+                  --  flags recording whether
 
                   Aitem :=
                     Make_Pragma (Loc,
@@ -1068,6 +1071,14 @@ 
 
                   Set_From_Aspect_Specification (Aitem, True);
 
+                  --  Set special flags for dynamic/static cases
+
+                  if A_Id = Aspect_Dynamic_Predicate then
+                     Set_From_Dynamic_Predicate (Aitem);
+                  elsif A_Id = Aspect_Static_Predicate then
+                     Set_From_Static_Predicate (Aitem);
+                  end if;
+
                   --  Make sure we have a freeze node (it might otherwise be
                   --  missing in cases like subtype X is Y, and we would not
                   --  have a place to build the predicate function).
@@ -3818,6 +3829,13 @@ 
       Object_Name : constant Name_Id := New_Internal_Name ('I');
       --  Name for argument of Predicate procedure
 
+      Dynamic_Predicate_Present : Boolean := False;
+      --  Set True if a dynamic predicate is present, results in the entire
+      --  predicate being considered dynamic even if it looks static
+
+      Static_Predicate_Present : Node_Id := Empty;
+      --  Set to N_Pragma node for a static predicate if one is encountered.
+
       --------------
       -- Add_Call --
       --------------
@@ -3903,6 +3921,12 @@ 
             if Nkind (Ritem) = N_Pragma
               and then Pragma_Name (Ritem) = Name_Predicate
             then
+               if From_Dynamic_Predicate (Ritem) then
+                  Dynamic_Predicate_Present := True;
+               elsif From_Static_Predicate (Ritem) then
+                  Static_Predicate_Present := Ritem;
+               end if;
+
                Arg1 := First (Pragma_Argument_Associations (Ritem));
                Arg2 := Next (Arg1);
 
@@ -3945,7 +3969,7 @@ 
    begin
       --  Initialize for construction of statement list
 
-      Expr  := Empty;
+      Expr := Empty;
 
       --  Return if already built or if type does not have predicates
 
@@ -4034,8 +4058,19 @@ 
                            E_Modular_Integer_Subtype,
                            E_Signed_Integer_Subtype)
            and then Is_Static_Subtype (Typ)
+           and then not Dynamic_Predicate_Present
          then
             Build_Static_Predicate (Typ, Expr, Object_Name);
+
+            if Present (Static_Predicate_Present)
+              and No (Static_Predicate (Typ))
+            then
+               Error_Msg_F
+                 ("expression does not have required form for "
+                  & "static predicate",
+                  Next (First (Pragma_Argument_Associations
+                                (Static_Predicate_Present))));
+            end if;
          end if;
       end if;
    end Build_Predicate_Function;
@@ -5002,10 +5037,12 @@ 
 
          --  Pre/Post/Invariant/Predicate take boolean expressions
 
-         when Aspect_Pre       |
-              Aspect_Post      |
-              Aspect_Invariant |
-              Aspect_Predicate =>
+         when Aspect_Dynamic_Predicate |
+              Aspect_Invariant         |
+              Aspect_Pre               |
+              Aspect_Post              |
+              Aspect_Predicate         |
+              Aspect_Static_Predicate  =>
             T := Standard_Boolean;
       end case;
 
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 176998)
+++ snames.ads-tmpl	(working copy)
@@ -137,8 +137,10 @@ 
    --  Names of aspects for which there are no matching pragmas or attributes
    --  so that they need to be included for aspect specification use.
 
+   Name_Dynamic_Predicate              : constant Name_Id := N + $;
    Name_Post                           : constant Name_Id := N + $;
    Name_Pre                            : constant Name_Id := N + $;
+   Name_Static_Predicate               : constant Name_Id := N + $;
 
    --  Some special names used by the expander. Note that the lower case u's
    --  at the start of these names get translated to extra underscores. These