diff mbox series

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

Message ID 20210707162531.GA2543133@adacore.com
State New
Headers show
Series [Ada] Implement new legality checks specified by AI12-0412 | expand

Commit Message

Pierre-Marie de Rodat July 7, 2021, 4:25 p.m. UTC 
Ada 2022, in AI12-0412, specifies that certain uses of primitives of an
abstract type that have Pre'Class or Post'Class aspect are illegal when
an aspect is given with a nonstatic expression. Specifically, if the
primitive is nonabstract and has such aspects, it's illegal to make a
nondispatching call to it, as well as to apply 'Access to it or pass it
as an actual for a nonabstract formal subprogram.

Furthermore, by AI12-0170, as revised by AI12-0412, one can specify
class-wide Pre and Post with calls to abstract functions, where any
actuals given by a formal parameter of the primitive with the class-wide
aspect are reinterpreted using a "notional (nonabstract) type" for any
primitive of an abstract type, whether or not the primitive is abstract,
and part of these changes now allows such aspects for nonabstract
primitive cases that were formerly being rejected (previously GNAT was
only allowing this for null procedures).

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

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 mbox series

Patch

diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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