From: Hristian Kirtchev Date: Mon, 21 May 2018 14:50:54 +0000 (+0000) Subject: [Ada] Spurious error on synchronous refinement X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bcc093dc813c77d15a8d99ce063a45fa01c7ed73;p=gcc.git [Ada] Spurious error on synchronous refinement This patch ensures that an abstract state declared with simple option "synchronous" is automatically considered "external". 2018-05-21 Hristian Kirtchev gcc/ada/ * einfo.adb (Is_External_State): An abstract state is also external when it is declared with option "synchronous". * einfo.ads: Update the documentation of synthesized attribute Is_External_State. * sem_util.adb (Find_Simple_Properties): New routine. (Is_Enabled_External_Property): New routine. (State_Has_Enabled_Property): Reimplemented. The two flavors of option External have precedence over option Synchronous when determining whether a property is in effect. gcc/testsuite/ * gnat.dg/sync2.adb, gnat.dg/sync2.ads: New testcase. From-SVN: r260453 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d8e644ee2db..71ef1ba346e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2018-05-21 Hristian Kirtchev + + * einfo.adb (Is_External_State): An abstract state is also external + when it is declared with option "synchronous". + * einfo.ads: Update the documentation of synthesized attribute + Is_External_State. + * sem_util.adb (Find_Simple_Properties): New routine. + (Is_Enabled_External_Property): New routine. + (State_Has_Enabled_Property): Reimplemented. The two flavors of option + External have precedence over option Synchronous when determining + whether a property is in effect. + 2018-04-04 Yannick Moy * sem_eval.adb (Static_Length): Take into account case of variable of diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 4e9aa0890a9..4352f42ea88 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -8083,8 +8083,14 @@ package body Einfo is function Is_External_State (Id : E) return B is begin + -- To qualify, the abstract state must appear with option "external" or + -- "synchronous" (SPARK RM 7.1.4(8) and (10)). + return - Ekind (Id) = E_Abstract_State and then Has_Option (Id, Name_External); + Ekind (Id) = E_Abstract_State + and then (Has_Option (Id, Name_External) + or else + Has_Option (Id, Name_Synchronous)); end Is_External_State; ------------------ @@ -8255,6 +8261,9 @@ package body Einfo is function Is_Synchronized_State (Id : E) return B is begin + -- To qualify, the abstract state must appear with simple option + -- "synchronous" (SPARK RM 7.1.4(10)). + return Ekind (Id) = E_Abstract_State and then Has_Option (Id, Name_Synchronous); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index b7d98572ad8..36967fd2632 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2553,7 +2553,7 @@ package Einfo is -- Is_External_State (synthesized) -- Applies to all entities, true for abstract states that are subject to --- option External. +-- option External or Synchronous. -- Is_Finalized_Transient (Flag252) -- Defined in constants, loop parameters of generalized iterators, and diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 21105635b12..958efb07cc8 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -10261,92 +10261,157 @@ package body Sem_Util is -------------------------------- function State_Has_Enabled_Property return Boolean is - Decl : constant Node_Id := Parent (Item_Id); - Opt : Node_Id; - Opt_Nam : Node_Id; - Prop : Node_Id; - Prop_Nam : Node_Id; - Props : Node_Id; + Decl : constant Node_Id := Parent (Item_Id); - begin - -- The declaration of an external abstract state appears as an - -- extension aggregate. If this is not the case, properties can never - -- be set. + procedure Find_Simple_Properties + (Has_External : out Boolean; + Has_Synchronous : out Boolean); + -- Extract the simple properties associated with declaration Decl - if Nkind (Decl) /= N_Extension_Aggregate then - return False; - end if; + function Is_Enabled_External_Property return Boolean; + -- Determine whether property Property appears within the external + -- property list of declaration Decl, and return its status. - -- When External appears as a simple option, it automatically enables - -- all properties. + ---------------------------- + -- Find_Simple_Properties -- + ---------------------------- - Opt := First (Expressions (Decl)); - while Present (Opt) loop - if Nkind (Opt) = N_Identifier - and then Chars (Opt) = Name_External - then - return True; - end if; + procedure Find_Simple_Properties + (Has_External : out Boolean; + Has_Synchronous : out Boolean) + is + Opt : Node_Id; - Next (Opt); - end loop; + begin + -- Assume that none of the properties are available - -- When External specifies particular properties, inspect those and - -- find the desired one (if any). + Has_External := False; + Has_Synchronous := False; - Opt := First (Component_Associations (Decl)); - while Present (Opt) loop - Opt_Nam := First (Choices (Opt)); + Opt := First (Expressions (Decl)); + while Present (Opt) loop + if Nkind (Opt) = N_Identifier then + if Chars (Opt) = Name_External then + Has_External := True; - if Nkind (Opt_Nam) = N_Identifier - and then Chars (Opt_Nam) = Name_External - then - Props := Expression (Opt); + elsif Chars (Opt) = Name_Synchronous then + Has_Synchronous := True; + end if; + end if; - -- Multiple properties appear as an aggregate + Next (Opt); + end loop; + end Find_Simple_Properties; - if Nkind (Props) = N_Aggregate then + ---------------------------------- + -- Is_Enabled_External_Property -- + ---------------------------------- - -- Simple property form + function Is_Enabled_External_Property return Boolean is + Opt : Node_Id; + Opt_Nam : Node_Id; + Prop : Node_Id; + Prop_Nam : Node_Id; + Props : Node_Id; - Prop := First (Expressions (Props)); - while Present (Prop) loop - if Chars (Prop) = Property then - return True; - end if; + begin + Opt := First (Component_Associations (Decl)); + while Present (Opt) loop + Opt_Nam := First (Choices (Opt)); - Next (Prop); - end loop; + if Nkind (Opt_Nam) = N_Identifier + and then Chars (Opt_Nam) = Name_External + then + Props := Expression (Opt); - -- Property with expression form + -- Multiple properties appear as an aggregate - Prop := First (Component_Associations (Props)); - while Present (Prop) loop - Prop_Nam := First (Choices (Prop)); + if Nkind (Props) = N_Aggregate then - -- The property can be represented in two ways: - -- others => - -- => + -- Simple property form - if Nkind (Prop_Nam) = N_Others_Choice - or else (Nkind (Prop_Nam) = N_Identifier - and then Chars (Prop_Nam) = Property) - then - return Is_True (Expr_Value (Expression (Prop))); - end if; + Prop := First (Expressions (Props)); + while Present (Prop) loop + if Chars (Prop) = Property then + return True; + end if; - Next (Prop); - end loop; + Next (Prop); + end loop; - -- Single property + -- Property with expression form - else - return Chars (Props) = Property; + Prop := First (Component_Associations (Props)); + while Present (Prop) loop + Prop_Nam := First (Choices (Prop)); + + -- The property can be represented in two ways: + -- others => + -- => + + if Nkind (Prop_Nam) = N_Others_Choice + or else (Nkind (Prop_Nam) = N_Identifier + and then Chars (Prop_Nam) = Property) + then + return Is_True (Expr_Value (Expression (Prop))); + end if; + + Next (Prop); + end loop; + + -- Single property + + else + return Chars (Props) = Property; + end if; end if; - end if; - Next (Opt); - end loop; + Next (Opt); + end loop; + + return False; + end Is_Enabled_External_Property; + + -- Local variables + + Has_External : Boolean; + Has_Synchronous : Boolean; + + -- Start of processing for State_Has_Enabled_Property + + begin + -- The declaration of an external abstract state appears as an + -- extension aggregate. If this is not the case, properties can + -- never be set. + + if Nkind (Decl) /= N_Extension_Aggregate then + return False; + end if; + + Find_Simple_Properties (Has_External, Has_Synchronous); + + -- Simple option External enables all properties (SPARK RM 7.1.2(2)) + + if Has_External then + return True; + + -- Option External may enable or disable specific properties + + elsif Is_Enabled_External_Property then + return True; + + -- Simple option Synchronous + -- + -- enables disables + -- Asynch_Readers Effective_Reads + -- Asynch_Writers Effective_Writes + -- + -- Note that both forms of External have higher precedence than + -- Synchronous (SPARK RM 7.1.4(10)). + + elsif Has_Synchronous then + return Nam_In (Property, Name_Async_Readers, Name_Async_Writers); + end if; return False; end State_Has_Enabled_Property; diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 4d10e0a9f7e..2ba0869ae2e 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-04-04 Hristian Kirtchev + + * gnat.dg/sync2.adb, gnat.dg/sync2.ads: New testcase. + 2018-05-21 Kyrylo Tkachov * gcc.c-torture/execute/ssad-run.c: New test. diff --git a/gcc/testsuite/gnat.dg/sync2.adb b/gcc/testsuite/gnat.dg/sync2.adb new file mode 100644 index 00000000000..2348166b225 --- /dev/null +++ b/gcc/testsuite/gnat.dg/sync2.adb @@ -0,0 +1,27 @@ +-- { dg-do compile } + +package body Sync2 with + SPARK_Mode, + Refined_State => (State => (A, P, T)) +is + A : Integer := 0 with Atomic, Async_Readers, Async_Writers; + + protected type Prot_Typ is + private + Comp : Natural := 0; + end Prot_Typ; + + P : Prot_Typ; + + task type Task_Typ; + + T : Task_Typ; + + protected body Prot_Typ is + end Prot_Typ; + + task body Task_Typ is + begin + null; + end Task_Typ; +end Sync2; diff --git a/gcc/testsuite/gnat.dg/sync2.ads b/gcc/testsuite/gnat.dg/sync2.ads new file mode 100644 index 00000000000..a9c45c98069 --- /dev/null +++ b/gcc/testsuite/gnat.dg/sync2.ads @@ -0,0 +1,6 @@ +package Sync2 with + SPARK_Mode, + Abstract_State => (State with Synchronous) +is + pragma Elaborate_Body; +end Sync2;