[Ada] AI12-0042: Type invariant checking rules

Message ID 20200716092051.GA146371@adacore.com
State New
Headers show
Series
  • [Ada] AI12-0042: Type invariant checking rules
Related show

Commit Message

Pierre-Marie de Rodat July 16, 2020, 9:20 a.m.
AI12-0042 specifies a couple of new rules for type invariants. The first
is that when a type extension inherits a nonabstract subprogram that is
a private operation of an ancestor type that has a class-wide invariant
and the parent subprogram is visible at that point, the subprogram must
be overridden. The second is the addition of a requirement to perform an
invariant check on a conversion from a specific tagged expression to a
class-wide type T'Class whose root type imposes a type invariant, when
the conversion occurs within the immediate scope of T (checking the
invariant on the part of the conversion expression that is of type T).

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

gcc/ada/

	* exp_ch4.adb (Expand_N_Type_Conversion): Handle the case of
	applying an invariant check for a conversion to a class-wide
	type whose root type has a type invariant, when the conversion
	appears within the immediate scope of the type and the
	expression is of a specific tagged type.
	* sem_ch3.adb (Is_Private_Primitive): New function to determine
	whether a primitive subprogram is a private operation.
	(Check_Abstract_Overriding): Enforce the restriction imposed by
	AI12-0042 of requiring overriding of an inherited nonabstract
	private operation when the ancestor has a class-wide type
	invariant and the ancestor's private operation is visible.
	(Derive_Subprogram): Set Requires_Overriding on a subprogram
	inherited from a visible private operation of an ancestor to
	which a Type_Invariant'Class expression applies.

Patch

diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -11951,6 +11951,39 @@  package body Exp_Ch4 is
          Remove_Side_Effects (N);
          Insert_Action (N, Make_Invariant_Call (Duplicate_Subexpr (N)));
          goto Done;
+
+      --  AI12-0042: For a view conversion to a class-wide type occurring
+      --  within the immediate scope of T, from a specific type that is
+      --  a descendant of T (including T itself), an invariant check is
+      --  performed on the part of the object that is of type T. (We don't
+      --  need to explicitly check for the operand type being a descendant,
+      --  just that it's a specific type, because the conversion would be
+      --  illegal if it's specific and not a descendant -- downward conversion
+      --  is not allowed).
+
+      elsif Is_Class_Wide_Type (Target_Type)
+        and then not Is_Class_Wide_Type (Etype (Expression (N)))
+        and then Present (Invariant_Procedure (Root_Type (Target_Type)))
+        and then Comes_From_Source (N)
+        and then Within_Scope (Find_Enclosing_Scope (N), Scope (Target_Type))
+      then
+         Remove_Side_Effects (N);
+
+         --  Perform the invariant check on a conversion to the class-wide
+         --  type's root type.
+
+         declare
+            Root_Conv : constant Node_Id :=
+              Make_Type_Conversion (Loc,
+                Subtype_Mark =>
+                  New_Occurrence_Of (Root_Type (Target_Type), Loc),
+                Expression   => Duplicate_Subexpr (Expression (N)));
+         begin
+            Set_Etype (Root_Conv, Root_Type (Target_Type));
+
+            Insert_Action (N, Make_Invariant_Call (Root_Conv));
+            goto Done;
+         end;
       end if;
 
       --  Here if we may need to expand conversion


diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -579,6 +579,12 @@  package body Sem_Ch3 is
    --  Extensions_Visible with value False and has at least one controlling
    --  parameter of mode OUT.
 
+   function Is_Private_Primitive (Prim : Entity_Id) return Boolean;
+   --  Subsidiary to Check_Abstract_Overriding and Derive_Subprogram.
+   --  When applied to a primitive subprogram Prim, returns True if Prim is
+   --  declared as a private operation within a package or generic package,
+   --  and returns False otherwise.
+
    function Is_Valid_Constraint_Kind
      (T_Kind          : Type_Kind;
       Constraint_Kind : Node_Kind) return Boolean;
@@ -10754,6 +10760,32 @@  package body Sem_Ch3 is
          elsif Present (Interface_Alias (Subp)) then
             null;
 
+         --  AI12-0042: Test for rule in 7.3.2(6.1/4), that requires overriding
+         --  of a visible private primitive inherited from an ancestor with
+         --  the aspect Type_Invariant'Class, unless the inherited primitive
+         --  is abstract. (The test for the extension occurring in a different
+         --  scope than the ancestor is to avoid requiring overriding when
+         --  extending in the same scope, because the inherited primitive will
+         --  also be private in that case, which looks like an unhelpful
+         --  restriction that may break reasonable code, though the rule
+         --  appears to apply in the same-scope case as well???)
+
+         elsif not Is_Abstract_Subprogram (Subp)
+           and then not Comes_From_Source (Subp) -- An inherited subprogram
+           and then Requires_Overriding (Subp)
+           and then Present (Alias_Subp)
+           and then Has_Invariants (Etype (T))
+           and then Present (Get_Pragma (Etype (T), Pragma_Invariant))
+           and then Class_Present (Get_Pragma (Etype (T), Pragma_Invariant))
+           and then Is_Private_Primitive (Alias_Subp)
+           and then Scope (Subp) /= Scope (Alias_Subp)
+         then
+            Error_Msg_NE
+              ("inherited private primitive & must be overridden", T, Subp);
+            Error_Msg_N
+              ("\because ancestor type has 'Type_'Invariant''Class " &
+               "(RM 7.3.2(6.1))", T);
+
          elsif (Is_Abstract_Subprogram (Subp)
                  or else Requires_Overriding (Subp)
                  or else
@@ -15676,6 +15708,9 @@  package body Sem_Ch3 is
       --  Ada 2005 (AI-228): Calculate the "require overriding" and "abstract"
       --  properties of the subprogram, as defined in RM-3.9.3(4/2-6/2).
 
+      --  Ada 202x (AI12-0042): Similarly, set those properties for
+      --  implementing the rule of RM 7.3.2(6.1/4).
+
       --  A subprogram subject to pragma Extensions_Visible with value False
       --  requires overriding if the subprogram has at least one controlling
       --  OUT parameter (SPARK RM 6.1.7(6)).
@@ -15692,7 +15727,23 @@  package body Sem_Ch3 is
                                                         Derived_Type
                              and then not Is_Null_Extension (Derived_Type))
                    or else (Comes_From_Source (Alias (New_Subp))
-                             and then Is_EVF_Procedure (Alias (New_Subp))))
+                             and then Is_EVF_Procedure (Alias (New_Subp)))
+
+                   --  AI12-0042: Set Requires_Overriding when a type extension
+                   --  inherits a private operation that is visible at the
+                   --  point of extension (Has_Private_Ancestor is False) from
+                   --  an ancestor that has Type_Invariant'Class.
+
+                   or else
+                     (not Has_Private_Ancestor (Derived_Type)
+                       and then Has_Invariants (Parent_Type)
+                       and then
+                         Present (Get_Pragma (Parent_Type, Pragma_Invariant))
+                       and then
+                         Class_Present
+                           (Get_Pragma (Parent_Type, Pragma_Invariant))
+                       and then Is_Private_Primitive (Parent_Subp)))
+
         and then No (Actual_Subp)
       then
          if not Is_Tagged_Type (Derived_Type)
@@ -18727,6 +18778,29 @@  package body Sem_Ch3 is
       end if;
    end Is_Null_Extension;
 
+   --------------------------
+   -- Is_Private_Primitive --
+   --------------------------
+
+   function Is_Private_Primitive (Prim : Entity_Id) return Boolean is
+      Prim_Scope  : constant Entity_Id := Scope (Prim);
+      Priv_Entity : Entity_Id;
+   begin
+      if Is_Package_Or_Generic_Package (Prim_Scope) then
+         Priv_Entity := First_Private_Entity (Prim_Scope);
+
+         while Present (Priv_Entity) loop
+            if Priv_Entity = Prim then
+               return True;
+            end if;
+
+            Next_Entity (Priv_Entity);
+         end loop;
+      end if;
+
+      return False;
+   end Is_Private_Primitive;
+
    ------------------------------
    -- Is_Valid_Constraint_Kind --
    ------------------------------