[Ada] Allow specifying volatility refinement aspects for types

2020-06-11  Steve Baird  <baird@adacore.com>

gcc/ada/

	* contracts.adb (Add_Contract_Item): Support specifying
	volatility refinement aspects for types.
	(Analyze_Contracts): Add call to Analyze_Type_Contract in the
	case of a contract for a type.
	(Freeze_Contracts): Add call to Analyze_Type_Contract in the
	case of a contract for a type.
	(Check_Type_Or_Object_External_Properties): A new procedure
	which performs the work that needs to be done for both object
	declarations and types.
	(Analyze_Object_Contract): Add a call to
	Check_Type_Or_Object_External_Properties and remove the code in
	this procedure which did much of the work that is now performed
	by that call.
	(Analyze_Type_Contract): Implement this new routine as nothing
	more than a call to Check_Type_Or_Object_External_Properties.
	* contracts.ads: Update comment for Add_Contract_To_Item because
	types can have contracts.  Follow (questionable) precedent and
	declare new routine Analyze_Type_Contract as visible (following
	example of Analyze_Object_Contract), despite the fact that it is
	never called from outside of the package where it is declared.
	* einfo.adb (Contract, Set_Contract): Id argument can be a type;
	support this case.
	(Write_Field34_Name): Field name is "contract" for a type.
	* einfo.ads: Update comment describing Contract attribute.
	* sem_ch3.adb (Build_Derived_Numeric_Type): Is_Volatile should
	return same answer for all subtypes of a given type. Thus, when
	building the base type for something like type Volatile_1_To_10
	is range 1 .. 10 with Volatile; that basetype should be marked
	as being volatile.
	(Access_Type_Declaration): Add SPARK-specific legality check
	that the designated type of an access type shall be compatible
	with respect to volatility with the access type.
	* sem_ch12.adb (Check_Shared_Variable_Control_Aspects): Add
	SPARK-specific legality check that an actual type parameter in
	an instantiation shall be compatible with respect to volatility
	with the corresponding formal type.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Perform checks
	for aspect specs for the 4 volatility refinement aspects that
	were already being performed for all language-defined aspects.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part,
	Analyze_Pragma): External properties (other than No_Caching) may
	be specified for a type, including a generic formal type.
	* sem_util.ads: Declare new subprograms - Async_Readers_Enabled,
	Async_Writers_Enabled, Effective_Reads, Effective_Writes, and
	Check_Volatility_Compatibility.
	* sem_util.adb (Async_Readers_Enabled, Async_Writers_Enabled,
	Effective_Reads, Effective_Writes): Initial implementation of
	new functions for querying aspect values.
	(Check_Volatility_Compatibility): New procedure intended for use
	in checking all SPARK legality rules of the form "<> shall be
	compatible with respect to volatility with <>".
	(Has_Enabled_Property): Update comment because Item_Id can be a
	type.  Change name of nested Variable_Has_Enabled_Property
	function to Type_Or_Variable_Has_Enabled_Property; add a
	parameter to that function because recursion may be needed,
	e.g., in the case of a derived typ).  Cope with the case where
	the argument to Has_Enabled_Property is a type.

1 files changed, 290 insertions, 101 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 79078df..42f36d5 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -61,6 +61,11 @@ package body Contracts is
    --
    --    Part_Of
 
+   procedure Check_Type_Or_Object_External_Properties
+     (Type_Or_Obj_Id : Entity_Id);
+   --  Perform checking of external properties pragmas that is common to both
+   --  type declarations and object declarations.
+
    procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
    --  Expand the contracts of a subprogram body and its correspoding spec (if
    --  any). This routine processes all [refined] pre- and postconditions as
@@ -244,18 +249,33 @@ package body Contracts is
             raise Program_Error;
          end if;
 
-      --  Protected units, the applicable pragmas are:
-      --    Part_Of
-
-      elsif Ekind (Id) = E_Protected_Type then
-         if Prag_Nam = Name_Part_Of then
-            Add_Classification;
+      --  The four volatility refinement pragmas are ok for all types.
+      --  Part_Of is ok for task types and protected types.
+      --  Depends and Global are ok for task types.
+
+      elsif Is_Type (Id) then
+         declare
+            Is_OK : constant Boolean :=
+              Nam_In (Prag_Nam, Name_Async_Readers,
+                                Name_Async_Writers,
+                                Name_Effective_Reads,
+                                Name_Effective_Writes)
+              or else (Ekind (Id) = E_Task_Type
+                         and Nam_In (Prag_Nam, Name_Part_Of,
+                                               Name_Depends,
+                                               Name_Global))
+              or else (Ekind (Id) = E_Protected_Type
+                         and Prag_Nam = Name_Part_Of);
+         begin
+            if Is_OK then
+               Add_Classification;
+            else
 
-         --  The pragma is not a proper contract item
+               --  The pragma is not a proper contract item
 
-         else
-            raise Program_Error;
-         end if;
+               raise Program_Error;
+            end if;
+         end;
 
       --  Subprogram bodies, the applicable pragmas are:
       --    Postcondition
@@ -299,16 +319,6 @@ package body Contracts is
       --    Global
       --    Part_Of
 
-      elsif Ekind (Id) = E_Task_Type then
-         if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then
-            Add_Classification;
-
-         --  The pragma is not a proper contract item
-
-         else
-            raise Program_Error;
-         end if;
-
       --  Variables, the applicable pragmas are:
       --    Async_Readers
       --    Async_Writers
@@ -338,6 +348,9 @@ package body Contracts is
          else
             raise Program_Error;
          end if;
+
+      else
+         raise Program_Error;
       end if;
    end Add_Contract_Item;
 
@@ -430,6 +443,15 @@ package body Contracts is
             end;
          end if;
 
+         if Nkind_In (Decl, N_Full_Type_Declaration,
+                            N_Private_Type_Declaration,
+                            N_Task_Type_Declaration,
+                            N_Protected_Type_Declaration,
+                            N_Formal_Type_Declaration)
+         then
+            Analyze_Type_Contract (Defining_Identifier (Decl));
+         end if;
+
          Next (Decl);
       end loop;
    end Analyze_Contracts;
@@ -720,6 +742,233 @@ package body Contracts is
       end if;
    end Analyze_Entry_Or_Subprogram_Contract;
 
+   ----------------------------------------------
+   -- Check_Type_Or_Object_External_Properties --
+   ----------------------------------------------
+
+   procedure Check_Type_Or_Object_External_Properties
+     (Type_Or_Obj_Id : Entity_Id)
+   is
+      function Decl_Kind (Is_Type     : Boolean;
+                          Object_Kind : String) return String;
+      --  Returns "type" or Object_Kind, depending on Is_Type
+
+      ---------------
+      -- Decl_Kind --
+      ---------------
+
+      function Decl_Kind (Is_Type     : Boolean;
+                          Object_Kind : String) return String is
+      begin
+         if Is_Type then
+            return "type";
+         else
+            return Object_Kind;
+         end if;
+      end Decl_Kind;
+
+      Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id);
+
+      --  Local variables
+
+      AR_Val       : Boolean := False;
+      AW_Val       : Boolean := False;
+      ER_Val       : Boolean := False;
+      EW_Val       : Boolean := False;
+      Seen         : Boolean := False;
+      Prag         : Node_Id;
+      Obj_Typ      : Entity_Id;
+
+   --  Start of processing for Check_Type_Or_Object_External_Properties
+
+   begin
+      --  Analyze all external properties
+
+      if Is_Type_Id then
+         Obj_Typ := Type_Or_Obj_Id;
+
+         --  If the parent type of a derived type is volatile
+         --  then the derived type inherits volatility-related flags.
+
+         if Is_Derived_Type (Type_Or_Obj_Id) then
+            declare
+               Parent_Type : constant Entity_Id :=
+                 Etype (Base_Type (Type_Or_Obj_Id));
+            begin
+               if Is_Effectively_Volatile (Parent_Type) then
+                  AR_Val := Async_Readers_Enabled (Parent_Type);
+                  AW_Val := Async_Writers_Enabled (Parent_Type);
+                  ER_Val := Effective_Reads_Enabled (Parent_Type);
+                  EW_Val := Effective_Writes_Enabled (Parent_Type);
+               end if;
+            end;
+         end if;
+      else
+         Obj_Typ := Etype (Type_Or_Obj_Id);
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers);
+
+      if Present (Prag) then
+         declare
+            Saved_AR_Val : constant Boolean := AR_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
+            Seen := True;
+            if Saved_AR_Val and not AR_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Async_Readers specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers);
+
+      if Present (Prag) then
+         declare
+            Saved_AW_Val : constant Boolean := AW_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
+            Seen := True;
+            if Saved_AW_Val and not AW_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Async_Writers specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads);
+
+      if Present (Prag) then
+         declare
+            Saved_ER_Val : constant Boolean := ER_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
+            Seen := True;
+            if Saved_ER_Val and not ER_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Effective_Reads specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes);
+
+      if Present (Prag) then
+         declare
+            Saved_EW_Val : constant Boolean := EW_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
+            Seen := True;
+            if Saved_EW_Val and not EW_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Effective_Writes specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      --  Verify the mutual interaction of the various external properties
+
+      if Seen then
+         Check_External_Properties
+           (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
+      end if;
+
+      --  The following checks are relevant only when SPARK_Mode is on, as
+      --  they are not standard Ada legality rules. Internally generated
+      --  temporaries are ignored.
+
+      if SPARK_Mode = On and then Comes_From_Source (Type_Or_Obj_Id) then
+         if Is_Effectively_Volatile (Type_Or_Obj_Id) then
+
+            --  The declaration of an effectively volatile object or type must
+            --  appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
+
+            if not Is_Library_Level_Entity (Type_Or_Obj_Id) then
+               Error_Msg_N
+                 ("effectively volatile "
+                    & Decl_Kind (Is_Type     => Is_Type_Id,
+                                 Object_Kind => "variable")
+                    & " & must be declared at library level "
+                    & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id);
+
+            --  An object of a discriminated type cannot be effectively
+            --  volatile except for protected objects (SPARK RM 7.1.3(5)).
+
+            elsif Has_Discriminants (Obj_Typ)
+              and then not Is_Protected_Type (Obj_Typ)
+            then
+               Error_Msg_N
+                ("discriminated "
+                   & Decl_Kind (Is_Type     => Is_Type_Id,
+                                Object_Kind => "object")
+                   & " & cannot be volatile",
+                 Type_Or_Obj_Id);
+            end if;
+
+            --  An object decl shall be compatible with respect to volatility
+            --  with its type (SPARK RM 7.1.3(2)).
+
+            if not Is_Type_Id then
+               if Is_Effectively_Volatile  (Obj_Typ) then
+                  Check_Volatility_Compatibility
+                    (Type_Or_Obj_Id, Obj_Typ,
+                     "volatile object", "its type",
+                     Srcpos_Bearer => Type_Or_Obj_Id);
+               end if;
+
+            --  A component of a composite type (in this case, the composite
+            --  type is an array type) shall be compatible with respect to
+            --  volatility with the composite type (SPARK RM 7.1.3(6)).
+
+            elsif Is_Array_Type (Obj_Typ) then
+               Check_Volatility_Compatibility
+                 (Component_Type (Obj_Typ), Obj_Typ,
+                  "component type", "its enclosing array type",
+                  Srcpos_Bearer => Obj_Typ);
+
+            --  A component of a composite type (in this case, the composite
+            --  type is a record type) shall be compatible with respect to
+            --  volatility with the composite type (SPARK RM 7.1.3(6)).
+
+            elsif Is_Record_Type (Obj_Typ) then
+               declare
+                  Comp : Entity_Id := First_Component (Obj_Typ);
+               begin
+                  while Present (Comp) loop
+                     Check_Volatility_Compatibility
+                       (Etype (Comp), Obj_Typ,
+                        "record component " & Get_Name_String (Chars (Comp)),
+                        "its enclosing record type",
+                        Srcpos_Bearer => Comp);
+                     Next_Component (Comp);
+                  end loop;
+               end;
+            end if;
+
+         --  The type or object is not effectively volatile
+
+         else
+            --  A non-effectively volatile type cannot have effectively
+            --  volatile components (SPARK RM 7.1.3(6)).
+
+            if Is_Type_Id
+              and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
+              and then Has_Volatile_Component (Type_Or_Obj_Id)
+            then
+               Error_Msg_N
+                 ("non-volatile type & cannot have volatile"
+                    & " components",
+                  Type_Or_Obj_Id);
+            end if;
+         end if;
+      end if;
+   end Check_Type_Or_Object_External_Properties;
+
    -----------------------------
    -- Analyze_Object_Contract --
    -----------------------------
@@ -738,15 +987,10 @@ package body Contracts is
       Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
       --  Save the SPARK_Mode-related data to restore on exit
 
-      AR_Val   : Boolean := False;
-      AW_Val   : Boolean := False;
-      ER_Val   : Boolean := False;
-      EW_Val   : Boolean := False;
       NC_Val   : Boolean := False;
       Items    : Node_Id;
       Prag     : Node_Id;
       Ref_Elmt : Elmt_Id;
-      Seen     : Boolean := False;
 
    begin
       --  The loop parameter in an element iterator over a formal container
@@ -813,41 +1057,8 @@ package body Contracts is
 
       else pragma Assert (Ekind (Obj_Id) = E_Variable);
 
-         --  Analyze all external properties
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
-            Seen := True;
-         end if;
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
-            Seen := True;
-         end if;
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
-            Seen := True;
-         end if;
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
-            Seen := True;
-         end if;
-
-         --  Verify the mutual interaction of the various external properties
-
-         if Seen then
-            Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
-         end if;
+         Check_Type_Or_Object_External_Properties
+           (Type_Or_Obj_Id => Obj_Id);
 
          --  Analyze the non-external volatility property No_Caching
 
@@ -911,47 +1122,6 @@ package body Contracts is
          else
             Check_Missing_Part_Of (Obj_Id);
          end if;
-
-         --  The following checks are relevant only when SPARK_Mode is on, as
-         --  they are not standard Ada legality rules. Internally generated
-         --  temporaries are ignored.
-
-         if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
-            if Is_Effectively_Volatile (Obj_Id) then
-
-               --  The declaration of an effectively volatile object must
-               --  appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
-
-               if not Is_Library_Level_Entity (Obj_Id) then
-                  Error_Msg_N
-                    ("volatile variable & must be declared at library level "
-                     & "(SPARK RM 7.1.3(3))", Obj_Id);
-
-               --  An object of a discriminated type cannot be effectively
-               --  volatile except for protected objects (SPARK RM 7.1.3(5)).
-
-               elsif Has_Discriminants (Obj_Typ)
-                 and then not Is_Protected_Type (Obj_Typ)
-               then
-                  Error_Msg_N
-                    ("discriminated object & cannot be volatile", Obj_Id);
-               end if;
-
-            --  The object is not effectively volatile
-
-            else
-               --  A non-effectively volatile object cannot have effectively
-               --  volatile components (SPARK RM 7.1.3(6)).
-
-               if not Is_Effectively_Volatile (Obj_Id)
-                 and then Has_Volatile_Component (Obj_Typ)
-               then
-                  Error_Msg_N
-                    ("non-volatile object & cannot have volatile components",
-                     Obj_Id);
-               end if;
-            end if;
-         end if;
       end if;
 
       --  Common checks
@@ -1304,6 +1474,16 @@ package body Contracts is
       Restore_SPARK_Mode (Saved_SM, Saved_SMP);
    end Analyze_Task_Contract;
 
+   ---------------------------
+   -- Analyze_Type_Contract --
+   ---------------------------
+
+   procedure Analyze_Type_Contract (Type_Id : Entity_Id) is
+   begin
+      Check_Type_Or_Object_External_Properties
+        (Type_Or_Obj_Id => Type_Id);
+   end Analyze_Type_Contract;
+
    -----------------------------
    -- Create_Generic_Contract --
    -----------------------------
@@ -2757,6 +2937,15 @@ package body Contracts is
                Analyze_Task_Contract (Defining_Entity (Decl));
             end if;
 
+            if Nkind_In (Decl, N_Full_Type_Declaration,
+                               N_Private_Type_Declaration,
+                               N_Task_Type_Declaration,
+                               N_Protected_Type_Declaration,
+                               N_Formal_Type_Declaration)
+            then
+               Analyze_Type_Contract (Defining_Identifier (Decl));
+            end if;
+
             Prev (Decl);
          end loop;
       end Freeze_Contracts;