[gcc/devel/c++-coroutines] [Ada] Allow specifying volatility refinement aspects for types
Iain D Sandoe
iains@gcc.gnu.org
Thu Jun 11 20:07:07 GMT 2020
https://gcc.gnu.org/g:4127ebece723b172aeecacbba9b523af98cc646b
commit 4127ebece723b172aeecacbba9b523af98cc646b
Author: Steve Baird <baird@adacore.com>
Date: Fri Jan 31 11:36:51 2020 -0800
[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.
Diff:
---
gcc/ada/contracts.adb | 391 +++++++++++++++++++++++++++++++++++++-------------
gcc/ada/contracts.ads | 17 ++-
gcc/ada/einfo.adb | 9 +-
gcc/ada/einfo.ads | 6 +-
gcc/ada/sem_ch12.adb | 47 ++++++
gcc/ada/sem_ch13.adb | 11 +-
gcc/ada/sem_ch3.adb | 21 +++
gcc/ada/sem_prag.adb | 67 ++++++---
gcc/ada/sem_util.adb | 229 +++++++++++++++++++++++------
gcc/ada/sem_util.ads | 33 +++--
10 files changed, 647 insertions(+), 184 deletions(-)
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 79078df3aef..42f36d5909c 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;
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index a41285f7249..9e7b95569fc 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -33,8 +33,8 @@ package Contracts is
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
-- Add pragma Prag to the contract of a constant, entry, entry family,
-- [generic] package, package body, protected unit, [generic] subprogram,
- -- subprogram body, variable or task unit denoted by Id. The following are
- -- valid pragmas:
+ -- subprogram body, variable, task unit, or type denoted by Id.
+ -- The following are valid pragmas:
--
-- Abstract_State
-- Async_Readers
@@ -114,6 +114,19 @@ package Contracts is
-- Freeze_Id is the entity of a [generic] package body or a [generic]
-- subprogram body which "freezes" the contract of Obj_Id.
+ procedure Analyze_Type_Contract (Type_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of object Obj_Id as
+ -- if they appeared at the end of the declarative region. The pragmas to be
+ -- considered are:
+ --
+ -- Async_Readers
+ -- Async_Writers
+ -- Effective_Reads
+ -- Effective_Writes
+ --
+ -- In the case of a protected or task type, there will also be
+ -- a call to Analyze_Protected_Contract or Analyze_Task_Contract.
+
procedure Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty);
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index ee1aecb9cd8..83beff6f0f1 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -1291,6 +1291,8 @@ package body Einfo is
E_Package,
E_Package_Body)
or else
+ Is_Type (Id) -- types
+ or else
Ekind (Id) = E_Void); -- special purpose
return Node34 (Id);
end Contract;
@@ -4146,6 +4148,10 @@ package body Einfo is
Ekind_In (Id, E_Generic_Package, -- packages
E_Package,
E_Package_Body)
+
+ or else
+ Is_Type (Id) -- types
+
or else
Ekind (Id) = E_Void); -- special purpose
Set_Node34 (Id, V);
@@ -11271,11 +11277,10 @@ package body Einfo is
| E_Package
| E_Package_Body
| E_Procedure
- | E_Protected_Type
| E_Subprogram_Body
| E_Task_Body
- | E_Task_Type
| E_Variable
+ | Type_Kind
| E_Void
=>
Write_Str ("Contract");
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index e28fcd0e663..75474cd232d 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -744,9 +744,9 @@ package Einfo is
-- Contract (Node34)
-- Defined in constant, entry, entry family, operator, [generic] package,
--- package body, protected type, [generic] subprogram, subprogram body,
--- variable and task type entities. Points to the contract of the entity,
--- holding various assertion items and data classifiers.
+-- package body, protected unit, [generic] subprogram, subprogram body,
+-- variable, task unit, and type entities. Points to the contract of the
+-- entity, holding various assertion items and data classifiers.
-- Contract_Wrapper (Node25)
-- Defined in entry and entry family entities. Set only when the entry
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 93a3ca59d5c..e366531d9bc 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -11315,6 +11315,44 @@ package body Sem_Ch12 is
Actual);
end if;
+ -- Check actual/formal compatibility with respect to the four
+ -- volatility refinement aspects.
+
+ declare
+ Actual_Obj : Entity_Id;
+ N : Node_Id := Actual;
+ begin
+ -- Similar to Sem_Util.Get_Enclosing_Object, but treat
+ -- pointer dereference like component selection.
+ loop
+ if Is_Entity_Name (N) then
+ Actual_Obj := Entity (N);
+ exit;
+ end if;
+
+ case Nkind (N) is
+ when N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ | N_Explicit_Dereference
+ =>
+ N := Prefix (N);
+
+ when N_Type_Conversion =>
+ N := Expression (N);
+
+ when others =>
+ Actual_Obj := Etype (N);
+ exit;
+ end case;
+ end loop;
+
+ Check_Volatility_Compatibility
+ (Actual_Obj, A_Gen_Obj, "actual object",
+ "its corresponding formal object of mode in out",
+ Srcpos_Bearer => Actual);
+ end;
+
-- Formal in-parameter
else
@@ -11510,6 +11548,7 @@ package body Sem_Ch12 is
and then Present (Actual)
and then Is_Object_Reference (Actual)
and then Is_Effectively_Volatile_Object (Actual)
+ and then not Is_Effectively_Volatile (A_Gen_Obj)
then
Error_Msg_N
("volatile object cannot act as actual in generic instantiation",
@@ -12480,6 +12519,14 @@ package body Sem_Ch12 is
("actual for& must have Independent_Components specified",
Actual, A_Gen_T);
end if;
+
+ -- Check actual/formal compatibility with respect to the four
+ -- volatility refinement aspects.
+
+ Check_Volatility_Compatibility
+ (Act_T, A_Gen_T,
+ "actual type", "its corresponding formal type",
+ Srcpos_Bearer => Act_T);
end if;
end Check_Shared_Variable_Control_Aspects;
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index f73b55aa443..4b042d8b678 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -2180,7 +2180,12 @@ package body Sem_Ch13 is
-- Check some general restrictions on language defined aspects
- if not Implementation_Defined_Aspect (A_Id) then
+ if not Implementation_Defined_Aspect (A_Id)
+ or else A_Id = Aspect_Async_Readers
+ or else A_Id = Aspect_Async_Writers
+ or else A_Id = Aspect_Effective_Reads
+ or else A_Id = Aspect_Effective_Reads
+ then
Error_Msg_Name_1 := Nam;
-- Not allowed for renaming declarations. Examine the original
@@ -2209,6 +2214,10 @@ package body Sem_Ch13 is
and then A_Id /= Aspect_Atomic_Components
and then A_Id /= Aspect_Independent_Components
and then A_Id /= Aspect_Volatile_Components
+ and then A_Id /= Aspect_Async_Readers
+ and then A_Id /= Aspect_Async_Writers
+ and then A_Id /= Aspect_Effective_Reads
+ and then A_Id /= Aspect_Effective_Reads
then
Error_Msg_N
("aspect % not allowed for formal type declaration",
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index ccb0ea9a2f1..f38d6e798ba 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1398,6 +1398,26 @@ package body Sem_Ch3 is
Set_Is_Tagged_Type (T, False);
end if;
+ -- For SPARK, check that the designated type is compatible with
+ -- respect to volatility with the access type.
+
+ if SPARK_Mode /= Off
+ and then Comes_From_Source (T)
+ then
+ -- ??? UNIMPLEMENTED
+ -- In the case where the designated type is incomplete at this point,
+ -- performing this check here is harmless but the check will need to
+ -- be repeated when the designated type is complete.
+
+ -- The preceding call to Comes_From_Source is needed because the
+ -- FE sometimes introduces implicitly declared access types. See,
+ -- for example, the expansion of nested_po.ads in OA28-015.
+
+ Check_Volatility_Compatibility
+ (Full_Desig, T, "designated type", "access type",
+ Srcpos_Bearer => T);
+ end if;
+
Set_Etype (T, T);
-- If the type has appeared already in a with_type clause, it is frozen
@@ -7265,6 +7285,7 @@ package body Sem_Ch3 is
Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Parent_Base));
Set_Parent (Implicit_Base, Parent (Derived_Type));
Set_Is_Known_Valid (Implicit_Base, Is_Known_Valid (Parent_Base));
+ Set_Is_Volatile (Implicit_Base, Is_Volatile (Parent_Base));
-- Set RM Size for discrete type or decimal fixed-point type
-- Ordinary fixed-point is excluded, why???
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d05b8fe2a8d..05171d45208 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2123,7 +2123,8 @@ package body Sem_Prag is
& """No_Caching"" (SPARK RM 7.1.2(6))", N);
else
SPARK_Msg_N
- ("external property % must apply to a volatile object", N);
+ ("external property % must apply to a volatile type or object",
+ N);
end if;
-- Pragma No_Caching should only apply to volatile variables of
@@ -7847,6 +7848,7 @@ package body Sem_Prag is
and then Prag_Id = Pragma_Volatile
and then not Nkind_In (Original_Node (Decl),
N_Full_Type_Declaration,
+ N_Formal_Type_Declaration,
N_Object_Declaration,
N_Single_Protected_Declaration,
N_Single_Task_Declaration)
@@ -13476,41 +13478,65 @@ package body Sem_Prag is
| Pragma_No_Caching
=>
Async_Effective : declare
- Obj_Decl : Node_Id;
- Obj_Id : Entity_Id;
-
+ Obj_Or_Type_Decl : Node_Id;
+ Obj_Or_Type_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- Obj_Decl := Find_Related_Context (N, Do_Checks => True);
-
- -- Object declaration
-
- if Nkind (Obj_Decl) /= N_Object_Declaration then
- Pragma_Misplaced;
- return;
+ Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
+
+ -- Pragma must apply to a object declaration or to a type
+ -- declaration (only the former in the No_Caching case).
+ -- Original_Node is necessary to account for untagged derived
+ -- types that are rewritten as subtypes of their
+ -- respective root types.
+
+ if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
+ if (Prag_Id = Pragma_No_Caching)
+ or not Nkind_In (Original_Node (Obj_Or_Type_Decl),
+ N_Full_Type_Declaration,
+ N_Private_Type_Declaration,
+ N_Formal_Type_Declaration,
+ N_Task_Type_Declaration,
+ N_Protected_Type_Declaration)
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
end if;
- Obj_Id := Defining_Entity (Obj_Decl);
+ Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl);
-- Perform minimal verification to ensure that the argument is at
- -- least a variable. Subsequent finer grained checks will be done
- -- at the end of the declarative region the contains the pragma.
+ -- least a variable or a type. Subsequent finer grained checks
+ -- will be done at the end of the declarative region that
+ -- contains the pragma.
- if Ekind (Obj_Id) = E_Variable then
+ if Ekind (Obj_Or_Type_Id) = E_Variable or Is_Type (Obj_Or_Type_Id)
+ then
+
+ -- In the case of a type, pragma is a type-related
+ -- representation item and so requires checks common to
+ -- all type-related representation items.
+
+ if Is_Type (Obj_Or_Type_Id)
+ and then Rep_Item_Too_Late (Obj_Or_Type_Id, N)
+ then
+ return;
+ end if;
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Ghost_Pragma (N, Obj_Id);
+ Mark_Ghost_Pragma (N, Obj_Or_Type_Id);
-- Chain the pragma on the contract for further processing by
-- Analyze_External_Property_In_Decl_Part.
- Add_Contract_Item (N, Obj_Id);
+ Add_Contract_Item (N, Obj_Or_Type_Id);
-- Analyze the Boolean expression (if any)
@@ -13521,7 +13547,8 @@ package body Sem_Prag is
-- Otherwise the external property applies to a constant
else
- Error_Pragma ("pragma % must apply to a volatile object");
+ Error_Pragma
+ ("pragma % must apply to a volatile type or object");
end if;
end Async_Effective;
@@ -30170,7 +30197,9 @@ package body Sem_Prag is
-- Skip internally generated code
- elsif not Comes_From_Source (Stmt) then
+ elsif not Comes_From_Source (Stmt)
+ and then not Comes_From_Source (Original_Node (Stmt))
+ then
-- The anonymous object created for a single concurrent type is a
-- suitable context.
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index d1c63abc9d4..76eb6653fb1 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -116,8 +116,8 @@ package body Sem_Util is
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean;
-- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
- -- Determine whether an abstract state or a variable denoted by entity
- -- Item_Id has enabled property Property.
+ -- Determine whether the state abstraction, variable, or type denoted by
+ -- entity Item_Id has enabled property Property.
function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
@@ -4911,6 +4911,96 @@ package body Sem_Util is
end if;
end Check_Unused_Body_States;
+ ------------------------------------
+ -- Check_Volatility_Compatibility --
+ ------------------------------------
+
+ procedure Check_Volatility_Compatibility
+ (Id1, Id2 : Entity_Id;
+ Description_1, Description_2 : String;
+ Srcpos_Bearer : Node_Id) is
+
+ begin
+ if SPARK_Mode /= On then
+ return;
+ end if;
+
+ declare
+ AR1 : constant Boolean := Async_Readers_Enabled (Id1);
+ AW1 : constant Boolean := Async_Writers_Enabled (Id1);
+ ER1 : constant Boolean := Effective_Reads_Enabled (Id1);
+ EW1 : constant Boolean := Effective_Writes_Enabled (Id1);
+ AR2 : constant Boolean := Async_Readers_Enabled (Id2);
+ AW2 : constant Boolean := Async_Writers_Enabled (Id2);
+ ER2 : constant Boolean := Effective_Reads_Enabled (Id2);
+ EW2 : constant Boolean := Effective_Writes_Enabled (Id2);
+
+ AR_Check_Failed : constant Boolean := AR1 and not AR2;
+ AW_Check_Failed : constant Boolean := AW1 and not AW2;
+ ER_Check_Failed : constant Boolean := ER1 and not ER2;
+ EW_Check_Failed : constant Boolean := EW1 and not EW2;
+
+ package Failure_Description is
+ procedure Note_If_Failure
+ (Failed : Boolean; Aspect_Name : String);
+ -- If Failed is False, do nothing.
+ -- If Failed is True, add Aspect_Name to the failure description.
+
+ function Failure_Text return String;
+ -- returns accumulated list of failing aspects
+ end Failure_Description;
+
+ package body Failure_Description is
+ Description_Buffer : Bounded_String;
+
+ ---------------------
+ -- Note_If_Failure --
+ ---------------------
+
+ procedure Note_If_Failure
+ (Failed : Boolean; Aspect_Name : String) is
+ begin
+ if Failed then
+ if Description_Buffer.Length /= 0 then
+ Append (Description_Buffer, ", ");
+ end if;
+ Append (Description_Buffer, Aspect_Name);
+ end if;
+ end Note_If_Failure;
+
+ ------------------
+ -- Failure_Text --
+ ------------------
+
+ function Failure_Text return String is
+ begin
+ return +Description_Buffer;
+ end Failure_Text;
+ end Failure_Description;
+
+ use Failure_Description;
+ begin
+ if AR_Check_Failed
+ or AW_Check_Failed
+ or ER_Check_Failed
+ or EW_Check_Failed
+ then
+ Note_If_Failure (AR_Check_Failed, "Async_Readers");
+ Note_If_Failure (AW_Check_Failed, "Async_Writers");
+ Note_If_Failure (ER_Check_Failed, "Effective_Reads");
+ Note_If_Failure (EW_Check_Failed, "Effective_Writes");
+
+ Error_Msg_N
+ (Description_1
+ & " and "
+ & Description_2
+ & " are not compatible with respect to volatility due to "
+ & Failure_Text,
+ Srcpos_Bearer);
+ end if;
+ end;
+ end Check_Volatility_Compatibility;
+
-----------------
-- Choice_List --
-----------------
@@ -11036,28 +11126,26 @@ package body Sem_Util is
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean
is
- function Protected_Object_Has_Enabled_Property return Boolean;
- -- Determine whether a protected object denoted by Item_Id has the
- -- property enabled.
+ function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean;
+ -- Determine whether a protected type or variable denoted by Item_Id
+ -- has the property enabled.
function State_Has_Enabled_Property return Boolean;
-- Determine whether a state denoted by Item_Id has the property enabled
- function Variable_Has_Enabled_Property return Boolean;
- -- Determine whether a variable denoted by Item_Id has the property
- -- enabled.
-
- -------------------------------------------
- -- Protected_Object_Has_Enabled_Property --
- -------------------------------------------
+ function Type_Or_Variable_Has_Enabled_Property
+ (Item_Id : Entity_Id) return Boolean;
+ -- Determine whether type or variable denoted by Item_Id has the
+ -- property enabled.
- function Protected_Object_Has_Enabled_Property return Boolean is
- Constits : constant Elist_Id := Part_Of_Constituents (Item_Id);
- Constit_Elmt : Elmt_Id;
- Constit_Id : Entity_Id;
+ -----------------------------------------------------
+ -- Protected_Type_Or_Variable_Has_Enabled_Property --
+ -----------------------------------------------------
+ function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean
+ is
begin
- -- Protected objects always have the properties Async_Readers and
+ -- Protected entities always have the properties Async_Readers and
-- Async_Writers (SPARK RM 7.1.2(16)).
if Property = Name_Async_Readers
@@ -11069,21 +11157,30 @@ package body Sem_Util is
-- properties Effective_Reads and Effective_Writes
-- (SPARK RM 7.1.2(16)).
- elsif Present (Constits) then
- Constit_Elmt := First_Elmt (Constits);
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ elsif Is_Single_Protected_Object (Item_Id) then
+ declare
+ Constit_Elmt : Elmt_Id;
+ Constit_Id : Entity_Id;
+ Constits : constant Elist_Id
+ := Part_Of_Constituents (Item_Id);
+ begin
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
+
+ if Has_Enabled_Property (Constit_Id, Property) then
+ return True;
+ end if;
- if Has_Enabled_Property (Constit_Id, Property) then
- return True;
+ Next_Elmt (Constit_Elmt);
+ end loop;
end if;
-
- Next_Elmt (Constit_Elmt);
- end loop;
+ end;
end if;
return False;
- end Protected_Object_Has_Enabled_Property;
+ end Protected_Type_Or_Variable_Has_Enabled_Property;
--------------------------------
-- State_Has_Enabled_Property --
@@ -11245,11 +11342,13 @@ package body Sem_Util is
return False;
end State_Has_Enabled_Property;
- -----------------------------------
- -- Variable_Has_Enabled_Property --
- -----------------------------------
+ -------------------------------------------
+ -- Type_Or_Variable_Has_Enabled_Property --
+ -------------------------------------------
- function Variable_Has_Enabled_Property return Boolean is
+ function Type_Or_Variable_Has_Enabled_Property
+ (Item_Id : Entity_Id) return Boolean
+ is
function Is_Enabled (Prag : Node_Id) return Boolean;
-- Determine whether property pragma Prag (if present) denotes an
-- enabled property.
@@ -11297,7 +11396,11 @@ package body Sem_Util is
EW : constant Node_Id :=
Get_Pragma (Item_Id, Pragma_Effective_Writes);
- -- Start of processing for Variable_Has_Enabled_Property
+ Is_Derived_Type_With_Volatile_Parent_Type : constant Boolean :=
+ Is_Derived_Type (Item_Id)
+ and then Is_Effectively_Volatile (Etype (Base_Type (Item_Id)));
+
+ -- Start of processing for Type_Or_Variable_Has_Enabled_Property
begin
-- A non-effectively volatile object can never possess external
@@ -11312,23 +11415,57 @@ package body Sem_Util is
-- property is enabled when the flag evaluates to True or the flag is
-- missing altogether.
- elsif Property = Name_Async_Readers and then Is_Enabled (AR) then
- return True;
+ elsif Property = Name_Async_Readers and then Present (AR) then
+ return Is_Enabled (AR);
- elsif Property = Name_Async_Writers and then Is_Enabled (AW) then
- return True;
+ elsif Property = Name_Async_Writers and then Present (AW) then
+ return Is_Enabled (AW);
- elsif Property = Name_Effective_Reads and then Is_Enabled (ER) then
- return True;
+ elsif Property = Name_Effective_Reads and then Present (ER) then
+ return Is_Enabled (ER);
- elsif Property = Name_Effective_Writes and then Is_Enabled (EW) then
- return True;
+ elsif Property = Name_Effective_Writes and then Present (EW) then
+ return Is_Enabled (EW);
+
+ -- If other properties are set explicitly, then this one is set
+ -- implicitly to False, except in the case of a derived type
+ -- whose parent type is volatile (in that case, we will inherit
+ -- from the parent type, below).
+
+ elsif (Present (AR)
+ or else Present (AW)
+ or else Present (ER)
+ or else Present (EW))
+ and then not Is_Derived_Type_With_Volatile_Parent_Type
+ then
+ return False;
+
+ -- For a private type, may need to look at the full view
+
+ elsif Is_Private_Type (Item_Id) and then Present (Full_View (Item_Id))
+ then
+ return Type_Or_Variable_Has_Enabled_Property (Full_View (Item_Id));
+
+ -- For a derived type whose parent type is volatile, the
+ -- property may be inherited (but ignore a non-volatile parent).
+
+ elsif Is_Derived_Type_With_Volatile_Parent_Type then
+ return Type_Or_Variable_Has_Enabled_Property
+ (First_Subtype (Etype (Base_Type (Item_Id))));
+
+ -- If not specified explicitly for an object and the type
+ -- is effectively volatile, then take result from the type.
+
+ elsif not Is_Type (Item_Id)
+ and then Is_Effectively_Volatile (Etype (Item_Id))
+ then
+ return Has_Enabled_Property (Etype (Item_Id), Property);
-- The implicit case lacks all property pragmas
elsif No (AR) and then No (AW) and then No (ER) and then No (EW) then
if Is_Protected_Type (Etype (Item_Id)) then
- return Protected_Object_Has_Enabled_Property;
+ return Protected_Type_Or_Variable_Has_Enabled_Property;
else
return True;
end if;
@@ -11336,7 +11473,7 @@ package body Sem_Util is
else
return False;
end if;
- end Variable_Has_Enabled_Property;
+ end Type_Or_Variable_Has_Enabled_Property;
-- Start of processing for Has_Enabled_Property
@@ -11348,7 +11485,11 @@ package body Sem_Util is
return State_Has_Enabled_Property;
elsif Ekind (Item_Id) = E_Variable then
- return Variable_Has_Enabled_Property;
+ return Type_Or_Variable_Has_Enabled_Property (Item_Id);
+
+ elsif Is_Type (Item_Id) then
+ return Type_Or_Variable_Has_Enabled_Property
+ (Item_Id => First_Subtype (Item_Id));
-- By default, protected objects only have the properties Async_Readers
-- and Async_Writers. If they have Part_Of components, they also inherit
@@ -11356,7 +11497,7 @@ package body Sem_Util is
-- (SPARK RM 7.1.2(16)).
elsif Ekind (Item_Id) = E_Protected_Object then
- return Protected_Object_Has_Enabled_Property;
+ return Protected_Type_Or_Variable_Has_Enabled_Property;
-- Otherwise a property is enabled when the related item is effectively
-- volatile.
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 07619fcde36..74fa2a63dbe 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -157,14 +157,12 @@ package Sem_Util is
-- force an error).
function Async_Readers_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Async_Readers and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Async_Readers.
function Async_Writers_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Async_Writers and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Async_Writers.
function Available_Full_View_Of_Component (T : Entity_Id) return Boolean;
-- If at the point of declaration an array type has a private or limited
@@ -456,6 +454,19 @@ package Sem_Util is
-- and the context is external to the protected operation, to warn against
-- a possible unlocked access to data.
+ procedure Check_Volatility_Compatibility
+ (Id1, Id2 : Entity_Id;
+ Description_1, Description_2 : String;
+ Srcpos_Bearer : Node_Id);
+ -- Id1 and Id2 should each be the entity of a state abstraction, a
+ -- variable, or a type (i.e., something suitable for passing to
+ -- Async_Readers_Enabled and similar functions).
+ -- Does nothing if SPARK_Mode /= On. Otherwise, flags a legality violation
+ -- if one or more of the four volatility-related aspects is False for Id1
+ -- and True for Id2. The two descriptions are included in the error message
+ -- text; the source position for the generated message is determined by
+ -- Srcpos_Bearer.
+
function Choice_List (N : Node_Id) return List_Id;
-- Utility to retrieve the choices of a Component_Association or the
-- Discrete_Choices of an Iterated_Component_Association. For various
@@ -664,14 +675,12 @@ package Sem_Util is
-- are looked through.
function Effective_Reads_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Effective_Reads and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Effective_Reads.
function Effective_Writes_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Effective_Writes and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Effective_Writes.
function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id;
-- Returns the enclosing N_Compilation_Unit node that is the root of a
More information about the Gcc-cvs
mailing list