[gcc r12-2121] [Ada] Implement new legality checks specified by AI12-0412

[gcc r12-2121] [Ada] Implement new legality checks specified by AI12-0412

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:14212dc422ed09f8324bbfd1dec662cbb2fdbe0e

commit r12-2121-g14212dc422ed09f8324bbfd1dec662cbb2fdbe0e
Author: Gary Dismukes <dismukes@adacore.com>
Date:   Mon May 17 03:35:25 2021 -0400

    [Ada] Implement new legality checks specified by AI12-0412
    
    gcc/ada/
    
            * freeze.adb (Check_Inherited_Conditions): Setting of Ekind,
            LSP_Subprogram, and Is_Wrapper needs to happen for null
            procedures as well as other wrapper cases, so the code is moved
            from the else part in front of the if statement.  (Fixes a
            latent bug encountered while working on this set of changes.)
            * sem_attr.adb (Resolve_Attribute): Report an error for the case
            of an Access attribute applied to a primitive of an abstract
            type when the primitive has any nonstatic Pre'Class or
            Post'Class expressions.
            * sem_ch8.adb (Analyze_Subprogram_Renaming): Report an error for
            the case of a actual subprogram associated with a nonabstract
            formal subprogram when the actual is a primitive of an abstract
            type and the primitive has any nonstatic Pre'Class or Post'Class
            expressions.
            * sem_disp.adb (Check_Dispatching_Context): Remove special
            testing for null procedures, and replace it with a relaxed test
            that avoids getting an error about illegal calls to abstract
            subprograms in cases where RM 6.1.1(7/5) applies in
            Pre/Post'Class aspects. Also, remove special test for
            Postcondition, which seems to be unnecessary, update associated
            comments, and fix a typo in one comment.
            (Check_Dispatching_Call): Remove an unneeded return statement,
            and report an error for the case of a nondispatching call to a
            nonabstract subprogram of an abstract type where the subprogram
            has nonstatic Pre/Post'Class aspects.
            * sem_util.ads
            (Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post): New function.
            (In_Pre_Post_Condition): Add a flag formal Class_Wide_Only,
            defaulted to False, for indicating whether the function should
            only test for the node being within class-wide pre- and
            postconditions.
            * sem_util.adb
            (Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post): New function
            to determine whether a subprogram is a primitive of an abstract
            type where the primitive has class-wide Pre/Post'Class aspects
            specified with nonstatic expressions.
            (In_Pre_Post_Condition): Extend testing to account for the new
            formal Class_Wide_Only.

Diff:
---
 gcc/ada/freeze.adb   | 12 +++++-----
 gcc/ada/sem_attr.adb | 19 +++++++++++++++
 gcc/ada/sem_ch8.adb  | 28 +++++++++++++++++-----
 gcc/ada/sem_disp.adb | 67 +++++++++++++++++++++++++++++++++-------------------
 gcc/ada/sem_util.adb | 67 +++++++++++++++++++++++++++++++++++++++++++++-------
 gcc/ada/sem_util.ads | 12 ++++++++--
 6 files changed, 159 insertions(+), 46 deletions(-)

diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index fa16887c0d7..37964337c3a 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -1671,6 +1671,12 @@ package body Freeze is
                --  type declaration that generates inherited operation. For
                --  a null procedure, the declaration implies a null body.
 
+               --  Before insertion, do some minimal decoration of fields
+
+               Mutate_Ekind (New_Id, Ekind (Par_Prim));
+               Set_LSP_Subprogram (New_Id, Par_Prim);
+               Set_Is_Wrapper (New_Id);
+
                if Nkind (New_Spec) = N_Procedure_Specification
                  and then Null_Present (New_Spec)
                then
@@ -1684,12 +1690,6 @@ package body Freeze is
                     Build_Class_Wide_Clone_Call
                       (Loc, Decls, Par_Prim, New_Spec);
 
-                  --  Adding minimum decoration
-
-                  Mutate_Ekind (New_Id, Ekind (Par_Prim));
-                  Set_LSP_Subprogram (New_Id, Par_Prim);
-                  Set_Is_Wrapper (New_Id);
-
                   Insert_List_After_And_Analyze
                     (Par_R, New_List (New_Decl, New_Body));
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index e0b2072307f..d1a91d8864e 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -11499,6 +11499,25 @@ package body Sem_Attr is
                Error_Msg_F ("context requires a non-protected subprogram", P);
             end if;
 
+            --  AI12-0412: The rule in RM 6.1.1(18.2/5) disallows applying
+            --  attribute Access to a primitive of an abstract type when the
+            --  primitive has any Pre'Class or Post'Class aspects specified
+            --  with nonstatic expressions.
+
+            if Attr_Id = Attribute_Access
+              and then Ekind (Btyp) in E_Access_Subprogram_Type
+                                     | E_Anonymous_Access_Subprogram_Type
+              and then Is_Entity_Name (P)
+              and then Is_Dispatching_Operation (Entity (P))
+              and then
+                Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Entity (P))
+            then
+               Error_Msg_N
+                 ("attribute not allowed for primitive of abstract type with "
+                   & "nonstatic class-wide pre/postconditions",
+                  N);
+            end if;
+
             --  The context cannot be a pool-specific type, but this is a
             --  legality rule, not a resolution rule, so it must be checked
             --  separately, after possibly disambiguation (see AI-245).
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index f056a189b2d..78d2426610c 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -3790,15 +3790,31 @@ package body Sem_Ch8 is
             Set_Has_Delayed_Freeze (New_S, False);
             Freeze_Before (N, New_S);
 
-            --  An abstract subprogram is only allowed as an actual in the case
-            --  where the formal subprogram is also abstract.
-
             if (Ekind (Old_S) = E_Procedure or else Ekind (Old_S) = E_Function)
-              and then Is_Abstract_Subprogram (Old_S)
               and then not Is_Abstract_Subprogram (Formal_Spec)
             then
-               Error_Msg_N
-                 ("abstract subprogram not allowed as generic actual", Nam);
+               --  An abstract subprogram is only allowed as an actual in the
+               --  case where the formal subprogram is also abstract.
+
+               if Is_Abstract_Subprogram (Old_S) then
+                  Error_Msg_N
+                    ("abstract subprogram not allowed as generic actual", Nam);
+               end if;
+
+               --  AI12-0412: A primitive of an abstract type with Pre'Class
+               --  or Post'Class aspects specified with nonstatic expressions
+               --  is not allowed as actual for a nonabstract formal subprogram
+               --  (see RM 6.1.1(18.2/5).
+
+               if Is_Dispatching_Operation (Old_S)
+                 and then
+                   Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Old_S)
+               then
+                  Error_Msg_N
+                    ("primitive of abstract type with nonstatic class-wide "
+                      & "pre/postconditions not allowed as actual",
+                     Nam);
+               end if;
             end if;
          end if;
 
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 06c4b07c0c7..064e2b5da14 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -612,29 +612,32 @@ package body Sem_Disp is
                Set_Entity (Name (N), Alias (Subp));
                return;
 
-            --  An obscure special case: a null procedure may have a class-
-            --  wide pre/postcondition that includes a call to an abstract
-            --  subp. Calls within the expression may not have been rewritten
-            --  as dispatching calls yet, because the null body appears in
-            --  the current declarative part. The expression will be properly
-            --  rewritten/reanalyzed when the postcondition procedure is built.
-
-            --  Similarly, if this is a pre/postcondition for an abstract
-            --  subprogram, it may call another abstract function which is
-            --  a primitive of an abstract type. The call is non-dispatching
-            --  but will be legal in overridings of the operation. However,
-            --  if the call is tag-indeterminate we want to continue with
-            --  with the error checking below, as this case is illegal even
-            --  for abstract subprograms (see AI12-0170).
-
-            elsif (Is_Subprogram (Scop)
-                    or else Chars (Scop) = Name_Postcondition)
+            --  If this is a pre/postcondition for an abstract subprogram,
+            --  it may call another abstract function that is a primitive
+            --  of an abstract type. The call is nondispatching but will be
+            --  legal in overridings of the operation. However, if the call
+            --  is tag-indeterminate we want to continue with with the error
+            --  checking below, as this case is illegal even for abstract
+            --  subprograms (see AI12-0170).
+
+            --  Similarly, as per AI12-0412, a nonabstract subprogram may
+            --  have a class-wide pre/postcondition that includes a call to
+            --  an abstract primitive of the subprogram's controlling type.
+            --  Certain operations (nondispatching calls, 'Access, use as
+            --  a generic actual) applied to such a nonabstract subprogram
+            --  are illegal in the case where the type is abstract (see
+            --  RM 6.1.1(18.2/5)).
+
+            elsif Is_Subprogram (Scop)
+              and then not Is_Tag_Indeterminate (N)
+              and then In_Pre_Post_Condition (Call, Class_Wide_Only => True)
+
+              --  The tagged type associated with the called subprogram must be
+              --  the same as that of the subprogram with a class-wide aspect.
+
+              and then Is_Dispatching_Operation (Scop)
               and then
-                ((Is_Abstract_Subprogram (Scop)
-                   and then not Is_Tag_Indeterminate (N))
-                  or else
-                    (Nkind (Parent (Scop)) = N_Procedure_Specification
-                      and then Null_Present (Parent (Scop))))
+                Find_Dispatching_Type (Subp) = Find_Dispatching_Type (Scop)
             then
                null;
 
@@ -663,7 +666,7 @@ package body Sem_Disp is
                --  provides a tag to make the call dispatching. This requires
                --  the call to be the actual in an enclosing call, and that
                --  actual must be controlling. If the call is an operand of
-               --  equality, the other operand must not ve abstract.
+               --  equality, the other operand must not be abstract.
 
                if not Is_Tagged_Type (Typ)
                  and then not
@@ -970,7 +973,6 @@ package body Sem_Disp is
             end loop;
 
             Check_Dispatching_Context (N);
-            return;
 
          elsif Nkind (Parent (N)) in N_Subexpr then
             Check_Dispatching_Context (N);
@@ -985,6 +987,23 @@ package body Sem_Disp is
             return;
          end if;
 
+         --  If this is a nondispatching call to a nonabstract subprogram
+         --  and the subprogram has any Pre'Class or Post'Class aspects with
+         --  nonstatic values, then report an error. This is specified by
+         --  RM 6.1.1(18.2/5) (by AI12-0412).
+
+         if No (Control)
+           and then not Is_Abstract_Subprogram (Subp_Entity)
+           and then
+             Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Subp_Entity)
+         then
+            Error_Msg_N
+              ("nondispatching call to nonabstract subprogram of "
+                & "abstract type with nonstatic class-wide "
+                & "pre/postconditions",
+               N);
+         end if;
+
       else
          --  If dispatching on result, the enclosing call, if any, will
          --  determine the controlling argument. Otherwise this is the
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 799f720e673..12e5aa89775 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -13295,6 +13295,44 @@ package body Sem_Util is
           and then Nkind (Node (First_Elmt (Constits))) = N_Null;
    end Has_Null_Refinement;
 
+   ------------------------------------------
+   -- Has_Nonstatic_Class_Wide_Pre_Or_Post --
+   ------------------------------------------
+
+   function Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post
+     (Subp : Entity_Id) return Boolean
+   is
+      Disp_Type  : constant Entity_Id := Find_Dispatching_Type (Subp);
+      Prag       : Node_Id;
+      Pragma_Arg : Node_Id;
+
+   begin
+      if Present (Disp_Type)
+        and then Is_Abstract_Type (Disp_Type)
+        and then Present (Contract (Subp))
+      then
+         Prag := Pre_Post_Conditions (Contract (Subp));
+
+         while Present (Prag) loop
+            if Pragma_Name (Prag) in Name_Precondition | Name_Postcondition
+              and then Class_Present (Prag)
+            then
+               Pragma_Arg :=
+                 Nlists.First
+                   (Pragma_Argument_Associations (Prag));
+
+               if not Is_Static_Expression (Expression (Pragma_Arg)) then
+                  return True;
+               end if;
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+      end if;
+
+      return False;
+   end Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post;
+
    -------------------------------
    -- Has_Overriding_Initialize --
    -------------------------------
@@ -14431,7 +14469,9 @@ package body Sem_Util is
    -- In_Pre_Post_Condition --
    ---------------------------
 
-   function In_Pre_Post_Condition (N : Node_Id) return Boolean is
+   function In_Pre_Post_Condition
+     (N : Node_Id; Class_Wide_Only : Boolean := False) return Boolean
+   is
       Par     : Node_Id;
       Prag    : Node_Id := Empty;
       Prag_Id : Pragma_Id;
@@ -14457,13 +14497,24 @@ package body Sem_Util is
       if Present (Prag) then
          Prag_Id := Get_Pragma_Id (Prag);
 
-         return
-           Prag_Id = Pragma_Post
-             or else Prag_Id = Pragma_Post_Class
-             or else Prag_Id = Pragma_Postcondition
-             or else Prag_Id = Pragma_Pre
-             or else Prag_Id = Pragma_Pre_Class
-             or else Prag_Id = Pragma_Precondition;
+         if Class_Wide_Only then
+            return
+              Prag_Id = Pragma_Post_Class
+                or else Prag_Id = Pragma_Pre_Class
+                or else (Class_Present (Prag)
+                          and then (Prag_Id = Pragma_Post
+                                     or else Prag_Id = Pragma_Postcondition
+                                     or else Prag_Id = Pragma_Pre
+                                     or else Prag_Id = Pragma_Precondition));
+         else
+            return
+              Prag_Id = Pragma_Post
+                or else Prag_Id = Pragma_Post_Class
+                or else Prag_Id = Pragma_Postcondition
+                or else Prag_Id = Pragma_Pre
+                or else Prag_Id = Pragma_Pre_Class
+                or else Prag_Id = Pragma_Precondition;
+         end if;
 
       --  Otherwise the node is not enclosed by a pre/postcondition pragma
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index bacf8b42459..fb8309f4a2b 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1516,6 +1516,12 @@ package Sem_Util is
    --  integer for use in compile-time checking. Note: Level is restricted to
    --  be non-dynamic.
 
+   function Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post
+     (Subp : Entity_Id) return Boolean;
+   --  Return True if Subp is a primitive of an abstract type, where the
+   --  primitive has a class-wide pre- or postcondition whose expression
+   --  is nonstatic.
+
    function Has_Overriding_Initialize (T : Entity_Id) return Boolean;
    --  Predicate to determine whether a controlled type has a user-defined
    --  Initialize primitive (and, in Ada 2012, whether that primitive is
@@ -1634,9 +1640,11 @@ package Sem_Util is
    function In_Pragma_Expression (N : Node_Id; Nam : Name_Id) return Boolean;
    --  Returns true if the expression N occurs within a pragma with name Nam
 
-   function In_Pre_Post_Condition (N : Node_Id) return Boolean;
+   function In_Pre_Post_Condition
+     (N : Node_Id; Class_Wide_Only : Boolean := False) return Boolean;
    --  Returns True if node N appears within a pre/postcondition pragma. Note
-   --  the pragma Check equivalents are NOT considered.
+   --  the pragma Check equivalents are NOT considered. If Class_Wide_Only is
+   --  True, then tests for N appearing within a class-wide pre/postcondition.
 
    function In_Quantified_Expression (N : Node_Id) return Boolean;
    --  Returns true if the expression N occurs within a quantified expression