* [Ada] Handle correctly current instance of PO in local subprogram Global
@ 2020-11-24 10:17 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2020-11-24 10:17 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 760 bytes --]
SPARK defines the current instance of a protected object as non-volatile
for internal calls, which allows to use it in the Global contract of a
local non-volatile function. This was not handled correctly, now fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_prag.adb (Analyze_Global_Item): Handle specially the
current instance of a PO.
* sem_util.ads (Is_Effectively_Volatile,
Is_Effectively_Volatile_For_Reading): Add parameter
Ignore_Protected.
* sem_util.adb (Is_Effectively_Volatile,
Is_Effectively_Volatile_For_Reading): Add parameter
Ignore_Protected to compute the query results ignoring protected
objects/types.
(Is_Effectively_Volatile_Object,
Is_Effectively_Volatile_Object_For_Reading): Adapt to new
signature.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 7400 bytes --]
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2476,11 +2476,22 @@ package body Sem_Prag is
and then Ekind (Item_Id) = E_Variable
and then Is_Effectively_Volatile_For_Reading (Item_Id)
then
+ -- The current instance of a protected unit is not an
+ -- effectively volatile object, unless the protected unit
+ -- is already volatile for another reason (SPARK RM 7.1.2).
+
+ if Is_Single_Protected_Object (Item_Id)
+ and then Is_CCT_Instance (Etype (Item_Id), Spec_Id)
+ and then not Is_Effectively_Volatile_For_Reading
+ (Item_Id, Ignore_Protected => True)
+ then
+ null;
+
-- An effectively volatile object for reading cannot appear
-- as a global item of a nonvolatile function (SPARK RM
-- 7.1.3(8)).
- if Ekind (Spec_Id) in E_Function | E_Generic_Function
+ elsif Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Is_Volatile_Function (Spec_Id)
then
Error_Msg_NE
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
@@ -16582,7 +16582,9 @@ package body Sem_Util is
-- Is_Effectively_Volatile --
-----------------------------
- function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
+ function Is_Effectively_Volatile
+ (Id : Entity_Id;
+ Ignore_Protected : Boolean := False) return Boolean is
begin
if Is_Type (Id) then
@@ -16610,15 +16612,16 @@ package body Sem_Util is
-- Test for presence of ancestor, as the full view of a
-- private type may be missing in case of error.
- return
- Present (Anc)
- and then Is_Effectively_Volatile (Component_Type (Anc));
+ return Present (Anc)
+ and then Is_Effectively_Volatile
+ (Component_Type (Anc), Ignore_Protected);
end;
end if;
- -- A protected type is always volatile
+ -- A protected type is always volatile unless Ignore_Protected is
+ -- True.
- elsif Is_Protected_Type (Id) then
+ elsif Is_Protected_Type (Id) and then not Ignore_Protected then
return True;
-- A descendant of Ada.Synchronous_Task_Control.Suspension_Object is
@@ -16644,7 +16647,7 @@ package body Sem_Util is
and then not
(Ekind (Id) = E_Variable and then No_Caching_Enabled (Id)))
or else Has_Volatile_Components (Id)
- or else Is_Effectively_Volatile (Etype (Id));
+ or else Is_Effectively_Volatile (Etype (Id), Ignore_Protected);
end if;
end Is_Effectively_Volatile;
@@ -16653,15 +16656,19 @@ package body Sem_Util is
-----------------------------------------
function Is_Effectively_Volatile_For_Reading
- (Id : Entity_Id) return Boolean
+ (Id : Entity_Id;
+ Ignore_Protected : Boolean := False) return Boolean
is
begin
- -- A concurrent type is effectively volatile for reading
+ -- A concurrent type is effectively volatile for reading, except for a
+ -- protected type when Ignore_Protected is True.
- if Is_Concurrent_Type (Id) then
+ if Is_Task_Type (Id)
+ or else (Is_Protected_Type (Id) and then not Ignore_Protected)
+ then
return True;
- elsif Is_Effectively_Volatile (Id) then
+ elsif Is_Effectively_Volatile (Id, Ignore_Protected) then
-- Other volatile types and objects are effectively volatile for
-- reading when they have property Async_Writers or Effective_Reads
@@ -16689,10 +16696,9 @@ package body Sem_Util is
-- Test for presence of ancestor, as the full view of a
-- private type may be missing in case of error.
- return
- Present (Anc)
- and then Is_Effectively_Volatile_For_Reading
- (Component_Type (Anc));
+ return Present (Anc)
+ and then Is_Effectively_Volatile_For_Reading
+ (Component_Type (Anc), Ignore_Protected);
end;
end if;
end if;
@@ -16706,6 +16712,9 @@ package body Sem_Util is
------------------------------------
function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is
+ function Is_Effectively_Volatile (E : Entity_Id) return Boolean is
+ (Is_Effectively_Volatile (E, Ignore_Protected => False));
+
function Is_Effectively_Volatile_Object_Inst
is new Is_Effectively_Volatile_Object_Shared (Is_Effectively_Volatile);
begin
@@ -16719,6 +16728,10 @@ package body Sem_Util is
function Is_Effectively_Volatile_Object_For_Reading
(N : Node_Id) return Boolean
is
+ function Is_Effectively_Volatile_For_Reading
+ (E : Entity_Id) return Boolean
+ is (Is_Effectively_Volatile_For_Reading (E, Ignore_Protected => False));
+
function Is_Effectively_Volatile_Object_For_Reading_Inst
is new Is_Effectively_Volatile_Object_Shared
(Is_Effectively_Volatile_For_Reading);
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
@@ -1879,7 +1879,9 @@ package Sem_Util is
-- . machine_emax = 2**10
-- . machine_emin = 3 - machine_emax
- function Is_Effectively_Volatile (Id : Entity_Id) return Boolean;
+ function Is_Effectively_Volatile
+ (Id : Entity_Id;
+ Ignore_Protected : Boolean := False) return Boolean;
-- Determine whether a type or object denoted by entity Id is effectively
-- volatile (SPARK RM 7.1.2). To qualify as such, the entity must be either
-- * Volatile without No_Caching
@@ -1887,9 +1889,14 @@ package Sem_Util is
-- * An array type whose component type is effectively volatile
-- * A protected type
-- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
+ --
+ -- If Ignore_Protected is True, then a protected object/type is treated
+ -- like a non-protected record object/type for computing the result of
+ -- this query.
function Is_Effectively_Volatile_For_Reading
- (Id : Entity_Id) return Boolean;
+ (Id : Entity_Id;
+ Ignore_Protected : Boolean := False) return Boolean;
-- Determine whether a type or object denoted by entity Id is effectively
-- volatile for reading (SPARK RM 7.1.2). To qualify as such, the entity
-- must be either
@@ -1901,6 +1908,10 @@ package Sem_Util is
-- reading
-- * A protected type
-- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
+ --
+ -- If Ignore_Protected is True, then a protected object/type is treated
+ -- like a non-protected record object/type for computing the result of
+ -- this query.
function Is_Effectively_Volatile_Object
(N : Node_Id) return Boolean;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2020-11-24 10:17 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-11-24 10:17 [Ada] Handle correctly current instance of PO in local subprogram Global Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).