Patchwork [Ada] Reorganize handling of predicates

login
register
mail settings
Submitter Arnaud Charlet
Date July 18, 2014, 10:07 a.m.
Message ID <20140718100709.GA7904@adacore.com>
Download mbox | patch
Permalink /patch/371437/
State New
Headers show

Comments

Arnaud Charlet - July 18, 2014, 10:07 a.m.
This reorganizes the handling of predicates, in preparation for proper
implementation of real predicates. Several minor errors are corrected
and we properly reject improper static real predicates. Static string
predicates are now always rejected, in line with latest ARG thinking.
The following shows how far we have got. Quite a few minor errors are
fixed in recognizing predicate-static expressions. Still to be done
is actual compile-time testing of real static predicates, and also
noting that constants for which a predicate fails should not be
considered as static.

     1. package TestSP is
     2.    subtype F1 is Float with -- OK
     3.      Static_Predicate => F1 > 0.0 and 4.7 > F1;
     4.    subtype F2 is Float with -- ERROR
     5.      Static_Predicate => (F2 + 1.0) > 0.0 and 4.7 > F2;
                                  |
        >>> expression is not predicate-static (RM 4.3.2(16-22))

     6.    subtype F3 is Float with -- OK
     7.      Dynamic_Predicate => (F3 + 1.0) > 0.0 and 4.7 > F3;
     8.    subtype F4 is Float with -- OK
     9.      Predicate => (F4 + 1.0) > 0.0 and 4.7 > F4;
    10.
    11.    subtype S1 is String with -- OK
    12.      Static_Predicate => S1 > "ABC" and then "DEF" >= S1;
    13.    subtype S2 is String with -- ERROR
    14.      Static_Predicate => S2'First = 1 and then S2(1) = 'A';
                                 |
        >>> static predicate not allowed for non-scalar type "S2"

    15.    subtype S3 is String with -- OK
    16.      Dynamic_Predicate => S3'First = 1 and then S3(1) = 'A';
    17.    subtype S4 is String with -- OK
    18.      Predicate => S4'First = 1 and then S4(1) = 'A';
    19.
    20.    subtype I1 is Integer with -- OK
    21.      Static_Predicate => I1 > 0 and 4 > I1;
    22.    subtype I2 is Integer with -- ERROR
    23.      Static_Predicate => (I2 + 1) > 0 and 4 > I2;
                                  |
        >>> expression is not predicate-static (RM 4.3.2(16-22))

    24.    subtype I3 is Integer with -- OK
    25.      Dynamic_Predicate => (I3 + 1) > 0 and 4 > I3;
    26.    subtype I4 is Integer with -- OK
    27.      Predicate => (I4 + 1) > 0 and 4 > I4;
    28.    subtype I5 is Integer with -- ERROR (not caught before)
    29.      Static_Predicate => Boolean'(I5 > 0);
                                 |
        >>> expression is not predicate-static (RM 4.3.2(16-22))

    30.
    31.    XF1 : constant F1 := 10.0;
                                |
        >>> warning: real predicate not applied

    32.    XF2 : constant F1 := 3.0;
                                |
        >>> warning: real predicate not applied

    33.    XF3 : constant := XF1; -- ERROR (not caught yet)
    34.
    35.    XI1 : constant I1 := 10;
                                |
        >>> warning: static expression fails predicate check on "I1"

    36.    XI2 : constant I1 := 3;
    37.    XI3 : constant := XI1; -- ERROR (not caught yet)
    38. end;

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

2014-07-18  Robert Dewar  <dewar@adacore.com>

	* einfo.adb (Has_Static_Predicate): New function.
	(Set_Has_Static_Predicate): New procedure.
	* einfo.ads (Has_Static_Predicate): New flag.
	* sem_ch13.adb (Is_Predicate_Static): New function
	(Build_Predicate_Functions): Use Is_Predicate_Static to reorganize
	(Add_Call): Minor change in Sloc of generated expression
	(Add_Predicates): Remove setting of Static_Pred, no longer used.
	* sem_ch4.adb (Has_Static_Predicate): Removed this function,
	replace by use of the entity flag Has_Static_Predicate_Aspect.
	* sem_eval.adb (Eval_Static_Predicate_Check): Check real case
	and issue warning that predicate is not checked for now.
	* sem_eval.ads (Eval_Static_Predicate_Check): Fix comments in
	spec.
	* sem_util.adb (Check_Expression_Against_Static_Predicate):
	Carry out check for any case where there is a static predicate,
	and output appropriate message.
	* sinfo.ads: Minor comment corrections.

Patch

Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 212802)
+++ sinfo.ads	(working copy)
@@ -4022,13 +4022,13 @@ 
       --  to deal with, and diagnose a simple expression other than a name for
       --  the right operand. This simplifies error recovery in the parser.
 
-      --  The Alternatives field below is present only if there is more
-      --  than one Membership_Choice present (which is legitimate only in
-      --  Ada 2012 mode) in which case Right_Opnd is Empty, and Alternatives
-      --  contains the list of choices. In the tree passed to the back end,
-      --  Alternatives is always No_List, and Right_Opnd is set (i.e. the
-      --  expansion circuitry expands out the complex set membership case
-      --  using simple membership operations).
+      --  The Alternatives field below is present only if there is more than
+      --  one Membership_Choice present (which is legitimate only in Ada 2012
+      --  mode) in which case Right_Opnd is Empty, and Alternatives contains
+      --  the list of choices. In the tree passed to the back end, Alternatives
+      --  is always No_List, and Right_Opnd is set (i.e. the expansion circuit
+      --  expands out the complex set membership case using simple membership
+      --  and equality operations).
 
       --  Should we rename Alternatives here to Membership_Choices ???
 
@@ -4271,7 +4271,7 @@ 
       --  CASE_EXPRESSION ::=
       --    case SELECTING_EXPRESSION is
       --      CASE_EXPRESSION_ALTERNATIVE
-      --      {CASE_EXPRESSION_ALTERNATIVE}
+      --      {,CASE_EXPRESSION_ALTERNATIVE}
 
       --  Note that the Alternatives cannot include pragmas (this contrasts
       --  with the situation of case statements where pragmas are allowed).
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 212797)
+++ einfo.adb	(working copy)
@@ -415,7 +415,7 @@ 
    --    Has_Aliased_Components          Flag135
    --    No_Strict_Aliasing              Flag136
    --    Is_Machine_Code_Subprogram      Flag137
-   --    Is_Packed_Array_Impl_Type            Flag138
+   --    Is_Packed_Array_Impl_Type       Flag138
    --    Has_Biased_Representation       Flag139
    --    Has_Complex_Representation      Flag140
 
@@ -559,12 +559,12 @@ 
    --    SPARK_Aux_Pragma_Inherited      Flag266
    --    Has_Shift_Operator              Flag267
    --    Is_Independent                  Flag268
+   --    Has_Static_Predicate            Flag269
 
    --    (unused)                        Flag1
    --    (unused)                        Flag2
    --    (unused)                        Flag3
 
-   --    (unused)                        Flag269
    --    (unused)                        Flag270
 
    --    (unused)                        Flag271
@@ -1719,6 +1719,12 @@ 
       return Flag211 (Id);
    end Has_Static_Discriminants;
 
+   function Has_Static_Predicate (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag269 (Id);
+   end Has_Static_Predicate;
+
    function Has_Static_Predicate_Aspect (Id : E) return B is
    begin
       pragma Assert (Is_Type (Id));
@@ -4436,6 +4442,12 @@ 
       Set_Flag211 (Id, V);
    end Set_Has_Static_Discriminants;
 
+   procedure Set_Has_Static_Predicate (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag269 (Id, V);
+   end Set_Has_Static_Predicate;
+
    procedure Set_Has_Static_Predicate_Aspect (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Type (Id));
@@ -8243,6 +8255,7 @@ 
       W ("Has_Specified_Stream_Read",       Flag192 (Id));
       W ("Has_Specified_Stream_Write",      Flag193 (Id));
       W ("Has_Static_Discriminants",        Flag211 (Id));
+      W ("Has_Static_Predicate",            Flag269 (Id));
       W ("Has_Static_Predicate_Aspect",     Flag259 (Id));
       W ("Has_Storage_Size_Clause",         Flag23  (Id));
       W ("Has_Stream_Size_Clause",          Flag184 (Id));
@@ -8325,7 +8338,7 @@ 
       W ("Is_Optional_Parameter",           Flag134 (Id));
       W ("Is_Package_Body_Entity",          Flag160 (Id));
       W ("Is_Packed",                       Flag51  (Id));
-      W ("Is_Packed_Array_Impl_Type",            Flag138 (Id));
+      W ("Is_Packed_Array_Impl_Type",       Flag138 (Id));
       W ("Is_Potentially_Use_Visible",      Flag9   (Id));
       W ("Is_Predicate_Function",           Flag255 (Id));
       W ("Is_Predicate_Function_M",         Flag256 (Id));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 212797)
+++ einfo.ads	(working copy)
@@ -1511,11 +1511,18 @@ 
 
 --    Has_Dynamic_Predicate_Aspect (Flag258)
 --       Defined in all types and subtypes. Set if a Dynamic_Predicate aspect
---       applies to the type. Note that we can tell if a dynamic predicate is
---       present by looking at Has_Predicates and Static_Predicate, but that
---       could have come from a Predicate aspect or pragma, and we need to
---       record the difference so that we can use the right set of check
---       policies to figure out if the predicate is active.
+--       was explicitly applied to the type. Generally we treat predicates as
+--       static if possible, regardless of whether they are specified using
+--       Predicate, Static_Predicate, or Dynamic_Predicate. And if a predicate
+--       can be treated as static (i.e. its expression is predicate-static),
+--       then the flag Has_Static_Predicate will be set True. But there are
+--       cases where legality is affected by the presence of an explicit
+--       Dynamic_Predicate aspect. For example, even if a predicate looks
+--       static, you can't use it in a case statement if there is an explicit
+--       Dynamic_Predicate aspect specified. So test Has_Static_Predicate if
+--       you just want to know if the predicate can be evaluated statically,
+--       but test Has_Dynamic_Predicate_Aspect to enforce legality rules about
+--       the use of dynamic predicates.
 
 --    Has_Entries (synthesized)
 --       Applies to concurrent types. True if any entries are declared
@@ -1870,13 +1877,23 @@ 
 --       case of a variant record, the component list can be trimmed down to
 --       include only the components corresponding to these discriminants.
 
+--    Has_Static_Predicate (Flag269)
+--       Defined in all types and subtypes. Set if the type (which must be
+--       a discrete, real, or string subtype) has a static predicate, i.e. a
+--       predicate whose expression is predicate-static. This can result from
+--       use of a Predicate, Static_Predicate or Dynamic_Predicate aspect. We
+--       can distinguish these cases by testing Has_Static_Predicate_Aspect
+--       and Has_Dynamic_Predicate_Aspect. See description of the latter flag
+--       for further information on dynamic predicates which are also static.
+
 --    Has_Static_Predicate_Aspect (Flag259)
 --       Defined in all types and subtypes. Set if a Static_Predicate aspect
 --       applies to the type. Note that we can tell if a static predicate is
---       present by looking at Has_Predicates and Static_Predicate, but that
---       could have come from a Predicate aspect or pragma, and we need to
---       record the difference so that we can use the right set of check
---       policies to figure out if the predicate is active.
+--       present by looking at Has_Static_Predicate, but this could have come
+--       from a Predicate aspect or pragma or even from a Dynamic_Predicate
+--       aspect. When we need to know the difference (e.g. to know what set of
+--       check policies apply, use this flag and Has_Dynamic_Predicate_Aspect
+--       to determine which case we have.
 
 --    Has_Storage_Size_Clause (Flag23) [implementation base type only]
 --       Defined in task types and access types. It is set if a Storage_Size
@@ -3873,15 +3890,15 @@ 
 --       the corresponding parameter entities in the spec.
 
 --    Static_Predicate (List25)
---       Defined in discrete types/subtypes with predicates (Has_Predicates
---       set). Set if the type/subtype has a static predicate. Points to a
---       list of expression and N_Range nodes that represent the predicate
---       in canonical form. The canonical form has entries sorted in ascending
---       order, with duplicates eliminated, and adjacent ranges coalesced, so
---       that there is always a gap in the values between successive entries.
---       The entries in this list are fully analyzed and typed with the base
---       type of the subtype. Note that all entries are static and have values
---       within the subtype range.
+--       Defined in discrete types/subtypes with static predicates (with the
+--       two flags Has_Predicates set and Has_Static_Predicate set). Set if the
+--       type/subtype has a static predicate. Points to a list of expression
+--       and N_Range nodes that represent the predicate in canonical form. The
+--       canonical form has entries sorted in ascending order, with duplicates
+--       eliminated, and adjacent ranges coalesced, so that there is always a
+--       gap in the values between successive entries. The entries in this list
+--       are fully analyzed and typed with the base type of the subtype. Note
+--       that all entries are static and have values within the subtype range.
 
 --    Status_Flag_Or_Transient_Decl (Node15)
 --       Defined in variables and constants. Applies to objects that require
@@ -5188,6 +5205,7 @@ 
    --    Has_Specified_Stream_Output         (Flag191)
    --    Has_Specified_Stream_Read           (Flag192)
    --    Has_Specified_Stream_Write          (Flag193)
+   --    Has_Static_Predicate                (Flag269)
    --    Has_Static_Predicate_Aspect         (Flag259)
    --    Has_Task                            (Flag30)   (base type only)
    --    Has_Unchecked_Union                 (Flag123)  (base type only)
@@ -6540,6 +6558,7 @@ 
    function Has_Specified_Stream_Read           (Id : E) return B;
    function Has_Specified_Stream_Write          (Id : E) return B;
    function Has_Static_Discriminants            (Id : E) return B;
+   function Has_Static_Predicate                (Id : E) return B;
    function Has_Static_Predicate_Aspect         (Id : E) return B;
    function Has_Storage_Size_Clause             (Id : E) return B;
    function Has_Stream_Size_Clause              (Id : E) return B;
@@ -7166,6 +7185,7 @@ 
    procedure Set_Has_Specified_Stream_Read       (Id : E; V : B := True);
    procedure Set_Has_Specified_Stream_Write      (Id : E; V : B := True);
    procedure Set_Has_Static_Discriminants        (Id : E; V : B := True);
+   procedure Set_Has_Static_Predicate            (Id : E; V : B := True);
    procedure Set_Has_Static_Predicate_Aspect     (Id : E; V : B := True);
    procedure Set_Has_Storage_Size_Clause         (Id : E; V : B := True);
    procedure Set_Has_Stream_Size_Clause          (Id : E; V : B := True);
@@ -7905,6 +7925,7 @@ 
    pragma Inline (Has_Specified_Stream_Read);
    pragma Inline (Has_Specified_Stream_Write);
    pragma Inline (Has_Static_Discriminants);
+   pragma Inline (Has_Static_Predicate);
    pragma Inline (Has_Static_Predicate_Aspect);
    pragma Inline (Has_Storage_Size_Clause);
    pragma Inline (Has_Stream_Size_Clause);
@@ -8378,6 +8399,7 @@ 
    pragma Inline (Set_Has_Specified_Stream_Read);
    pragma Inline (Set_Has_Specified_Stream_Write);
    pragma Inline (Set_Has_Static_Discriminants);
+   pragma Inline (Set_Has_Static_Predicate);
    pragma Inline (Set_Has_Static_Predicate_Aspect);
    pragma Inline (Set_Has_Storage_Size_Clause);
    pragma Inline (Set_Has_Stream_Size_Clause);
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 212802)
+++ sem_util.adb	(working copy)
@@ -1695,13 +1695,13 @@ 
    begin
       --  When the predicate is static and the value of the expression is known
       --  at compile time, evaluate the predicate check. A type is non-static
-      --  when it has aspect Dynamic_Predicate.
+      --  when it has aspect Dynamic_Predicate, but if the dynamic predicate
+      --  was predicate-static, we still check it statically. After all this
+      --  is only a warning, not an error.
 
       if Compile_Time_Known_Value (Expr)
         and then Has_Predicates (Typ)
-        and then Is_Discrete_Type (Typ)
-        and then Present (Static_Predicate (Typ))
-        and then not Has_Dynamic_Predicate_Aspect (Typ)
+        and then Has_Static_Predicate (Typ)
       then
          --  Either -gnatc is enabled or the expression is ok
 
@@ -1710,12 +1710,14 @@ 
          then
             null;
 
-         --  The expression is prohibited by the static predicate
+         --  The expression is prohibited by the static predicate. There has
+         --  been some debate if this is an illegality (in the case where
+         --  the static predicate was explicitly given as such), but that
+         --  discussion decided this was not illegal, just a warning situation.
 
          else
             Error_Msg_NE
-              ("??static expression fails static predicate check on &",
-               Expr, Typ);
+              ("??static expression fails predicate check on &", Expr, Typ);
          end if;
       end if;
    end Check_Expression_Against_Static_Predicate;
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 212787)
+++ sem_ch4.adb	(working copy)
@@ -1331,9 +1331,6 @@ 
    -----------------------------
 
    procedure Analyze_Case_Expression (N : Node_Id) is
-      function Has_Static_Predicate (Subtyp : Entity_Id) return Boolean;
-      --  Determine whether subtype Subtyp has aspect Static_Predicate
-
       procedure Non_Static_Choice_Error (Choice : Node_Id);
       --  Error routine invoked by the generic instantiation below when
       --  the case expression has a non static choice.
@@ -1350,28 +1347,6 @@ 
            Process_Associated_Node   => No_OP);
       use Case_Choices_Checking;
 
-      --------------------------
-      -- Has_Static_Predicate --
-      --------------------------
-
-      function Has_Static_Predicate (Subtyp : Entity_Id) return Boolean is
-         Item : Node_Id;
-
-      begin
-         Item := First_Rep_Item (Subtyp);
-         while Present (Item) loop
-            if Nkind (Item) = N_Aspect_Specification
-              and then Chars (Identifier (Item)) = Name_Static_Predicate
-            then
-               return True;
-            end if;
-
-            Next_Rep_Item (Item);
-         end loop;
-
-         return False;
-      end Has_Static_Predicate;
-
       -----------------------------
       -- Non_Static_Choice_Error --
       -----------------------------
@@ -1493,7 +1468,7 @@ 
       --  to bogus errors.
 
       if Is_Static_Subtype (Exp_Type)
-        and then Has_Static_Predicate (Exp_Type)
+        and then Has_Static_Predicate_Aspect (Exp_Type)
         and then In_Spec_Expression
       then
          null;
Index: sem_eval.adb
===================================================================
--- sem_eval.adb	(revision 212797)
+++ sem_eval.adb	(working copy)
@@ -3306,28 +3306,42 @@ 
       Typ : Entity_Id) return Boolean
    is
       Loc  : constant Source_Ptr := Sloc (N);
-      Pred : constant List_Id := Static_Predicate (Typ);
-      Test : Node_Id;
 
    begin
-      if No (Pred) then
-         return True;
-      end if;
+      --  Discrete type case
 
-      --  The static predicate is a list of alternatives in the proper format
-      --  for an Ada 2012 membership test. If the argument is a literal, the
-      --  membership test can be evaluated statically. The caller transforms
-      --  a result of False into a static contraint error.
+      if Is_Discrete_Type (Typ) then
+         declare
+            Pred : constant List_Id := Static_Predicate (Typ);
+            Test : Node_Id;
 
-      Test :=
-        Make_In (Loc,
-          Left_Opnd    => New_Copy_Tree (N),
-          Right_Opnd   => Empty,
-          Alternatives => Pred);
-      Analyze_And_Resolve (Test, Standard_Boolean);
+         begin
+            pragma Assert (Present (Pred));
 
-      return Nkind (Test) = N_Identifier
-        and then Entity (Test) = Standard_True;
+            --  The static predicate is a list of alternatives in the proper
+            --  format for an Ada 2012 membership test. If the argument is a
+            --  literal, the membership test can be evaluated statically. This
+            --  is easier than running a full intepretation of the predicate
+            --  expression, and more efficient in some cases.
+
+            Test :=
+              Make_In (Loc,
+                Left_Opnd    => New_Copy_Tree (N),
+                Right_Opnd   => Empty,
+                Alternatives => Pred);
+            Analyze_And_Resolve (Test, Standard_Boolean);
+
+            return Nkind (Test) = N_Identifier
+              and then Entity (Test) = Standard_True;
+         end;
+
+      --  Real type case
+
+      else
+         pragma Assert (Is_Real_Type (Typ));
+         Error_Msg_N ("??real predicate not applied", N);
+         return True;
+      end if;
    end Eval_Static_Predicate_Check;
 
    -------------------------
Index: sem_eval.ads
===================================================================
--- sem_eval.ads	(revision 212640)
+++ sem_eval.ads	(working copy)
@@ -248,7 +248,7 @@ 
    --  In general we take a pessimistic view. False does not mean the value
    --  could not be known at compile time, but True means that absolutely
    --  definition it is known at compile time and it is safe to call
-   --  Expr_Value on the expression Op.
+   --  Expr_Value[_XX] on the expression Op.
    --
    --  Note that we don't define precisely the set of expressions that return
    --  True. Callers should not make any assumptions regarding the value that
@@ -365,9 +365,11 @@ 
    procedure Eval_Unchecked_Conversion   (N : Node_Id);
 
    function Eval_Static_Predicate_Check
-     (N  : Node_Id;
-     Typ : Entity_Id) return Boolean;
-   --  Evaluate a static predicate check applied to a scalar literal
+     (N   : Node_Id;
+      Typ : Entity_Id) return Boolean;
+   --  Evaluate a static predicate check applied to a known at compile time
+   --  value N, which can be of a discrete, real or string type. The caller
+   --  has checked that a static predicate does apply to Typ.
 
    procedure Fold_Str (N : Node_Id; Val : String_Id; Static : Boolean);
    --  Rewrite N with a new N_String_Literal node as the result of the compile
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 212798)
+++ sem_ch13.adb	(working copy)
@@ -134,6 +134,34 @@ 
    --  that do not specify a representation characteristic are operational
    --  attributes.
 
+   function Is_Predicate_Static
+     (Expr : Node_Id;
+      Nam  : Name_Id) return Boolean;
+   --  Given predicate expression Expr, tests if Expr is predicate-static in
+   --  the sense of the rules in (RM 3.2.4 (15-24)). Occurrences of the type
+   --  name in the predicate expression have been replaced by references to
+   --  an identifier whose Chars field is Nam. This name is unique, so any
+   --  identifier with Chars matching Nam must be a reference to the type.
+   --  Returns True if the expression is predicate-static and False otherwise,
+   --  but is not in the business of setting flags or issuing error messages.
+   --
+   --  Only scalar types can have static predicates, so False is always
+   --  returned for non-scalar types.
+   --
+   --  Note: the RM seems to suggest that string types can also have static
+   --  predicates. But that really makes lttle sense as very few useful
+   --  predicates can be constructed for strings. Remember that:
+   --
+   --     "ABC" < "DEF"
+   --
+   --  is not a static expression. So even though the clearly faulty RM wording
+   --  allows the following:
+   --
+   --     subtype S is String with Static_Predicate => S < "DEF"
+   --
+   --  We can't allow this, otherwise we have predicate-static applying to a
+   --  larger class than static expressions, which was never intended.
+
    procedure New_Stream_Subprogram
      (N    : Node_Id;
       Ent  : Entity_Id;
@@ -7509,9 +7537,6 @@ 
       Raise_Expression_Present : Boolean := False;
       --  Set True if Expr has at least one Raise_Expression
 
-      Static_Predic : Node_Id := Empty;
-      --  Set to N_Pragma node for a static predicate if one is encountered
-
       procedure Add_Call (T : Entity_Id);
       --  Includes a call to the predicate function for type T in Expr if T
       --  has predicates and Predicate_Function (T) is non-empty.
@@ -7557,9 +7582,10 @@ 
 
             if No (Expr) then
                Expr := Exp;
+
             else
                Expr :=
-                 Make_And_Then (Loc,
+                 Make_And_Then (Sloc (Expr),
                    Left_Opnd  => Relocate_Node (Expr),
                    Right_Opnd => Exp);
             end if;
@@ -7630,16 +7656,6 @@ 
             if Nkind (Ritem) = N_Pragma
               and then Pragma_Name (Ritem) = Name_Predicate
             then
-               --  Save the static predicate of the type for diagnostics and
-               --  error reporting purposes.
-
-               if Present (Corresponding_Aspect (Ritem))
-                 and then Chars (Identifier (Corresponding_Aspect (Ritem))) =
-                            Name_Static_Predicate
-               then
-                  Static_Predic := Ritem;
-               end if;
-
                --  Acquire arguments
 
                Arg1 := First (Pragma_Argument_Associations (Ritem));
@@ -7963,51 +7979,80 @@ 
             end;
          end if;
 
-         if Is_Discrete_Type (Typ) then
+         --  See if we have a static predicate. Note that the answer may be
+         --  yes even if we have an explicit Dynamic_Predicate present.
 
-            --  Attempt to build a static predicate for a discrete subtype.
-            --  This action may fail because the actual expression may not be
-            --  static. Note that the presence of an inherited or explicitly
-            --  declared dynamic predicate is orthogonal to this check because
-            --  we are only interested in the static predicate.
+         declare
+            PS : constant Boolean := Is_Predicate_Static (Expr, Object_Name);
+            EN : Node_Id;
 
-            Build_Discrete_Static_Predicate (Typ, Expr, Object_Name);
+         begin
+            --  Case where we have a predicate static aspect
 
-            --  Emit an error when the predicate is categorized as static
-            --  but its expression is dynamic.
+            if PS then
 
-            if Present (Static_Predic)
-              and then No (Static_Predicate (Typ))
-            then
-               Error_Msg_F
-                 ("expression does not have required form for "
-                  & "static predicate",
-                  Next (First (Pragma_Argument_Associations
-                    (Static_Predic))));
-            end if;
+               --  We don't set Has_Static_Predicate_Aspect, since we can have
+               --  any of the three cases (Predicate, Dynamic_Predicate, or
+               --  Static_Predicate) generating a predicate with an expression
+               --  that is predicate static. We just indicate that we have a
+               --  predicate that can be treated as static.
 
-         --  If a static predicate applies on other types, that's an error:
-         --  either the type is scalar but non-static, or it's not even a
-         --  scalar type. We do not issue an error on generated types, as
-         --  these may be duplicates of the same error on a source type.
+               Set_Has_Static_Predicate (Typ);
 
-         elsif Present (Static_Predic) and then Comes_From_Source (Typ) then
-            if Is_Real_Type (Typ) then
-               Error_Msg_FE
-                 ("static predicates not implemented for real type&",
-                  Typ, Typ);
+               --  For discrete subtype, build the static predicate list
 
-            elsif Is_Scalar_Type (Typ) then
-               Error_Msg_FE
-                 ("static predicate not allowed for non-static type&",
-                  Typ, Typ);
+               if Is_Discrete_Type (Typ) then
+                  Build_Discrete_Static_Predicate (Typ, Expr, Object_Name);
 
+                  --  If we don't get a static predicate list, it means that we
+                  --  have a case where this is not possible, most typically in
+                  --  the case where we inherit a dynamic predicate. We do not
+                  --  consider this an error, we just leave the predicate as
+                  --  dynamic. But if we do succeed in building the list, then
+                  --  we mark the predicate as static.
+
+                  if No (Static_Predicate (Typ)) then
+                     Set_Has_Static_Predicate (Typ, False);
+                  end if;
+               end if;
+
+            --  Case of dynamic predicate (expression is not predicate-static)
+
             else
-               Error_Msg_FE
-                 ("static predicate not allowed for non-scalar type&",
-                  Typ, Typ);
+               --  Again, we don't set Has_Dynamic_Predicate_Aspect, since that
+               --  is only set if we have an explicit Dynamic_Predicate aspect
+               --  given. Here we may simply have a Predicate aspect where the
+               --  expression happens not to be predicate-static.
+
+               --  Emit an error when the predicate is categorized as static
+               --  but its expression is not predicate-static.
+
+               --  First a little fiddling to get a nice location for the
+               --  message. If the expression is of the form (A and then B),
+               --  then use the left operand for the Sloc. This avoids getting
+               --  confused by a call to a higher level predicate with a less
+               --  convenient source location.
+
+               EN := Expr;
+               while Nkind (EN) = N_And_Then loop
+                  EN := Left_Opnd (EN);
+               end loop;
+
+               --  Now post appropriate message
+
+               if Has_Static_Predicate_Aspect (Typ) then
+                  if Is_Scalar_Type (Typ) then
+                     Error_Msg_F
+                       ("expression is not predicate-static (RM 4.3.2(16-22))",
+                        EN);
+                  else
+                     Error_Msg_FE
+                       ("static predicate not allowed for non-scalar type&",
+                        EN, Typ);
+                  end if;
+               end if;
             end if;
-         end if;
+         end;
       end if;
    end Build_Predicate_Functions;
 
@@ -10293,6 +10338,210 @@ 
       end if;
    end Is_Operational_Item;
 
+   -------------------------
+   -- Is_Predicate_Static --
+   -------------------------
+
+   function Is_Predicate_Static
+     (Expr : Node_Id;
+      Nam  : Name_Id) return Boolean
+   is
+      function All_Static_Case_Alternatives (L : List_Id) return Boolean;
+      --  Given a list of case expression alternatives, returns True if
+      --  all the alternative are static (have all static choices, and a
+      --  static expression).
+
+      function All_Static_Choices (L : List_Id) return Boolean;
+      --  Returns true if all elements of the list are ok static choices
+      --  as defined below for Is_Static_Choice. Used for case expression
+      --  alternatives and for the right operand of a membership test.
+
+      function Is_Static_Choice (N : Node_Id) return Boolean;
+      --  Returns True if N represents a static choice (static subtype, or
+      --  static subtype indication, or static expression or static range).
+      --
+      --  Note that this is a bit more inclusive than we actually need
+      --  (in particular membership tests do not allow the use of subtype
+      --  indications. But that doesn't matter, we have already checked
+      --  that the construct is legal to get this far.
+
+      function Is_Type_Ref (N : Node_Id) return Boolean;
+      pragma Inline (Is_Type_Ref);
+      --  Returns if True if N is a reference to the type for the predicate in
+      --  the expression (i.e. if it is an identifier whose Chars field matches
+      --  the Nam given in the call). N must not be parenthesized, if the type
+      --  name appears in parens, this routine will return False.
+
+      ----------------------------------
+      -- All_Static_Case_Alternatives --
+      ----------------------------------
+
+      function All_Static_Case_Alternatives (L : List_Id) return Boolean is
+         N : Node_Id;
+
+      begin
+         N := First (L);
+         while Present (N) loop
+            if not (All_Static_Choices (Discrete_Choices (N))
+                     and then Is_OK_Static_Expression (Expression (N)))
+            then
+               return False;
+            end if;
+
+            Next (N);
+         end loop;
+
+         return True;
+      end All_Static_Case_Alternatives;
+
+      ------------------------
+      -- All_Static_Choices --
+      ------------------------
+
+      function All_Static_Choices (L : List_Id) return Boolean is
+         N : Node_Id;
+
+      begin
+         N := First (L);
+         while Present (N) loop
+            if not Is_Static_Choice (N) then
+               return False;
+            end if;
+
+            Next (N);
+         end loop;
+
+         return True;
+      end All_Static_Choices;
+
+      ----------------------
+      -- Is_Static_Choice --
+      ----------------------
+
+      function Is_Static_Choice (N : Node_Id) return Boolean is
+      begin
+         return Is_OK_Static_Expression (N)
+           or else (Is_Entity_Name (N) and then Is_Type (Entity (N))
+                     and then Is_OK_Static_Subtype (Entity (N)))
+           or else (Nkind (N) = N_Subtype_Indication
+                     and then Is_OK_Static_Subtype (Entity (N)))
+           or else (Nkind (N) = N_Range and then Is_OK_Static_Range (N));
+      end Is_Static_Choice;
+
+      -----------------
+      -- Is_Type_Ref --
+      -----------------
+
+      function Is_Type_Ref (N : Node_Id) return Boolean is
+      begin
+         return Nkind (N) = N_Identifier
+           and then Chars (N) = Nam
+           and then Paren_Count (N) = 0;
+      end Is_Type_Ref;
+
+   --  Start of processing for Is_Predicate_Static
+
+   begin
+      --  Only scalar types can be predicate static
+
+      if not Is_Scalar_Type (Etype (Expr)) then
+         return False;
+      end if;
+
+      --  Predicate_Static means one of the following holds. Numbers are the
+      --  corresponding paragraph numbers in (RM 3.2.4(16-22)).
+
+      --  16: A static expression
+
+      if Is_OK_Static_Expression (Expr) then
+         return True;
+
+      --  17: A membership test whose simple_expression is the current
+      --  instance, and whose membership_choice_list meets the requirements
+      --  for a static membership test.
+
+      elsif Nkind (Expr) in N_Membership_Test
+        and then ((Present (Right_Opnd (Expr))
+                    and then Is_Static_Choice (Right_Opnd (Expr)))
+                  or else
+                    (Present (Alternatives (Expr))
+                      and then All_Static_Choices (Alternatives (Expr))))
+      then
+         return True;
+
+      --  18. A case_expression whose selecting_expression is the current
+      --  instance, and whose dependent expressions are static expressions.
+
+      elsif Nkind (Expr) = N_Case_Expression
+        and then Is_Type_Ref (Expression (Expr))
+        and then All_Static_Case_Alternatives (Alternatives (Expr))
+      then
+         return True;
+
+      --  19. A call to a predefined equality or ordering operator, where one
+      --  operand is the current instance, and the other is a static
+      --  expression.
+
+      elsif Nkind (Expr) in N_Op_Compare
+        and then ((Is_Type_Ref (Left_Opnd (Expr))
+                    and then Is_OK_Static_Expression (Right_Opnd (Expr)))
+                  or else
+                    (Is_Type_Ref (Right_Opnd (Expr))
+                      and then Is_OK_Static_Expression (Left_Opnd (Expr))))
+      then
+         return True;
+
+      --  20. A call to a predefined boolean logical operator, where each
+      --  operand is predicate-static.
+
+      elsif (Nkind_In (Expr, N_Op_And, N_Op_Or, N_Op_Xor)
+              and then Is_Predicate_Static (Left_Opnd (Expr), Nam)
+              and then Is_Predicate_Static (Right_Opnd (Expr), Nam))
+        or else
+            (Nkind (Expr) = N_Op_Not
+              and then Is_Predicate_Static (Right_Opnd (Expr), Nam))
+      then
+         return True;
+
+      --  21. A short-circuit control form where both operands are
+      --  predicate-static.
+
+      elsif Nkind (Expr) in N_Short_Circuit
+        and then Is_Predicate_Static (Left_Opnd (Expr), Nam)
+        and then Is_Predicate_Static (Right_Opnd (Expr), Nam)
+      then
+         return True;
+
+      --  22. A parenthesized predicate-static expression. This does not
+      --  require any special test, since we just ignore paren levels in
+      --  all the cases above.
+
+      --  One more test that is an implementation artifact caused by the fact
+      --  that we are analyzing not the original expresesion, but the generated
+      --  expression in the body of the predicate function. This can include
+      --  refereces to inherited predicates, so that the expression we are
+      --  processing looks like:
+
+      --    expression and then xxPredicate (typ (Inns))
+
+      --  Where the call is to a Predicate function for an inherited predicate.
+      --  We simply ignore such a call (which could be to either a dynamic or
+      --  a static predicate, but remember that we can have Static_Predicate
+      --  for a non-static subtype).
+
+      elsif Nkind (Expr) = N_Function_Call
+        and then Is_Predicate_Function (Entity (Name (Expr)))
+      then
+         return True;
+
+      --  That's an exhaustive list of tests, all other cases are not
+      --  predicate static, so we return False.
+
+      else
+         return False;
+      end if;
+   end Is_Predicate_Static;
+
    ---------------------
    -- Kill_Rep_Clause --
    ---------------------