From 56a05ce0839d83fbbbc7e57d085ca483b884b805 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Wed, 30 May 2018 08:57:21 +0000 Subject: [PATCH] [Ada] Spurious error on legal synchronized constituent This patch corrects the predicate which determines whether an entity denotes a synchronized object as per SPARK RM 9.1. to account for a case where the object is not atomic, but its type is. The patch also cleans up various atomic object-related predicates. 2018-05-30 Hristian Kirtchev gcc/ada/ * sem_util.adb (Is_Atomic_Object): Cleaned up. Split the entity logic in a separate routine. (Is_Atomic_Object_Entity): New routine. (Is_Atomic_Prefix): Cleaned up. (Is_Synchronized_Object): Check that the object is atomic, or its type is atomic. (Object_Has_Atomic_Components): Removed. * sem_util.ads (Is_Atomic_Object): Reword the comment on usage. (Is_Atomic_Object_Entity): New routine. gcc/testsuite/ * gnat.dg/synchronized1.adb, gnat.dg/synchronized1.ads: New testcase. From-SVN: r260933 --- gcc/ada/ChangeLog | 12 +++ gcc/ada/sem_util.adb | 110 ++++++++++++------------ gcc/ada/sem_util.ads | 12 ++- gcc/testsuite/ChangeLog | 4 + gcc/testsuite/gnat.dg/synchronized1.adb | 14 +++ gcc/testsuite/gnat.dg/synchronized1.ads | 7 ++ 6 files changed, 100 insertions(+), 59 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/synchronized1.adb create mode 100644 gcc/testsuite/gnat.dg/synchronized1.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 964d63d369f..e14d14eb32d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2018-05-30 Hristian Kirtchev + + * sem_util.adb (Is_Atomic_Object): Cleaned up. Split the entity logic + in a separate routine. + (Is_Atomic_Object_Entity): New routine. + (Is_Atomic_Prefix): Cleaned up. + (Is_Synchronized_Object): Check that the object is atomic, or its type + is atomic. + (Object_Has_Atomic_Components): Removed. + * sem_util.ads (Is_Atomic_Object): Reword the comment on usage. + (Is_Atomic_Object_Entity): New routine. + 2018-05-30 Ed Schonberg * sem_ch3.adb (Access_Subprogram_Declaration): The flag diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 16ba8e890ac..7aafa8d5df0 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13156,86 +13156,84 @@ package body Sem_Util is ---------------------- function Is_Atomic_Object (N : Node_Id) return Boolean is + function Is_Atomic_Entity (Id : Entity_Id) return Boolean; + pragma Inline (Is_Atomic_Entity); + -- Determine whether arbitrary entity Id is either atomic or has atomic + -- components. - function Object_Has_Atomic_Components (N : Node_Id) return Boolean; - -- Determines if given object has atomic components - - function Is_Atomic_Prefix (N : Node_Id) return Boolean; - -- If prefix is an implicit dereference, examine designated type + function Is_Atomic_Prefix (Pref : Node_Id) return Boolean; + -- Determine whether prefix Pref of a indexed or selected component is + -- an atomic object. ---------------------- - -- Is_Atomic_Prefix -- + -- Is_Atomic_Entity -- ---------------------- - function Is_Atomic_Prefix (N : Node_Id) return Boolean is + function Is_Atomic_Entity (Id : Entity_Id) return Boolean is begin - if Is_Access_Type (Etype (N)) then - return - Has_Atomic_Components (Designated_Type (Etype (N))); - else - return Object_Has_Atomic_Components (N); - end if; - end Is_Atomic_Prefix; + return Is_Atomic (Id) or else Has_Atomic_Components (Id); + end Is_Atomic_Entity; + + ---------------------- + -- Is_Atomic_Prefix -- + ---------------------- - ---------------------------------- - -- Object_Has_Atomic_Components -- - ---------------------------------- + function Is_Atomic_Prefix (Pref : Node_Id) return Boolean is + Typ : constant Entity_Id := Etype (Pref); - function Object_Has_Atomic_Components (N : Node_Id) return Boolean is begin - if Has_Atomic_Components (Etype (N)) - or else Is_Atomic (Etype (N)) - then - return True; + if Is_Access_Type (Typ) then + return Has_Atomic_Components (Designated_Type (Typ)); - elsif Is_Entity_Name (N) - and then (Has_Atomic_Components (Entity (N)) - or else Is_Atomic (Entity (N))) - then + elsif Is_Atomic_Entity (Typ) then return True; - elsif Nkind (N) = N_Selected_Component - and then Is_Atomic (Entity (Selector_Name (N))) + elsif Is_Entity_Name (Pref) + and then Is_Atomic_Entity (Entity (Pref)) then return True; - elsif Nkind (N) = N_Indexed_Component - or else Nkind (N) = N_Selected_Component - then - return Is_Atomic_Prefix (Prefix (N)); + elsif Nkind (Pref) = N_Indexed_Component then + return Is_Atomic_Prefix (Prefix (Pref)); - else - return False; + elsif Nkind (Pref) = N_Selected_Component then + return + Is_Atomic_Prefix (Prefix (Pref)) + or else Is_Atomic (Entity (Selector_Name (Pref))); end if; - end Object_Has_Atomic_Components; + + return False; + end Is_Atomic_Prefix; -- Start of processing for Is_Atomic_Object begin - -- Predicate is not relevant to subprograms + if Is_Entity_Name (N) then + return Is_Atomic_Object_Entity (Entity (N)); - if Is_Entity_Name (N) and then Is_Overloadable (Entity (N)) then - return False; + elsif Nkind (N) = N_Indexed_Component then + return Is_Atomic (Etype (N)) or else Is_Atomic_Prefix (Prefix (N)); - elsif Is_Atomic (Etype (N)) - or else (Is_Entity_Name (N) and then Is_Atomic (Entity (N))) - then - return True; + elsif Nkind (N) = N_Selected_Component then + return + Is_Atomic (Etype (N)) + or else Is_Atomic_Prefix (Prefix (N)) + or else Is_Atomic (Entity (Selector_Name (N))); + end if; - elsif Nkind (N) = N_Selected_Component - and then Is_Atomic (Entity (Selector_Name (N))) - then - return True; + return False; + end Is_Atomic_Object; - elsif Nkind (N) = N_Indexed_Component - or else Nkind (N) = N_Selected_Component - then - return Is_Atomic_Prefix (Prefix (N)); + ----------------------------- + -- Is_Atomic_Object_Entity -- + ----------------------------- - else - return False; - end if; - end Is_Atomic_Object; + function Is_Atomic_Object_Entity (Id : Entity_Id) return Boolean is + begin + return + Is_Object (Id) + and then (Is_Atomic (Id) or else Is_Atomic (Etype (Id))); + end Is_Atomic_Object_Entity; ----------------------------- -- Is_Atomic_Or_VFA_Object -- @@ -17353,7 +17351,9 @@ package body Sem_Util is -- The object is synchronized if it is atomic and Async_Writers is -- enabled. - elsif Is_Atomic (Id) and then Async_Writers_Enabled (Id) then + elsif Is_Atomic_Object_Entity (Id) + and then Async_Writers_Enabled (Id) + then return True; -- A constant is a synchronized object by default diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 6cb7db87839..ad7760c0cbe 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1512,12 +1512,16 @@ package Sem_Util is -- Determine whether package E1 is an ancestor of E2 function Is_Atomic_Object (N : Node_Id) return Boolean; - -- Determines if the given node denotes an atomic object in the sense of - -- the legality checks described in RM C.6(12). + -- Determine whether arbitrary node N denotes a reference to an atomic + -- object as per Ada RM C.6(12). + + function Is_Atomic_Object_Entity (Id : Entity_Id) return Boolean; + -- Determine whether arbitrary entity Id denotes an atomic object as per + -- Ada RM C.6(12). function Is_Atomic_Or_VFA_Object (N : Node_Id) return Boolean; - -- Determines if the given node is an atomic object (Is_Atomic_Object true) - -- or else is an object for which VFA is present. + -- Determine whether arbitrary node N denotes a reference to an object + -- which is either atomic or Volatile_Full_Access. function Is_Attribute_Result (N : Node_Id) return Boolean; -- Determine whether node N denotes attribute 'Result diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index f1c217960af..2e35d647f63 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-05-30 Hristian Kirtchev + + * gnat.dg/synchronized1.adb, gnat.dg/synchronized1.ads: New testcase. + 2018-05-29 Uros Bizjak PR target/85950 diff --git a/gcc/testsuite/gnat.dg/synchronized1.adb b/gcc/testsuite/gnat.dg/synchronized1.adb new file mode 100644 index 00000000000..d07c351654e --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized1.adb @@ -0,0 +1,14 @@ +-- { dg-do compile } +-- { dg-options "-gnatws" } + +package body Synchronized1 + with SPARK_Mode, + Refined_State => (State => Curr_State) +is + type Reactor_State is (Stopped, Working) with Atomic; + + Curr_State : Reactor_State + with Async_Readers, Async_Writers; + + procedure Force_Body is null; +end Synchronized1; diff --git a/gcc/testsuite/gnat.dg/synchronized1.ads b/gcc/testsuite/gnat.dg/synchronized1.ads new file mode 100644 index 00000000000..f814c91d8c6 --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized1.ads @@ -0,0 +1,7 @@ +package Synchronized1 + with SPARK_Mode, + Abstract_State => (State with Synchronous), + Initializes => State +is + procedure Force_Body; +end Synchronized1; -- 2.30.2